Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2016-01-28

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

All times shown according to UTC.

Time Nick Message
11:43 xstill mornfall: vymyslel jsi teda nějakej lepší název než store buffer?
11:44 xstill aha už vidím
11:45 xstill mornfall: nezapoměl jsi něco pushnout? na to že jsi mi tvrdil, že mám dodělat jen conclusion a Jiřík related work tam toho chybí dost
12:15 mornfall jaký conclusion?
12:15 mornfall evaluation snad
12:15 xstill jo to
12:16 mornfall no a kde je? :)
12:16 xstill to je jedno, každopádně kapitolu 2 a 3 jsem pochopil, že  děláš ty
12:16 xstill je to u mě, píšu to, ono se špatně píše evaluation než jsou výsledky
12:17 mornfall no, ono se taky píše špatně všechno ostatní když nevíš jak to dopadne
12:17 xstill nojo, ale aura je jen jedna, žejo
12:18 xstill dopadá to tak, že s bufferem délky 4 a PSO změřím tak maximálně ty fronty
12:18 xstill TSO je na tom výrazně líp
12:28 xstill hodil jsem ti předběžné tabulky do repa
13:06 mornfall kolik prostoru budeš potřebovat na tu evaluation?
13:06 mornfall teď tam zbývá necelá stránka, sekce 3 bude kratší ale zase nejsou conclusion
13:06 mornfall počítám že related work se taky možná trochu stáhne
13:27 xstill počítám, že stránka a půl by mohla stačit
13:27 xstill máme 15 stránek textu (bez referencí prý)
13:27 mornfall stránka a půl navíc k tomu co tam je teď?
13:27 xstill celkem
13:28 mornfall no teď je to stránka
13:28 mornfall a kousek
13:28 mornfall je tam potřeba určitě aspoň popsat jaký chyby to našlo
13:29 xstill tak možná 2 já si musím rozmyslet co tam napíšu. a taky si nejsem jistej, že ta tabulka s pamětí má smysl
13:29 mornfall asi víc než se stavama :-)
13:29 xstill tak ok
13:30 mornfall (tzn. asi bych spíš vypustil tu stavovou, kdyby byl problém s místem)
13:35 xstill jenže zas čas máš úměrnej spíš stavům, ona ta paměťová trochu maskuje ty nárůsty
13:36 xstill což pro nás může být dobře, ale není to úplně fér
13:36 xstill takže bych tam nechal spíš obě
13:36 mornfall to platí jen pro explicit-state nástroje
13:36 xstill to asi jo
13:37 mornfall (což je taky potřeba tam nějak vysvětlit, jak to jde nebo nejde interpolovat k jiným přístupům)
13:37 xstill ty teda s tím zbytekem ještě něco uděláš, jo?
13:37 mornfall no zbývá sekce 3 a conclusions
13:37 mornfall sekci 3 mám rozdělanou
13:37 xstill ok
13:37 mornfall (sekci 2 jsem commitnul)
13:37 mornfall conclusions napíšu až bude všechno ostatní
13:38 xstill a ten vztah výsledků k ostatním nástrojům vysvětlíš? protože o tom já mám dost mizernou představu
13:40 mornfall no něco zkus vymyslet, stejně to ještě někdo bude celý číst
13:44 mornfall (a kdybys neměl co dělat, přidat tam tu facebookovou tabulku by určitě nebylo marný)
13:44 xstill to by marný nebylo, otázka je jestli to máme šanci stihnout zverifikovat
13:46 mornfall já vim, aura je jen jedna a vždycky říkáme že budeme měřit v předstihu a nikdy se to nepovede
13:46 xstill protože v předstihu není ani implementace
13:46 xstill a divine je pomalej
13:47 xstill když jsem měřil na memics tak jsem těch 600 M stavů dělal za 1 den, teď to trvá týden, žejo
14:40 xstill a ty paměťový měření jsou beztak hrozně pomatený tím jak se zvětšují tabulky, jinak by nebylo možný, že na některý hs benchmarcích to téměř neroste a jinde to roste skoro 2x
14:41 xstill i když, možná ne, protože ten na kterým je to nejvíc vidět má celkem 100k stavů a ta tabulka se předalokuje na 500k, ale zas fork tabulka může být větší
15:28 xstill mornfall: ono s tím použitím mimo explicitní MC to bude stejně docela slabší, ne? Protože pokud umíš symbolický data, tak se asi víc vyplatí to celý dělat symbolicky a ne explicitním bufferem
15:32 mornfall co je na tom bufferu explicitního?
15:33 xstill tak ten buffer sám je docela explicitní, ne? to že existuje a má konkrétní délku a obsahuje data pro konkrétní místa v paměti, místo toho že by to celý mohlo být zakódovaný jako formule nad daty nějak asi
15:34 xstill nebo nevím, stejně nevím o nikom kdo by sybolicky řešil paralelní programy jinak než serializací
15:34 mornfall no když máš nějakej takovej nástroj, tak bude mít asi spíš symbolický ukazatele než konkrétní místa v paměti ne?
15:35 xstill nevím, tak třeba ten bazmek co vyhrál concurrency v sv-comp měl místa explicitní tuším
15:35 mornfall a ta délka je taky daná parametrem
15:36 xstill celkově mi nějak chybí informace o konkurenci…
15:36 mornfall no to je ta related work
15:36 mornfall ale v principu
15:36 mornfall když máš nástroj který používá symbolická data, tak skončí symbolická data v store bufferu, no big deal
15:36 mornfall pokud má i symbolickou paměť, tak tam budou i symbolický lokace
15:36 xstill nemyslím teď v článku, ale celkově verifikace paralelních programů
15:37 mornfall však related work není jen teď v článku
15:37 mornfall a vůbec, na to máte ten slavnej paradise seminář ne? :)
15:38 mornfall tam se teda většina článků asi odpíská jako že to není zajímavý
15:51 xstill tak já jsem přemýšlel, že by stálo za to prezentovat tam verifikátory paralelních programů
15:59 xstill mornfall: ještě bych teoreticky z té tabulky mohl vyhodit PSO s velikostí 1 (protože to celkem stejně nedává smysl) a místo toho tam dát TSO s 8
16:11 xstill udělám to tak
16:14 mornfall kolik je maximum na TSO kam umíme dojít?
16:14 xstill pro fifo až na konec
16:15 xstill pro ten hashset to můžu taky zkusit, ale to bude trvat
16:15 xstill ale byl bych relativně optimistickej k tomu
16:15 xstill tso roste pomalu většinou
16:16 mornfall no, vypadá to tak
16:16 xstill sakra, ono tam je vlastně ta věc, že TSO-4 na ring je z nějakého neznámého důvodu větší než TSO-8
16:17 mornfall ve stavech nebo v paměti?
16:17 xstill na stavech, na paměti by to mohla být prostě náhoda
16:17 mornfall to je radosti
16:18 xstill jenže to nemám šanci zdebugovat žejo, má to 20k stavů
16:22 xstill to je ale v háji, protože se to projevuje i na té atomické verzi
16:27 xstill ono to dokonce dělá míň context switchů (měřím to csdr), což by sice mohlo být tím algoritmem, ale je to taky podezřelý trochu
16:29 xstill jakože, 24, 23, 25, 25, a pak už pořád 21
16:29 mornfall já nevim
16:30 xstill může být někde bug, nebo to není monotonní a málo jsme se nad tím zamysleli
16:30 mornfall pokud to není monotonní tak to skoro určitě není dobře
16:31 mornfall ty bugy co to našlo jsou legitimní?
16:32 xstill nojo, jenže ta transformace je stejná až na jedno blbý číslo, takže tý bych docela věřil, to leda, že by pak byl bug v divine, někde v redukci nebo v isPrivate
16:32 mornfall stejná jako co?
16:32 xstill no, ono jich to tak moc nenašlo, co jsem namádkou koukal tak vypadaly legitimně
16:33 xstill že ta transformace se mezi různýma délakama liší v podstatě jen tím N
16:33 mornfall a jak víme že pro nějaké N to funguje dobře?
16:34 xstill to nevím jak bych měl ověřit
16:34 mornfall no právě, ale tvrdíš že je asi dobře protože se mění jen to N a není mi jasný proč
16:35 mornfall kdybychom věděli že pro N=3 to určitě funguje, tak beru že pro ostatní N nejspíš funguje taky :)
16:35 xstill jo tak, hm
16:35 xstill jako mám na to nějaký testy a nějaký další protipříklady jsem kontroloval u diplomky, ale úplně jistej si bejt nemůžu
16:36 mornfall tak *něco* špatně je, protože čekáme že to bude monotonní a není
16:38 xstill hm, takovej drobnej detail, sakra, pořadí cleanupů zjevně není deterministický (protože set pointrů, žejo), to by to teoreticky dělat mohlo, i když teda ten cleanup kód vlastně běží pod maskou, tak by to mohlo být skoro jedno
16:39 xstill mornfall: Jiřík prý udělal nějaký změny v intru.
16:40 xstill ještě zkusím co se stane, když to fakt jen ručně přepíšu to číslo
16:40 mornfall a teď mi navíc někdo vyrobil konflikt
16:40 mornfall to mam fakt radost
16:45 xstill nojo, to máš těžký, to byl počítám Jiřík, já nikam krom evaluation nehrabal
16:45 xstill jo a když změním jen to číslo tak to stačí na to aby to nebylo monotonní
16:59 mornfall to je dva kroky vpřed krok vzad tohle
17:00 xstill co?
17:00 mornfall Jiřík mi to úplně rozbil
17:00 mornfall asi na to kašlu
17:00 xstill tak jste se měli domluvit na představě
17:00 mornfall mně přišlo rozdělení práce jasný dost
17:10 mornfall jak to vypadá s tou evaluation teda? protože momentálně mi stejně přijde že nemá moc smysl to posílat, tak se mi nechce s tím bojovat
17:20 mornfall Jiřík samozřejmě nereaguje, do SVN jsem to nějak zmergoval a vyznačil kterej kus textu je určitě potřeba dořešit
17:21 mornfall vzhledem k tomu že to vrátil na Store Buffers tak to chce asi celý dělat nějak jinak
17:22 xstill evaluation je nějak zhruba napsaná, jen čekám na doměření TSO-8, Jiřík jel vyzvednout děti, tak asi proto neodpovídá
17:22 mornfall no já mu psal už v půl druhý
17:22 mornfall původně
17:23 xstill ale s tím bugem je to blbý, i kdybych ho teď našel a opravil tak to stejně nepřeměřím, na to není čas
17:23 mornfall napsal jen „ještě to budu ladit“ a přestal se se mnou bavit
17:23 mornfall a to ladění dopadlo takhle
17:23 xstill máš představu kdy jsou další slušný konference?
17:24 mornfall chvíli jsem koukal na wikicfp
17:24 mornfall je atva, tam jsem sice chtěl poslat něco jinýho, ale může se tam poslat obojí
17:24 xstill ta je daleko zas
17:25 mornfall no
17:25 mornfall aura je jen jedna
17:25 mornfall a někdo musí rozanalyzovat protipříklady a ideálně sehnat další modely
17:28 mornfall sefm má deadline koncem února
17:28 mornfall nfm 19.2.
17:28 xstill a ty maj dobrý bobříky jo?
17:28 xstill NFM jako NASA formal methods?
17:29 mornfall jo
17:29 mornfall to asi furt nemá rating
17:29 xstill ty zatracený ratingy někde najdu?
17:29 mornfall těžko říct
17:29 mornfall publish or perish :D
17:30 xstill byď teda vlastně nevím co se podle nich počítá, protože teď zas někdo tvrdil na kolegiu že lncs bylo fixně 25 bobříků
17:30 mornfall to jsou jiný bobříky
17:30 xstill no já si taky myslím, jen nevím k čemu jsou ty ratingy
17:31 xstill SEFM je ve vídni, tam bychom měli něco poslat
17:32 mornfall pak je asi až ICFEM na konci dubna (deadline)
17:33 mornfall a ten je taky v Tokiu
17:34 xstill hm, tak to SEFM by asi šlo, dávali jsme tam tu kompresi, tuším že to bylo A nebo B, ale pořád teda nevím co se od toho odvíjí
17:34 mornfall nějaké hodnocení něčeho, asi
17:34 mornfall :-)
17:36 mornfall pak je ještě tohle, http://www.wikicfp.com/cfp/servlet/event.showcfp?eventid=51448&copyownerid=84996 :-) do konce března
17:37 xstill našel jsem foto Jiříkovi tabule z loňska SEFM byl B
17:37 xstill ještě tam bylo ACE (letos 29. 4.)
17:37 xstill ((deadline))
17:38 xstill singapur ovšem
17:40 xstill toho červenýho je nějak hodně koukám
17:41 xstill (pushnul jsem rozpracovaný výsledky)
18:50 mornfall co se stane když dojde místo protože všechny položky v bufferu jsou označený jako flushed?
18:51 xstill to nemůže, vždycky po flush se odstraní všechny flushed položky před kterýma není nic co je ne-flushed a ne-fence
18:52 xstill jediný co je potenciálně divný je, že store může vyhazovat položky z bufferu a vyhazuje jen tu nejstarší, ale to se projeví jen pokud se to přeplní pod maskou
18:53 mornfall nejstarší, nebo nejstarší která není označená flushed?
18:54 xstill nejstarší komplet (s tím, že zachovává invariant, že první položka nemůže být flushed ani fence, takže jich může vyhodit i víc naráz)
18:54 xstill prostě pokud tam není bug, tak flushed stejně nemůže být první
18:54 xstill první = nejstarší
18:55 xstill a to jsem teď kontroloval, že to čištění se fakt děje
19:06 mornfall ještě jeden dotaz... assume false se vždycky děje ve stejný atomický sekci která udělala příslušnej choice kterej způsobil to že je ten běh špatnej, jo?
19:09 xstill tak ten ve flush jo, pak je tam ještě assume, kterej hlídá jestli v bufferu není něco co tam být nesmí (v loadu/fence), ten se samozřejmě děje v úplně jiný atomický sekci, než je ta co způsobila co je v bufferu
19:10 xstill (ten se děje v atomické sekci toho load/fence)
19:11 xstill jenže zas tím, že to že se ten load nemůže vyvolat se určitě nezpraví tím, že se do bufferu něco přidá
19:12 xstill s/tím/to/
19:13 xstill spíš se kdyžtak podívej na ty podmínky v textu (str 9 u mě), myslím, že jejich implementace by měla snad sedět
19:23 mornfall no já se ptal kvůli popisu, ty podmínky jsem četl několikrát
19:24 mornfall nemůže to pak vyrábět ve stavovým prostoru slepý větve?
19:29 mornfall jedinej popis k čemu je 'observed' jsem našel ve figure 4.13 ve tvý diplomce
19:29 mornfall a je to dost vágní :)
19:31 mornfall jo už to asi vidim
19:33 mornfall no určitě nevidim důvod proč by to mohlo nebýt monotonní
19:33 mornfall pokud se nikdy neevictuje nic co by mohlo zabránit vykonání instrukce
19:35 mornfall ale když si vezmu třeba 'monotonic atomic compound', tam se píše že 'there is no not-flushed monotonic entry location in any foreign store buffer'
19:35 mornfall to zní dost jako že když jedna taková je a někdo ji evictuje protože došlo místo, tak se tím tady ta instrukce enabluje
19:36 mornfall ale pokud se ten evict chová korektně tak by to mělo být jedno
19:36 mornfall (evict prostě udělá flush ne?)
19:37 mornfall vždycky by tam měl být nějakej sousední běh kde se zrovna v ten moment flushla ta věc co tomu bránila
20:22 mornfall v alt.tex zbývají 2 strany červenýho textu a půl strany je volné na conclusions
22:15 mornfall no zbyla asi strana, nějak se rozmyslete co s tím teda chcete
22:16 mornfall zítra kolem poledne se na to podívám a případně dotáhnu
22:16 mornfall nebo si to zmergujte jak chcete
22:17 mornfall budu-li ve vlaku při smyslech ještě před devátou commitnu ten červenej zbytek
22:42 xstill slepý větve to dělat nemůže, pokud někdy vypne něco assume pak můžě běžet flusher
22:43 xstill observed slouží k implementaci bariér a acquire-release synchronizace, ta funguje jen pokud je tam ten atomickej objekt na kterým se potkaj
22:44 xstill ano, vyhození nejstaršího záznamu z bufferu bude dost možná zapínat insturkce
22:44 xstill jenže pokud přidáš políčko ve store bufferu, tak by mělo být možný to samý pořád dosáhnout tím, že to co se dřív vyhodilo kvůli místu se vyhodí flusher thredem
22:45 xstill jo, evict v nedostatku místa flushne nejstarší položku
22:46 xstill díky, zítra dopoledne se na to podívám, teď už by to asi nemělo moc velký smysl
22:47 xstill s Jiříkem jsi se o tom nějak bavil? Mě jen odepsal, že to posílat chce a pak už ho nejspíš rodina nepustila k počítači…
22:52 xstill jako kdyby šlo o PSO tam bych si tím evictem při store úplně jistej nebyl (potenciálně může přeskočit nějaký běh), ale pro TSO v tom problém snad není
22:53 xstill (pro PSO může být potenciálně problém, pokud se v rámci jedné atimické sekce zapíše víc než je délka bufferu, pak se některé věci nedají přehzovat i když by jinak mohly)

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