Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2016-08-25

| 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:21 yaqwsx joined #divine
07:21 mornfall yaqwsx: brýtro
07:21 mornfall ten syscall flag nemusí být nutně uvnitř kontextu
07:22 mornfall a privilegovaný mód jaksi potřebujeme
07:24 mornfall jde o to, že ke globální proměnné se dostane uživatelský program a mohl by pak rozhasit stav dios-u
07:32 yaqwsx Ok, to dává smysl. Takže si ještě píšu na svůj todo list změnit ten flag na globální a implementaci syscallů předávat context explicitně.
07:33 mornfall OK
07:36 yaqwsx A teď ještě jeden dotaz k faultům; včera jsme se bavili, že po faultu, který nepokračuje, bych mě nastavit flag pomocí __vm_trace a v scheduleru pozabíjet vlákna -> je třeba je zabíjet? Nestačí prostě ze scheduleru vrátit null?
07:36 mornfall no nestačí, null by znamenalo že tam žádný stav není
07:39 yaqwsx Ok, myslel jsem, že i __vm_trace umí vyrobit stav. Teďuž je to jasné
07:40 mornfall __vm_trace jen něco ohlásí, ono by to šlo ohackovat tak, že divine by něco vyrobil když dostane null ale na tý hraně byl flag, ale moc hezký by to nebylo
07:40 yaqwsx JJ, jasné.
09:09 yaqwsx U mě v homu je první verze fault handleru. Má hotové API pro konfiguraci z pragramu, UI ještě chybí.
09:14 mornfall teď vlastně nevim jestli má smysl aby __vm_trace( _VM_T_Flag ) jakýkoliv další parametr bral
09:14 mornfall ale to pak upravím
09:17 mornfall není to #ifdef __cplusplus v dios/syscall.h trochu divný?
09:19 xstill_ mornfall: ten flag má být jen goal?
09:19 mornfall resp. asi bych cokoliv co je uživatelské přesunul do dios.h a dios/*.h nechal jako interní hlavičky dios-u?
09:19 mornfall případně dios/*.hpp
09:20 mornfall xstill_: no já nevim jestli má nějakej smysl tam něco rozlišovat
09:20 mornfall možná error a accepting
09:20 mornfall proto tam ten parametr vlastně asi je
09:20 mornfall ale enum jsem k tomu nevyrobil :)
09:21 xstill_ to možná jo, i když pak je skoro otázka jestli radši nemít _VM_T_Error/_VM_T_Goal a _VM_T_Accepting
09:21 yaqwsx mornfall: Tak to je myšleno, to #ifdef __cplusplus je relikt z původního rozdělení DiOSu, který mám teď v plánu při změně Sycallů odstranit
09:21 yaqwsx BTW: Teď jsem si uvědomil - Divine používá *.hpp, neměl by i DiOS, ať jsme konzistentní?
09:22 mornfall yaqwsx: ok, jen jsi ho tam zrovna teď přidal :-)
09:22 xstill_ ono to stejně teď není konzistetní, lart používá .h
09:22 yaqwsx Meh, tak to jsem nechtěl... :/
09:22 mornfall no tak přesuneme i lart na .hpp
09:22 xstill_ to můžem
09:22 mornfall to není takovej problém
09:22 mornfall radši ne hned teď, protože Heňo z toho zešediví
09:23 mornfall ale už by to mohl dotáhnout a pak už můžem
09:23 xstill_ On LART je stejně zralý na refaktoring, je to celé horzně upatlané
09:23 mornfall no to je
09:23 mornfall čím dál tim víc :)
09:27 yaqwsx Po obědě tedy předělám ty sycally a na závěr přesunu dios/*.h na dios/*.hpp
09:27 mornfall fajn
10:03 yaqwsx Chápu správně, že zápis do globálních proměnných je drahá operace, kvůli které se musí zkopírovat všechny proměnné, že? Takže je lepší si při implementaci sycallů nechat globální jenom ukazatel a měnit malý blok paměti naalokovaný pomocí _vm_make_object?
10:22 mornfall yaqwsx: zas tak horký to není
10:23 yaqwsx Ok. Jak na tom vlastně jsme s rychlostí teď?
10:24 mornfall furt stejně, ale zase co chceš když stavy ukládám do std::set a operator< je, no, dost drahej
10:24 mornfall (ale pracuju na tom)
10:29 mornfall xstill_: btw. jedna věc která by mohla všemu dost pomoct je oddělat mem interrupty které náleží striktně lokálním proměnným (tzn. neutíkajícím alloca)... co si pamatuju tak na to už v lartu něco bylo
10:29 yaqwsx Lart má v sobě escape analýzu?
10:29 mornfall llvm snad dokonce
10:30 mornfall asi nebude moc chytrá, ale ono to v podstatě asi stačí
10:30 mornfall je teda pravda, že jak jsem to tak procházel v sim-u, tak většinu alloca oddělá optimalizátor úplně
10:31 mornfall (počítám že podle tý stejný escape analýzy)
10:31 xstill_ yaqwsx: něco jo, ale funguje to trochu divně tuším
10:31 xstill_ yaqwsx: proč?
10:33 yaqwsx xstill_: Jen tak, jak jsem před pár týdny četl ten článek, tak jsem nabyl pocitu, že pořádná escape analýza je asi peklo naimplementovat.
10:34 mornfall yaqwsx: no to záleží, je relativně jednoduchý to dobře aproximovat
10:34 mornfall (a bezpečně)
10:34 yaqwsx mornfall: proto tam bylo to slovo "pořádná" ;)
10:35 mornfall tam je čistě otázka kolik toho dokážeš ještě ušetřit
10:35 yaqwsx Samozřejmě
10:35 mornfall protože pokud ti v celým programu zbydou 3 alloca tak nemá smysl investovat měsíc práce do lepší analýzy, abys zničil tu 1 která ve skutečnosti neutíká :))
10:36 xstill_ yaqwsx: co to bylo za článek?
10:38 yaqwsx Ten, který jsem ti slíbil a stále ještě nenašel :D
10:38 yaqwsx Resp. to byl článek + dizertačka nějaké holky.
10:38 xstill_ aha… to už jsem zapomněl
10:40 yaqwsx BTW: Už se ví letošní téma Paradise semináře?
10:44 xstill_ asi nejlepší by bylo prostě prezentovat nějaké články
10:48 xstill_ pobavíme se o tom s Jiříkem
11:40 xheno joined #divine
11:49 xstill_ yaqwsx: jo tak prezentace článků, třeba z CAVu prej
11:50 xheno mornfall: Mam problem s buildom aktualneho divinu. Chyba mu subor 'histedit.h'.
12:21 xstill_ (už to našel)
12:29 mornfall nj já byl venku
12:30 xstill_ chtělo by to přidat check do cmake
12:32 mornfall chtělo
13:12 mornfall xstill_: určitě jsi dobře zarecordoval ty tabulky na haldě?
13:12 mornfall xstill_: jak to je to nemůže fungovat...
13:35 xstill_ mornfall: proč?
13:37 mornfall protože sice vyrábíš nový objekty v haldě ve vm::Program, ale pak je vesele zahodíš
13:37 xstill_ ne, však je zapíšu (writeMetaElem)
13:38 mornfall no ale to je furt v tý dočasný haldě
13:38 xstill_ no a to se nevyexportuje samo?
13:38 mornfall jak samo?
13:38 mornfall vždyť jsme řešili že se musí opravit exportHeap aby používal clone
13:39 xstill_ to jsem dělal
13:39 mornfall a přesně na to se ptám, protože v patchi to není :)
13:39 xstill_ aha není
13:39 xstill_ sorry
13:39 xstill_ já zapoměl, že je to v program.hpp a ne .cpp
13:39 xstill_ mám to amendovat nebo už to bylo v nextu?
13:40 mornfall přidej to jako extra patch radši
13:40 mornfall xheno už to asi má taky
13:41 xstill_ je to tam
13:41 mornfall ok
14:26 xstill__ joined #divine
15:37 mornfall no, máme to dobře otestovaný, hashset::Concurrent s velkým klíčem vůbec nefunguje :P
15:40 xstill__ hm? no fast verze nejde přeložit pokud má klíč víc než 64b, ne? nebo ještě něco jiného?
15:41 mornfall no hashset::Concurrent< T > se zacyklí a vůbec se neobtěžuje testovat rovnost
15:42 mornfall no to je jedno nějak to vyřeším
15:42 xstill__ aha, to je veselý, co tam máš za klíče?
15:43 mornfall struktura ze 4 pointrů
15:45 mornfall nějak se ti množí podtržítka :D
15:57 xstill__ jo, protože jsem si zabil xka a přihlásil se dřív než ten starej stihnul vytimeoutovat
16:00 mornfall a já se zase divim proč je hashset pomalejší než std::set... jsem to pustil v debug-u
16:03 xstill__ hm, skoro bych čekal, že debug hashset bude rychlejší než debug std::set
16:04 mornfall no jistě, std::set jsem právě pustil správně (v release)
16:04 xstill__ aha :-D
16:16 mornfall searching: 9583 edges and 5100 states found in 0:04, for 1275.0 states/s average
16:16 mornfall to už je trochu lepší :p
16:17 xstill__ to dost
16:17 xstill__ jednovláknově?
16:17 mornfall jo, vlákna jsem ještě neřešil
16:17 mornfall musím opravit ten concurrent hashset prvně
16:17 xstill__ tak to je slušná rychlost
16:18 xstill__ starej divine dělal podobnou (s kompresí a s tau teda)
16:19 xstill__ co jsi s tím udělal?
16:21 mornfall nic zásadního, pár drobností... to bude ještě plavat sem tam
16:25 mornfall (a tau+ tam teď je, ale taustore ne)
16:44 yaqwsx joined #divine
17:09 spito co se v concurrent hashsetu pojebalo?
17:10 spito ah, už to vidím
19:28 xstill_ joined #divine
19:55 xstill joined #divine

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