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