Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2015-07-20

| 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:12 xstill joined #divine
06:50 xbarnat joined #divine
07:06 xstill xbarnat: do svn jsem nahrál první hodně hrubý draft části memics článku, ještě nemá moc smysl aby to někdo po mě upravoval, zbytek textu bych chtěl tak do středy dodělat
07:06 xbarnat ok
07:06 xbarnat jak je na tom implementace?
07:08 xstill je v takovém stavu, že to na memics +- stačí -- umíme TSO, jen neumíme uklidit stack (takže nemumíme testovad bad dereferrence), a chybí podpora pro foating point typy a základní typy větší než 64 bit, což nám ale zatím nevadí asi. Jediné co by do memicsu mohlo být vhodné je ta fairness vylévání bufferů, ale to pokud bude fungovat tak je věc na naprogramování max za půl hodinu
07:09 xbarnat nejaky obrazek transformace bude?
07:09 xstill já akorát teď nevím kdy se objevím v labu, nejpozdějš ve středu, ale do té doby nevím jak mi to výjde
07:10 xstill jaký obrázek transformace?
07:10 xbarnat no treba kde a jak se dela buffer ...
07:10 xstill jo, to jo
07:10 xbarnat kdyz dve vlakna zapisuji do stejne promenne a ctou ..
07:10 xbarnat ok
07:11 xstill ještě mi chybí popsat celá implementace a poladit ten text, obrázky příjdou potom
07:11 xbarnat kdy je deadlina vlastne?
07:12 xstill v pátek na abstrakt, příští na celé, jenže já tu příští týden velmi pravděpodobně nebudu
07:29 mornfall ve středu se můžu v labu objevit taky
07:43 mornfall 13:30 mám zápis tak někdy do té doby (a tento týden v pátek nebudu)
07:43 mornfall spito: asi by nebylo zlý kdyby student mohl tu prezentaci udělat ve středu dopoledne
07:47 xbarnat na webu paradise kdysi byly fotky ze starych petnague closed a pleneru ... jsou tam nekde jeste? nevite?
09:22 spito mornfall: v kolik a kde?
09:51 xbarnat proc ve fifo.cpp v examples/llvm se predefinovava new ?
09:55 xbarnat redukce stavoveho prostoru ...? asi
10:02 xstill xbarnat: jo redukce stavového prostoru
10:06 spito mornfall: hmm, hlásí se mi další student, mám si ho vzít? :D
10:09 * spito -> ven
10:41 mornfall xbarnat: s tím že mask/unmask by se mělo dát k dispozici uživatelům docela nesouhlasim, je to fakt nebezpečný
10:41 mornfall je teda pravda že je to lepší než to bývalo, když už není interrupt, ale i tak
10:42 xbarnat naivni blbec to nepouzije, a clovek, kterej poterbuje redukovat stavovy prostor protoze ho zajima jen jedna konkretni vec,  nekde v kodu, dle me to pouzije smysluplne ...
10:42 mornfall by ses divil co všechno naivní blbec použije
10:42 xbarnat stejne jako __divine_choice,
10:42 mornfall viz CESMI
10:43 xbarnat stejne jako predefinovavat new kvuli redukci stavoveho prostoru ...
10:43 xbarnat proste me to prijde fer ... rict, ze to existuje, pouziti samozrejme na vlastni nebezpeci ...
10:44 mornfall a ten operator new ve fifo.cpp není ani tak kvůli redukci jako kvůli tomu že se nechtělo řešit OOM
10:44 mornfall ten model je jinak dost malej
10:44 xbarnat OOM?
10:45 mornfall out of memory
10:45 mornfall k mask/unmask bych asi radši vyrobil ty atributy jak jsme to řešili v pátek... tzn. atribut pro funkci který ji označí jako atomickou
10:45 xbarnat aha, no ale kdyz to smazu, tak verify projde ... takze moc nechapu co to resi
10:46 xbarnat no ale porad mam typicky zacatek programu, kde vytvarim vlakna a cosi kdesi, kde nechci aby se mi to prokladalo ...
10:47 xbarnat proste zatajovat to, me prijde ujety ... leda bysme chteli to do budoucna zrusit ....
10:47 mornfall mi*
10:48 mornfall no, a kolikrát jsi použil SYSCALL napřímo?
10:48 xbarnat 1) nevim co to je a 2) me to urazi
10:49 mornfall no, jak často voláš jádro podle čísla, aniž bys použil libc?
10:49 mornfall __divine_* je nebezpečný a interní
10:49 xbarnat stejne tak, je dle meho nazoru naprosto korektni rici, ze zakomentujte si couty/printfy, protoze delaji ve stavovem prostoru neplechu, a chyby vznikle prolozenim s couty (ne ze by nebyly) jsou irelevantni ...
10:49 mornfall pokud to chceme nějak dát uživateli, mělo by se pro to vymyslet slušný rozhraní
10:50 xbarnat asi jako divine_choice?
10:50 xbarnat to je prece taky __divine_choice ...
10:51 xbarnat ok o patro vys, myslim si, ze je treba dat uzivateli moznost oznacit neco jako atomicke
10:51 mornfall to taky nechceš moc napřímo používat
10:51 mornfall záleží co si představuješ jako uživatele
10:52 xbarnat mozna teda __i_mask a __i_unmask nejsou optimalni, ale proste do modelarskeho pouziti model checkingu to patri
10:52 mornfall jo, ale 'modelářsky' to nikdo moc používat nechce, aspoň ne mimo 'komunitu'
10:52 xbarnat nedeterministicka volba, i atomicka sekce, ja to bezne pouzivam, oboji
10:53 xbarnat viz clanek na icfem :-)
10:53 xstill tak jako někde by mělo být napsané co to dělá, už proto, aby to věděli budoucí vývojíři. A dokážu si představit, že to člověk použije.
10:53 mornfall xbarnat: nojo, ale ty nejseš cílovej uživatel... ty to používáš jako lepší DVE
10:54 xstill no otázka je kdo je cílovej uživatel, můžeš to napsat jako manuál pro pokročilého uživatele, když to někdo použije blbě, jeho mínus
10:54 mornfall a to je sice taky použití, ale jakmile to bez atomických sekcí nejde moc používat, tak to vlastně nejde moc používat vůbec
10:55 mornfall jeho mínus, ale naše špatná reklama
10:55 xstill tak co když si budeš chtít namodelovat vlastní vlákna nebo něco
10:55 mornfall tady to divine zverifikoval a ono to v reálu padá
10:55 xbarnat atomicky sekce jsou zeleny, min stavu, kratsi vypocet, mensi naroky na spotrebu energie ...
10:55 xbarnat tady to je co?
10:56 mornfall no, cokoliv co obsahuje chybu v použití atomických sekcí
10:56 xstill nepříjde mi prostě úplně dobrý to tajit, ale je třeba k tomu napsat dostatečně důrazně že to nejspíš nepotřebují
10:57 xstill mornfall: ale __divine_interrupt bych asi zničil, pokud nemáš v úmyslu ho někdy oživovat (doufám, že ne)
10:58 xbarnat porad si stojim za tim, ze zatajovat to je divny ... a melo by to byt v manualu ... v sekci LLVM a boj se stavovou explozi ...
10:59 mornfall jo, jenže v manuálu chybí asi sto důležitějších věcí (a v kódu taky)... nemluvě o tom že ten manuál stejně nikdo nečte?
10:59 mornfall a když se do něj podívá tak akorát najde jak se ty funkce jmenujou a popis si domyslí z názvu
10:59 mornfall jak to lidi typicky dělaj
11:00 mornfall radši bych to zkusil udělat tak aby atomický sekce fakt nebylo potřeba použít, aspoň v 99 % případů
11:06 mornfall btw. ta fairness se store bufferama nefunguje sama od sebe?
11:07 mornfall hm, jo, tak jak je flusher() napsaný tak asi ne
11:07 mornfall ale mělo by být triviální to opravit
11:24 xstill no to je to co jsem psal dopoledne
14:31 mornfall mám něco dělat s článkem? vím že mam učesat scalarmem a pushnout patche, ale jinak?
14:32 mornfall jinak je asi pomalu čas zamyslet se nad testama pro lart :-)
14:32 mornfall teďka to ještě nechám, udělám release (jen opravim ty instances) a pak bychom se na to mohli podívat
14:37 mornfall hm to bylo jednodušší než jsem čekal
15:31 xstill co?
15:31 xstill na článek asi jinak nic (zatím, pak budu chtít abys to přečetl)
15:46 mornfall no, ten bug s instance.sh
15:46 mornfall nicméně to teď segví takže to zas tak jednoduchý asi nebude
16:52 mornfall to je dost veselý že partial matching v brick-commandline kdy fungoval :-)
16:52 xstill jakto?
16:52 mornfall _partialMatches vrací iterátor do lokální mapy
16:52 mornfall (už jsem to opravil)
16:52 xstill zajímavý
16:52 xstill asi jsem měl slabší chvilku
16:54 xstill na to to fungovalo docela dobře no…
17:01 mornfall (aspoň teď vím že mam zaplej debug malloc v celým systému, to je až s podivem že funguje docela rychle :P)
17:08 xstill se divím že jsme si toho nikdy ve valgrindu nevšimli
17:09 mornfall asi to ve valgrindu pouštíme vždycky s plnýma switchema
17:09 xstill pokud jsem to kdy pouštěl ve valgrindu s kompresí tak dost pravděpodobně ne, ale to je fuk
17:10 mornfall ono to docela řvalo, to by sis asi všiml
17:10 xstill tak jsem to asi nepouštěl
17:55 xstill mornfall: no, mohl bys mi alespoň poslat scalarmem kterej má opravený to rozbíjení basic bloků
17:59 spito mornfall: student dojde ve středu v 11:00
17:59 spito má prezentaci v google docs (latex se prý nestihl naučit)
18:00 xstill hmhm, já s Jiříkem máme schůzku na IB015 od 10, ale tak to asi budeme muset buď stihnout nebo přerušit
18:21 spito to jsem v logu nenašel
18:21 xstill ono to tam není
18:26 xstill hm asi není šance donutit clang aby konstantu nezainlinoval, co?
18:28 spito vzít adresu?
18:29 xstill teda přesnějš chci aby se skutečně loadovala na všech místech který ji používaj
18:30 xstill asi ne, vrazím tam nekonstantu a bude
18:31 mornfall spito: ok budu tam
18:31 spito bych prosil... :P
18:32 mornfall resp. budu tam už asi v 10:15, ne-li 9:15
18:58 xstill mornfall: pošli mi ten opravenej scalarmem
18:59 mornfall rozkaz...
19:31 xstill dík
19:31 spito xstill: nemáš nějaký kontakt na Heňu?
19:31 spito protože jinak budu muset napsat rozhraní pro sockety do divine sám :/
19:31 xstill kromě mailu?
19:32 xstill jako facebook, ale dost pochybuju že ti z třítýdenního cyklovíletu napíše sockety…
19:32 xstill budeš muset čekat nebo si je napsat sám
19:33 spito *výlet ;)
19:33 spito kdy se vrací?
19:34 xstill odjely tak minulý týden
19:35 xstill 13.
19:41 mornfall odjeli*
20:00 xstill začínám mít největší strach z toho, že to prostě nedáme zverifikovat, člověk přidá k module co má 400 stavů store buffer velikosti 1 a ono to má přes 4M stavů a ne a ne končit
20:09 mornfall o tom tak trochu víme, žejo :) někam jsem kdysi psal že se bude muset zapracovat na redukcích ;-) aby to šlo reálně používat
20:26 xstill nicméně je docela pěkné, že divine u mě generuje 7k stavů za sekundu
20:30 xstill tímhle tempem začíná být 8GB paměti už zase málo na divine
20:46 mornfall jo, trochu jsem to vylepšil minule
20:47 xstill nojo, ale že já se vůbec snažím to počítat u sebe, aura dělá 90k/s
20:49 xstill počítám-li správně tak za 12-24 hodin naplníme celou paměť na auře… to je docela pokrok oproti těm skoro dvěma týdnům když jsem to naposledy zkoušel…
20:49 xstill mornfall: co jsi s tím udělal?
20:50 mornfall ono tou změnou kolem mask/unmask se isPrivate volá ještě výrazně víckrát, takže jsem to přepsal aby to běhalo rychle
20:51 mornfall ještě tam je prostor to trochu stáhnout, ale asi až po releasu
20:51 xstill :-)
20:51 xstill už aby byl ten novej server…
20:56 xstill spito: zkoušel jsi někdy benchmarkovat tu tabulku při větším prahu zaplnění než těch ?
20:56 xstill 75%
21:00 xstill si tak říkám, že při těch miliardách prvků by mohlo stát za to to posunout, přeci jen plýtváme dost paměti
21:00 mornfall já jdu spát, dneska jsem rozebral něco jako 3/4 tuny komína a nějak mě to zmohlo... zítra snad dořeším release a patche &c.
21:01 xstill já budu zítra přes den asi offline, ale k večeru už tu zase budu
21:28 spito xstill: ne
21:33 xstill a máš nějaké benchmarky, které se dají jednoduše pustit?

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