Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-04-12

| 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/
07:51 xstill mornfall: ještě jsem zapoměl zarecordovat jeden řádek do toho posledního patche
07:52 xstill poslal jsem to znova
08:17 xstill (jinak testy potom neprojdou, opravuju to)
08:51 xstill jo ono totiž nejde jen tak přehozovat alokátory v průběhu verifikace, LLVM se pak rozbije (kvůli tomu stavu co má generátor v sobě)
09:08 mornfall to vybírání default algoritmu není úplně ideální
09:09 xstill proč? to že to padá taky není ideální (byť teda v nedefaultní konfiguraci)
09:09 xstill jako není to moc hezký to uznávám
09:09 mornfall asi bych preferoval kdyby to řešil select (a divine by tam napsal DefaultReachability/DefaultLTL nebo něco v tom smyslu)
09:10 xstill hm, to by mohlo jít… časem
09:10 mornfall DefaultSafety / DefaultLTL možná
09:10 xstill tak ten neposílej já si ho unpullnu
09:11 mornfall spito: v tom manuálu vyrábíš konflikty
09:12 mornfall xstill: ok
09:32 xstill mornfall: skoro bych řekl, že potřebujeme aby ephemeral paměť fungovala i přes různé store (nemusí jí asi jít uvolňovat jinde, ale kdyby fungovalo size tak v podstatě nemusíme řešit to, že někde natvrdo rveme LongTerm protože by se tam hodil alloc ze store). Alternativně by si generátory nikdy nesměly zapamatovat Blob v sobě (což LLVM dělá)
09:33 xstill jako pokud bysme velikost v ephemeral ukládali před ten pointr tak nás to asi nemusí moc bolet a fungovalo by to myslím
09:37 mornfall jakože se někde přeskládává vztah generátor<->store?
09:37 mornfall to mi přijde že se rozbije i jinak
09:38 xstill no třeba ltlce používá longterm alokátor
09:38 xstill jenže tam je koukám problém že on je v podstatě musí používat protože si ukládá celý trace
09:38 xstill teda on by nemusel ukládat stavy, ale to pak zase neuděláme protipříklad až bude HC
09:39 mornfall jo, tomu asi neutečeme... ale moc nerozumím proč se zrovna tohle rozbije... (i když to že generování protipříkladu umírá jsem si někde všiml nedávno)
09:40 xstill protože LLVM vygeneruje stav v průběhu verifikace, LLVM rewind alokuje blob přes ephemeral -> generování protipříklad: LLVM drop-ne ten blob přes longterm
09:40 xstill a padne to
09:40 mornfall ah
09:40 xstill krom toho různé graph::release, ale to už jsem opravil
09:41 xstill (a to že draw padá s kompresí a shared taky)
09:41 mornfall tak jedna možnost je 'vyresetovat' ten generátor na konci algoritmu nebo tak něco
09:41 mornfall což dropne ten blob ještě s odpovídajícím alokátorem
09:41 mornfall ale nevim no
09:42 xstill jako napadlo mě, že by všechno muselo normálně používat alloc ze store a ve chvíly kdy by se to začalo přehaozvat mezi vlákny (ltlce, explict) tak by se musel překopírovat do permanent
09:43 xstill resetovat generátor je taky takový divný
09:43 mornfall no, je taky možnost vyrobit úplně novej generátor
09:44 mornfall nebo upravit ephemeral tak aby fungoval s libovolně velkou pamětí
09:44 mornfall a pak by asi nevadilo že LtlCE si ty stavy uloží
09:45 mornfall tím že to je dedikovanej blok se to dá přemapovat na v podstatě libovolnou velikost (a starou paměť překopírovat)
09:46 xstill no ne tak jednoduše protože velikost offsetu v pointru
09:46 xstill což ná steď limituje na ty 2 MB co tam jsou
09:46 mornfall hm, pravda, to je jen 19 bitů
09:47 mornfall tak nic no :-)
09:47 mornfall mít víc než jeden ephemeral blok bude dost bolet
09:47 xstill to asi jo
09:50 mornfall jinak teda jo, flavours vyrobily nový sloupce :-)
09:50 mornfall už tam nějaký jsou
09:52 xstill hm, to bude vypadat teda, navíc tam bude dost šedých políček teď
09:53 mornfall uvidíme
09:53 xstill ale tak alespoň jsme přili na to, že to nefunguje
09:55 mornfall myslím že ephemeral bych asi řešil tak že LLVM si vyrobí blob do kterýho si to bude v rewind() kopírovat
09:55 mornfall a nebude (de)alokovat v rewind
09:55 mornfall jdu to zkusit
09:56 xstill zkus, poslal jsem patche co opravují část toho problému (graph::release, draw)
09:57 mornfall nechápu proč to tam tak nebylo doteď... hm
09:58 mornfall ten jeden whichInitial v LtlCE se fakt nepoužívá?
09:59 mornfall hm, asi ne
10:01 xstill ne
10:01 xstill asi historické důvody
10:02 mornfall to co asi můžem udělat je trochu osekat počet buildů
10:03 mornfall to jsou taky tak trochu historické důvody
10:10 spito mornfall: tak já ten manuál trochu opravim, no
10:12 mornfall a ty přepínače sis rozmyslel? :-)
10:22 spito přesný popis jsem chtěl dát ještě do 3. sekce
10:23 spito nebo by se to hodilo napsat jenom jednou?
10:52 mornfall no, přehled přepínačů do 3. sekce, co to umí tam jak to máš
10:54 mornfall a když budeš připisovat longjmp do limitations, tak tam radši piš `longjmp`/`setjmp` protože co je 'long jumps' není moc jasný
10:54 mornfall to evokuje 8086 kde byl jump long nebo short podle toho kolik bitů měl offset :-)
11:54 spito mornfall: jo, bude
11:54 spito ale asi až pojedu vlakem
12:04 xstill tak hashset s vložením 2 prvků na 3 vláknech dojel, 922M stavů
12:07 spito a není tam chyba? :)
12:07 xstill není, kdyby byla tak napíšu
12:08 xstill ale docela mě překvapilo, že to nebylo o tolik větší
12:08 xstill (jen o půlku zhruba)
12:09 xstill jinak necelé 3 dny na 48 vláknech (reálně teda nebylo úplně volných 48 jader)
12:10 xstill zkusím ještě větší model
12:10 xstill kterej bude vkládat i nějakej prvek víckrát
12:16 xstill mornfall: bude hodně zlý když vecpu figury do llncs formátu na 2 sloupce?
12:17 xstill ono totiž jinak je tam asi nemáme moc šanci nacpat
12:23 mornfall ne, to je v klidu
12:44 xstill spito: asi bysme snesli jeden odstavec o vztahu té naší tabulky k té Frisově
12:44 xstill (a dokonce se tam i vejde)
12:48 xstill zatím jsem ten paper přehodil do llncs a vmáčkne se do limitu, ale ty figury jsou dost malý (byť na papíře by měli být čitelný)
12:48 xstill ale teď jdu asi opravit ltlce spíš
12:48 mornfall teď jsem tam vrátil LongTerm() :P
12:48 mornfall to by možná už zase mohlo stačit ne?
12:49 xstill hm
12:50 xstill asi i mohlo, ale já si teď nejsem jistej kde se to rozpadá, protože tam kde bylo potřeba jsem ho nechával
12:50 xstill mornfall: zkus ./tools/divine verify --reachability --report -w 1 --shared --compression=tree --property=assert --reduce=tau+,taustores,heap --max-time=600 test/global-bug.bc
12:50 mornfall whichInitials se rozpadá
12:50 xstill aha
12:51 mornfall -s
12:51 xstill otázka je jestli se store nepokusí delokovat to ve fetch svým alokátorem
12:52 xstill aha fetch nedealokuje
12:52 mornfall to by fakt nemusel
12:53 xstill ale moc nechápu co se na tom rozpadá
12:53 xstill (s ephemeral)
12:53 mornfall whichInitial právě volá size() cross-store
12:53 mornfall resp. cross-pool
12:54 mornfall shared store vrací v knows vždycky true
12:55 xstill hm, ale to musí být cross-pool ten handle, a ten se vezme někde úplně jinde, ne?
12:55 xstill protože whichIntial sám nikam nic neposílá
12:55 mornfall však jo, volá se _ceIsInitial
12:56 mornfall ten hned v prvním vlákně projde do větve s.knows...
12:56 mornfall bez ohledu na to odkud to shared().ce.current přišlo
12:57 xstill no jasně, ale podstatné je odkud jde ten shared().ce.current ne jakej akoátor se používá ve whichInitial
12:57 mornfall hm, pravda :)
12:57 mornfall nicméně s LongTerm to funguje
12:57 xstill spíš může být problém v getInitialById
12:57 xstill ten by měl mít LongTerm a změnil jsem ho
12:58 mornfall no, assertilo to ve whichInitial
12:59 xstill hm
12:59 mornfall (je možný že z getInitialById se ten výsledek dopracuje do whichInitial kde to lehne)
13:00 spito xstill: vztah naší tabulky je takový, že je omezenější
13:01 xstill hm, a nemůžeme tam napsat něco hezčího?
13:01 mornfall v jakém smyslu?
13:01 mornfall xstill: spito kecá aby se to zařízlo ;-)
13:01 spito oni umí neomezený počet změn velikosti
13:01 spito + mazání prvků
13:02 spito mornfall: to ne
13:02 xstill spíš "neomezený"
13:03 mornfall maxGrows = sizeof( void* ) * 8 myslíš? :)
13:04 xstill tak mi budeme mít dost velkou maximální velikost
13:05 xstill víc než půjde použít
13:05 mornfall no, dokud máš konečně velkej pointr tak není problém mít tabulku která může být stejně velká (maximálně) jako adresní prostor
13:05 spito mornfall: tak, že umí recyklovat použité ukazatele na řádky
13:06 spito používají řádkovník o velikosti 2*P, kde P je počet vláken
13:06 spito tzn každé vlákno má případně místo, kam by zvětšovalo
13:06 mornfall jo, to je docela detail ale :)
13:06 spito a oni umí tabulku i smršťovat...my jenom zvětšovat
13:06 spito a tak
13:07 * spito odjíždí
13:07 mornfall protože když to pustíme na 48 vláken tak to máš víc resizů než se vleze do 64b adresního prostoru
13:09 xstill hm no dobře, tak neumíme odebírat, protože to nepotřebujeme, ale pokud tam něco k té Frisově tabulce nic nenapíšeme tak mám obavu, že nám to zase nevezmou…
13:10 mornfall já se na to podívám až to doformátuješ
13:11 xstill pushnul jsem to naformátované
13:11 xstill teda snad, nevidím jestli nám nepřetýká výška někde
13:11 mornfall v tom případě se na to podívám až se vrátim z procházky :D
13:11 mornfall (bbiab)
17:52 xstill mornfall: existuje něco co nejde do lambdy zachytit referencí?
18:12 mornfall nevím, asi by nemuselo
18:12 mornfall v jakém smyslu 'nejde'?
18:12 spito Problém budeš mít v případě, že to, co jsi zachytil, ta umřelo dřív, než jsi zavolal lambdu.
18:13 spito *tak
18:13 xstill jo tak to jo, mě jde o to jestli může existovat něco kde by to nebylo syntakticky dobře (tak jak když máš zachycení hodnotou tam nemůžeš mít věci co nemaj copy-konstruktor)
18:18 spito Ono věci, který jsou zachycený referencí, nejsou (dle vyjádření na cppreference) reálně nijak zakomponované v lambda-objektu, používá se reference na původní proměnné.
18:19 xstill jako já si myslím, že by to mělo jít se vším, tak mi spíš šlo o to jestli jsem něco nepřehlédl
18:21 mornfall spito: no v tý lambdě (pokud někde fyzicky existuje) je uloženej ukazatel
18:21 mornfall to je stejný jako member reference
18:24 spito mornfall: http://cecko.eu/public/pb071/cviceni/09
18:25 spito rozpracovaná verze náplně na cvičení; ještě budu posílat mail
18:25 spito toto bych s nimi chtěl dělat na přednášce a posléze na cvičeních
18:32 xstill hm, dokážu dost drasticky zrychlit debug :-) (mutex test 252s vs 32s)
18:36 mornfall spito: napsat funkc_i_, něakou funkc_i_ :)
18:37 mornfall jinak jo
18:38 mornfall umí rozzipovat zip? :)
18:45 xstill i když teda ve výsledku ty testy ztráví asi dost času jen pouštěním příkazů, ale zrychlil jsem je u sebe z 35 na 26 minut
19:19 spito mornfall: to s tou funkcí nějak nechápu
19:19 spito nic...už to mám...
19:46 xstill mornfall: poslal jsem ti patche (zrychlení assertů a news)
20:03 xstill hm, status -> details začáná vypadat dost špatně :-D
20:03 mornfall no, říkám máme tam dost buildů který jde sloučit/vyhodit
20:04 xstill a uděláš to?
20:05 mornfall časem, teď mám dost jiných věcí
20:06 xstill no a v timed máme assert
20:07 xstill divine/toolkit/ntreehashset.h: 295: assertion `pos + ls <= this->pool().size( item.i )' failed; got [36] > [4] instead
20:07 xstill to může bejt nějakej jetej alokátor zase
20:09 mornfall tohle přesně dělalo LtlCE když tam byl ephemeral
20:10 xstill nojo, ale ten patch už by tam měl být, ne?
20:11 mornfall na druhý straně timed celkově haluzí
20:11 mornfall [ 1:17] ### States-Visited: 2 expected, 3 got
20:11 mornfall v zeno.xml
20:11 xstill ale taky s kompresí, což se mi moc nelíbí…
20:43 xstill tak jsem to snad našel
20:45 xstill i když teda u mě to assertilo v valgrind dealokace, ale možná nemáme valgrind v buildu
20:48 mornfall jinak nebylo by jednodušší dát do Location const char *stmt radši?
20:48 xstill to jsem chtěl, ale cpe se do toho brick::fmt někde
20:49 mornfall aha, v tom unreachable
20:49 mornfall to by se taky dalo řešit... někdy jindy, možná
20:49 mornfall --> postel
20:50 mornfall spin zítra ve vlaku
20:50 xstill no myslím, že teď to funguje dobře

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