Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-09-23

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
01:47 ilbot3 joined #divine
01:47 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
08:57 xstill mornfall: hodilo by se mít intrinsic něco jako __divine_discard_state(), který kdyby se zavolal, tak divine tenhle stav nevygeneruje/zahodí, dalo by se tím vyřešit blokující čekání pod maskou, což by vedlo na efektivnější userspace + by se to dalou použít na nějakou formu statické POR (případně kdyby někdo chtěl dělat userspace s kooperativním multitaskingem)
10:24 mornfall to je v podstat assume ne?
10:24 mornfall hm, asi bych si mel nastavit locale
10:38 xstill to možná je, každopádně to chce asi promyslet s ohledem na tau, takže to můžeme zítra
12:31 mornfall ono by davalo smysl zrusit __divine_assert celkove a mit je assert_fail a assume_fail ktery se exponujou assert-em a assume-em
12:31 mornfall jen*
12:31 mornfall a to co chces ty je bud __divine_assume_fail() nebo assume( false )
12:32 mornfall aspon v BMC se to tak obvykle chape, ze assume je jako assert ale kdyz failne tak se ten beh chape jako infeasible
12:32 mornfall misto aby se chapal jako chybovej
12:34 xstill no, ono asi není potřeba tu podmínku cpát do toho, to už je jedno, takže __divine_assert je už obsaženej v __divine_problem
12:35 xstill jo a to co popisuje (pokud unfeasible = nevygeneruje se) je to co chci
12:40 mornfall tak, neznamena to *nutne* nevygeneruje se, ale proste nema vliv na vysledek modelcheckingu (coz v nasem pripade asi vzdy znamena nevygeneruje se)
12:41 mornfall to bychom mohli mozna mit aj klasicky deadlocky v DVE->LLVM pak
12:42 xstill jo, to taky, a co to znamená jinde je mi clkem fuk
12:43 mornfall tak v symdivinu to mozna bude znamenat neco jinyho prave
12:43 xstill aha, co?
12:43 xstill jo přidání do path condition?
12:44 mornfall jo
12:44 mornfall tezko rict, ale mohlo by to byt smysluplny pokud to zavisi na symbolickych vstupech
12:45 mornfall a mozna pak precijen dava smysl mit assert/assume s parametrem, protoze pak je ta datova zavislost jasna
12:45 mornfall kdyz to je jen v control flow tak to asi seslozituje analyzu
12:45 xstill aha, ok
12:46 xstill ale ono v llvm je to stejně skoro to samý, ne? nejdřív se to vyhodnotí a pak se volá funce
12:46 mornfall no to jo, ale kdyz tam je parametr tak ten parametr je to co vede na datovy zavislosti, kdyz to je v control flow musis najit odpovidajici branch instrukci
12:47 xstill ok
12:47 mornfall ktera hlida basic block ve kterym ten assume/assert je
13:08 xstill mornfall: na divine pořád nefunguje certifikát
13:35 xstill proč se vlastně v pthread funkcích explicitně vyžaduje pozorovatelnost?
15:27 xpetkan joined #divine
18:09 xpetkan joined #divine
18:09 peteru_ joined #divine
18:09 peteru__ joined #divine
18:14 xpetkan joined #divine
18:14 peteru_ joined #divine
18:14 peteru__ joined #divine
18:17 xpetkan joined #divine
18:17 peteru_ joined #divine
18:17 peteru__ joined #divine
18:18 xpetkan joined #divine
18:18 peteru_ joined #divine
18:18 peteru__ joined #divine

| Channels | #divine index | Today | | Search | Google Search | Plain-Text | summary