Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2013-05-07

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

All times shown according to UTC.

Time Nick Message
06:49 spito joined #divine
09:52 xstill mornfall: co to teda dává divine za číslo v Memory-Used? To je peak čeho?
09:52 mornfall xstill: VM
09:52 mornfall To je v podstatě vrchní mez.
09:53 xstill ok
09:53 mornfall Víc paměti určitě použít nemohl, protože jí víc neměl namapovaný. :)
17:46 spito mornfall: je validní říct o něčem, co bylo napsáno v DVE, že je to program?
17:46 mornfall V podstatě asi jo.
17:47 spito kujů
17:47 mornfall Záleží co to bylo. :-)
17:47 spito tak, já to smolím do bakalářky
17:48 spito a protože jsem nejprve popisoval program a že ten má stavy a rpogram countery
17:48 spito no a že tohle jako divajn verifikuje
17:48 spito a že podle dalších specifikací hledá zajímavé vrcholy v grafu
17:49 spito jakože jestli jsou například nějaké vrcholy dosažitelné, nebo je na akceptujících vrcholech cyklus
17:50 mornfall hmm
17:50 mornfall to zní trochu divoce
17:50 spito ono to tak není?
17:50 mornfall program counter je součást stavu
17:50 mornfall implementační detail, dalo by se říct
17:50 spito jo, stav obsahuje paměť + PC
17:51 spito to tam mám pospaný
17:51 mornfall no, PC každýho procesu
17:51 spito jo, to tam mám taky napsaný
17:51 spito Pro všechny programy platí, že v určitém okamžiku mají nějaký stav. Stavem se myslí obsah paměti a tzv. \textit{program counter}, což je číselná hodnota, která udává instrukci, která se má právě provést. Zde platí, že každé vlákno má svůj vlastní \textit{program counter}. Běh programu je pak složen z posloupnosti těchto stavů.
17:52 mornfall Hmm.
17:52 spito je to blábol?
17:52 mornfall Trochu. :D
17:52 mornfall V první řadě bych do toho netahal čas a okamžiky.
17:53 mornfall Běh programu lze chápat jako posloupnost stavů, kde stav je obsah paměti.
17:53 mornfall Program countery a proměnné jsou uloženy v paměti.
17:54 mornfall (Registr je nakonec taky paměť...)
17:56 spito no, jestli bych mohl, tak ti za chvilu pošlu něco jako 2. návrh textu, jestli by ses mi na to nemrknul a neoznačil místa, která jsou evidentně špatně
18:14 mornfall jo, přečtu si to, ale počítej tak s hodinovou prodlevou
18:15 spito mě to tak ještě hodinu bude trvat, než to dosmolím
18:16 Erbureth joined #divine
18:32 spito mornfall: existují symbolické model-checkery, které se zabývají verifikací paralelních programů?
18:34 spito mornfall: website, titulní strana
18:35 spito DVE – the original DIVINE modelling languageg
18:35 spito to g tam asi nemá být, že?
18:36 spito mornfall: LLVM bitcode (suitble for model checking C and C++ code)
18:36 spito suitable?
18:37 xstill mornfall: díval jsi se na tu mojí práci kromě úvodu?
18:46 xstill spito: no pokud bereš vážně takové věci jako jsem prezentoval na semináři, tak se dá říct že je to symbolický "model checking" "paralelních" programů
18:46 xstill mornfall: na antee je nová verze i s pdf, pokud by ses na to podíval byl bych ti vděčný
18:58 spito xstill: a dělali taky takové věci jako je explicitní vyjmenování všech možných proložení?
18:59 xstill spito: no oni udělali formuli a tu hodili SMT solveru, a bylo omezené kolik to má mít synchronizací
19:00 spito nevíš, jak to má být s tím petanque closed?
19:01 xstill nevím, ono by bylo asi potřeba aby se někdo chopil organizace
19:11 xstill mornfall: generování protipříkladu v pro LTL projde celý stavový prostor?
19:12 xstill (mě příjde že jo)
19:53 spito hmm, tak mám asi problém
19:54 spito neškáluje mi to tak, jak by mělo
19:54 spito tedy na 3 vláknech mám1/2 čas oproti 1 vláknu
19:57 xstill spito: to není tak špatné, nemůžeš čekat, že budeš 2x tak rychlý na 2 vláknech
19:58 xstill jsi rychlejší než partitioned?
19:58 spito http://www.win.tue.nl/ipa/archive/springdays2010/Laarman.pdf
19:58 spito je to špatné
20:00 xstill zase oni?
20:00 spito no jasně
20:00 spito a ještě se jim smějou
20:00 spito na 9. slidu
20:02 xstill a zkusil jsi je nezávisle změřit?
20:02 spito ne
20:02 xstill to by za to stálo
20:02 xstill je jenom potřeba starý divine na překlad dve
20:03 xstill což je docela problém vzhelem k tomu že poslední binárka zdechla s předchozí hydrou
20:04 xstill tak ne
20:04 xstill https://divine.fi.muni.cz/hydra/build/5787
20:04 xstill aha tak jo "Product /nix/store/mjbdifav38zln271bmmh3i905bck7ldz-divine-full-2.5.2+pre1638 has disappeared."
20:04 xstill super :-D
20:05 xstill naštěstí máme někoho kdo ten build má antea:/home/xtomast1/tools/divine-2.5.2/_build/tools
20:06 xstill alespoň k něčemu nám je
20:06 spito :D
20:09 xstill pokud se ovšem vůbec dá ltsmin zbuildit na nixu
20:12 xstill ale dá se najít ve stejném zdroji :-D
20:14 spito jo, s tím počítám
20:14 mornfall kdy to máte mít hotový?
20:14 spito no, 20. 5 je konec
20:14 spito poslal jsem patch
20:14 spito na web
20:15 spito mornfall: ono mi to neškáluje
20:15 xstill ti šmejdi nepoužívaj normální divine, ale nějakej opatchovanej asi na ten překlad
20:16 mornfall spito: Co ti neškáluje?
20:16 spito shared
20:16 spito tedy na 3 vláknech mám1/2 čas oproti 1 vláknu
20:21 mornfall To nemusí být nutně problém, 3 vlákna nás až tak moc nebolí.
20:23 spito jak je velký elevator2.3.dve?
20:24 mornfall Ne moc. Co to bastlíš?
20:24 spito nějaký test bych chtěl udělat
20:24 spito jestli to škáluje
20:24 mornfall Ty nic nemáš?
20:25 spito no, zatím jsem běhal nad dummy
20:27 mornfall ... :-)
20:27 mornfall Jako bych ti neříkal že to je příliš specifický.
20:27 mornfall Možná jsem dokonce zmiňoval Jaromíra.
20:27 xstill mornfall: co?
20:29 mornfall No, „to neděláš dobře Jaromíre“ ... to je z filmu
20:30 xstill aha to
20:31 xstill zkoušel někdy někdo jestli ltsmin ty dve skutečně umí načíst?
20:32 mornfall spito: Ten patch na web je z jaký doby?
20:32 spito dnes
20:32 spito teď
20:33 mornfall spito: Že to je proti nějaké historické verzi.
20:33 spito já to aktuálně ten překlep vidím na webu
20:33 mornfall To sice jo, ale všechno kolem je jiný. :-)
20:33 mornfall Takže to vyrobilo několikanásobnej konflikt.
20:33 spito chjo
20:34 spito tak si to oprav sám, bude to jednodušší
20:34 mornfall Jasně.
20:35 spito aspoň víš, kde chybí a přebývají písmenka
20:35 mornfall No, to suitble jsem tady už někdy aj zmiňoval. :-))
20:44 mornfall Hele, pošlete mi odkazy na ty PDFka, teď už to nedávám, ale zkusím se na to co nejdřív podívat.
20:45 spito mornfall: no, já jsem zase skončil na tom, že napsat kapitolu úvoda asi nezvládnu
20:45 spito ...do konce studia
20:46 xstill mornfall: chceš to poslat  mailem nebo kam?
20:46 mornfall URL do mailu asi ideálně, tam mi to neodskroluje.
20:46 xstill spito: antea:/home/xstill/LTSmin/ltsmin je wrapper který pouští ltsmin kdyby jsi si chtěl hrát, nezabij anteu
20:47 xstill ok
20:47 mornfall A teď jsu dead for the world, dobrou noc. :-)
20:48 xstill dobrou
20:48 mornfall (nebo spíš to... achjo, fakt brou)
20:50 spito brouk
20:55 xstill spito: vrždíš anteu
20:57 xstill když ti to swapuje tak ti to fakt škálovat nebude
20:59 spito já ji vraždim?
20:59 spito proč?
20:59 xstill tak bereš až 16GB paměti
21:00 spito jo, to bude ono, že na 1 vlákně to trvá 351s
21:00 spito a na 8 vláknech jen 20s
21:01 spito ale jo, zvedlo mi to náladu, škáluje to
21:01 spito nad CESMI
21:01 spito tak jdu hajat
21:01 xstill to je dobře že to funguje
21:01 xstill dobrou
21:01 spito left #divine

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