Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-04-18

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

All times shown according to UTC.

Time Nick Message
08:40 xstill mornfall: můžu udělat deploy abych nastavil tu skupinu?
08:40 mornfall xstill: jo
08:40 mornfall co to vlastně bude až to bude?
08:41 xstill chci skupinu kvůli repozitáři na iv112, aby nám tam nikdo nelezl
08:59 mornfall :-)
09:42 mornfall jak to je s tím CESMI?
09:43 mornfall bylo to blbě předtím nebo je to blbě teď? :-)
09:43 xstill podle mě předtím
09:43 xstill ale na 100% si jistej nejsem
09:44 mornfall no, předtim clone_node mazal extension a teď nemaže, nebo se mi to zdá?
09:45 xstill moment
09:45 mornfall hmm, to duplicate v alokátoru je dost matoucí
09:45 xstill duplicate maže extension, to je matoucí?
09:45 mornfall dost
09:45 mornfall ta implementace ale taky
09:45 xstill graf by neměl o extension muset cokoli vědět
09:46 mornfall nj, místo toho o ní ví toolkit, nevim jestli to je výhra :-)
09:48 mornfall ta myšlenka že se bude alokátor posílat jako parametr umřela proč vlastně?
09:50 mornfall a nešlo by to udělat tak, že graf dostane od alokátoru Pointer s nenulovým offsetem a 0-offset toho pointru bude extension?
09:54 xstill no kdyby to byl parametr tak by alokátor musal být v datastruct nebo visitoru, což se mi moc nelíbilo
09:54 xstill a llvm tuším alokuje ještě před voláním initials
09:55 mornfall jenže llvm alokuje z poolu, ne stavy
09:55 xstill ad ten offset to myslíš jak? Jako že by to dostalo strukturu s pointrem a offsetem odkut má číst?
09:55 mornfall potřebuje prostě nějaký kusy paměti
09:55 mornfall ne, Lake::Pointer je rozdělený na blok a offset
09:55 mornfall offset je vždy nula když se naalokuje
09:56 mornfall nebo ne?
09:56 mornfall možná ne...
09:57 mornfall škoda, na offset tam místo fakt není...
09:57 mornfall to co se jmenuje offset je offset do většího bloku
09:57 mornfall ale myšlenka to byla dobrá ;-)
09:58 mornfall ale je pravda že protlačit ten alokátor skrz visitor/datastruct je problém
09:59 mornfall ale oni mají všichni store
10:00 xstill jo a konstruktor llvm interpretru konstruuje nějakej state za pomoci poolu a slacku
10:00 mornfall kde?
10:00 mornfall myslíš to state( info(), pool, slack )?
10:01 mornfall to je konstruktor MachineState, ten nic nealokuje
10:01 mornfall slack potřebuje znát protože dostane blob do kterýho potřebuje koukat
10:01 mornfall (někdy pak v budoucnu)
10:02 xstill hm ok
10:02 xstill jo a do store ten alokátor jednoduše dostat nejde, store nemůže být parametrizovaný algoritmem
10:03 xstill proč se ti nelíbí, že by graf dostal paměť a nemusal se starat o extension?
10:04 mornfall no to se mi líbí, ale to že do toolkitu přidáváme třídy který jsou ušitý na míru tomu jak funguje algoritmus o 3 vrstvy nad tím je trochu nešťastný
10:05 mornfall třeba to že duplicate maže kus paměti je dost informační leak zhora
10:06 mornfall celá záležitost se slackem/extension je problém proto že to je leak od vrchní vrstvy (algoritmus) do nižší (graf)
10:07 mornfall teď to sice z grafu částečně zmizí, ale objeví se to ještě níž
10:08 mornfall rozhodně by bylo lepší kdyby všechnu správu paměti zastřešoval store, kterej o tom stejně musí dost vědět
10:18 xstill hm, no to že je to zrovna v toolkitu je proto že jsem nevěděl kam to lépe dát
10:18 xstill ten duplicate by to možná chtělo pojmenovat jinak jen nevím jak
10:21 xstill můžu přesunout alokátor do graf/, ale musí být různá instance v grafu a v algoritmu kvůli extension (coin si řeší svůj por, a por-c3 taky potřebuje extension)
10:27 mornfall ještě nad tím budu chvíli meditovat... to co není přímo alokátor jsem pushnul
10:27 mornfall bbiab :)
17:42 xstill dokáže nějak llvm interpreter zpřístupnit informaci o tom, které problémy zrovna verifikuje?
18:10 xstill (mohl bych se vrhnout na pthread deadlocky jako další úkol)
18:19 xstill proč sakra nejsou phthread typy bitfield (jsou int a Milan tam dělá nějakou magii s posunama ručně)
18:19 xstill navíc teda to že jsou int není moc typově dobré
18:41 xstill mornfall: máš představu jestli Milan ještě něco dělá s userspace llvm?
19:12 mornfall nevím o tom že by něco dělal
19:12 mornfall takže lze předpokládat že nedělá
19:13 mornfall interpret vlastnosti moc neřeší
19:13 mornfall viz isGoal v generátoru
19:13 mornfall (v podstatě interpret označuje vždycky všechno a generátor se rozhoduje co s tím)
19:14 mornfall jo ty myslíš do userspace?
19:14 mornfall jako že chceš ušetřit nějakej overhead když se zrovna pthread deadlocky neřeší?
19:15 xstill jo
19:15 mornfall a bitfieldy maj trochu problém s inicializací
19:15 xstill na bitfieldy nefunguje c inicializátor?
19:15 mornfall ono totiž prostě nejde poznat kterej bit je inicializovanej a kterej ne
19:15 xstill aha jako pro divine?
19:15 mornfall jo
19:15 mornfall tzn. že musíš tu strukturu explicitně vynulovat než s ní něco začneš
19:16 mornfall ne že by to byl problém
19:16 xstill a co se stane pokud bude v programu bitfield? dosnate chybu na neinicializovanou paměť?
19:16 mornfall pokud se inicializuje po složkách tak jo
19:16 xstill to je dost na houby ne?
19:17 mornfall tzn. když alokuješ bitfield na haldě a pak budeš OR-ovat a AND-ovat nějaký kousky k tý neinicializovaný paměti, tak se nepozná že tam už žádnej neinicializovanej bit nezbyl
19:17 xstill jako jistě označit to za inicializované taky není ideální
19:17 mornfall to čistě záleží jakej kód se vygeneruje ve frontendu
19:17 xstill hm aha ty bitoperace dávaj smysl že výsledek není inicializovaný
19:17 mornfall pokud je to celý inicializovaný konstantou, tak se třeba vyrobí jeden store
19:18 mornfall a pak není problém
19:18 mornfall ale pokud se to vygeneruje jako load, něco bitwise, store... tak pech
19:18 xstill chápu
19:19 xstill zpět k deadlockům, ta inicializace by se dala nějak obejít, to bych tam viděr raději než magický posun o 24
19:19 mornfall dokud budeš volat na bitfieldy calloc tak je to v klidu :-)
19:19 mornfall jo, souhlas
19:20 mornfall a s tou optimalizací bych si prozatím nelámal hlavu
19:20 xstill ono udělat detekci deadlocků totiž není zadarmo (zatím teda nevím jak to udělat ale předpokládám že budu muset udělat nějakou detekci cyklického čekání)
19:21 mornfall no, detekce cyklů je klasika, to jsem chtěl dělat původně já, jen Jiříkovi se to nějak nezdálo :)
19:21 xstill co se mu nelíbilo?
19:21 mornfall ono to nakonec dělá aj glibc když ten mutex nastavíš jako PTHREAD_MUTEX_ERRORCHECK_NP
19:22 xstill fakt?
19:22 mornfall jasně
19:22 xstill já myslel že to kontroluje je znovuzamknutí
19:22 mornfall hmm, možná to fakt detekuje jen selfloop
19:24 mornfall máš pravdu, maj tam jen kontrolu na self-deadlock
19:24 mornfall to je trapný :P
19:25 mornfall ale klidně by to dělat mohlo
19:28 mornfall problém je, že to nechytne nutně všechny druhy deadlocků, výhoda je že to je relativně jednoduchý a je to safety
19:28 mornfall a má to ještě jednu výhodu:
19:28 mornfall Moreover, we look at one important safety property, notably deadlock-freedom,
19:28 mornfall in the context of pthread-based parallel programs with mutual exclusion
19:28 mornfall locks. More traditional deadlock analyses fail in cases where a deadlock only
19:28 mornfall affects a subset of threads, while the rest of the system continues to be
19:28 mornfall alive, even though possibly live-locked in response to the partial
19:28 mornfall deadlock. We propose an extension to the \divine software model checker that
19:28 mornfall allows detection of this broader class of ``partial deadlock'' bugs.
19:29 xstill no chytne to jen deadlocky mezi mutexy
19:29 mornfall tak, šlo by to asi rozšířit na condition variables taky
19:29 mornfall ale na nějaký atomic-based spinlocky to nemá šanci
19:29 xstill co to je za text?
19:30 mornfall to je nějakej starej abstrakt
19:30 mornfall nejspíš jsem ho posílal aj na divine@ někdy
19:32 mornfall bylo to myšlený jako společnej paper s atomickýma propozicema
19:32 mornfall tzn. kdybys udělal ty deadlocky a já došudlal silk, tak to můžem dopsat a někam poslat :)
19:33 xstill :-), silk má být na to dotazování stavů z LTL?
19:34 mornfall jo
20:09 mornfall ty OOM na execution.cpp jsou ale dost trapný
20:10 mornfall já vim že jsem ten soubor de-facto zdvojnásobil, ale i tak...
20:12 xstill hydra má k dispozici "jen" 5GB
20:12 xstill ale pokud je potřebujeme tak je to dost otrava
20:12 mornfall 5? ne 4?
20:13 xstill +1 GB swap
20:13 xstill (mám pocit že víc pheme namají)
20:13 mornfall jo, asi jo
20:46 xstill nemáš náhodou po ruce nějakej algoritmus na detekci deadlocků?
20:46 mornfall v jakém smyslu?
20:47 xstill na zjištění jestli mezi mutexy je kruhové čekání
20:47 mornfall nemělo by to být o moc složitější než v každém volání _lock skontrolovat jestli jsi neuzavřel cyklus
20:50 mornfall jinak je to jen dosažitelnost, když už máš nějak schovaný závislosti
20:51 xstill asi jo
20:53 mornfall pozitivní je, že každý vlákno může v daný moment čekat nejvýše na jeden mutex
20:53 mornfall takže to má docela dobrý boundy na paměť aj čas
20:54 mornfall (to kdo má zamčenej kterej mutex už si ten mutex beztak pamatuje)
20:57 mornfall kdybys třeba uložil do Thread ukazatel na mutex na kterej to vlákno čeká (normálně null)
20:58 mornfall tak v _lock když je ten mutex zamčenej a jdeš čekat, podíváš se na wait toho vlákna který ho zrovna teď vlastní
20:58 mornfall (pak na ten mutex na který to wait ukazuje a tak dál, a když dojdeš až k tomu svýmu mutexu tak máš deadlock)
20:59 mornfall (snad :-)
20:59 xstill hm, jo to by mělo jít
20:59 xstill půjdu si to rozmyslet
21:00 mornfall já si zatim asi pustim doktora ... a tu alokaci furt nevim, achjo :)
21:00 mornfall s tím visitorem je to marný
21:10 xstill hm, ale dneska už na to kašlu
21:35 xstill hm, nechtělo by se ti vysvětlit tomu Hollasovi proč mu nefunguje to LTL?
21:50 mornfall neříkal jsi mu už náhodou že G pro AP(x) nemůže platit?

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