| 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 |
