Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-07-15

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

All times shown according to UTC.

Time Nick Message
03:20 mornfall joined #divine
03:23 ChanServ joined #divine
05:39 xstill jo k tomu jsem taky nakonec došel. Má to asi problém, že do stejného stavu můžu dojít po víc vláknech. Musím si to nakreslit a rozmyslet co se s tím dá udělat.
10:00 mornfall joined #divine
13:02 xstill hm, kde jsi našel ten bug ve fifo, já tam nic nevidím (v tom co je v toolkit/examples)
13:08 mornfall http://pastebin.dqd.cz/HR73/
13:11 mornfall plus ty dva patche co jsem teď pushnul plus -U__unix v --cflags
15:08 xstill nojo a teda ten protipříklad je nechutně dlouhek
15:11 mornfall (-U__unix by asi bylo dobrý přidat do divine compile)
15:13 xstill hm, já to přeložil bez toho, ale to asi ovlivňuje bricks co? (jsem to vypreparoval)
15:13 mornfall jo
15:14 xstill ale vtipné je, že mi při tom nedetrministicky segví divine
15:14 mornfall je možný že jsem rozhasil pooly
15:14 xstill no já musím zkusit jestli za to muže CSDR, nebo jestli to dělá i reachabilita
15:20 xstill ten stacktrace je fakt divnej, protože na konci je signal handler
15:46 xstill jo a teda s CSDR jsem nÄ›co udÄ›lal ale má to jeden problém: tím, že do daného stavu se dá dostat po víc vláknech je to aproximace, protože záleží který tid si tam uložím (jinak bych musal ukládat celý parent graf a to nemá moc smysl dÄ›lat). Můžu sice dÄ›lat to, že uložím tid který má doteÄ� míň context-switchů, ale pokud jich je víc tak nevím který vybrat (= uloží se první), což může znamenat, že se zapoÄ�Ã
15:47 xstill (jinak se zdá že to funguje, ve smyslu, že to generuje stejné množství CS s i bez redukcí snad)
15:48 mornfall usekl tě irc limit
15:48 xstill kde?
15:48 mornfall znamenat, že se započí
15:48 xstill což
15:48 xstill může znamenat, že se započítá nějaký CS
15:48 xstill navíc.
15:49 xstill (sorry za ten bordel)
15:49 mornfall jo, to si myslim že ničemu nevadí
15:49 xstill no nesmí, jinak to totiž asi ani při rozumné pamětové náročnosti nejde
15:50 xstill sem o tom přemýšlel a ani kdybych do toho extension dal set na tid kterým se tam dalo přijít tak to nepomůže protože z toho nevygeneruju ten správný protipříklad a mít v extension něco proměnlivě velkého je hodně na nic
15:50 xstill ještě zjistit co mi tu segví
15:59 xstill poslal jsem ti zatím update CSDR (a teda v tom prvním patchi je i modifikace v llvm/, ale to by snad nemusalo vadit ty dva řádky)
15:59 xstill na ten segv se ještě zkusím podívat
16:01 xstill (jenže on nastává jen pokud člověk nemá zapnutý coredump, nebo alespoň nemá debug info zdá se)
16:04 mornfall to je milý
20:23 mornfall no, verify-ipcqueue.bc jsem stáhl z 18k stavů s τ+ na 519 s τ₅ ... teď jen jestli to mám správně ;-) asi ne...
20:25 xstill :-), co to chystáš?
20:25 mornfall naja, blbě to je :-)
20:27 mornfall ale vzhledem k tomu že τ+ (aka τ₃) dává taky divný výsledky... :-)
20:29 xstill co znamenaj ty čísla? A koukám, že unicode bereš dost vážně :-)
20:29 mornfall hm, ale s τ₄ to ve fifo protipříklad našlo... (celej stavovej prostor 3.3k) ... to je slibný ;-)
20:33 mornfall jo, <compose> g t <compose> _ 1 ;-)
20:35 mornfall a mám teda osmilevelovou keymapu, ale na řečtinu a subskripty není úplně místo :P
20:35 mornfall hm, nebo vlastně je
20:37 xstill :-)
20:41 xstill hm, začínám mít obavu, že Jiřík měl pravdu a CSDR je dost na nic
20:43 xstill respektive teda je to jak kdy a potřeboval bych víc modelů
20:45 mornfall ₁₂₃₄₅₆₇₈₉₀¹²³⁴⁵⁶⁷⁸⁹⁰ a jsou namapovaný ;-)
21:01 mornfall jinak teda test/llvm/mutex.sh je nějaký vadný
21:01 mornfall pak to opravim
21:08 xstill jak vadný?
21:08 mornfall no, nekontroluje to co má
21:08 mornfall třeba ten // dead locker má sice chybu, ale rozhodně ne tu kterou bys chtěl
21:09 mornfall (chyba je že když hlavní vlákno vyleze z main tak to druhý hrabe na neexistující stackframe)
21:09 mornfall pokud jde o mutexy tak je ten program dobře
21:11 xstill hlavní vlákno nemá co vylézt z main, to by mělo zabít i to druhé
21:11 mornfall ne na returnu
21:11 mornfall mezi returnem a exitem je ještě jeden stackframe
21:12 mornfall aj v normální glibc
21:13 xstill tak správně by tam měl být ještě join hned za tím pthread_create
21:13 xstill pak by to bylo jasný
21:13 mornfall main() je zavolaný, neskáče se na něj, a překladač generuje return
21:14 mornfall hlavně ještě můžou běžet globální destruktory mezi tím kdy vylezeš z main a kdy pomřou vlákna
21:15 xstill jo, mám pocit že standart specifikuje, že po return z main zdechnou vlákna, ale nemusí to být hned, takže máš pravdu a chce to ten join
21:15 xstill jen je divný, že to ještě nezdechlo
21:15 mornfall no, zdechlo :-)
21:15 xstill no u mě ne
21:15 xstill ale to je asi dost náhodný
21:16 mornfall není, říkám že ten test netestuje co má :-)
21:16 mornfall žádná jiná chyba v tom testcasu není -- divine vždycky najde ten invalid memory access
21:16 xstill no to by mi ten test selhal žejo
21:16 mornfall neselhal
21:16 mornfall „ten test netestuje co má“ :-)
21:17 mornfall jsou tam blbě parametry u toho llvm_verify
21:17 xstill no ale pak musí být chyba v llvm_verify, protože to má ověřit, že v protipříkladu je "Deadlock: Nonrecursive mutex locked again"
21:19 mornfall to by muselo být v tom parametru co je "" ale aby to takhle fungovalo
21:19 mornfall ten parametr co je "Deadlock..." je $where, který nic nedělá pokud je $what prázdný
21:20 mornfall hm
21:20 mornfall což je teda asi obráceně než by mělo být
21:21 xstill hm sakra
21:22 mornfall je to celý nějaký zmatený s tím llvm_verify :-)
21:23 xstill no problém je to "test -n "$what" && \"
21:24 xstill spíš bych tam dal test -n "$where$what"
21:24 xstill protože pokud tam není $where tak bych čekal, že je to taky chyba
21:26 mornfall no, ještě je teda problém že na $what se grepuje s ^ a ty Deadlock problémy píšou jako typ ???? :-)
21:26 mornfall ale teď je asi každopádně užitečnější řešit CSDR
21:26 mornfall tohle dořeším někdy až budu mít chvíli volno
21:27 xstill něco jsem zapoměl k té propery vyplnit
21:28 mornfall describe.cpp:339 +/-
21:29 mornfall a já mam pocit že s tím __divine_interrupt() jste všichni co jste říkali že by to nemělo být po _mask() potřeba pravdu, teď mi to dělá problémy...
21:30 mornfall ne že bych stejný problémy neměl s AP i kdyby __divine_interrupt potřeba nebyl

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