Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-03-01

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

All times shown according to UTC.

Time Nick Message
02:49 ilbot3 joined #divine
02:49 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
07:09 xstill joined #divine
08:21 xstill je garantováno že bool se vejde do bitfieldu o velikosti 1?
08:21 xstill teda že bool hodnota true bude vždy binární 1
09:09 xstill hm, člověk hrábne do poolu a hned vidí segv
09:30 mornfall no garantovaný zrovna nevim, ale neviděl jsem překladač kde by to nefungovalo :-)
10:05 xstill jinak mám takový jednoduchý gc na pool bloky, ale ještě mi to segví v destruktoru s valgrindem
10:07 xstill jo protože hrabu na hlavičku smazanýho bloku
10:07 mornfall hm, gc... kdy ho chceš spouštět?
10:08 xstill občas před alokací bloku (pokud dochází k tomu, že je hodně free)
10:09 mornfall a jak řešíš zamykání?
10:09 mornfall nebo se collectuje jen sdílenej freelist?
10:10 xstill collectuje se jen lokální freelist
10:10 xstill teda nesdílené bloky
10:10 mornfall hm, zajímavý ... pomáhá to něčemu?
10:11 xstill no collectuje to
10:11 xstill ale ještě jsem neviděl statistiky poolu protože mi to na nich padne
10:11 mornfall no to jo, ale jestli to aj zůstane dealokovaný... ok
10:11 xstill zjistím za chvíli
10:12 mornfall ona je asi spíš zajímavá RSS statistika a walltime
10:12 mornfall než statistiky poolu
10:13 xstill to taky no
10:13 mornfall mně tak napadlo co vlastně brání tomu aby se ten stav hashoval do tabulky rovnou z generátoru, když je to shared
10:14 mornfall mě*
10:30 xstill hm nefunguje to
10:30 xstill jako vůbec
10:30 mornfall jako že to padá?
10:30 mornfall nebo že to nic neušetří?
10:30 xstill neuspoří, spíš naopak
10:31 mornfall jo, to mě zas tak nepřekvapuje
10:31 xstill proč?
10:31 mornfall no, proč by to mělo fungovat?
10:32 mornfall stavů je mnohem mnohem víc než těch mrtvých bloků v poolu, tzn. že každej ten blok se za běh divinu použil hodněkrát
10:32 xstill tak proto že většina těch bloků se používá jen občas a na tak málo stavů že se nestihnou dát globálnímu freelistu tak jsem si myslel, že ty starý prostě zahodím
10:32 mornfall no nevim jestli většina
10:33 mornfall to je dost odvážnej předpoklad
10:34 xstill asi je…
10:34 mornfall já bych čekal že to bude rozložený relativně rovnoměrně
10:35 mornfall tohle by fungovalo kdyby se stavy rychle zvětšili na nějakou finální velikost a pak už se to neměnilo
10:38 mornfall taky by to asi fungovalo kdyby nebyl interleaving, ale takhle se jednak každej stav nageneruje hodněkrát a druhak sousedi budou mít tendenci mít stejnou velikost (i přesto že v search order budou od sebe hodně daleko jsou to sousedi protože vypadaj skoro stejně, jen tam vedlo nějaký dostatečně jiný proložení vláken)
10:40 xstill nojo je to na nic :-/
10:41 mornfall no, nějaký řešení kde se z generátoru rovnou hashuje by fungovat mohlo (s tím že se díky tomu ví že ten stav je alokovanej krátkodobě a bude se uvolňovat ve stejným vlákně)
10:41 mornfall ale to je osud toho že benchmarky děláme jen když je článek na obzoru
10:41 mornfall to už je pozdě tohle nějak víc řešit
10:46 xstill jo no
10:59 spito jak fungují priority u hlavičkových souborů?
11:00 mornfall jaký priority?
11:00 spito při kompilaci divinem
11:00 spito protože mi clang bere systémové a ne ty přiložené
11:00 mornfall jo, to nejsou priority
11:01 spito by se mi jako líbilo, aby bral hlavně jenom ty naše
11:01 mornfall to mně taky, ale ...
11:01 mornfall doporučuju libclang
11:01 spito a co s tím?
11:01 mornfall vy sice furt brblete na ty switche co tomu clangu cpu a generuje to warningy, ale ono ani tohle nestačí
11:02 spito takže v podstatě jediná možnost je zakompilovat clang do divine?
11:03 mornfall zhruba
11:04 mornfall jestli vymyslíš jak ten commandline přesvědčit aby ignoroval systémový cesty tak do toho
11:04 mornfall ještě tam možná nějakej switch bude
11:05 mornfall (a teda na libclang potřebujeme clang 3.5, takže asi aj llvm 3.5, .....)
11:05 mornfall ale možná je na to pomalu čas
11:05 spito no to dělat asi teď úplně nechci
11:06 mornfall asi nechceš no
11:09 mornfall spito: ale to co bys mohl je opravit unistd.h:103
11:09 mornfall spito: unknown type name useconds_t
11:09 spito tohle je docela sympatický přepínač: -fdiagnostics-show-template-tree
11:12 spito nechtěli bychom doplnit do pdclibu toto: #pragma clang system_header ?
11:19 mornfall čemu to pomůže?
11:19 mornfall (versus -isystem)
11:20 spito co dělá -isystem?
11:21 mornfall co dělá #pragma clang system_header?
11:21 spito vypne v daném souboru vypisování warningů
11:21 spito i když ho includuješ
11:21 mornfall tzn. to stejný co -isystem
11:21 spito oh, ok
11:22 mornfall máme tam -nostdinc a -nostdlibinc?
11:22 mornfall hm, -nostdlibinc  bych tam přidal
11:23 mornfall hm
11:24 mornfall ono teda clang-wrapper to asi stejně dost kazí
11:24 mornfall možná mu chceš dávat nezawrapovanej clang
11:25 mornfall spito: jak to konfiguruješ?
11:25 spito přes ccmake ..
11:26 mornfall myslím CMD_CLANG
11:26 mornfall jakej mu dáváš
11:26 spito clang
11:26 mornfall jo to bude ono
11:26 spito a co tam chci dát?
11:28 mornfall /nix/store/mq13x6jdp4npgq04yigbgfc3nv2nc2vv-clang-3.4.2/bin/clang asi
12:40 mornfall spito: pošleš ten fix na unistd nebo si to mám spravit?
12:41 spito pošlu
12:47 spito done
13:00 mornfall | [ 0:04] ../libcxx/std/cstddef:50:1: error: unknown type name '_LIBCPP_BEGIN_NAMESPACE_STD'
13:00 mornfall hm
13:03 mornfall aha jo já tady zase mám něco rozhasený
13:09 mornfall hm, ještě bych asi mohl používat clang 3.4 když divine llvm 3.5 neumí že
13:10 mornfall | [ 0:06] Linker error: Invalid value
13:10 mornfall ale tohle je trochu matoucí
13:11 mornfall (když to ve skutečnosti není linker error ale chyba z ParseIRFile)
13:14 spito tak s tím ti nepomůžu už vůbevc
13:22 mornfall neboj já si s tim poradim ;-)
13:28 mornfall to jen tak brblu
13:58 mornfall spito: hm, ty FS_NOINLINE na začátku mi taky moc nejde přeložit
13:58 mornfall | [ 0:15] ../unistd.h:54:12: error: expected ';' after top level declarator
13:58 mornfall | [ 0:15] FS_NOINLINE int close( int fd );
13:59 mornfall ah, omyl, tohleto byl ztracenej středník
14:33 mornfall ty locale mě zabijou
14:45 mornfall hurá
14:56 mornfall xstill: hm, ty state flags v divine info by možná bylo dobrý nějak zalomit, nevejde se mi to na šířku okna
15:00 spito xstill tu není
15:01 mornfall on si to časem přečte
15:40 mornfall hm
15:41 mornfall ten try v main-u úplně nefunguje protože vlákna
16:36 spito noinline musí být kupodivu za funkcí
16:37 spito nebo jsem něco přehlédl?
16:44 spito přehlédl :D
16:58 mornfall spito: no, ono to funguje aj takhle (teda aspoň se to přeloží, jestli to dělá to co chceš, nevim)
16:58 spito no tam chyběl ten středník
16:59 spito to je to, na co sis tu před chvilkou stěžoval
16:59 spito chvilka == cca 2 hodiny
16:59 mornfall spito: no, stěžoval protože to je přinejmenším divný mít to na začátku
17:00 mornfall spito: ale to že to nešlo přeložit nebyla chyba noinline
17:00 spito no to už vím taky
17:00 mornfall uvidíme co na to teď řekne hydra...
17:15 mornfall xstill: hm, testuje hydra vůbec nějakej build kterej má zároveň ntree aj llvm?
17:15 mornfall hm, snad *_full
17:16 mornfall jo, tam to je
19:04 mornfall joined #divine
19:32 spito ha, přeložil jsem PDCLIB
19:33 mornfall v jakém kontextu?
19:34 spito v kontextu toho, že jsem překopal hlavičkové soubory
19:34 spito definice jednotlivých typů a tak
19:35 mornfall doufám že nějak smysluplně :-)
19:36 spito snaha byla
19:36 spito bych to mohl zarecordovat a poslat, co?
19:36 mornfall můžeš to zkusit :-)
19:41 xstill mornfall: newrapovanej clang je podle mě na nic, protože to pomůže jen tomu, že si těch problémů nevšimneme
19:41 mornfall xstill: jakto?
19:41 mornfall wrapovanej prostě nemůže nikdy fungovat
19:42 mornfall můžeš mu cpát -noXXX kolik chceš, to ty -I co tam dá ten wrapper nepřebije
19:42 xstill ad ten linker error, no je to chyba z toho jak linker načítá modul… jako dalo by se tam napsat, že je to load no
19:43 mornfall no já si to našel ve zdrojáku, bez toho bych měl nulovou šanci pochopit co je špatně
19:44 xstill testuje clang_med a gcc_full ty mají ntree i llvm
19:45 xstill jo on ten wrapper tomu cpe přímo -I?
19:45 mornfall a co by tak jinýho mohl udělat?
19:45 mornfall ty builtin cesty jsou... builtin
19:45 xstill nevím, sem myslel že existuje něco trochu inteligentnějšího
19:45 mornfall jo, libclang :)
19:46 xstill tak spíš něco na způsob -B, ale to zase asi nejde použít jen na include
19:48 mornfall to se nevztahuje na libc a u clang-u to ani není zdokumentovaný
19:48 mornfall resp. gcc to interně přepíše na -isystem
19:48 mornfall (což je -I minus warningy)
19:50 mornfall i když je asi pravda že ty -I dává ten wrapper na špatný místo
19:50 mornfall což se může opravit
19:51 mornfall ale furt to bude mít ten efekt že to bude vesele nacházet systémový headery který nejsou překrytý
19:51 mornfall což je špatně
19:51 xstill no pokud to -no* funguje mimo nixos tak můžeme vesele používat wrapper
19:51 xstill teda newrapper
20:23 spito mornfall: asi mi hrabe, ale mohl bys mi prosím vysvětlit kód v divine/external/pdclib/_PDCLIB_config.h:297 ?
20:23 spito obzvlášť nechápu to +sizeof(type)-sizeof(type)
20:25 mornfall protože blbě vidíš
20:25 mornfall to je +=...-...
20:25 mornfall ap se na pravé straně makra nesmí objevit víc než jednou, protože vedlejší efekty
20:25 mornfall tohle je postfixový ++ jen ne o 1 ale o sizeof(type)
20:30 spito jo, blbě vidím
20:30 spito vždyť jsem to psal, že mi hrabe
20:31 spito ještě - __divine_memcpy modifikuje paměť z oblasti, kterou kopíruje?
20:31 spito že má v hlavičce jenom void *
20:31 spito a ne const void *
20:33 mornfall to asi záleží jestli se počítá případ kdy se src a dst překrývaj
20:34 mornfall hm, zapomněl jsem na break
20:34 mornfall to je dost trapný :D
20:41 mornfall hm, trochu trapný je že počet vláken budu asi muset přilepit k prvnímu vláknu
20:41 mornfall protože vyrobit na to extra čtyřbajtovej chunk je tak trochu antiefektivní
20:42 mornfall upravovat splitHint tak aby mohl ten stav aj přeskládat se mi teď úplně nechce
20:50 mornfall xstill: nechce se ti zjistit jestli to někam vede? :) jestli máš nějakej příklad kterej se nepočítá moc dlouho
20:50 xstill můžu to zkusit, pošli mi patch
20:50 mornfall už jsem ho pushnul
20:51 mornfall defaultně tam je ten novej (rozpracovanej) splitter
20:51 mornfall momentálně respektuje hranice globálních proměnných a vláken
20:51 xstill hm, aisa mi zalčela všechny maily mimo inbox od 27. :-/
20:52 xstill jdu si udělat build
20:52 xstill dá se to i nějak přepínat potom?
20:52 mornfall ve zdrojáku
20:53 mornfall ale já bych byl pro commandline switch (tys byl proti)
20:53 xstill no protože to znamená instanci nejspíš
20:53 mornfall kdyby jednu :)
20:53 xstill no právě, alespoň 4
20:54 xstill pro každý algoritmus
20:54 xstill jako cmake přepínač by mi přišel jako rozumný kompromis
20:55 mornfall něco jako DEV_NOPOOL jo?
20:56 mornfall tam je otázka jestli to budem chtít ještě někdy benchmarkovat
20:56 mornfall a jestli chcem psát nějakej benchmarkovací udělátor
20:57 mornfall protože asi nechceme aby to rebuildovalo divine podle toho jaký tomu chceš dát parametry
20:58 xstill tohle asi zrovna nebudebe potřebovat měřit znova. Udělátor by to docela chtělo ideální by bylo mít něco co by pouštělo divine pravidelně a upozorňovalo na změny, ale to mi příjde jako plýtvání časem pro kohokoli z nás tří…
20:58 mornfall (a další věc je, že když se bude někdy divine jit-ovat tak je jedno kolik má instancí)
20:58 xstill někdy…
20:59 mornfall no, mě to už asi brzo omrzí a naimplementuju to
21:02 xstill hm, tak nevím jestli za to může moct to že mám build s podporou valgrindu, ale moc dobře to zatím nevypadá. Ještě to přebuilduju
21:07 xstill jako že o 15% víc paměti při stejném počtu stavů za 2x čas :-/
21:10 mornfall no, valgrind má dost velkej overhead
21:12 mornfall 8M konstanta + 8 bajtů na blok nebo něco takovýho
21:15 mornfall (ale jestli to udělá 15 procent to fakt nevim, asi spíš ne, pokud to nebylo něco hodně malýho)
21:18 mornfall jako riziko s tímhle splitterem je že to nadělá hodně „ocásků“ když bude typickej thread mít třeba 20 bajtů
21:19 xstill hm tak bez valgrindu se docela spravil ten čas (je to pro změnu rychlejší), ale pořád je to horší paměťově (2540 b/stav vs 3226 b/stav při 200K stavech)
21:21 mornfall můžeš ještě zkusit zakomentovat generator/llvm.h:217 (celej ten case ChunkT::Threads) a zkusit to jen s těma globálníma proměnnýma?
21:21 mornfall a ideálně pak ještě zakomentovat ten nad tím (globals) a ten threadovej nechat
21:22 mornfall teď jsem si uvědomil že globals udělá jeden uzel se spoustou dětí
21:22 mornfall takže se to může chovat výrazně jinak
21:22 spito mornfall: k poslaným patchům
21:22 spito llvm: Add FileSystemError as a Problem.
21:22 spito je špatně?
21:23 mornfall no, nemam z toho zrovna radost
21:23 mornfall dost to kazí dělení vrstev
21:23 spito a co by místo toho mělo být?
21:23 mornfall jakože divine zrazu ví něco o nějakým filesystému
21:24 mornfall zatím asi Other
21:25 spito ok
21:25 mornfall ono to bere textovej popis jako další parametr
21:25 mornfall počítám že časem si bude moct model deklarovat nový typy problému (stejným mechanismem jako APčka)
21:26 mornfall (jen se to bude muset dělat nějak jinak než enum-em, ale to aj pro ty AP)
21:33 xstill bez threads zdá se pořád špatný (+ 15%)
21:34 mornfall takžé to bude ten dlouhej node... asi; uvidíme
21:34 mornfall takže*
21:35 xstill jako pořád by to asi chtělo změřit na víc modelech…
21:35 xstill ale i tak
21:36 spito mornfall: pačééé
21:45 xstill hm, bez globals je to +- stejné
21:46 xstill (s threads)
21:53 spito mornfall: a ještě jeden chybějící cmake
21:54 spito jinak testoval jsem změny oproti divine functional a všechny llvm testy proběhly
21:54 mornfall hm, nevim jestli se mi tenhle směr úplně líbí... jakmile někdo hrábne v pdclib-u na ty makra a budeme to mergovat tak z toho bude milion konfliktů
21:56 spito zase jsem nechtěl dělat userspace úplně závislým na pdclibu
21:57 spito a jinak - jak to tedy udělat lépe?
21:57 spito změnit jenom makra v _PDCLIB_config.h?
21:59 mornfall no, v první řadě nechápu co je špatně na těch co tam jsou a pokud tam je chyba proč ji prostě neopravit?
22:00 spito protože používám specifické clang makra
22:01 spito v bits/types.h
22:01 mornfall no dobře, ale k čému to bits/types.h je?
22:01 mornfall čemu*
22:01 mornfall kruci
22:01 spito k definici typů
22:02 spito aby celý userspace nebyl závislý na _PDCLIB_int16_t
22:02 spito a podobně...
22:02 mornfall protože int16_t z stdint.h nejde použít?
22:03 spito ale jde
22:03 spito tak já to někdy změním
22:03 spito teď jdu spát
22:50 mornfall hm, já bych asi měl vyrobit slajdy nebo co

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