Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-07-01

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

All times shown according to UTC.

Time Nick Message
07:42 mornfall hm, failuje nám llvm/stacksave.sh
07:42 mornfall divine/llvm/execution.h: 1307: assertion `i != e' failed;
07:43 mornfall veselý je že ne ve všech buildech kde se spustí
07:43 mornfall hm, ale to je možná proto že clang 3.3 generuje jinej bitkód
07:52 xstill podíváš se na to? já teď řeším ty undefined paměti a už bych se měl docela blížit
07:54 mornfall hm, zajímavý že se to rozbilo teď, nevidím která změna by za to mohla být odpovědná
07:54 xstill jakože než jsem pushnul ty memory flagy tak to nebylo rozbité?
07:55 xstill prosímtě, za EvalContex v evaluátoru se dosazuje co?
07:55 mornfall rozbilo se to mezi 20150625120324 a 20150625191016
07:56 xstill že by Interpreter se tam dosazoval?
07:56 mornfall jo, mimo jiné Interpreter
07:56 mornfall s memoryflags to ještě fungovalo
07:57 mornfall to bude ta změna v test/lib :)
07:57 mornfall nebo tak něco
07:57 mornfall hm, to je ale blbost, tam se na vstupu nic neměnilo ne?
07:57 xstill tam jsem měnil jen výpis
09:05 xstill mornfall: je možný, že bys neměl nastavené flagy na static thread_local proměnných?
09:06 xstill konkrétně external/libcxxabi/src/cxa_exception_storage.cpp
09:06 xstill :26
09:07 xstill btw. kdyby byly vidět ve výpisu, bylo by to taky fajn (ale přiznám se, že doteď jsem nevěděl, že něco takového existuje)
09:14 xstill btw. https://github.com/nidhugg/nidhugg
09:15 xstill jo aha tak mi neumíme (teda clang neumí) thread_local, takže je to chyba v pthread asi
09:16 mornfall 'mi' ... :p
09:17 xstill nojo
09:17 mornfall my hlavne nedelame c++ ale llvm
09:17 mornfall a tam nic takoveho neni
09:17 mornfall to musi vygenerovat prekladac
09:19 xstill takže překladač by to stejně přeložil na pthread?
09:20 mornfall to je na překladači na co by to přeložil
09:21 mornfall automatická proměnná se generuje jako alloca v hlavičce fce, statická s inicializací na docela složitej kus kódu kterej dělá zhruba ekvivalent pthread_once, co dělá thread_local můžeme jen odhadovat
09:22 mornfall resp. nedělá nic protože clang :-P
09:23 mornfall počítám že HAS_THREAD_LOCAL je nedefinovaný ale
09:24 xstill jo
09:24 mornfall a #ifdef __divine__ už tam je, stačí tam do něj přidat memset
09:24 xstill chyba je v tom, že v inicializaci je __divine_malloc
09:24 xstill jo no
09:24 mornfall nebo alternativně (a to byl asi původní plán) dodělat nějaký API na označování paměti jako neinicializované
09:24 mornfall přijde mi to stejnej princip jako malloc kterej failuje
09:26 xstill no já jsem zatím přidal __divine_calloc (v userspace), kterej volá memset, calloc pak volá toto, kdyby byl interface na flagy tak stačí aby volal to
09:26 mornfall __divine_* nemá co dělat v userspace
09:26 xstill no tak to udělám jinak no
09:36 xstill mornfall: nevíš jestli Jiřík odpovídal na to o těch serverech?
09:36 mornfall nevím
09:36 xstill a ty jsi neodpovídal předpokládám
09:38 mornfall ne
09:39 xstill já bych k tomu jen potvrdi, že 5U se nám tam vejde a (teda doufám) a řekl, že ty disky nemusí být nutně 2.5 ani nutně 10K
09:39 xstill kolik máme vlastně v racku místa? 5U nebo 7U?
09:40 mornfall no, nenosím to v hlavě
09:40 mornfall je tam switch + 3x1U servery + 2x2U pole + asi 3x5U pheme?
09:41 xstill asi jo, ale nevím kolik je tam celkem místa…
09:41 xstill asi tam mrknu
09:42 mornfall to bude asi jistější :)
09:46 xstill no 5U místa tam je, ale někdo nám cpe cizí servery do racku
09:46 mornfall už zas? :)
09:46 xstill jo no, už jou tam 3
09:50 xstill hm, tag a personality v _DivineLP_* asi nejsou heap pointry, že?
09:59 xbarnat joined #divine
10:05 mornfall asi ne
10:05 mornfall personality je funkce
10:05 mornfall tag je ukazatel na globální data
10:06 xstill ok, jo když je nastavím jako že to jsou data tak to funguje
10:09 xstill ale moc netuším kde se mi berou ty neinicializované hodnoty v pthread_join
10:12 xstill xbarnat: doufám, že to co jsem poslal Yenyovy souhlasí s tvou představou
10:26 mornfall xstill: no, bylo by asi lepší to zkopírovat ze zdroje než to přeplácnout na data
10:26 mornfall ale fungovat to bude i takhle
10:26 mornfall (kopírovat to bude asi trochu bolet)
10:32 xstill hm, tak jsem myslel, že to zkopíruju, ale dostal jsem `invalid pointer passed to memoryflags'
10:41 xstill hm, zjistit odkud se vzala neinicializovaná paměť je docela peklo
10:47 mornfall ano
10:47 mornfall ale to je jedna z věcí která by šla řešit analýzou protipříkladu
10:49 mornfall isPthreadJoin ... :)
10:49 mornfall a tak
10:49 mornfall (nidhugg)
10:50 xstill no já to nezkoumal skoro vůbec zatím
10:52 mornfall je to psaný pro tacas competition, zdá se
10:54 mornfall http://www.researchgate.net/profile/Konstantinos_Sagonas/publication/270763468_Stateless_Model_Checking_for_TSO_and_PSO/links/5512da790cf270fd7e339c0f.pdf?disableCoverPage=true tohle bude asi k tomu
11:18 xstill tyjo, záznam běhu v gdb je tak pekelně pomalý, že snad divine by to udělal rychlejš
11:59 xstill beztak je chyba v interpretru a ne v pthreadech
12:01 xstill a nebo taky ne
12:26 xstill mornfall: asi by se měli flagy nastavit na všechny bajty výsledku (v execution.h:1317), ale nevím jistě jestli to můžu bezpečně nastavit i na pointer, nebo jestli pro pointer se má první bajt nastavit jako pointer a zbytek jako data
12:30 mornfall určitě jen první
12:38 xstill ok, ale pořád mám teda podezření, že mi tam někde lezou undefined bity kde nemaj a blbě se to ladí :-/
12:47 mornfall no, interpret se ladí blbě vždycky
12:48 mornfall proto se snažíme toho co nejvíc vytlačit do userspace
12:50 xstill nj ono by bylo třeba fajn moct vidět flagy k jednotlivým registrům
13:25 mornfall hmm
13:25 mornfall tady ten patch s hardware_concurrency má jeden veselej dopad, testy který nemaj -w mi běhaj na 16 vláknech
13:26 mornfall a pak mi na tom gdb vygeneruje bus error
13:26 xstill :-D
13:28 mornfall a když pak tady ten automat otevře to gdb.core tak se gdb zacyklí
13:36 xstill se mi ještě nepovedlo pustit divine bez -w ani na arke ani na auře… ale třeba to jednou příjde :-D
13:38 mornfall teď mi zase gdb píše 'invalid thread selected' to je zase výhra
13:40 mornfall že já se vůbec snažim
13:53 xstill mornfall: fakt už nevím, posílám to tak jak to je, třeba na něco příjdeš, anebo se k tomu časem ještě vrátím
13:53 xstill padá pthread_join a fs testy já bych si tipnul, že ten join je nějakou chybou v interpretru a ty fs věci jsem nezkoumal
14:05 spito heh, jak to, že mi padají fs testy?
14:07 spito je v pohodě dát jako příklad model, který má 102M stavů?
14:17 xstill protože jsem udělal detekci neinicializované paměti a ta je asi někde rozbitá, nebo máš neinicializovanou paměť
14:17 xstill spito: no, pokud to nebude jedinej, a napíšeš to tam
14:17 xstill a dělá něco zajímavýho třeba
14:54 ilbot3 joined #divine
14:54 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
16:48 mornfall xstill: proč to nebude fungovat na BE?
18:33 zak111 joined #divine
18:33 zak111 ahoj, nemeli bychste nahodou nejaky dve soubor, ktery ma akceptujici stavy? popr. obsahuje cyklus na tech stavech. Dík
18:54 mornfall no, skoro všechny, spíš tomu asi musíš dát -p
19:00 xstill nebyl by tam ten pointer na druhé straně? i když vlastně nevím, možná je to blbost
19:07 zak111 co je -p?
19:08 mornfall divine help verify
19:08 mornfall divine info
19:08 zak111 ok, ok chapu blbej dotaz
19:09 zak111 je self_loop na acekptujicim stavu, akceptujici cyklus? je takovy stav vubec mozny
19:09 xstill jo
19:09 xstill je to dost běžný
19:12 zak111 -p property kterou chci verifikovat? jak to pouzit v kontextu dve?
19:12 xstill no divine info ti řekne co tam je za property
19:13 mornfall stejně jako v jakémkoliv jiném kontextu
19:15 zak111 dík
19:22 zak111 uzel se expanduje jen jednou v celem programu?
19:23 zak111 asi ne
19:23 xstill záleží na algoritmu
19:23 zak111 uz chapu, ten readonly visitor musi pouzit nucenou expanzi?
19:24 xstill no podívej se do edge ve visitor.h, tam je to vidět
19:24 xstill já si to teď přesně nepamatuju, ale inner si bude muset expanzi vynutit asi
19:26 xstill jakože nejde o to, že je to read only, ale o to, že to potřebuješ expandovat podruhé, poprvé se to řídí tím, jestli jsi už ten vrchol viděl (je v tabulce)
19:27 zak111 vlastnost "je v tabulce" je globalni ano?
19:28 xstill jo, tabulka je jedna
19:28 xstill (nebo teda ne nutně jedna, ale každý vrchol patří do jedné, pokud je to partitioned a je jich víc)
19:29 zak111 ok, díky
19:31 mornfall no, 'poprvé se to řídí' je zavádějící, tím jestli je v tabulce se to řídí pokud vrátíš TransitionAction::Follow
19:33 xstill tak já myslel v ndfs, ale jo samozřejmě že je to tím co se v rací z transition
20:28 spito joined #divine
21:35 spito joined #divine

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