Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-01-15

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

All times shown according to UTC.

Time Nick Message
00:05 xstill joined #divine
06:32 ilbot3 joined #divine
06:32 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
08:24 xbarnat joined #divine
08:34 xbarnat zdravim vsechny chytraky
08:35 xbarnat jen jsem chtel (sice trochu se zpozdenim) prispet do diskuze  o fairness
08:36 xbarnat muj nazor je, ze tak jak je to implementovano ted je ok, ale ze uzivatel nutne potrebuje mit moznost tu weak fairness si zapnout, protoze detekovat chybi, ktere v navrhu jsou i kdyz uvazuji pouze fair scheduling je podle me fakt dulezite
08:38 xstill já souhlasím
08:38 xbarnat chyby*
08:39 xstill jak by se ta fairness dala implementovat? Jako jestli je to na úrovni generátoru nebo někde výš?
08:39 xbarnat no otazka zni jak to udelat sikovne, kdyz mi vznikaji a zanikaji vlakna ...
08:39 xstill to je problém?
08:40 xbarnat no standardni reseni je prinasobit k tomu monitor, ktery sleduje, zda se vlakno pohlo kdyz mohlo,  a timto se roznasobi stavovy prostor (exp blow-up)
08:40 xbarnat neco jako kdyz se z GBA buduje BA
08:41 xbarnat no ale tento nejde predpocitat, pokud mi vlakna vznikaji a zanikaji za behu (resp. musi se aktualizovat patricne)
08:41 xbarnat jinak si myslim, ze by to mohlo jit v generatoru
08:41 xstill hm, to je stejně moc velký blow-up aby to bylo s llv
08:41 xstill m použitelné
08:41 xstill + prakticky
08:41 xstill nebo nenvím no
08:41 xbarnat no je to blowup vuci poctu vlaken
08:42 xstill takže musíš vědět počet vláken?
08:42 xbarnat no tak nejak ano
08:43 xbarnat otazka zni, zda staci lokalne, nebo globalne
08:43 xstill asi bych si o tom musal něco načíst, vím kuloví
08:44 xbarnat alternativni reseni je vymyslet algoritmus pro detekci akceptujicich cyklu, ktere v sobe maji garantovany progress vsech vlaken co se mohly pohnout
08:45 xstill :-)
08:46 xstill můžeš mě odkázat na nějaký "úvod k fairness"?
08:49 xbarnat http://www-i2.informatik.rwth-aachen.de/i2/fileadmin/user_upload/documents/MC08/mc_lec15.pdf
08:55 xstill ok, pak se na to podívám, teď mám cviko
08:56 xstill btw. uvažoval jsem o tom, že by stálo za to mít jemnější dělení verifikovaných vlastností v llvm, obvzlášť až budeme mít pthread deadlocky tak bysme je měli oddělit
09:06 xbarnat s tou fairness by mozna slo udelat neco jako ze fair behy v ramci PTHREAD funkci
09:10 mornfall xstill: to je v plánu už docela dlouho :) teda jiný dělení, ideálně nějaký aditivní, pro safety
09:15 mornfall kdybychom chtěli dělat fairness monitorem, tak už má smysl udělat monitory obecně
09:17 xstill xbarnat: co tím myslíš?
09:17 mornfall proměnlivý počet vláken nemusí být nutně problém, to záleží na tom jak ten monitor popíšeš
09:18 xbarnat no standardne se uvazuje fairness pres vsechny akce procesu/vlakna, ale je smysluplne definovat fairness jen pres vybrane akce
09:19 mornfall tak, v první řadě nemáme akce :-)
09:19 xbarnat :-) no a to je ten problem. ze
09:19 xbarnat s celou fairness, protoze bez nich je to fakt bolestivy
09:19 mornfall to záleží co od těch akcí chceš
09:20 xbarnat no v zakladni verzi me staci zakodovat, ktere vlakno se pohlo, a ktere ne
09:21 xbarnat (protoze v LLVM jsou vsechny 'akce' enabled)
09:21 mornfall a to jsme u definice toho co znamená pohlo
09:21 xbarnat vykonalo instrukci
09:22 mornfall pravda, to by mohlo stačit
09:23 mornfall a na to ani nepotřebuješ ty akce, stačí mít monitor kterej vidí aj cílovej stav
09:23 xbarnat no a to jsem myslel vyse je, ze me to nemusi zajimat pro vsechny instrukce vlakna ale jen pro vybrane (napriklad ty, ktere jsou v PTHREAD*), coz by pak mohla byt cesta k detekci nejakych tech deadlocku i pod fairness
09:23 xbarnat ale to je nastrel na vode
09:24 mornfall to by mělo být jedno, opravdovej deadlock ti fairness nerozbije
09:24 xbarnat problem je, ze v ciste state-based pristupu k model checkingu se ten fakt ktere vlakno vykonalo instrukci bez dalsi prostorove zateze neda dobre detekovat
09:25 mornfall no, to jsme zase u toho jak popíšeš ten monitor
09:25 xbarnat pokdu to neni postranni informace genenratoru, a algoritmus si to nejak prebere a neni to soucasti stavu
09:25 mornfall ty můžeš synchronizovat tak, že vygeneruješ následníka v systému a pak se zeptáš monitoru jestli ho chceš
09:25 xbarnat jj, je to proste spatne
09:26 xbarnat ale pro rozhodnuti monitoru potrebuju tu informaci o tom, kdo vykonal instrukci
09:27 mornfall to zjistíš z program counteru (jediný co se ti asi může přihodit je že se „nehlo“ ani jedno vlákno -- selfloop, i přesto že jedno něco udělalo jen to nemělo efekt a vrátilo se do stejný pozice)
09:27 mornfall ale to mi přijde že jde skoro řešit jako special case
09:28 xbarnat no pokud vidim predchudce i naslednika, tak asi z toho to umim vycist ...
09:28 mornfall (víš že takový vlákno bylo nejvýše jedno, jen nevíš který)
09:28 xbarnat ale to mi nestaci
09:29 mornfall pro ten selfloop case? mi přijde že to bude OK i když to budeš brát že se nikdo nehnul
09:29 xbarnat ale moji nejmladsi dceri je toilik, kolik je dveri v tamhletom domu :-)))
09:29 xbarnat hm to by mozna slo
09:30 xbarnat pak uz je to fakt special case kdy se donekonecna nepohne nikdo, a muze takovy krok mit dopad na pamet? (jinak je to ten tebou zminovany selfloop garantovane)
09:31 mornfall to asi záleží co ten monitor v takový moment udělá
09:31 mornfall kdyby si to počítal tak se nedopočítá, ale to by snad nemusel
09:32 xbarnat no ten monitor je cyklus, ktery nejprve ceka az se pohne 1. vlakno, pak ceka na 2. vlakno, atd. a uzavre se az se pohly vsechny vlakna, kdyz se nic nehybe nehybe se ani on
09:32 xbarnat (jak se vznikajicima vlaknama nevim)
09:33 mornfall no, monitor v podstatě potřebuje dvě počítadla
09:33 xbarnat ale takto musi ten monitor mit jeste akceptujici stav, repsektive, akceptujici stavy jsou jen ty, ve kterych je monitor v nulte urovni, ze ktere se jde ven kdyz se nekdo pohne
09:33 mornfall # aktivních vláken a # non-starved vláken
09:33 xbarnat to si neni su jisty
09:34 xbarnat kdy mas ty country resetovat?
09:34 xbarnat nedeteministicky?
09:34 mornfall aktivní vlákna se neresetujou, pthread_create je ++ a ukončení vlákna --
09:35 xbarnat jo tak navic k tomu co ten monitor dela
09:35 mornfall a non-starved budeš inkrementovat jen pod přechodem vlákna n + 1
09:35 xbarnat j
09:35 mornfall když se rovnají tak non-starved = 0
09:35 mornfall teda <- 0
09:35 mornfall (to by mělo implementovat ten cyklus)
09:36 xbarnat j, implementace prechodoveho systemu pocitadly
09:36 mornfall jen to teda znamená že potřebuješ na popis toho monitoru poměrně silný jazyk
09:36 xbarnat nj
09:37 mornfall (ve skutečnosti # aktivních vláken půjde vytáhnout ze stavu takže si to nebude muset počítat sám)
09:37 xbarnat a hlavne koncept vlaken/procesu musi byt viditelny pomerne v sirokem kontextu
09:37 xbarnat pokud bychom to chteli zabudovat dovnitr do divine
09:38 xbarnat coz teda nechceme asi (spis ala buchi v CESMI)
09:38 mornfall ono se to vrací k tomu co leží v šuplíku
09:38 xbarnat a ot je?
09:38 mornfall atomický propozice v LLVM
09:38 xbarnat :-)
09:38 xbarnat aspon na tom zapracujeme no
09:38 xstill jako to co bylo v tom veselém úvodu k nějakému paperu?
09:39 xbarnat j
09:39 xstill :-)
09:39 xstill to znělo dost dobře
09:39 mornfall jo, fold přes vlákna ti v podstatě stačí
09:39 xbarnat :-) zhyralci
09:39 mornfall zbytek toho monitoru bys mohl skoro napsat v LLVM
09:39 mornfall nad stejnýma atomama jako máš pro lTL
09:39 mornfall LTL*
10:00 xstill btw. jak je to se změnami kateder na FI?
10:18 xbarnat dobra otazka, zatim nikdo nevi, posledni impuls smerem k dekanovi ze setkani habilitovanych pracovniku byl pomerne negativni
10:19 xstill jako že spíš nechat jak to je?
10:22 xbarnat jo, ale co se bude dit dal to si fakt netroufnu rict
10:30 xstill aha, no je to celý takový divný na můj vkus
11:17 xstill hm, v llvm mají build bug který má patch na 6 řádků a vědí o něm 2 měsice a neopravili ho do release
23:18 ilbot3 joined #divine
23:18 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/

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