Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-08-06

| 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/
09:51 xstill sakra něco mi zprasilo fonty v nixosu
09:52 xstill aha to jen 10.5 font je nemá celou češtinu
10:27 mornfall 474M stavů ...
10:39 xstill to je dost, ten divine zatím vypotil 49M stavů, ale když jsem to pro kontrolu pustil s jedním workerem v modelu tak jsem našel assert, což moc nedává smysl
10:39 xstill ASSERTION FAILED (thread 1): <brick::hashset::_ConcurrentHashSet<brick::hashset::AtomicCell<divine::PondInDivine::Pointer, divine::algorithm::Hasher> >::WithTD::rehashSegment()> [ ../bricks/brick-hashset.h:799 ]
10:43 xstill a teda ten assert je it < end, a ono je it == end
10:46 xstill no a ten assert failne i když to pustím bez divine
11:04 mornfall a není to je vadnej assert?
11:04 mornfall jen*
11:09 xstill musím se na to mkrnou, asi to bude okrajovej případ protože ta tabulka je malá
11:15 xstill aha já měl nastavelnou počáteční velikost na 1
11:20 xstill a mám řádek o velikosti 0
11:21 xstill hm, jak může být row.empty() == false a zároveň row.size() == 0?
11:26 xstill no to je jedno, jediná chyba je, že tabulka nefunguje pokud se nastaví inicální velikost na 1
11:27 mornfall nevim proč to tak je, spito by mohl
11:28 xstill protože to interně nastaví velikost nějakého virtuálního řádku na 0 a tím pádem všechny řádky mají velikost 0 (velikost předchozího * k)
11:28 xstill ten virtuální se nastavuje na n / 2
11:28 xstill což je asi chyba vzhledem k tomu jak vypadá nextSize
11:28 xstill ale to je detail
11:29 xstill takže je to bug ale není zajímavej
11:29 mornfall jo no
11:30 mornfall lamport postoupil na půl miliardy stavů
11:30 xstill to je ten bez redukcí?
11:30 mornfall j
11:30 xstill to měříš redukce?
11:30 mornfall jo, redukovaný to má necelýho půl mega
11:31 xstill :-)
11:31 mornfall ale tak szymanski se taky redukoval na 0.05 procenta
11:31 mornfall z 9.5M na <5k
11:31 xstill hm, další goal, teď jen počkat až mi to vyblije těch milion věcí na konzolu
11:32 xstill (divine má prefix asi 500 stavů než nastartuje 2. vlákno, většinou konstruktory před mainem)
11:32 mornfall :-)
11:33 xstill asi bych to měl pouštět rovnou do simulate a ne -d na konzolu
11:33 xstill je poněkud trapné pokud vypsat protipříklad tvrá dýl než ho najít
12:54 xstill hm, tak je to jen nějakej bordel ve streamech
12:57 mornfall vyrobíš ticket?
12:57 xstill spíš to opravím, vypadá to, že je to tím, že jsi nahradil VLA za malloc v pdclib
12:58 xstill vyměním ho za __divine_malloc
13:11 mornfall to je otázka co s tím :-)
13:13 mornfall navíc tam je teda leak, ono to fixme tam není nadarmo
13:14 mornfall „In practice, this pops any alloca blocks from the stack that were allocated after the llvm.stacksave was executed.“
13:14 mornfall to není zas tak těžký udělat
13:15 mornfall i když... :-)
13:22 xstill hm, jo je tam leak, otázka je proč ho to nenašlo
13:23 xstill nějak se to zdá se zacyklilo
13:27 xstill hm, super gdb mi padá když se chci dostat na staktrace
13:27 xstill každopádně to padlo až při vytváření protipříkladu
13:27 xstill teda cyklí
13:28 xstill poslední co vidím na trace je llvm::Value::print(llvm::raw_ostream&, llvm::AssemblyAnnotationWriter*) a pak gdb hodí segv
13:30 xstill jo mám celej backtrace (z lldb)
13:33 xstill aha, tak ono to necyklilo
13:34 xstill jen ten protipříklad zabírá celou obrazovku jen ve formě číselného trace
13:39 mornfall :D
14:23 xstill tak prej máme leak v destruktoru hashsetu
14:29 xstill je to divný, najednou v destruktoru Row se tam objeví 7 leaků
14:29 xstill aha
14:30 xstill za to může ten pool co sem udělal
14:30 xstill on to totiž neuvolní
14:30 xstill a ani na to nemá pointer, takže je to ztracený
14:30 xstill takže to zase není bug
14:30 xstill otázka je co s tím
14:45 mornfall opravit ten pool? :-)
14:45 mornfall zsh: segmentation fault  divine metrics -w 10 --shared --max-memory=80000 lamport.bc --no-reduce
14:45 mornfall tak nic no...
14:46 mornfall podle statistik to sežralo jen asi 26G paměti takže limit to snad neyl
14:46 mornfall nebyl*
14:47 mornfall aha houby ono to zesegvilo až po tom co to dojelo
14:47 mornfall veselý
14:48 xstill no ten pool nic nedělá, ani si nedrží informace o blocích
14:59 mornfall ten PondInDivine je dost děsivej ...
14:59 xstill je
15:00 xstill jenže Pond nejde ani zkompilovat kvůli všem tagům
15:01 mornfall to že to nějak funguje je menší zázrak :-)
15:01 xstill a Pool se mi nezdál leho zmenšitelný
15:02 mornfall tak, asi bych se nesnažil za každou cenu to pakovat
15:02 xstill no jako nebyl jsem si jistej, že to bude fungovat, ale tak dává to smysl, i když jen na little-endian asi a díky tomu že llvm pointer je 32 bit
15:02 mornfall trochu se divím že ti to nenuluje _tag a _size teda
15:02 xstill no tag se nedá umístit do alokované paměti
15:02 xstill aha
15:03 xstill kde ho nenuluje?
15:03 mornfall no ale nic ti nebrání mít sizeof( Pointer ) == 16, žejo
15:03 mornfall 8 pointer a 4 + 4 tag, size
15:03 xstill nebrání
15:03 mornfall nebo 12 jestli chceš
15:03 xstill možná by to bylo rozumnější
15:04 mornfall výrazně :-)
15:04 xstill tak já to pak předělám
15:04 mornfall to je čistě náhoda že kanonizace prvně překopíruje ten originální pointr a pak přepíše jen první 4 bajty
15:05 xstill hm aha, to mi vlastně nedošlo že ty s těma pointrama děláš docela psí kusy
15:05 xstill koukám, že je větší náhoda že to funguje než jsem si myslel
15:06 mornfall tak on ti nikdo negarantuje že si můžeš po pointrech psát co chceš :-))
15:07 mornfall to ale furt neřeší jak je rozumně uvolňovat
15:08 mornfall nabízí se možnost přidat parametr do __divine_malloc kterej by říkal jestli je ta paměť explicit-free nebo GCable
15:09 mornfall to by taky vyřešilo leak v tom VLA hacku :-)
15:09 xstill tak ten zrovna řeší jedno free, ale ten parametr by i tak byl užitečnej
15:14 mornfall já nějak vůbec nemůžu přijít na důvod proč bych v divinu měl stacksave/stackrestore potřébovat (jinak než noop)
15:14 mornfall potřebovat*
15:16 mornfall jedinej případ asi je když ten stackrestore není v exit bloku fce
15:17 xstill a co vyhodit/invalidovat ty alloca bloky, pokud se to teda už nestane nějak jinak?
15:18 mornfall na to by sis právě musel držet spoustu extra paměti
15:18 mornfall (každej alloca by musel vyrobit buňku do linked listu abys mohl oddělat jen ty který je potřeba)
15:19 xstill to je dost nepraktický no
15:20 mornfall no a otázka teda je jestli někdy clang vyrobí stackrestore kterej není v exit bloku, protože tam je to fakt jedno -- jde čistě o správnost výpočtu velikosti rámce a to se nás netýká
15:22 xstill no otázka je co se stane když alokuješ VLA uvnitř nested bloku: int f( int a ) { …; { int vla[ a ]; … }; …; }
15:22 mornfall hm, volá to na konci platnosti
15:23 mornfall jo, zrovna to jsem testoval
15:23 mornfall tam hrozí že nepochytáme když do toho pole vyrobí pointr s delší životností než to samotný pole
15:24 mornfall nerad bych kvůli stackrestore zatěžoval všechny alloca
15:25 mornfall horší je že ani neznáme cestu kterou se to dostalo od stacksave ke stackrestore, pak bychom mohli staticky napočítat registry který obsahujou neplatný alloca
15:28 xstill a nejseš schopnej alloca interně uspořádat jako zásobník?
15:29 mornfall no, na to bych potřeboval ten linked list, žejo
15:29 mornfall jak jinak chceš udělat nafukovací zásobník?
15:32 mornfall spíš by bylo smysluplný v stacksave naalokovat blok ukazatelů na validní alloca a v stackrestore všechny krom zapamatovaných smazat
15:33 mornfall to vyrobí overhead jen když reálně stacksave/stackrestore použiješ
15:36 xstill to by mohlo fungovat (týkalo by se to vždy jen alloca v dané funkci, ne?)
15:37 mornfall jistÄ›
16:26 mornfall xstill: tys vyměnil rekurzivní mutex za nerekurzivní, v barrier.h?
16:39 xstill jo, ale myslím že tam bylo jen jedno místo kde byl potřeba rekurzivní a to jsem změnil
16:39 xstill nebo je tam ještě něco?
16:39 mornfall to bys možná mohl oddělovat takový změny ... :P
16:40 mornfall kdo to má pak číst
16:40 xstill hm, to mÄ› nenapadlo
16:40 xstill změnil jsem done, nikde jinbe by se to snad rekurzivně volat nemělo
16:41 xstill částečně to bylo i tím, že sem si všiml, že je rekurzivní až když už jsem to měl skoro celé předělané
16:42 mornfall tak, změnit mutex na recursive_mutex v typedefu by taky nebyl takovej problém :)
16:42 mornfall teď musim zjistit jak funguje ukončování v MPI :-)
16:42 mornfall ale řekl bych že to je OK
16:43 xstill mpi testy prošly, ale to asi ještě neznamená že to je ok
16:44 xstill no na m_globalMutex přistupuje jen barrier.h
16:44 xstill takže by to mělo být OK, protože tam jsem to kontroloval
16:44 mornfall jo, žádnej callback nevidim
16:44 mornfall kde by se teda s tou bariérou dál manipulovalo
16:45 mornfall (isBusy aj workWaiting jsou safe)
19:58 xstill hm s texem je zábava, nějak se nemůžu rozhodnout jestli čeština vypadá hůř s lmodern nebo bez, asi s protože háček na ď je sotva vidět
19:59 xstill jenže computer modern zase nemá bold texttt
20:11 mornfall http://paradise.fi.muni.cz/~xrockai/draft-aug6.pdf :-)
20:11 mornfall ne že by tam byla čeština... ale tak, CM není jedinej font na světě
20:18 xstill no jasnÄ›
20:18 xstill jak k tomu vypadá zdroják?
20:37 mornfall jestli někdy doběhne darcs put tak ti pošlu link :D
20:37 mornfall http://paradise.fi.muni.cz/~xrockai/thesis-src/
20:38 mornfall lib/style.tex je většina nastavení
20:40 mornfall (a chybí tam asi milion změn, ale to je snad jedno :)
20:45 xstill to vypadá vcelku dobře no

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