Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-01-13

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

All times shown according to UTC.

Time Nick Message
10:13 xstill ten člověk začíná bejt dost otravnej
10:31 mornfall kterej?
10:34 xstill ten s tou promelou, ale Jiřík mu už stihl odepsat
10:35 mornfall někde je bug, já ty maily od něj nevidim (vůbec žádný teda)
10:37 xstill no já tady mám 6 mailů na divine/paradise od pátku, nějakej číňan asi
10:38 xstill btw. právě jsem poslal ticket do tracu
10:39 xstill podivnej cyklus v pthread_entry
10:40 mornfall :D to vyřadil už fakultní/univerzitní filtr
10:42 xstill :-D ani se mu nedivím vzhledem k tomu jak ten mail vypadá. Ale já mám fakultní filtr vypnutej.
10:43 mornfall já vzhledem k tomu že mám filtr před frontou a fakultní poštu si doručuju SMTP tak nemá smysl ten fakultní vypínat
10:47 mornfall xstill: obávám se, že ten cyklus v pthread_entry není ani spurious ani divnej
10:47 mornfall xstill: je tam spinlock
10:50 mornfall on ten cyklus hlavně není v pthread_entry ale v pthread_create
10:50 mornfall WAIT( !args->initialized )  // wait, do not free args yet
10:52 mornfall jediný co ten cyklus je je unfair
10:53 mornfall horší je že mi došel černý čaj
10:53 mornfall budu muset na nákup... bez jídla se žít dá, ale bez čaje?
10:54 mornfall xstill: ale fairness by mohla většinu těch non-progress cyklů který tě nezajímaj vyřadit, teoreticky
11:11 xstill hm
11:12 xstill potom ale nedokážeme řešit žádné LTL s thready
11:12 xstill dokud neuděláme fairness
11:20 xstill to čeka až spouštějící thread dokončí inicializaci?
11:20 xstill proč se to neudělá před tím než se začne startovat thread?
11:22 xstill aha, ne čeká spouštěcí thread
11:28 xstill hm, já ale nevidím jak může dojít k tomu, že se nenastaví args->initialized = true, v pthread_entry není žádnej cyklus před tím
11:35 xstill aha, on simuluje to, že ten novej thread stojí a ten druhej cyklí v tom WAIT
11:35 xstill to je dost na nic
11:37 xstill tu fairness asi potřebujeme docela
11:52 mornfall proč bychom nemohli řešit LTL?
12:01 xstill no tak nefunguje to moc. Já nechci aby mi to našlo cyklus, kterej je implementační detail v divine, žejo.
12:02 xstill dá se to napsat nějak jinak aby to fungovalo?
12:13 mornfall napsat co?
12:24 xstill tu property, že end je dosažitelnej
12:24 xstill resp. v tom příkladu bych chtěl aby mi to našlo cyklus s těma lockama
12:24 xstill (je tam pthread deadlock)
12:32 xstill prostě bych chtěl abych na F( něco ) neměl protipříklad kterej je mi k ničemu protože je v divine userspace
13:02 mornfall no, ale to jsme už řešili že najít pthread deadlock pomocí LTL v podstatě nejde
13:03 mornfall to že bys to chtěl je sice super, ale tím se to nestane řešitelnej problém :-)
17:16 xstill ok, ale to nic nemění na tom, že to co jsem tam našel není něco co by se tam mělo ukazovat, tenhle protipříklad bude protipříklad pro libovolnou F( x ) vlastnost pokud program zavolá pthred_create
17:17 xstill pokud ten cyklus s lockama nejde najít LTL pak by mě zajímalo proč
17:24 mornfall bude, a pokud nepředpokládáš fairness tak je ten protipříklad správně, on v tom programu prostě takovej cyklus je
17:28 xstill ok, a teď si představ, že jsi uživatel divine a dostateš tenhle protipříklad -- jak máš tušit že je to způsobené implementačním detailem v divine a jak se toho máš zbavit?
17:29 mornfall jenže to není implementační detail, pthread_create se takhle prostě chová
17:29 mornfall kdyby se scheduler rozhodl že to vlákno na který se čeká nikdy nespustí tak ten program zůstane viset
17:30 mornfall pokud specifikuješ že tohle se nestane (= fairness) tak tam ten cyklus nebude
17:32 mornfall můžeš si zkusit naimplementovat wait-free pthread_create :-)
17:35 mornfall a pokud jsem uživatel divine tak moje reakce na ten protipříklad asi hlavně záleží jestli vím nebo nevím co ta LTL formule znamená
17:36 mornfall ono se sice říká že LTL je intuitivní, ale to platí pro srovnání s mu-kalkulem
17:36 xstill hm, ale kdyby tu paměť uvolnil ten novej thread tak na něj nemusíš čekat
17:36 mornfall pak bys měl leak
17:38 xstill jakto?
17:38 mornfall jako neříkám že to absolutně nejde řešit, ale hlavně na tom nesejde, protože spousta jiných funkcí na něco čeká
17:39 mornfall můžeš do LLVM dodat synchronizaci
17:39 mornfall ale protože ji tam nemáme a je to asynchronní, tak čekání znamená cyklus
17:43 xstill no dobře, to asi přežijeme (i když man pthreadu neříká nic o tom, že by to mohlo blokovat)
18:12 xstill divine neumí dát buchi na výstup, že?
18:17 mornfall umí vyrobit dve s buchi (combine s prázdným DVE), asi
18:18 xstill protože totiž jsem našel formuli při které má ten model najednou 1 stav bez cyklu
18:19 mornfall asi nemá žádný enabled následníky (iniciální stav v buchi)
18:21 xstill no nicméně formule a -> F( a -> F( a ) ) by měla mít
18:21 xstill -> možná chyba v LTL2BA
18:24 mornfall to nevim proč, a v iniciálním stavu neplatí, tudíž ta formule je triviálně true
18:24 mornfall takže ten produkt s jedním stavem je správně
18:37 xstill hm
18:41 xstill ok, začínám to chápat
18:41 xstill fuj je to
18:47 ilbot3 joined #divine
18:47 topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
19:43 xstill ach LTL fakt není intuitivní
19:47 xstill btw. vyšlo llvm 3.4
19:48 mornfall jo, už je to dýl
19:48 xstill mají ho už v stdenv-updates nebo někde?
19:48 mornfall x-updates
19:48 xstill ok
19:48 mornfall iirc
20:00 xstill hm ale jen llvm, ne clang
20:06 xstill mornfall: 3.4 má windows build
20:07 xstill jen nevím jestli je to mingw nebo msvc
20:10 mornfall to nedělá rozdíl, /nix/store/xh8f2vj5i6chq57a8afp8qscllaflrab-windows-llvm
20:10 mornfall LLVM na Windows si překládáme
20:10 mornfall divine+llvm na windows zrovna teď umírá na C:/WORK/source/wibble/string.h:514:50: error: exception handling disabled, use -fexceptions to enable
20:10 xstill ok
20:11 xstill aha to je toto
20:16 xstill kašlu na clang
20:17 xstill jdu to zbuildovat proti llvm 3.4 s libstdc++
20:19 xstill hm až na to, že to nejspší nebude fungovat bez kompatibilního clangu
20:20 xstill ale to je jedno stejně se nejdřív nejspíš nepřeloží divine
20:22 mornfall to je taky řešitelný
20:22 xstill no proto to zkouším
20:24 xstill do řitě já mám gcc 4.8 :-D
20:28 xstill ať žije nix jinak bych se z těch verzí kompilátorů musel zbláznit
21:59 xstill zajímavý 3.4 nic nerozbilo při kompilaci
21:59 xstill to tu ještě nebylo

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