Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2016-06-20

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

All times shown according to UTC.

Time Nick Message
01:48 ilbot3 joined #divine
01:48 Topic for #divine is now DIVINE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
06:05 xstill já si to do požadavků napsal, a jelikož jaksi nemám povinné předměty tak to znamená, že pokud se ten požadavek bude dát splnit tak budu mít volno
06:07 xstill asi vlastně nechápu pořádně co chceš, protože se mi pořád zdá, že to co jsme ti slíbili by mělo stačit
08:05 xstill hm, ovšem donutit libunwind aby fungoval v nativním běhu s tou naší knihovnou bude docela peklo
08:06 xstill protože on samozřejmě potřebuje parsovat dwarf
08:33 mornfall jasně, já pořád něco chci... no tak já už tě nebudu obtěžovat
08:34 mornfall left #divine
09:14 mornfall joined #divine
09:14 mornfall achjo já už ani neumim číst
09:14 mornfall no to je jedno, zjevně toho mám tak akorát dost
09:14 mornfall takže beru timeout a o prázdninách se uvidí co s tím jde nebo nejde dělat
09:58 xstill klid prosím tě, nikdo neříká, že obtěžuješ
11:28 mornfall (do tý doby k zamyšlení: když nechám věcem volný průběh, tak se neděje buď nic nebo se dějou věci typu téma pro Viki (wtf) ale když začnu cokoliv organizovat, tak narážím jen na odpor... mě fakt nebaví se s váma natahovat a když pak i na něco neochotně kývnete -- sprint, středeční divine -- tak to silně působí jako že mi teda vyhovíte abych už neotravoval... je dost těžký
11:28 mornfall nemít dojem, že by bylo jednodušší se na tady ty bolestivý kulhající pokusy o spolupráci vykašlat a dělat si každý na vlastním písečku, jak je nakonec v labu docela tradiční)
12:13 xstill myslím, že na sprint tu každý řekne, že to smysl mělo, Katka akorát říká, že by to bylo lepší kdyby do toho neměla zkoušky a pro Viki to bylo holt moc C++ najednou
12:14 xstill ad nedění se… koho myslíš, před DIVINE sprintem jsem byl v DIVINE týmu v podstatě jen já. No a já měl pravda blbej semestr na produktivitu, ale to nebylo nechtěním ale tím, že jsem moc učil
12:16 xstill na druhou stranu, od tebe se taky moc nedělo, alespoň co jsme viděli… v podstatě dva semestry jsme od teme nevyděli nic až do sprintu
12:39 spito skoro to vypadá, že vám chybí pevná ruka šéfa :D
12:40 mornfall to mám chápat tak, že když nebudu pravidelně informovat o své činnosti tak se nebude nic dít? a proč před sprintem nebyl nikdo v „divine týmu“? minimálně kolem symdivine merge je spousta práce která nijak nezávisí na kódu v divinu a ví se o ní už rok
12:43 mornfall pak tady jsou ti nešťastní studenti s verifikací, to jde taky od devíti k pěti... já vim, nikdo nemá čas a studenti jsou blbí a líní a tak, ale i tak
12:44 mornfall spito: pevná ruka sice chybí, ale protože jsme zavedli demokracii tak asi už žádnej progress nebude :P
12:45 spito já to věděl, že demokracie nefunguje
12:45 spito potřebujete zavést diktaturu
12:48 mornfall spito: nojo, ale diktatura potřebuje diktátora
12:48 spito vy žádného nemáte?
12:49 mornfall asi spíš ani ne... já mam třeba na diktátora hodně vysoké nároky :p
12:52 spito jako když ty jsi diktátor, nebo když si máš vybrat svého oblíbeného diktátora?
12:52 mornfall kdybych si měl diktátora vybrat
12:53 spito co by měl umět dělat? neustále kopat do lidí, aby pracovali?
12:53 mornfall měl by umět dělat dobrá rozhodnutí (víceméně všeho druhu)
12:56 mornfall kopat do lidí by nemělo být nutný, kdo pracovat chce tak při vhodných podmínkách bude a kdo nechce tak může dělat třeba něco jinýho
12:57 mornfall jenže to znamená že úspěšný diktátor potřebuje páky jak ty vhodné podmínky vyrobit a to já třeba nemam
13:23 xstill mornfall: tak Honza pracoval dost
13:24 xstill s Viki se zkoušely různý věci, třeba sumarizace cylků
13:25 xstill studenti jsou do značný míry moje chyba to chápu, ale tam mám největší problém je dokopat k nějaké aktivitě, což je problém toho že moc nevím jak motivovat lidi (nějak bych totiž předpokláda, že když se na něco takovýho přihlásí tak už jsou motivovaní…)
13:28 xstill ad informace, neříkám, že nám musíš pravidelně reportovat co děláš, ale pokud člověk má nápady, jako třeba ty registry, ale zároveň ví, že to může implementovat tak maximálně do verze která za chvíli umře, tak to je demotivační. Podobně ti studenti mají problém ve chvíli kdy mají protipříklad, ale jaký smysl má zlepšovat protipříklady v divine 3?
13:32 xstill problém trochu je, že lidi čas od času potřebují dělat závěrečné práce, a to se někdy blbě slučuje se spoluprácí… protože nemůže vykázat "implementoval jsem tady 10 různých kousků do divine 4" jako diplomku
13:32 xstill ačkoli pro DIVINE by to bylo lepší kdybych mohl
17:31 mornfall tak minimálně od bakalářky se žádná průlomovost nečeká a stvořit dostatečně ucelený téma není v divinu zas takovej problém (si myslim)
17:35 mornfall a pokud jde o registry, tak tam je zase jednou závislost na čemkoliv dalším v divinu dost minimální, prostě se to musí napočítat a případně na to napsat unit testy, použít to pak už je nejmíň
17:36 mornfall (a zrovna tady si taky myslim, že opravit/dotáhnout ten alokátor v divine 3 by byl docela dobrej první krok, s tím že portovat to na divine 4 je trivialita)
17:41 mornfall sice úplně chápu, že psát věci od začátku po svém je větší zábava a taky bych kolikrát radši příchozí patche zahodil a napsal si je po svém, ale není to úplně škálovatelný
17:42 mornfall (viz také: aa v lartu)
17:44 mornfall a když už jsme u toho, tak alokace registrů by mohla být taky dobrá bakalářka pro Viki :) je to dost oddělené, sekvenční algoritmus bez nějakých C++ zákeřností, je za tím spousta potenciálně zajímavé teorie k nastudování a zpracování
17:45 xstill nemyslel jsem tím průlomovost jako spíš ucelenost, teda to, že DIVINE často potřebuje spoustu menších věcí a na nich dost dobře nemůžou dělat lidi co právě mají dělat závěrečnou práci
17:45 mornfall navíc to má okamžitý praktický dopad
17:48 mornfall (ltl pro divine4 je IMHO taky dostatečně ucelený téma a Strejda by to určitě obrblal, ale jinak to je stoprocentně obhajitelný a zároveň pro nás užitečný)
17:51 mornfall dios by stačilo i na diplomku, shadowmapy by taky mohla být klidně bakalářka (ani se to nemusí brát moc zeširoka a taky je za tím teoretická analýza která na bakalářku nejspíš úplně stačí jak rozsahem tak hloubkou)
17:52 xstill LTL pro DIVINE má ten problém, že to odrbal skoro každý kromě nás dvou
17:53 xstill ad registry, to mě nenapadlo, což je moje chyba protože to beru moc jako svoje téma, protože mám nějakou představu jak to udělat. A ano, velký vliv na to že to není má to, že jsem neměl na jaře moc čas
17:53 xstill ty shadowmapy mě nenapadly jako téma, vážně je toho tolik?
17:55 xstill (u toho LTL mi taky nepříjde, že by bylo až tak velký… nevím možná mám blbou představu o rozsahu bakalářek…)
17:57 mornfall něco jako 5 dnů fulltime práce, M ./divine/vm/shadow.hpp -308 +1127 a myslim že to ani není kompletní (aj kdyby bylo, tak si myslim že úplně stačí)
17:58 mornfall většina jsou testy, budiž... ale pochopit a sepsat širší kontext je taky kus práce
17:58 xstill pět dnů fulltime kódění na bakalářku?
17:58 mornfall a kolik si představuješ že typickej student dá?
17:58 mornfall dva?
17:58 mornfall viděl jsi někdy nějakou bakalářku? :D
17:59 xstill to je možná ten problém, ty co jsem viděl nebyly od typických studentů
18:00 mornfall já bych popravdě spíš ocenil menší téma dotažený na nějakou úroveň preciznosti a detailu, než nástřel něčeho velkýho
18:01 mornfall nemusí každej začít PhD téma bakalářkou :-)
18:02 xstill hm, to dává smysl
18:04 mornfall navíc když to srovnám s rh projektem, tak mám skoro dojem že „normální“ student by za 5-7 dnů ani nepochopil co má programovat, ne to aby stvořil něco více nebo méně fungujícího
18:07 mornfall (taky si třeba myslim, že kdybych před těma X rokama měl víc jasno v tom co a jak a po pár měsících rozkoukávání si s váma na týden sedl, tak ty vaše bakalářky implementačně taky dáme dohromady)
18:11 xstill hm, možná máš pravdu, toho kódu tam zas tolik není… i když tam ještě bylo nějaké vyhodnocení. Což se ale nakonec i u shadowmap dá asi něco vyhodnocovat
18:12 mornfall no nebo se dá udělat širší teorie kolem, pak třeba nastudovat co dělá valgrind a srovnat to třeba i teoreticky
18:14 mornfall ale bottom line je, že témat se všude válí spousta a určitě to jde i smysluplně skloubit s implementací něčeho pro divine
18:15 mornfall dneska určitě víc než kdysi, protože přecijen máme dneska lepší představu o tom jak do sebe věci zapadají a co jde kde rozumně oddělit malým rozhraním
18:16 xstill jinak teda, Jiřík dneska Viki nabídl něco s interpolantama (nastudovat co existuje a tak…), ty jeho hybridní systémy a ještě něco, co teď nevím jestli to byly ty Ivaniny věci, nebo jsem to zapomněl; byl jsem u toho, Viki prohlásila, že chce něco co bude spíš teoreticky náročné než technicky náročné… nějak se mi nepodařilo navrhnout nic divine-related co by Jiřík nezavrh
18:16 mornfall a taky se nám kolem LLVM dost rozšířil obzor, takže i toho prostoru je víc
18:17 mornfall jaj, interpolanty... další phd téma
18:17 xstill hm, asi jsem mířil s těma tématama moc vysoko, a Jiřík zdá se taky (pokud jde o práce pro lidi v labu… jinak míří i nízko)
18:20 mornfall já sice chápu že lidi v labu maj ambice, ale zase to si myslím že jde mnohem lépe podchytit tím, že jako starší budem ty témata brát dostatečně vážně i když nejsou zrovna phd-level
18:20 xstill navíc teda, Jiřík mi dneska (před Viki :-/) v podstatě řekl, že nevěří v to, že dokážeme DIVINE dovést k prakticky použitelné verifikaci, ani ve spolupráci s RH. S čímž teda nesouhlasím. Nicméně v tomhle kontextu jde chápat, že se rozhlíží po jiných věcech…
18:21 mornfall já jen nevim jestli to je nějakej pokus o reverzní psychologii (jakože čeká že se zatnem a ukážem mu jak se plete), nebo tomu fakt úpřimně nevěří
18:22 xstill hm, možná dává větší smysl aby člověk napsal bakalářku za půl roku a pak se věnoval něčemu z čeho může být článek, nebo prostě tak, protože nakonec, z čí bakalárky/diplomky byl hned a bezbolestně článek? Z tvojí a teď možná z Honzové bude…
18:23 xstill to já nevím, ale mě příjde, že za ty čtyři roky co jsem v labu jsme se hodně posunuli, a tudíž bych to viděl pozitivně
18:25 mornfall to je jednoduchý, za tu dobu jsme nasbírali zkušenosti a vyřešili X dílčích problémů... jediný co nám může zabránit v prakticky použitelné verifikaci je, že se rozpadneme dřív než to bude hotový
18:32 xstill to by nebylo dobrý. Což mě přivádí k myšlence, že bychom kromě pravidelných týdenní kódicích session mohli obnovit i pravidelné pivo/posezení, protože preci jen tím že nejsi v Brně tak nejsi tolik v kontaktu s námy jako my mezi sebou, já tím třeba dostávám pocit, že nevím moc kam to směřuješ. Příjde mi, že když jsme byli my dva + Jirka a chodili jsme skoro každý pátek
18:32 xstill do alterny tak jsme neměli ...
18:32 xstill ... taková nedorozumnění jako teď a spousta věcí se tam zvládla prořešit
18:38 mornfall ano... víceméně jde jen o to najít nějaký společný čas (a přijde mi že na tom to posledních pár semestrů celkově troskotalo nejvíc, proto ta zoufalá snaha obnovit nějaký pravidelný sešny)
18:41 xstill a ještě bych tě požádal o konzultaci k protipříkladům: moje původní představa byla, že knihovna už je v modelu a tudíž není skoro nic potřeba a těch pár syscallů co jsou potřeba se vytáhne z muslu. Tak jsem to začal dělat, nicméně jsem narazil na problém s libunwindem, který potřebuju zkompilovat tak aby řešil nativní zásobníky, no a kdybych měl kompilovat musl v
18:41 xstill divine.cc tak se z toho asi ***** protože ...
18:41 xstill ... má závislost na ELF parserech a dlfcn z libc. Nicméně dneska mě napadlo, prož na to vlastně nejdu úplně jinak, proč to nevyřeším dynamickou knihovnou: jestli to dobře chápu, tak může model zkompilovat do něčeho co bude dynamicky linkované k libunwind, přičemž ten libunwind už ale klidně může být přeložený nativně (tj. ten který používá DIVINE a který sám využívá
18:41 xstill glibc). Jestli jsem dobře ...
18:41 xstill ... nastudoval dynamický linker tak by to mělo fungovat, protože ten model si věci které může vyresolvuje sám ze sebe a libunwind už nebude resolvovat symboly z modelu, ale z glibc, protože model je dynamicky neexportuje. Je tak, nebo něco přehlížím?
18:41 mornfall jen jsem taky postupně nabyl dojmu, že Jiřík je spíš proti a že mě chce radši od studentů držet dál a taky nevim jak si to vyložit
18:41 xstill ad sešny, Honza i Heňo si tu středu taky napsali do požadavků
18:42 mornfall fungovat by to mělo, možná bude potřeba dát všemu co je „naše“ internal linkage
18:43 xstill jestli tam bude nebo nebude Jiřík není ve výsledku až tak podstatný, stejně tam nebude celou dobu. A Katka si podle mě zvládne dát rozvrh tak, aby tam mohla být většinu doby.
18:43 xstill když jsem to testoval, tak loader neuměl vyresolovat symbol volanej z .so do toho co je v binárce
18:44 mornfall jo, to funguje jen když překládáš s -Bsymbolic
18:44 mornfall (teda, na většině systémů asi)
18:45 xstill tak jo, v tom případě to zítra implementuju takto a snad to bude fungovat
18:45 mornfall (nicméně to myslim ELF nespecifikuje, ale je atribut jak tu neviditelnost z so do binárky vynutit)
18:45 mornfall hm, v binárce vlastně možná i specifikuje, ten atribut je pro .so který si nechcou nechat přepsat symboly jinou so
18:45 xstill hm, ld má --export-dynamic což zdá se explicitně zapíná tuhle viditelnost
18:46 mornfall jo to bude to stejný jako -Bsymbolic
18:46 mornfall to je nejspíš jen historickej název pro to stejný
18:48 mornfall https://www.technovelty.org/c/what-exactly-does-bsymblic-do.html to je taky trochu ujetý
18:52 mornfall to co by teoreticky mohlo hrozit je opačný leak, kdyby ten model měl nějakou nedefinovanou funkci tak by omylem mohl zavolat do glibc pak
18:54 mornfall s tím asi ale nejde bojovat o moc jinak než udělat z toho modelu .so který se slinkuje s -z defs a kód kterej používá libunwind mít v driveru kterej se přilinkuje k tomu modelu a k libunwind/glibc
18:54 mornfall (zase typicky máme zaručený, že pokud ten model divine načetl tak tam je všechno definovaný)
19:06 xstill hm, když dám ld main.o -lx a x je shared tak se symboly nedefinovaný v main můžou resolvovat i něčím co je dynamická závislost x?
19:15 mornfall můžou
19:16 mornfall (pro jistotu jsem to zkusil, ale v NEEDED se v a.out objeví obě .so a ani to nepípne že ten symbol co se použije je v tom nepřímým)
19:19 xstill svině, nicméně teda pokud to bude jen něco co předtím projde divine tak by to nemělo být potřeba řešit
19:21 xstill jinak, pokud mají výjimky rozumně fungovat tak bychom je asi měli implementovat na úrovni _Unwind_* rozhraní libunwindu, tak aby pro nativní běh stačilo stripnout z toho .bc náš "libunwind" a použít systémovej.
19:22 xstill tím pádem navíc celé c++abi bude upstreamové myslím
19:25 mornfall ono by to mělo fungovat aj s __vm_jump, ne? jakože mít libunwind api by nejspíš zjednodušilo port jiných jazyků na divine, ale nemělo by to být nutný pro smysluplný výjimky
19:26 xstill pravda, ono by to vlastně fungovalo taky
19:26 mornfall je pravda, že by to bylo i lepší z hlediska věrnosti verifikace
19:26 mornfall asi dobrý téma na (technickou) bakalářku :-)
19:28 mornfall to co mě ale napadlo je, že by možná bylo dobrý ohackovat ty thready tak, že se skutečně vytvoří aj threadová struktura v jádře a zamkne se scheduler, protože by pak mohlo fungovat přepínání vláken v gdb
19:30 mornfall nebo teda nějakej jinej hack kterej tomu zabrání běhat, ale přesvědčí gdb že to má normální (p)thready
19:30 mornfall snad by neměl být problém to udělat dodatečně, jen to říkám než na to zase zapomenu
19:43 xstill hm, ono vlastě s tou dynamickou knihovnou by to mohlo celkem snadno jít udělat (až na to zamikání scheduleru, to nevím jak zatím, ale při nejhorším se tam prostě vrazí mutex)
19:44 xstill jakože mě tohle už taky napadlo, jenže v tom předchozím modelu implementace co jsem zamýšlel to nedávalo smysl

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