Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2016-09-08

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

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #divine
01:48 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
09:03 xstill_ hm, ten Katky problém je dost divnej, ono se to na ten soubor ve filesystem ani neptá
09:07 mornfall nesnaží se vylistovat ten adresář nebo tak něco?
09:10 xstill_ ne, ono to totiž nemá fungovat :-/ ona má fs-storage.h v runtime/ a ten dělá #include "fs-utils.h" který je ale v runtime/filesystem
09:11 xstill_ a samozřejně fs-storage se najde, protože je v -I
09:14 xstill_ je možné, že ve starém compile bylo -Ifilesystem u kompilace fs
09:15 xstill_ jo, byl tam
09:23 xstill_ jinak ad divine-cc došel jsem k tomu, že je nutné mít možnost kompilovat s různými define pro divine a native (minimálně kvůli libc a libunwind). To ještě není problém, předpokládám, že bych přidal přepínač, který umožní kompilaci "rozdvojit" a případně přidat define pro DIVINE. Tím by se snad měla dát pokrýt libc, co je trochu větší problém je potenciálně libunwind,
09:23 xstill_ tam hrozí, že ta knikovna bude úplně jiná (moc se mi nechce prasil LLVM libunwind tím, že bych do něj přidával spoustu define, navíc máme podporu jen pro exception část libunwindu a ne pro celý (zatím)). Problém není ani tak kompilovat to zvlášť, jako že to rozbíjí práci s archivy, já totiž teď předpokládám, že mi stačí k bitcode přilikovat právě bitcode objektů
09:23 xstill_ odpovídajících elf objektům které se přilinkovali k native, což předpokládá, že native i divine implementace stejné funkce je vždy ve stejném .o. Otázka je jestli to pro libunwind nějak dohackovat (typu k DIVINE bc se vždy nakonec přilinkuje ten jeden object file s libunwind), nebo to řešit nějak složitěji
09:25 mornfall no, vyrobit libunwind.a ve skutečnosti zas takový problém nebude, i kdyby se měla lepit 'ručně'
09:26 mornfall jaký #define potřebujeme pro libc?
09:26 mornfall (teda takto, pokud to je jen v implementaci tak to takový problém není, pokud to má dopad na hlavičky je to horší)
09:26 xstill_ no předpokládám, že libc bude potřeba na divine nějak portovat, že to nebude úplně stejný kód co na linux
09:27 xstill_ no to doufám, že na hlavičky ne, to by byl problém
09:27 xstill_ rozhraní funkcí musí být stejné, jinak se to asi dost rozbije
09:27 xstill_ ale zas to je definované
09:27 mornfall taky si myslim
09:28 mornfall pokud jde o rozdvojený překlad, přidal bych přepínač
09:28 mornfall kterej danej unit přeloží s -D__divine__ pro .bc a s něčím jiným pro nativní kód
09:28 mornfall a používal ho jen na ty soubory kde to bude potřeba
09:29 xstill_ OK, asi bych vždy definoval něco jako __divinecc__
09:29 mornfall resp. to by bylo asi nejjednodušší, #pragma by byla možná trochu elegantnější
09:29 xstill_ pragma která to rozdvojí?
09:30 mornfall jo
09:30 xstill_ to bude trochu težší
09:30 mornfall no, ušetří to starosti v buildsystému pak... ale jo, je to víc práce (no, nebo se to může vygrepovat, že)
09:30 mornfall ^#pragma a nějakej vhodnej regex to jistí ;-)
09:31 mornfall případně jen pak dolepit někam do clang/ prázdnou implementaci aby neházel warningy
09:33 mornfall jiná (možná nakonec ještě lepší) možnost by byla systémově závislý knihovny lepit až jako .a
09:35 mornfall (teda, ono by to prostě šlo udělat tak, že když máš krom .a ještě .bc tak se použije to .bc, kdyby to .a obsahovalo bitkód tak to vypíše warning)
09:35 mornfall u knihoven tohle zdaleka nevadí tak jako u .o, protože na ty systémový nám nebude buildsystém moc hrabat
09:36 mornfall a všechny ty kterých se to týká budeme stejně portovat ručně, takže kdyžtak si přiohneme trochu aj ten build
10:53 xstill_ jo, umět to lepit ručně by taky bylo užitečné
11:03 xstill_ joined #divine
12:01 xstill_ hm, iterovat přes všechna metadata v modulu je těžší než bych čekal
13:41 xstill_ mornfall: tak já tu nakonec ve středu budu (den otevřených dveří je ve čtvrtek), ale budu mít asi od 3 schůzku s Nikolou
13:41 xstill_ Honza a Heňo tu nebudou
13:46 xstill_ ha, možná jsem zvítězil na debug info
13:55 xstill_ hm, objevují se tam podezřelé cesty typu /home/xstill/DIVINE/divine4/runtime/pdclib/functions/wctype/<stdin>
13:55 xstill_ to by mě zajímalo kde se to vezme
14:00 mornfall <stdin>?
14:00 mornfall nevim no :)
14:19 xstill_ hm,  (std::for_each( rs.begin(), rs.end(), [&]( auto *x ) { rewriteFileDebugPath( x->getFile(), map, ctx ); } ),...); to je zas jednou C++
14:20 mornfall tak, nemusí to být nutně za každou cenu patch na jeden řádek :P
14:21 xstill_ no to není
14:21 xstill_ jenže tam je pět různých věcí z kterých se tahaj ty DIFile a každý je range jiného iterátoru, takže se přes to dost blbě iteruje normálně
14:21 xstill_ a 5 je dost na to aby to bylo 5 stejných for cyklů pod sebou
14:22 mornfall nojo
14:22 mornfall jen doufám že to nikam jinam než do DIFile necpou...
14:22 xstill_ to taky doufám
14:22 xstill_ ale to zjistím
14:23 xstill_ hm, akorát mi pořád nějaké přežily :-/
14:24 xstill_ a pak je ještě otázka co s directory v DIFile, ale to vypadá, že je working dir kompilátoru, tak to bych asi nechal
14:26 mornfall no, zatím to k ničemu nepoužíváme, takže to asi není potřeba řešit
14:37 mornfall hm, chce to __sync_val_compare_and_swap_16 a není mi úplně jasné proč
14:38 xstill_ někde máš 16B atomic asi
14:39 xstill_ nemáš fast hashset s nějakým velkým klíčem?
14:39 mornfall no jedině v hashtabulce, ale kde se tam bere
14:40 mornfall (a je to obráceně, Fast má 32b hashlock, 128b CAS by mohl chtít leda AtomicCell)
14:40 xstill_ jo, to jsem myslel
14:41 mornfall nicméně když tam dám static_assert na sizeof(...) == 8 tak to prochází, tak nevim
14:41 mornfall je to akési čudné
14:41 xstill_ a neřekne kde to chybí, to by skoro mohl, ne?
14:43 mornfall no, je to celý zainlinovaný do Verify::run() :P
14:43 mornfall takže linker už toho moc nezmůže
14:43 xstill_ :-D
14:43 xstill_ ty metadata jsou těžce retardovaný
14:44 mornfall to je ale divný, to je přece debug build
14:44 mornfall nojo ale clang
14:44 mornfall achjo
14:52 mornfall aha ne ono to je fakt přímo v tý funkci...
14:53 mornfall mea culpa
14:54 xstill_ kde?
14:56 mornfall no já tam měl std::atomic na explore::State místo na Snapshot
14:56 mornfall a ten state má navíc nějaký flagy
14:56 mornfall (tzn. nemohla za to hashtabulka)
14:57 xstill_ aha
15:07 xstill_ hm, tak jsem ten remaper napsal, ale bylo to výrazně náročnější než jsem čekal
15:07 xstill_ a je to hnusnýý
15:07 mornfall co z toho plyne? je nějaká lepší cesta?
15:07 xstill_ to ne, jen mě to nepotěšilo
15:08 mornfall teoreticky by šlo místo toho načíst ty dva adresáře celý do VFS
15:08 mornfall bude to asi pomalejší, ale třeba ani ne o moc
15:08 xstill_ tak když už to funguje tak asi není moc důvod
15:10 xstill_ příjde mi trochu ujetý, že to nejde udělat bez prolezení všech metadat jako grafu
15:13 xstill_ mornfall: je to u mě v repu
15:14 xstill_ ale alespoň jsem nakonec nepoužil ten úchylný fold
15:25 xstill_ ještě ti to amendnu
15:25 xstill_ (hotovo)
15:27 mornfall ok (už jsem to měl pullnutý, amendnutý byl jen ten poslení jo?)
15:27 xstill_ jo
15:28 xstill_ (jen jsem teda přehodil řádky kódu aby to dávalo větší smysl)
15:31 mornfall teď by mě zajímalo proč je hasher v concurrent hashsetu sdílenej
17:02 xstill mornfall: až budeš odpovídat tomu člověku z RH, tak vem v úvahu, že v pondělí nemůžu (ve středu bych mohl, i pokud by se to krylo s C++ poradou)
17:08 mornfall já bych mohl ve středu tak ve tři
17:08 mornfall ve dvě mám jakousi zkouškovou prezentaci v UKB...
17:08 mornfall z angličtiny
17:09 xstill OK, Nikola bude mít smůlu ale co už…
17:22 mornfall kdy a jak dlouho je plánovaný to C++?
17:23 xstill ve tři právě, těžko říct na jak dlouhou, asi 2 hodiny (a původně to stejně vypadalo, že tam nebudu moct být)
17:25 mornfall ono taky hrozí, že to bude v RH (což mi výjimečně zas tolik nevadí)
17:26 xstill mě taky ne
17:27 mornfall kdyby to bylo na FI, má pro tebe smysl jít na to C++ třeba na hodinu?
17:28 mornfall meeting ve 4 není tak tragicky pozdě
17:29 xstill jako má
17:33 mornfall ok, zkusím teda FI 16:00 a uvidíme co nám řekne
17:38 xstill ok
17:52 divine-buildbot joined #divine
19:23 divine-buildbot joined #divine
21:11 mornfall btw. nefunguje mi gdb -p na arke, prej permission denied na ptrace
21:11 mornfall (teda, mně funguje když před to napíšu sudo, ale to není úplně řešení...)
21:14 xstill jo, to je https://wiki.archlinux.org/index.php/Security#ptrace_scope, sám nevím jestli to vypnout nebo ne (capability není řešení protože pak se to umí attachnout k procesu kohokoli :-/)
21:18 mornfall tak, je otázka jak moc nám vadí normální ne-scoped ptrace
21:19 mornfall to tě ochrání jen když ti třeba někdo nabourá sandboxovanej proces a ptrace je jediná možnost jak se z toho sandboxu vylomit
21:20 mornfall a moc sandboxů tam řekl bych nemáme
21:20 mornfall služby počítám běhají jako oddělení uživatelé
21:25 xstill měly by
21:25 xstill zítra zjistím jak to vypnout, vypnul bych to teda všude kromě anny a pak antey (které stejně nechceme aby na nich lidi programovali)
21:26 mornfall jo tam je to jedno, jen se mi moc nechce štelovat to tak abych dostal test a případný gdb do stejnýho scopu
21:27 mornfall je teda otázka jestli někdo jinej někdy použije gdb -p :-)
21:28 xstill občas někdo, dost výjimečně
21:29 mornfall zdá se že vícevláknovej search už taky funguje, searching: 965655 edges and 506235 states found in 0:19, averaging 26635.5 states/s
21:29 mornfall na 8 vláknech na arke
21:30 mornfall vtipný je, že to dost krutě záleží na tom, kolik paralelizmu je v tom programu kterej to prohledává
21:30 xstill tak to dává smysl
21:30 mornfall když jedno vlákno dělá skoro všechnu práci, tak to zdaleka tak dobře neškáluje
21:31 mornfall dává no
21:31 xstill Jiřík bude mít radost, se dnes moc netvářil na to, že DIVINE verifikuje jednovláknově (místo aby měl radost, že je to i tak rychlejší než ve starém)
21:32 mornfall no, ještě aby to neleakovalo paměť na hranách a mohlo by to být podobně použitelný jako divine 3 (vyjma ltl, který jsme ale moc nepoužívali)

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