Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2014-07-22

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

All times shown according to UTC.

Time Nick Message
08:04 xbarnat joined #divine
08:06 xbarnat Hola, v uvodu se tvrdi, ze prozkoumavani stavoveho prostoru CSDR strategii defacto ma vyssi pravdepodobnost nalezeni chyby, proc si to myslime? Je podil chybovych stavu na velikost prozkoumaneho stavoveho prostoru v teto oblasti nejak  vetsi? nez kdyby se to merilo pres cely stavovy prostor?
08:07 xbarnat teda snad uz nespite ...
08:13 xstill já nespím
08:13 xbarnat BTW s tim padajicim php na antee je potreba neco udelat ...
08:15 xstill nemám to podložené nijak, spíš mi příjde intuitivní že pokud omezíš počet CS tak odložíš prohledávání stavů, které jsou zbytečně obtížně dosažitelné
08:15 xbarnat a vubec se mi vlastne nelibi, ze v uvedu piseme co ocekavame ... to je prece uplne blbe ...
08:16 xbarnat nemuzu to polozit v rovine hypotezy ...
08:16 xbarnat jako ze myslime si, ze je to lepsi ...
08:18 xstill nevím no, to by se pak celé podat jako že cílem je zhodnocení přínosů
08:18 xbarnat j presne ...
08:18 xstill + minimálně můžeme zmínit, že příklady s méně CS jsou (subjektivně) lépe čitelné
08:19 xbarnat to jo
08:19 xbarnat ale ani experimenty jednoznacne nepotrvdili, ze je to vzdy lepsi ... je to proste heuristika ...
08:19 xbarnat nepotvrdily
08:19 xstill to jo
08:20 xstill ale těch experimentů je pořád relativně málo (především s ohledem na to, že to má v podstatě jen 3 typy programů), našel bych nějaké použitelně velké modely třeba v tom co dělal Milan Lenčo?
08:21 xstill protože LLVM modelů máme dost málo a většina z nich navíc nemá chybu nebo jsou hodně velké
08:24 xstill (jdu se přesunout do labu, pak si přečtu backlog)
08:24 xbarnat jo s modelama je problem ...
08:25 xbarnat muze nekdo kompetentnejsi nez ja odpovedet dotaz (viz email)
08:57 xstill no já bych řekl, že to bude ten bug v llvm, ale nevím, mornfall by mohl vědět víc. Minimálně se mu dá doporučit zkusit nejnovější llvm (3.4.1), a pokud to nepomůže může nám poslat model
08:58 mornfall jo... a teda verifikovat program s floatama je docela odvážný ;-)
08:59 xstill no, pokud to tak bereš tak bys to asi měl někde napsat
09:00 mornfall proč? to je tak trochu self-evident ne?
09:04 xstill z čeho? To že floaty mají veselou semantiku neznamená že žádnej program kterej je používá nemůžeš chtít verifikovat
09:07 mornfall joined #divine
09:07 mornfall hm, teď ale vypadává celej blok (elektrika)
09:07 mornfall chtít můžeš, to ještě neznamená že to půjde, hlavně pokud ta aritmetika není úplně triviální
09:11 mornfall hlavně teda ta aritmetika není úplně přesně definovaná, takže podle toho na jakým CPU (resp. FPU) divine pustíš může mít vliv na výsledek
09:11 mornfall neříkám že tím nenajdeš chybu, ale rozhodně bych netvrdil že to je zverifikovaný :-)
09:25 xstill ale jo, to já netvrdím
09:39 xbarnat bude se v clanku CSDR nejak resit kombinace CSDR s tau redukci? nebo to ma zustat jako takova poznamecka v uvodu?
09:45 mornfall to jsem se ptal včera :D
10:01 mornfall já bych to trochu rozepsal
10:04 mornfall a co je špatný na tom něco očekávat?
10:06 mornfall navíc teda ty předpoklady (assumptions) co tam jsou prostě udělat potřebuješ, náhodnej graf rozhodně tuhle vlastnost mít nebude
10:06 mornfall a samozřejmě budou třídy programů které taky ne
10:06 mornfall ale jsou třídy programů kde to platí -- dává smysl předpokládat že máš vstupy pro který je smysluplný dělat to co děláš, ne? :-)
10:39 xbarnat zavedl jsem sekci Connections (predbezne) kam prijdou ty ony vselijake poznamky a poupravil jsem intro
10:43 xbarnat a mam hlad
10:44 xbarnat a to jsem se prave vratil z obeda
10:44 xbarnat kurna drat
10:44 mornfall :D
10:44 mornfall já to chtěl nazvat Behaviour asi naposled
10:45 xbarnat uvidime, co tam bude, pak se to snadno prejmenuje
10:49 xbarnat napise nekdo odpoved na to floating point? poslat na Chang Liu <changl@vt.edu> a na divine?
10:52 mornfall hm, a já prej píšu komplikovaný věty...
10:54 xbarnat :-o
10:56 xbarnat prepis ...
10:56 mornfall hm, a proč given input data vector?
11:46 xstill (svn update)
11:50 xbarnat to jsem myslel, jako ze pro uzavrene programy ...
11:52 xbarnat pridej do svnky plot-time.pdf jinak mi to nejde prelozit
11:53 xbarnat pripadne pravidlo, jak ho vytvorit ze stavajiciho plot-time bez pripony
11:54 xstill hm, to tam někde bylo
11:54 xstill podívám se
11:54 xstill co ti to dělá když dáš make?
11:55 xstill mě to normálně přeloží plot-time
11:55 xstill (přišlo mi zbytečné dávat do svn binární soubor)
11:56 xbarnat jj, jasne, sorry
11:56 xbarnat ja prekladam primo z emacsu, tak ze nevolam make, ale pdflatex ... historicky duvody :-)
11:56 xbarnat takze, ok
11:57 xstill :-)
11:57 xbarnat 12 stranek je limit?
11:58 xbarnat j je
11:58 xstill no ty grafy podle mě bude vhodné zmenšit aby se vešli 3 na stránku, nebo je tam nedávat všechny, nebo bobojí
11:58 xbarnat jj aspon 3 na stranku
12:03 mornfall no, mně input vector evokuje přesnej opak :-)
12:04 mornfall že máš program s IO a krmíš ho fixníma datama
12:15 xbarnat no vidis, jak je svet rozdilnej
12:15 xbarnat mozna given -> fixed?
12:16 xbarnat nebo for a given  initial state
12:17 mornfall no to je úplně jedno, existence input vektoru implikuje IO, žejo :)
12:30 xbarnat jasne chapu, staci rict, proste to zrusim a bude ... zustane to vagne presny
12:30 xbarnat :-D
12:32 xbarnat tak ja jsem dopsal i related work ... ted od toho davam ruce pryc (nanejvys opravim nejake formulace, nebo preklepy) a je to vase
12:36 xstill hm, stejně by mě zajímalo jak je možný, že single threaded běh má takový rozptyl, vždyť i shared by měl na jednom vlákně být deterministický, ne?
12:38 xbarnat jo je tam neco blbe ....
12:38 xbarnat stejne ale i s jednim vlaknem, nebezi jeste nejake dalsi, kontrolni?
12:39 xbarnat myslim ridici?
12:39 mornfall však to je všechno čas, ne?
12:40 xbarnat :-) jako ze cas je elastickej?
12:40 mornfall kdyby to byl počet stavů chápu vaši konsternaci
12:40 mornfall ale desetiprocentní rozptyl času?
12:40 mornfall meh :)
12:42 xbarnat no me to spis prekvapuje ... nez znepokojuje, pokud je to fakt proste nejakym nedeterminismem v rozlozeni pameti procesu, zateze procesoru OS a podobne tak jsem si myslel, ze to teda takovej efekt nema (nemivalo, kdyz jsem jeste programovaval ja)
12:43 xbarnat taky to muze byt jednoduse CPUcke, se zahreje, tak si ubere takty, ze jo ...
12:43 mornfall nevim, je to měřený na arke
12:43 mornfall ta furt něco dělá, i když ne na všech corech
12:43 xbarnat moderni technologie
12:43 mornfall taky má víceméně plnou paměť, když se trefíš do momentu kdy je jí dost nezapsaný tak musíš holt počkat až se flushnou buffery na disk
12:44 mornfall hm, i když ty modely jsou zase dost malý
12:44 xbarnat jasne pokud je stroj pod zatezi, tak to se na ty cisla ani neda moc spolihat ...
12:44 mornfall 20G by mělo stačit na všechno
12:44 xstill jo no
12:44 mornfall co by se nedalo
12:44 xbarnat predpokladam, ze je to walltime
12:44 xstill nevím, může to být jen fluktuace
12:44 xstill jo walltime
12:46 mornfall xstill: hm, cos tam dal za font tomu gnuplotu? protože to úplně zmastil...
12:47 xstill ten cos tam měl
12:47 xstill jen jsem změnil velikost terminálu
12:48 xstill nepodařilo se mi najít/nastavit lmodern
12:51 xstill hm a zmizel mi popisek y osy
12:52 xstill to bude tím že jsem ho nepřepozicoval (ještě jsem to nenaprogramoval, chci nejdřív napsat něco k výsledkům)
12:52 mornfall Latin Modern Sans,13 vypadá tak nějak plusminus OK... evince to rendruje trochu líp než okular ale furt to není úplně ono
12:53 mornfall a nevim teda proč 13, někde je chyba s velikostí něčeho
12:54 xstill hm, to když tam dám tak dostanu nějaký divný bezpatkový font
12:55 mornfall no, Sans je bezpatkový, logicky :-)
12:55 mornfall Roman je patková verze
12:56 mornfall fc-list | grep Modern
12:56 xstill jo no já dostanu stejný font i když tam zadám Roman
12:57 xstill aha já totiž žádný Latin Modern nemám
12:57 mornfall :D
12:57 xstill jakou máš definici fontů v nix configu?
12:58 xstill (+ myslel jsem že pointa je mít stejný font jako latex, proto jsem čekal patkový)
13:00 mornfall no, stejnou rodinu :-)
13:00 mornfall stejnej font jako je DIVINE třeba
13:01 mornfall jenže to je celý trochu futile, protože tam stejně cpe naškálovanej LMSans 10
13:01 mornfall a asi ho nedokážu ukecat aby tam dával LMSans 12
13:01 mornfall ha, umim
13:02 mornfall nix-env -i lmodern stačí udělat jinak
13:04 mornfall když tam napíšeš LMSans12 jako font (bez čárky a velikosti) tak to asi dělá to co má, zhruba
13:05 xstill jo
13:07 mornfall hm, ono to je nějaký celý zmršený... změnou velikosti fontu v gnuplotu se mi mění rozměr celýho výslednýho PDFka
13:15 xstill tak to se u mě teda neděje, jako posouvají se divně popicky, ale to je tak všechno
13:33 mornfall asi potřebuju 4K displej nebo co :|
13:33 mornfall ty fonty mě začínaj dost prudit :P
14:12 xstill :-D já toho potřebuju tímhle způsobem (i když 30" dispej by mi asi stačil :-P)
15:10 xstill tak připsal jsem něco k algoritmu a jdu nějak zhodotit výsledky (u výsledků mi zatím nic nepřepisuj)
16:16 xstill zajímavý, kromě jednoho případu csdr nikdy nenašlo delší protipříklad než nejdelší co našla reachabilita
16:50 mornfall :P
19:00 mornfall asi nejvíc mi vadí že se podle zoomu mění kerning
19:00 mornfall a na některých zoomech je vysloveně špatně
19:08 xstill no teoreticky bysme mohli zkusit exportovat to do latexu místo pdf, ale nevím jestli si pomůžeme nebo přiděláme spoustu "zábavy"
19:15 mornfall no, tohle je problém pdf prohlížečů :-)
19:15 mornfall to asi nevyřešíš změnou terminálu
19:16 mornfall (pokud si chceš hrát s terminálama, tak rozhodně tikz, v latexu)
19:17 mornfall a dost rychle nám dochází místo :-)
19:18 mornfall fig 1 a 2 maj dost podobnou strukturu, tak bych jeden z nich asi škrtnul
19:20 mornfall taky by bylo dobrý nějak výrazně rozlišit bug a non-bug obrázky
19:27 xstill nojo ale jak
19:27 xstill ad fig 1, 2 -- asi jo vyhodím 1, je menší
19:30 mornfall hele ten pseudokód je nějakej vadnej
19:31 mornfall na cyklu s jen cs hranama to poběží donekonečna ne?
19:33 mornfall (a i když se to zrovna nezacyklí tak to skoro určitě není lineární)
19:49 xstill podívám se
20:04 mornfall no, na 4K monitor to úplně nevypadá...
20:09 xstill co, prodávají se nová auta za nižší cenu? :-D
20:09 mornfall to nevim, ale jedinej solidní 4K monitor do 30 tisíc je jen 24" 16:9 :-)
20:11 xstill a prodávaj ho s lupou?
20:11 xstill já ti nevím co se ti na tom algoritmu nelíbí
20:12 mornfall tak, co se bude dít pod cs hranama?
20:12 mornfall začneš s V_next = {1}, máš cs hranu do 2, máš V_next{2} (Q je prázdný)
20:13 mornfall v 2 máš cs hranu do 1, V_next bude {2}
20:13 mornfall etc.
20:13 mornfall {1}
20:14 mornfall pro cs hrany se ignoruje V_seen, nevim jestli stačí přidat tohle jako podmínku a už to bude OK
20:14 xstill na cyklu jen s cs hranama to nepoběží donekonečna protože: jseš na první hraně, hodíš v' do V_next a nemáš co dalšího -> next level, vybereš v' z fronty, teď je to v, přidáš do V_seen
20:14 xstill jo problém je že nekontoluju V_seen pokud tam je CS
20:16 mornfall do Q nikdy nic nedáš, tam jdou jen non-cs hrany
20:16 mornfall teda, krom toho že tam dáš ten jeden vrchol z V_next
20:17 xstill no ten nemusí být jen jeden
20:17 mornfall tak jasně, ale na cs cyklu je jen jeden
20:17 xstill no to není problém, problém je, že si musíš kontrolovat V_{seen} před tím než něco přidáš do V_{next}
20:18 xstill tím se ti ten cyklus ukončí když ho uzavřeš
20:18 xstill opravím a pushnu
20:19 mornfall by mě zajímalo jestli to Jiřík četl...
20:20 xstill sakra, konflikt
20:21 mornfall ajo, já opravoval kerning v identifikátorech
20:22 mornfall $next$ je n*e*x*t :-)
20:28 xstill tak už
20:28 xstill jsem nad tím nakonec zvítězil
20:29 xstill sice mi zmizel můj patch a místo tohe se tam udělal resolve patch ale to je jedno
20:41 xstill už s tím souhlasíš? Nebo to mám dokázat?
20:42 xstill u toho pseudokódu by se dala dokonce dokázat i ta složitost, u divine ale ne protže tam neplatí
20:44 xstill hm, existuje i model kde je rozdíl mezi CSDR a reachabilitou nekonečno
20:45 xstill teda csdr nemusí najít protipříklad přesto že tam je
20:46 xstill otázka je jestli to tam psát
20:51 mornfall no, to se doufám stát nemůže
20:53 xstill no může, vezmi si: f() { while ( true ) ++i; } main() { …; pthread_create( &f, … ); assert( false ); }
20:53 xstill tohle technicky vzato skončí, ale když tam budeš dělal linked list místo toho…
20:54 xstill ten assert je dosažitelný v 2 CS, ale f() je nekonečné na úrovni 1 CS
20:55 mornfall jak tam můžeš nenajít protipříklad s CSDR?
20:55 mornfall hm
20:55 mornfall jo, protože pthread_create je CS
20:56 xstill jo, ale to je jedno, principielně bys to dokázal i jinak
20:56 mornfall resp. nemůže se bez těch dvou CS hnout
20:56 mornfall když budeš dělat linked list tak to taky skončí, protože pointer má konečnou šířku
20:57 mornfall ale chápu co myslíš :)
21:01 mornfall to je stejnej rozdíl jako mezi BFS a DFS, nakonec
21:01 mornfall if ( __divine_choice( 2 ) ) while ( true ) i ++; else assert( false )
21:02 mornfall !__divine_choice, whatever
21:04 mornfall jo, ještě tam je teda typová chyba v tom pseudokódu, V_seen ∪ v
21:07 mornfall hm, a pop(Q) taky chybí
21:07 xstill hm
21:08 xstill jo
21:10 xstill opraveno
21:10 mornfall taky by se asi někam mělo napsat že to je fronta (nebo to udělat jako množinu, a zrušit ten vnitřní for cyklus)
21:11 xstill spíš bych tam asi napsat, že je to fronta (ale kam)
21:12 mornfall (teda něco jako V_next = { v' | (v, v') ∈ succ(v), (v, v') is a context switch, v' ∉ V_seen }
21:12 mornfall )
21:12 mornfall eh, v' ∈ succ(v), v ∈ Q ...
21:13 mornfall nevim :-)
21:13 mornfall možná přidat ř. 3 Q ← empty queue
21:13 xstill :-)
21:24 mornfall no
21:24 mornfall ještě to má teda problém že pro patologický grafy to je kvadratický
21:24 mornfall ten check na V_seen se bude muset přesunout do toho while Q not empty
21:26 mornfall možná kecám
21:27 mornfall jo kecám (uf) :-)
21:28 xstill heh, no já už taky nejsem moc schopnej přemýšlet, jdu spát
21:28 mornfall může to projít vrcholem nejvýše dvakrát, když je následník aj pod cs aj pod necs
21:28 mornfall to sice není úplně ideální, ale asi to je jedno
21:29 xstill co? aha
21:29 xstill jo protože se neodstraňuje z v_next
21:29 xstill což se ve skutečnosti v divine dělá
21:29 xstill ach jo, ten pseudocode moc nesedí na divine
21:30 xstill jenže ten algorimus v divine je moc složitej na popis
21:30 mornfall hm, fakt je to kvadratický
21:31 xstill kde?
21:31 mornfall když máš n selfloopů pod necs a k hran ven tak uděláš n*k kontrol na V_seen
21:33 mornfall to se teda nestane pokud je succ množina
21:33 xstill no to ne, projdu následníky, pro každýho se podívám na v_seen, to vyhodí self-loopy a způstanou mi jen ty hrany ven do v_next
21:34 mornfall aha pravda, selfloopy se neprochází nikdy
21:35 mornfall hm, ale stane se to pokud to nejsou selfloopy ale multihrana do nenavštíveného vrcholu
21:36 mornfall (ale furt to řeší to že succ je množina)
21:39 xstill nojo multihrana
21:40 mornfall (v divinu se multihrany dít můžou, ale to neznamená že je chceme dovolit v pseudokódu)
21:40 xstill jako můžu hodit V_seen <- V_seen u { v' } před ten if na řádku 15, místo toho 11
21:40 xstill pak se to navíc bude chovat víc jako divine asi
21:41 xstill no ne
21:41 mornfall za něj
21:41 mornfall resp. dovnitř
21:41 xstill protože to by porušilo prohledávání pokud tam bude multihrana a jedna bude s CS a druhá bez
21:41 mornfall pravda
21:41 xstill mohl bych to dát za ten else, ale pak by tam byl dvakrát
21:43 mornfall je to tak trochu nevýherný... ale kdyby se CS udělalo jako fce z (v, v') a řeklo se že succ(v) je množina tak to bude OK (ani se nebude moct stát že by byla jinak stejná hrana pod cs aj necs)
21:45 xstill ale pak by to bylo skoro jako v divine, protože fakticky V_seen se chová jako "je v tabulce && extension.done()"
21:45 xstill hm, ale potom v divine prakticky nemůžeš mít multihranu, ne?
21:45 mornfall ono nakonec LLVM bez tau redukce multihranu snad ani vyrobit nemůže... hm, může protože __divine_interrupt_mask, asi
21:45 mornfall nevim, draw mi je maluje :-)
21:45 xstill jak?
21:46 mornfall v poslední době jsem jich vyrobil spoustu
21:47 xstill hm, už jsem se lekl, že tam divine udělá několikanásobnej expand, ale neudělá
21:47 xstill to by mě ale fakt zajímalo jak ti vznikne multihrana
21:47 mornfall když uděláš __divine_choice a do konce atomický sekce stihneš zapomenout žes ho dělal tak dostaneš multihranu
21:50 mornfall no, možná taky nedostaneš :D
21:51 mornfall jen to je možná tak trochu bug
21:51 mornfall ale jo, dostaneš
21:52 mornfall (ale shodou okolností to jak jsem to napsal ji má jen když vypnu redukce)
21:55 mornfall http://pastebin.dqd.cz/JHxX/
21:56 mornfall (to má multihrany aj s tau aj bez tau)
21:56 xstill nojo, to je dost obskurní
21:57 xstill možná kdybys pod mask pouštěl thready, tak ti taky vznikne, pokud to vůbec jde

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