Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-04-11

| 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/
06:03 xstill mornfall: není to divný, že v DVE jsou dvě hrany mezi stejnými vrcholy a popsaný úplně stejně?
07:08 mornfall xstill: divný to není
07:09 mornfall xstill: vezmi si třeba dva procesy se selfloopem který v efektu inkrementuje globální proměnnou
07:09 mornfall xstill: a popis hrany se v dve počítá čistě z těch dvou stavů, když jsou stejný musí být stejný aj popis
07:09 mornfall nemá to žádný speciální Label
07:09 xstill ok
07:10 xstill ona ta chyba s tím stejně nesouvisí
07:11 xstill jako vypadá to, že se mi projdou některý hrany 2x, v druhý iteraci přes stavovej prostor
07:14 xstill (nebo minimálně se projdou jiný 2x)
07:15 mornfall jako shared by to určitě dělat neměl
07:15 mornfall jestli jo tak je to docela bug
07:15 mornfall owcty by se muselo rozsypat
07:16 xstill jak jsem koukal do visitoru tak se mi nezdá, že by to bylo možný, tak jsem si myslel, že mám blbě udělaný rozhodování jestli projít hranu v druhý iteraci, ale nemůžu tam najít chybu
07:16 xstill takže zatím nevím
07:16 mornfall a tos tam už dal zámky jo?
07:16 mornfall nebo se nerozhoduješ podle extension?
07:17 xstill jo dal jsem tam zámky, ale psal jsem si původně ten lock a unlock ručně, je ještě možný, že to bylo blbě
07:17 xstill teď jsem tam vrazil bitlock a tváří se to, že to nepadá, ale nevím nakolik tomu mám věřit
07:20 xstill http://pastebin.dqd.cz/arfH/ to je ten původní lock, je na tom něco blbě?
07:22 xstill protože teď se to tváří, že to funguje
07:22 xstill s bitlockem
07:22 xstill hm blbě je na tom úplně všechno
07:23 xstill specielně nevím co vrací cas :-/
07:23 xstill takže ten zámek nemohl fungovat
07:23 mornfall no, chybí tam not
07:23 xstill jo no
07:24 xstill no ono je to jedno, ten bitlock je asi lepší v nakonec
07:24 mornfall ok (kdybys to tam chtěl vrátit asi je lepší pojmenovat si ten bit ne tu masku a masku psát jako ~bit)
07:25 xstill dokonce je extension teď menší (porotože jsem si řekl, že 60bitů na index fakt stačí a přibalil jsem iteraci to toho BitTuple)
07:25 mornfall první myšlenka byla (než jsem si všiml ten not) jestli IXMASK odpovídá tomu 1 << 63
07:25 xstill jo to je dobrá připomínka
07:28 xstill hm, ten explicit test je teď ale dost dlouhej (u mě cca 5 minut)
07:28 mornfall no nebo psát bit jako ~IXMASK to by nakonec taky fungovalo
07:28 xstill (ale prošel)
07:28 mornfall pouštíš to na něčem velkým?
07:29 xstill na tomtéž co se pouští reachability = all_small tuším
07:30 xstill (jako že je delší protože jsem tam přidal shared)
07:30 mornfall vidíš to jsem chtěl -- proč jsi vlastně potřeboval aby se ten jeden test pustil v rámci toho druhýho?
07:30 mornfall mi přišlo že se z toho žádnej výstup nepoužije
07:31 mornfall genexplicit v genexplicit-reach
07:31 xstill protože pokud genexplicit sám o sobě neprojde tak genexplicit-reach bude dávat nejspíš nějaký blbosti
07:32 xstill a přišlo mi, že se to v něm bude blbě hledat
07:32 xstill (obvzlášť když ten genexplicit.sh běží normálně až po genexplicit-reach.sh)
07:32 mornfall tak, zase uvidíš že genexplicit umřel a většinou člověka asi napadne že když failuje ten tak se prvně podívá tam
07:33 xstill takže myslíš, že to mám vyhodit?
07:33 mornfall asi jo, ušetří to trochu času ... jinak jsem se podíval testy běží podle abecedy
07:33 mornfall takže když to přejmenuješ tak to poběží správně
07:34 mornfall genexplicit-basic, genexplicit-reach
07:34 mornfall třeba
07:34 mornfall (já to původně pochopil že v -basic vygeneruješ soubory který -reach potřebuje, ale tam by se to rozbilo s T=, občas a dost záhadně asi)
07:35 xstill ok přejmenuju
07:36 mornfall spito: requests -> requires
07:36 mornfall (recompilation of the ...)
07:37 mornfall spito: jinak myslím OK
07:37 mornfall spito: jo, ještě asi zmínit že ty --snapshot/--stdin patří k divine compile
07:38 mornfall spito: (a rovnou upravit commands.mdwn ;-)
07:40 mornfall spito: a test: zase píšeme malým obvykle ;-)
07:43 xstill odesláno (snad nevadí, že jsem  algorithm: Make Gen-Explicit work with shared. nerozdělil do víc)
08:33 xstill myslím, že by pomalu stálo za to zapnout shared jako výchozí režim (a případně ani nekompilovat partitioned pokud není zapnuté MPI)
08:50 mornfall jo, nezapomeň překopat testy až to budeš dělat ;-)
11:01 xstill k čemu ten tag?
11:06 mornfall release tag mi to nechce brát do kontextu v send-u, nevim proč a tohle funguje... uvidíme jestli se na další release chytne nebo ne
11:09 mornfall xstill: pak si napiš NEWS ideálně
11:09 mornfall spito: a ty pošli ten manuál jako patch ;-)
11:11 xstill jo pošlu NEWS, dokonce už jsem tam lokálně přidal řádek, ale ještě asi zkusím zapnout ten shared a pak to poslat
11:12 mornfall když už budeš hrabat tady do toho, tak by mohlo stát za to upravit default na -w podle std::hardware_concurrency
11:13 xstill hm, to by mohlo
11:13 mornfall std::thread::hardware_concurrency
11:14 mornfall (jen teda na SMT to píše počet vláken ne jader)
15:09 spito mornfall: poslal bych manuál jako patch
15:10 mornfall kdyby co?
15:10 spito nechtělo by to náhodou udělat i v llvm sekci manuálu něco jako přehledný seznam přepínačů?
15:11 mornfall přepínačů čeho?
15:12 spito pro divine
15:12 mornfall no ale kterých?
15:12 spito divine compile --llvm
15:13 mornfall to patří do sekce 3 spíš
15:15 spito takže tam popsat navíc všechny příkazy pro divine compile
15:15 spito ?
15:17 mornfall nějak smysluplně, jo
15:24 mornfall /tmp/nix-build-divine-explicit_relwithdebinfo_x64-3.3.1+pre5854.drv-0/divine-3.3.1+pre5854/divine/algorithm/genexplicit.h:503:41: error: converting to 'std::tuple<divine::Lake::Pointer, long int>' from initializer list would use explicit constructor 'constexpr std::tuple<_T1, _T2>::tuple(_U1&&, _U2&&) [with _U1 = divine::Lake::Pointer&; _U2 = int; <template-parameter-2-3> = void; _T1 = divine::Lake::Point
15:24 mornfall er; _T2 = long int]'
15:24 mornfall xstill: ^^
15:24 mornfall /nix/store/qxpwyjgwxsvq5zvmsfpd02jpyf0ck5hl-gcc-4.8.3/include/c++/4.8.3/type_traits:2026:12: error: invalid use of incomplete type 'std::__result_of_impl<false, false, divine::algorithm::_GenExplicit<Setup>::writeFile() [with Setup = divine::instantiate::Setup_Algorithm_GenExplicit__Generator_LLVM__Transform_Fairness__Visitor_Shared__Store_DefaultStore__Topology_Local__Statistics_NoStatistics_]::__lambda6
15:24 mornfall 7, char*, long int>::type'
15:24 mornfall /tmp/nix-build-divine-explicit_relwithdebinfo_x64-3.3.1+pre5854.drv-0/divine-3.3.1+pre5854/divine/algorithm/genexplicit.h:546:13: error: no matching function for call to 'divine::dess::DataBlock::FInserter::emplace(std::basic_string<char>::size_type, divine::algorithm::_GenExplicit<Setup>::writeFile() [with Setup = divine::instantiate::Setup_Algorithm_GenExplicit__Generator_LLVM__Transform_Fairness__Visit
15:25 mornfall or_Shared__Store_DefaultStore__Topology_Local__Statistics_NoStatistics_]::__lambda67)'
15:25 mornfall http://divine.fi.muni.cz/status/log/1zrlzdhwzlyqqg2yv49ym9191dn9sb89-divine-explicit_relwithdebinfo_x86-3.3.1+pre5854.drv
15:27 mornfall hm, a už zase nestačí 4G na build, co se stalo
15:29 spito (na mě nekoukej...)
16:02 spito umíme překlad murphi na nativní kód?
16:02 mornfall jakej nativní kód?
16:02 mornfall umíme murphi na cesmi
16:08 spito no a z toho to pak jde na nativní kód
16:08 mornfall nechápu
16:09 mornfall možná si přečti sekci cesmi ;-)
16:12 spito takže jestli to chápu dobře: pomocí CESMI můžu napsat vlastní generátor stavů, přibalit k tomu LTL a celý to zkompilovat do *.so
16:13 spito pomocí -> s využitím rozhraní
16:14 mornfall tak něco, i když to LTL je dost marginální zrovna tady
16:22 spito a to *.so je ale nativní kód, ne?
16:27 xstill mornfall: gcc počítám :-/ mrknu na to
16:34 mornfall spito: tak nativní kód to je, ale je hodně matoucí o tom tak mluvit
16:34 mornfall aniž bys důkladně vysvětlil co to znamená
16:35 spito jo, to já chápu
16:35 spito a u DVE a MURPHI je výsledek stejný - *.so soubor, že?
16:35 mornfall no, vždycky to je cesmi modul
16:36 mornfall tzn. .so nebo .dll podle platformy
16:36 mornfall asi bych tam spíš napsal cesmi module a odkázal na odpovídající sekci
16:40 spito jinak poslal jsem zatím aspoň rozšíření llvm sekce
16:56 xstill hm, by mě ale zajímalo proč se gcc nechce zavolat ten konstruktor
17:00 xstill ono má asi nakonec pravdu možná, protože je tam ještě typová konverze na té -1 z int na int64_t
17:02 xstill i když ani s explicitní konverzí se mu to nelíbí, už asi vím proč to tam bylo původně tak divně :-/
17:06 xstill mornfall: máš tam patch
17:08 xstill a na auře už nám DIVINE vygeneroval 800M stavů
17:22 xstill spito: měřil jsi někdy jestli je shared na jednom vlákně pomalejší než partitioned, a o kolik?
17:50 spito záleží na tom, jestli se musí zvětšovat tabulka
17:50 xstill řekněme že musí
17:51 spito AURA, 1 vlákno
17:51 xstill pokud je model tak malej, že se vejde do předinicializované tak je to skoro jedno asi
17:52 spito generátor dummy
17:52 spito partitioned, iniciální velikost 2^29 - 164.1s
17:52 spito shared, iniciální velikost 2^29 - 209.4s
17:53 spito shared, inici8ln9 velikost 2^19 - 233.13s
17:53 xstill hm, to je docela znát
17:53 spito ANTEA, 1 vlákno
17:53 spito partitioned, iniciální velikost 2^29 - 147s
17:53 spito shared, iniciální velikost 2^29 - 150s
17:54 spito shared, iniciální velikost 2^19 - 191s
17:54 xstill hm to vypadá líp
17:54 xstill partitioned se zvětšováním máš taky?
17:54 spito ne
17:55 spito to jsem vzal z bakalářky
17:55 xstill ok
17:56 spito ale obecně zvětšování partitioned není takový problém
17:56 spito protože i to zvětšování probíhá paralelně
18:01 xstill jo, no jako já bych skoro nejradši kompliloval partitioned jen pokud je zapnuté MPI, tak mi jde o to, jestli tím nezpůsobím nějaký větší výkonnostní problém na 1 vlákně, asi ještě zkusím co dělá to zvětšování
18:05 xstill pro zajímavost: rehashovat tabulku z 1G na 2G slotů trvalo 48 vláknům půl hodiny)
18:17 xstill mornfall: co s testy? nechat všechny běžet tak jak jsou (tj. efektivně je změnit na shared) a místo shared testů udělat partitioned testy?
18:19 xstill nebo testovat všechno naráz, jako s kompresí?
18:19 xstill to by možná dávalo větší smysl nakonec
18:36 mornfall xstill: no, testovat asi všechno nějak inteligentně :-)
18:37 mornfall xstill: možná by šlo zneužít ty flavours co jsou v tom brick-shelltest
18:37 mornfall tzn. vyházet shared, compression, etc. testy
18:37 mornfall a pustit je 3x nebo 4x všechny s různou kombinací nastavení
18:38 xstill mornfall: jaký flavours? co je to za věc a jak se to používá?
18:40 mornfall ./runner --flavours shared,partitioned,compression
18:40 mornfall spustí každej test 3x, s TEST_FLAVOUR=shared pak partitioned pak compression
18:40 mornfall teď tam je vždycky jen 'vanilla'
18:40 xstill TEST_FLAVOUR je env proměnná?
18:40 mornfall jj
18:41 xstill ok to zní docela dobře
18:42 mornfall možná bych mohl upravit brick-shelltest aby pak bral F= který vyfiltruje --flavours jako teď bere T=
18:44 xstill tak partitioned vs. shared (na dummy s 4M stavy a 1 vlákně): 211s vs. 193s
18:44 xstill tak nevím jestli by nebylo lepší přece jen zapnout shared jen pokud jsou tam alespoň 2 vlákna
18:45 mornfall shared vs. partitioned myslíš?
18:45 mornfall teda, shared je těch 211?
18:45 xstill jo
18:46 mornfall nevím, těžko říct
18:46 xstill jako na llvm to asi nikdo nepozná no
19:12 xstill hm  /home/xstill/DiVinE/mainline/divine/toolkit/pool.h: 155: assertion `_vhandles[ p.block ].load()' failed
19:12 xstill na ./tools/divine verify --reachability --report -w 1 --shared --compression=tree --property=assert --reduce=tau+,taustores,heap --max-time=600 test/global-bug.bc
19:13 xstill (deterministicky)
20:20 xstill mornfall: neaplikuj ten můj patch
20:20 xstill mornfall: chybí v něm -
20:20 mornfall nefunguje?
20:20 mornfall ah
20:22 xstill dost zásadně
20:22 xstill naštěstí začal padat test
20:22 xstill už jsem odeslal opravenou verzi
20:24 xstill btw. co udělají flavours se statusem?
20:26 mornfall details budou mít víc sloupců, počítám
20:26 mornfall uvidíme :D
20:27 xstill sloupců… tak to jsem zvědavej :-D
21:17 spito mornfall: ta moje manuál llvm věc nee?
22:12 mornfall (spim, podivam se rano)

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