Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-09-27

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

All times shown according to UTC.

Time Nick Message
09:52 xstill jo domluvil jsem se s Jiříkem, že se podívám teď na slicing a povedu to celé směrem k praktické verifikaci. LART měl v plánu i slicing, ne? Máš někde tu nejnovější verzi potom?
10:26 mornfall no
10:27 mornfall Jiřík a jeho posedlost slicingem... :)
10:36 xstill no, mě se to taky zdá použitelné, ve chvíli kdy nemáš úplně malý model
10:36 xstill a potom bude potřeba dotáhnout LTL nad LLVM
10:38 mornfall no, užitečný to je... ale to je trochu jako říct že statická analýza je užitečná
10:39 mornfall pokud poslední dobou něco zásadního nevymysleli, tak není vůbec jasný jak/co dělat aby to byl slicing a zároveň to nebyla identita :-)
10:41 mornfall slicing není tak úplně rozhodnutelnej, takže to je o tom najít heuristiku která bude fungovat
10:43 mornfall nedivil bych se kdyby to bylo podobně těžký jako počítat statický ample sety
10:45 mornfall jakmile ti může cizí vlákno hrabat do proměnný, tak se celá klasická dataflow analýza na který klasickej slicing stojí rozsype
10:46 mornfall takže jo, chceme dělat slicing, ale zatím mi nikdo nebyl schopnej říct co se tím myslí :-)
10:55 mornfall slicing se dělá staticky a když to vztáhnu na LLVM, tak dělá to že odstraňuje instrukce
11:01 mornfall teď je otázka kdy můžu odstranit instrukci...
11:01 mornfall klasicky slicing funguje tak, že vybereš nějaký proměnný co tě zajímaj a k tomu nějakou instrukci
11:01 mornfall a přidáváš do slicu všechno na čem ty proměnný datově závisí
11:02 mornfall jenže jakmile v těch závislostech najdeš load o kterým nedokážeš ukázat že je z privátní paměti, tak to začne být zlý
11:02 mornfall pokud bys na ten program zároveň vytáhl nějakou abstrakci, tak bys mohl říct že ten load je nedeterministickej a mohl vidět cokoliv
11:02 mornfall jenže pokud ne, tak zrazu musíš do slicu zahrnout všechno co může vytvořit vlákna a všechno co ty vlákna můžou spustit a mohlo by mít na ten load dopad
11:06 mornfall takže „research problem“ je zjistit jestli jde předejít tomu abys tam vtáhl celej program
11:06 mornfall a pokud ano jak (a počítám že abstrakce je no-no)
11:06 mornfall (no a pokud má ten kus programu jen loady který nejsou sdílený, tak zase nemá moc smysl modelcheckovat)
11:12 xstill no musím se nad tím zamyslet. Otázkou je pak jestli nejde jít cestou podmíněného scicingu, kdy bych mohl staticky napočítat i místa kde si nejsem jistej jestli load je ze sdílené paměti a pak se podle informací co má \tau rozhodl.
11:12 xstill jo a abstrakce bych úplně nezahazoval
11:13 xstill naopak by mě měli dost práci přesvětčit, že ty Vilíkovy množiny můžou mít smysl pro reálnej kód (a verifikovat cčko bez alokace se mi fakt nechce)
11:13 mornfall to je dávno pozdě
11:15 mornfall teda otázka není jak poznat jestli je load sdílenej
11:15 mornfall otázka je co udělat když je
11:15 mornfall když load sdílenej není tak se to redukuje na triviální případ
11:15 mornfall a víme že zajímavý případy budou právě ty kdy nějaký sdílený loady potkáš
11:17 mornfall (a divine ti sice dokáže o každým loadu říct jestli je nebo není sdílenej, ale neumí to jinak než že napočítá celej stavovej prostor)
11:17 mornfall to je totiž stejně těžká otázka jako zjistit jestli assert platí nebo ne
11:18 xstill hm
11:18 xstill to je problém
11:18 mornfall takže v praxi by to muselo fungovat tak, že zkusíš ukázat že je privátní a pokud se to nepovede tak počítáš že je sdílenej
11:18 mornfall ono se to občas povede levně
11:20 mornfall no, když máš alias analýzu která je dost konzervativní aby platila pro threadový programy...
11:20 mornfall tak můžeš přidat všechny story který píšou do stejnýho alias setu
11:20 mornfall a doufat že se to napropaguje na něco menšího než všechno
11:21 mornfall (plus teda všechny pthread_create ze kterých jsou ty story dosažitelný)
11:32 mornfall ale hlavně už nějaká skupina na slicing byla a nevim co se s ní stalo?
17:43 xstill tak to by mě taky zajímalo, a co to bylo zač?
18:55 xstill ahjo studenti neumí číst zadání
20:42 xhire_ joined #divine
21:05 xstill hm, https://isocpp.org/blog/2014/08/we-have-cpp14
21:05 xstill jsem nějak nezaznamenal
21:06 xstill clang 3.5 prý už umí -std=c++14
21:06 xstill (ale jinak umí totéž co 3.4 s -std=c++1y zdá se)

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