Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2016-01-29

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

All times shown according to UTC.

Time Nick Message
08:55 xbarnat joined #divine
08:56 xbarnat jste tu?
08:56 xstill jo
08:57 xbarnat ja jsem do ted zil v predstave, ze se snazime prodat lepsi transformaci LLVM na LLVM nez ktera byla na memicsu
08:57 xstill xbarnat: no já bych to postavil buď jako C++ memory model (což je trochu nepřesný), nebo jako LLVM memory model
08:58 xbarnat co to znamena postavil jako C++ model
08:58 xbarnat ja si potrebuju precist intro a musim pochopit co je prinosem clanku, nebo co se v nem popisuje
08:58 xstill no podle mě je potřeba říct, co za memory model vlastně děláme
08:58 xbarnat nepredpokladam, ze opublikujeme popis C++ memory modelu
08:58 xstill to teď z toho nového intra úplně neplyne
08:58 xbarnat ok to se da doplnit
08:59 xstill no to ne, ale teď z toho intra vyplývá, že děláme nějaký memory model, neznámo jaký
08:59 xstill tak bych tam někde napsal, že je to LLVM memory model, který je dost blízký tomu co používá C++11 standard
08:59 xbarnat aha, no to bylo cilem ne? protoze prinasime obecne metodu, ktera skousne vic modelu zaraz, to tam uz bylo napsane ... a  ano muzeme doplnit, ze to dokumentujeme tim, ze delame ten a ten ...
09:00 xbarnat model
09:01 xstill no ne úplně, ono je to tak, že ta metoda implementuje LLVM memory model + možnost omezit ho, což ti reálně dává možnost vyjádřit v tom strinktnější mm než LLVM, například TSO
09:01 xbarnat a jeslti si mornfalle nastvanej, ze sem zmenil strukturu intra, tak ja jsem nastvanej taky, protoze to pri cteni odshora dolu nedavalo moc smysl
09:01 xstill jakože z toho co umíne je LLVM memory model to nejrelaxovanější
09:02 xbarnat porad si myslim, ze nemuzeme zacit clanek tim, ze umime LLVM memory model, protoze proste nechapu co to znamena umet llvm model
09:03 xbarnat ten flow intra musim byt, delame verifikaci programu v relaxed memory modelch, delame to pres LLVM-LLVM tranformace  a teprve jako treti dodavame, ze nase tra-ce zvlada LLVM model, coz je mozna ten, ktery je dostatecne svobodny na to, aby se v nem vyjadrilo vse dulezite
09:03 xstill no, začít úplně ne, ale k tomu konci úvodu bych čekal, že se člověk dozví, co za memory model jsme udělali, asi tam můžeš napsat něco ve stylu, že náž memory model vychází z memory modelu LLVM, což je v podstatě partial store order s atimickými instrukcemi, které můžou specifikovat míru synchronizace
09:04 xbarnat ok to se tam da samozrejme doplnit
09:04 xstill dobře, ještě jedna věc k tomu úvodu, co je přesně finite behaviour?
09:05 xstill protože ta vlastnost platí pro končící programy, nikoli však nutně pro konečně stavové programy
09:05 xstill (nekonečný cyklus store instrukcí způsobí neomezený buffer)
09:06 xbarnat no ja si myslim, ze pro konecne stavove muzes mit nekonecne chovani tudiz nekonecne dlouhe odlozene zapisy
09:06 xbarnat nojo, ale ty to emris na programu po transformaci, ale musis to merit na programu pred transformaci
09:06 xbarnat emris -> meris
09:06 xstill a když jsme do toho, mornfall to přejmenoval ze store buffer na memory reorder buffer (protože store buffer je v podstě něco co jen pozdržuje zápisy, ale my v tom ještě počítáme happens-before)
09:07 xbarnat ok
09:08 xbarnat ikdyz si myslim, ze store-reorder buffer by bylo vyrazne lepsi
09:08 xstill teď to nechápu, já tu konečnost uvažuju na netransformovaném, proto se ptám co se vlastně myslí tím finite behaviour, jestli je to končící program
09:08 xstill no tam je problém, že některý z těhlech názvů už někdo použil, mornfall to hledal
09:08 xbarnat ja si myslim, ze ano
09:09 xstill ok, pak to platí
09:09 xbarnat respektive to jsem tim chel rici, presved mne, ze to plati i na nekonecnych programech
09:09 xstill no neplatí
09:09 xbarnat ok
09:10 xstill jen tak pro zajímavost, nechal jsem přes noc běžet hashset na TSO s rostoucí délkou bufferu, už jsem na 157…
09:10 xstill což je dost za hranicí toho co bude v procesorech bych řekl
09:10 xbarnat aha, ale i tak, zavedenim noveho nazvu se to nevysvetli, ze jo, ... snazsi je rici mame store buffer a happen-before a nazyvame to memory reorder buffer
09:13 xstill to je mi asi jedno
09:22 xstill dopíšeš teda ten úvod? Já zjistím jak udělat do evaluation graf růstu stavového prostoru a aktualizu tam ten text ať to odpovídá tabulkám a pak si přečtu co mornfall udělal s textem v té 3. kapitole
09:26 xbarnat ok potrebuju poradit
09:26 xbarnat LLVM ma svuj memory model
09:26 xbarnat je tak?
09:27 xstill jo, LLVM má svůj memory model kterej je docela odvozenej od C++11, ale má nějaké odchylky
09:27 xbarnat ten je obecny natolik, ze umoznuje dostatecne presne popsat chovani programu pro libovolny memory model  (vetinu) pouzivanych  CPU
09:27 xstill bohužel nevím o tom, že by ho měli popsanej někde jide nž na webu
09:27 xbarnat protoze ze jo, co je to memory model LLVM
09:28 xbarnat LLVM neni executor codu
09:31 xstill jazyky mají taky memory model, v tom smyslu, že ale dávají minimální garance co se musí dodržet, a kompilátor to může zkompilovat striktnějš, no LLVM memory model je memory model dostatečně obecný na to, aby dokázal obsáhnout memory model C++ (a javy a dalších) a zároveň se dal namapovat na memory model konkrétního CPU
09:31 xstill on vlastně over-approximu memory model CPU
09:31 xstill cpu bude typicky striktnější
09:32 xstill asi by teoreticky mohli existovat CPU který jsou relaxovanější, ale moc sis to nedokážu představit
09:33 xstill v podstatě by asi musely umožňovat přeřazování zápisů do stejné paměťové lokace
09:34 xstill jakože cílem LLVM memory modelu je řekl bych být dostatečně expresivní aby se ten program dal efektivně zkompilovat na skoro libovolné CPU, pokud si někdo dá práci s tím mít správně co možná nejmenší nutný atomic ordering u těch instrukcí
09:35 xstill dává to smysl?
09:37 xbarnat hm
09:37 xbarnat ja teda nejak zminim ten llvm model v intru, ale precti si to prosim potom jestli to dava smysl ...
09:38 xstill jo, dobře
09:53 xbarnat svn up
10:05 xstill jo chvíli
10:18 mornfall ok, beru to tak že si to vyřešíte jak chcete
10:19 mornfall v alt.tex je text kterej navazuje na to původní intro
10:19 mornfall tak si to kdyžtak překopte
10:49 xstill mornfall: doděláš prosím ten červenej text ve 3.3?
10:50 xstill já si to pak klidně integruju
10:51 xbarnat strukturalne se nic nezmenilo, jen se posunulo cislovani o jedna vys, protoze jsem dal related work jako separe kapitolu
10:52 xbarnat takzo to co je v alt jako sekce 2 je v main zhruba od 2. odstavce sekce 3 jedna k jedne ... (akorat nazvy sekci jsem zmenil a nemel jsem ...)
10:52 xbarnat takze podle mne ten monrfalluv text jde pouzit ...
10:54 xstill však jo, půjde
10:54 xbarnat ok
10:57 xstill xbarnat: pošli Dirkovi co má citovat na SymDIVINE
10:59 xstill a zkontrouluj ty tabulky, za divine mu tam chbí concurrency, za symdivine taky a celkově tam nevím co by mělo být
11:05 xbarnat citovat asi nic ... tool paper nemame
11:07 xstill něco co Vilík publikoval nejde použít?
11:08 xbarnat asi by slo, jenze ja nemam ted tabulku publikaci ...
11:09 xstill ale máš to cos dělal k prosfesůře, ne?
11:09 xbarnat je tam honza mrazek?
11:09 xbarnat at si to vezme na starost ...
11:09 xstill mám ho na facebooku
11:09 xbarnat jo ja mu psal pres messanger
11:10 xstill DIVINE už má concurrency support v tabulkce, jen teda nechápu jak u nástroje kterýž soutěží jen v concuirrency to mohl nezadat…
11:11 xbarnat symdivine taky, ne?
11:15 xstill to vyřeší Honza, mi přišlo že u toho je těch chyb víc
11:23 xstill tak konečně umím udělat graf (viz svn) teď už jen doufat, že to doběhne
11:24 xstill jdu se podívat na ten úvod
11:26 xstill to jsem ti vlastně mohl napsat dřív, ale spíš než LLVM bitcode bych používat LLVM IR, protože bitkód je jen konkrétní způsob reprezentace LLVM IR
11:28 xstill xbarnat: můžu ti tam udělat drobné úpravy, nebo tam něco měníš?
11:34 xstill no, přinejhorším ty konflikty vyresolvuju
12:02 xbarnat nemenim nic opravuj dle svych predstav
12:04 xstill ok super
12:04 xstill za dávám to dohromady s tím mornfallovým, za chvíli to pushnu
12:16 xstill svn up
12:20 xstill (uprvoval jsem předposlední dva odstavce v úvodu a dal jsem ty další kapitoly dohromady s tím v alt.tex)
12:40 mornfall víte o tom že hned v první větě abstraktu máte chybu?
12:40 mornfall (vlastnosti se typicky nedetekujou)
12:41 xstill hm jo to ne
12:43 mornfall v related work jsou překlepy (realxed, eventhough)
12:44 mornfall a ten červený text do 4. zcela jistě nepatří
12:44 xstill teď to čtu, budeš to opravovat, nebo mám nejdřív já?
12:45 xstill proto je červený, abych si rozmyslel kam ho dát
12:47 mornfall jo a v evaluation si oprav 'verified to be incorrect'
12:47 mornfall (aspoň)
12:47 xstill jo evaluation potřebuje víc úprav
12:48 xstill prosím tě: "Since that point" to je trochu divný, ne? Spíš asi "From that point" (…, state space grows no more)
12:48 mornfall co je 'the LLVM approach to verification'?
12:49 mornfall jo, since that point je taky blbě
12:49 mornfall hned ta další věta je taky špatně složená
12:50 mornfall primaryly focused to handle...
12:50 mornfall (pravopis, gramatika)
12:51 xstill jo to už jsem u sebe opravil
12:52 mornfall 4. odstavec intra by taky potřeboval spravit
12:55 mornfall a ten červenej text v 4.3 můžeš asi smazat, jinak ti asi stejně nezbyde místo na conclusion
12:57 xstill (svn up, intro, částečně)
12:58 mornfall no ta první věta je teď zase děsivě krkolomná :-)
12:58 mornfall detection of violation of deadlock freedom?
13:00 mornfall a ten čtvrtej odstavec je blbě nejen stylisticky ale podkopává aj myšlenku že to jde použít s něčím jiným než divinem
13:02 mornfall (LLVM interpreter existuje jen v (semi)explicitních nástrojích)
13:02 mornfall 'such the transformation can be combined'
13:03 xstill sakra
13:03 xstill musím to přepsat pořádně
13:06 mornfall 'generous' radši ne, a 'the so called' by bylo vhodný spíš kdyby to nebyla první zmínka o tý věci v literatuře :-)
13:07 mornfall (a 'insertion' teda taky radši ne)
13:08 xstill vlastně nevím co se Jiříkovi nelíbilo na tý tvý úvodní větě, mě příjde v pohodě
14:05 xstill to je zas radosti, Milan po mě chtěl nějakej dess, tak jsem vyblil dess s 131M stavama, vygenerovat to trvalo asi 15 minut a teď se mi to tu hodinu transponuje… to jsem zas něco dobře naprogramoval
14:23 mornfall (jo, reference jsou pak taky těžce nekonzistentní)
14:41 mornfall (to 'as our contribution' v abstraktu mi přijde dost trapné, ale když už to tam musí být tak za to přijde čárka)
14:42 mornfall a to 'but not used in practice' dost rozbilo návaznost těch vět kolem toho
14:42 xstill mrknu na to
15:25 xbarnat joined #divine
15:51 xstill xbarnat: napíšeš prosím conclusion (+ svn up)
15:55 xstill mornfall: máš někde tu citaci na The purpose of the store buffer in a CPU is to reduce the overhead of the cache coherence protocol~\cite{mckenney}?
16:10 mornfall jo, google mckenney barriers
16:10 mornfall bib nemám
16:11 mornfall ale citeseerx něco má
16:12 xstill http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.5245 ?
16:12 mornfall jo
16:20 xstill nondeterministically s pomlčkou nebo bez?
16:28 mornfall si vyber, obojí může být
16:32 xstill ok
17:11 xstill hm, a ty verifikace tabulky se zvětšujícím se store bufferem pořád běží, kdybych já blbec věděl, že to doleze tak daleko, tak jsem to mohl zvětšovat rychlejš
17:13 xbarnat pisu conclusion
17:13 xstill ok, já jsem zatím zvládl dopsat tu 4 kapitolu, takže už nemáme nic červeného
17:14 xstill problém ale je, že jsem ubral místo na conclusion, ale tak něco pokrátím
17:49 xbarnat svn up
17:50 xbarnat conoclusion jsem napsal tak se na to kouknete
17:50 xbarnat jinak ja musim jit na osmou na ples, takze ja uz koncim, Vlado prosim udelej zaverecne zkouknuti a submitni to
17:51 xbarnat diky, za hekticky den (teda aspon ja jsem mel)
17:51 xbarnat jestli to ma sanci, to se uvidi
17:52 xstill díky, ok, provedu
18:13 mornfall 'a primitives' (conclusion)
18:14 xstill jo, opravím
18:17 mornfall no ten 4. a 5. odstavec intra jsou furt dost humpolácký a related work znovu vysvětluje co je LLVM IR (a v conclusion je to navíc napsaný jako LLVM-IR)
18:17 mornfall 'under setting' taky nejde (první odstavec conclusion)
18:17 mornfall in (a) setting, nebo under bez setting
18:21 mornfall to co se v tabulkách jmenuje dfifo je v grafu asi pojmenovaný divine-fifo
18:24 xstill na ten úvod se ještě jednou podívám pořádně. Závěr snad opraven. to dfifo už mám u sebe opravený, jen jsem nechtěl pořád commitovat to pdf s grafem
18:27 xstill jdu si sehnat něco k večeři a pak se vrhnu na ten úvod znova
19:50 xstill že bych teda věděl co s tím to se říct nedá :-/

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