Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2013-10-19

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

All times shown according to UTC.

Time Nick Message
01:47 _ilbot joined #divine
01:47 Topic for #divine is now DiVinE: A Parallel LTL Model Checker (http://divine.fi.muni.cz) | http://irclog.perlgeek.de/divine/
16:51 xbarnat joined #divine
16:51 xbarnat darcs pull; make clean; make
16:51 xbarnat Linking CXX executable ../divine.ide ../../divine/libdivine.a(explicit.cpp.o): In function `divine::dess::PrealocateHelper::operator()()': explicit.cpp:(.text+0xd3f): undefined reference to `wibble::sys::v2::MMap::MMap(int, wibble::StrongEnumFlags<wibble::sys::v2::MMap::ProtectMode>)' ../../divine/libdivine.a(explicit.cpp.o): In function `divine::dess::Explicit::open(std::string, divine::dess::Explicit::OpenMode)': explicit.cpp:(.te
16:52 mornfall xbarnat: to je asi na xstill
16:52 xbarnat `wibble::sys::v2::MMap::map(std::string const&, wibble::StrongEnumFlags<wibble::sys::v2::MMap::ProtectMode>)' collect2: error: ld returned 1 exit status
16:52 xstill xbarnat: hmm, máš zapnutý explicit?
16:52 xstill i když to je asi jedno
16:52 xbarnat Compile-Flags: POSIX COIN PERFORMANCE DVE COMPRESSION EXPLICIT POOLS NVALGRIND CURSES TIMED LLVM MPI OMPI_VERSION
16:54 xstill to je divné, zkusím to reprodukovat u sebe
16:55 xbarnat uz to trva delsi dobu ...
16:55 xbarnat neni to neco co se ted objevilo ...
16:56 xbarnat mornfall: jde nejak zkontrolovat, ze jsou vsechny soubory v poradku vuci repozitari?
16:56 xstill (kompiluju, bude to chvíli trvat)
16:56 xbarnat (jako ze rucne needituju soubor, ale chyba na disku ho modifikuje ...)
16:58 xbarnat proste CRC check ...
16:59 xstill xbarnat: chybí ti #include <unistd.h> v main v 3. úkole IV112
16:59 xbarnat darcs check tvrdi ze repo mam v poradku ...
16:59 xstill main.cc:110:50: error: ‘getopt’ was not declared in this scope
16:59 xbarnat nj, meni se prekladace ...
17:02 xstill xbarnat: bude ti vadit když si nenápadně do makefile přidám -std=c++11? Potřeboval bych unique_ptr a na nymfe už je gcc 4.7
17:02 xbarnat ne
17:02 xbarnat jako vadit mi to nebude
17:03 xstill díky
17:05 xbarnat mornfall: zkousel jsi jaky dopad na velikost stavovych prostoru ma, kdyz se opravi ta TAU redukce?
17:07 xstill xbarnat: napadlo mě, že bys do IV112 mohl pomalu cpát něco jako: vaše řešení musí projít verifikací pomocí divine
17:07 xstill jen teda potřebujeme detekci deadlocků
17:08 xbarnat no to by bylo supr ... ale DIVINE jeste neni na to zraly ...
17:08 xstill snad bude za rok
17:09 xstill co nám chybí kromě detekce deadlocků? (a memory modely, takže je to under-approx. což by ale až tak vadit nemusalo)
17:09 xbarnat pokud toho bude jednoho dne schopny, budu to osobne povazovat za velky uspech
17:10 xstill tak ten 3. úkol je podle mě plně v velikostech co divine zvládá
17:10 xbarnat No ono kdyby se to pripravilo jako ze do makefilu dal cil check, ktery vola divine na pripraveny test ... tak snad
17:10 xbarnat hmm, to je vyzva ... zkusim na posbiranych resenich z letoska ...
17:17 xstill hm, mě se divine z repa zkompiloval normálně
17:19 xstill xbarnat: zkus ještě rm -rf _build/wibble a nebo rovnou smazat celý _build
17:21 xbarnat ok, tak ja se zase zitra ozvu (az se to zkompili ...)
17:23 xstill ty máš to gcc 48?
17:24 xstill hm, moje bariéra má asi deadlock
17:34 xstill ale jenom pokud neběží v debuggeru, super
17:41 xstill potřeboval bych detekci deadlokců v DIVINE...
17:44 xstill ach jo...
17:44 xstill to jsou zase bugy
17:51 xstill zajímavé, atomická bariéra je nejpomalejší
17:51 mornfall no, není deadlock jako deadlock
17:52 xstill tak čekání na podmínkovou proměnnou která se nikdy nesignalizuje je třeba veselý deadlock...
17:56 xstill otázka teda je jak takovou věc detekova
17:57 mornfall no, to by ještě šlo
17:58 xstill to ve stavovém prostoru nejspíš bude dělat cyklus uvnitř pthread_cond_wait, ne?
17:58 mornfall ale jakmile tam budeš mít vlastní spinlocky bude to horší
17:58 xstill hm
18:00 mornfall jakože pthread mutexy (a condition proměnný) můžou udržovat čekací graf interně
18:00 mornfall a když se zacyklí tak to ohlásit
18:01 xstill ten spin-lock, to by v podstatě znamenaho hledat cyklus, který nemění data a není z něho úniku...
18:01 xstill tak zrovna na nesignalizovanou podmínku by čekací graf nepomohl, ne?
18:02 mornfall hm
18:02 mornfall může se stát že ne, asi, ale může se stát že jo
18:03 xstill je to děs, protoře to s tím cyklem by fungovalo jen pokud by byla v deadlocku všechna vlákna
18:04 xstill je to zdá se větší problém než to vypadá
18:08 mornfall je :-)
18:09 mornfall s tím cyklem by to navíc nefungovalo vůbec
18:09 mornfall (protože tuhle vlastnost má každej selfloop, třeba když nějaký vlákno čeká)
18:09 mornfall resp. „není úniku“ se hrozně blbě definuje pak
18:10 mornfall můžeš hledat podezřelý koncový SCC snad
18:11 xstill to jsem asi myslel tím cyklem z kterého není úniku
18:12 mornfall to teda skutečně deadlock nepozná pokud v něm není celej systém (stačí monitorovací vlákno někde a už houby poznáš)
18:12 mornfall občas se to řeší detekcí neprogresivních cyklů, ale to musí uživatel dodat nějaký měřítko progressu
18:13 xstill hm
18:14 mornfall trochu se taky obávám, že zápis do paměti není úplně dobrý měřítko progressu
18:19 xstill tak pokud vlákno je v cyklu kde nemění data tak je to podle mě (live|dead)lock, ale může asi být i livelock kde se data mění
18:21 xstill asi to chce probrat v úterý
18:24 mornfall no, tak jako tak je to 3.2 stuff, radši bych dořešil hashcompaction
18:26 mornfall no, problém je že to že se nemění data nemusí nutně implikovat to že to je deadlock -- kdybys měl třeba nějakou službu ve vlákně která jen čeká na requesty, a testcase vypadá tak že se vytvoří tohle a pak se pustí pár requestů, tak ti divine hodí deadlock i když ten systém prostě už nemá co dělat
18:27 mornfall jen tím že tam není exit to vypadá jako deadlocková end komponenta
18:30 mornfall posix-mutexový deadlocky můžeme chytat spolehlivě a bez false positives (myslím si)
18:30 xstill to je ovšem problém, protože to se asi nedá rozlišit
18:30 mornfall condition wait je horší, protože ten čeká na potenciálně libovolný vlákno
18:31 mornfall ale reálně to může být jedno konkrétní a my nevíme který, takže částečnej deadlock s condition waitem asi nepoznáme
18:32 xstill a nedokážeš to vyjádřit jako LTL ve stylu G( wait -> F( signaled) )?
18:33 xstill jen teda je problém, že tohle potřebuješ pro každou cond-var
18:33 mornfall to dokážeš, ale nebude to platit
18:33 mornfall resp. není to úplně to co chceš
18:33 xstill proč ne?
18:34 mornfall protože občas někdo condition wait použije právě na probouzení nějakýho pomocnýho vlákna kterýho normální stav je čekat
18:34 mornfall na libovolným cyklu kde se nepoužije to platit nebude
18:34 mornfall resp. cestě
18:35 mornfall takže fungovat to bude jen pokud uživatel řekne že tenhle condition wait má mít tuhle vlastnost
18:37 xstill ach jo
18:37 mornfall prostě ten předpoklad, že každej wait co neskončí je deadlock je moc specifický
18:39 mornfall šlo by to řešit částečně tím, že bys hledal ty koncový komponenty jen v programech o kterých uživatel řekne že mají mít jen konečný chování
19:48 xbarnat xstill: rebuild na cisto nepomohl. Skoncilo to se stejnou chybou
19:48 xbarnat explicit.cpp:(.text+0xd3f): undefined reference to `wibble::sys::v2::MMap::MMap(int, wibble::StrongEnumFlags<wibble::sys::v2::MMap::ProtectMode>)'
19:49 xstill xbarnat: divné. Já momentálně builduju gcc 4.8.2 z nixu snad to konečně doběhne tak to pak ozkouším i s tím.
19:49 xstill ještě to můžu zkusit s 4.7 vlastně
19:49 xstill já nevím ten konstruktor tam prostě musí být podle mě
19:54 mornfall xstill: no, když zapnu explicit tak to umírá aj s clangem
19:55 xstill mě ne
19:55 xstill totéž co Jiříkovi?
19:55 mornfall /home/mornfall/dev/divine/mainline/divine/explicit/explicit.cpp:132: undefined reference to `wibble::sys::v2::MMap::MMap(int, wibble::StrongEnumFlags<wibble::sys::v2::MMap::ProtectMode>)'
19:55 xstill hm
19:56 xstill zajímavé
19:56 mornfall no a není to proto že libwibble.a se překládá bez -std=c++11?
19:56 xstill to se snad nepřekládá bez toho, ne?
19:56 xstill pak by to nemohlo fungovat u mě
19:57 mornfall -stdc++11 tam je, máme to v toplevel-u
19:57 mornfall tak nevim :)
20:00 xstill můžeš udělat nm na libwibble a zkusit ten symbol grepnout?
20:00 xstill mě se to normálně kompiluje i s gcc 47
20:10 mornfall jestli ono to není proto že libwibble.a je před libdivine.a ... /nix/store/m4y0jd5y9m0ryz4m52ikm5pdxk8a3g8h-clang-wrapper-3.3/bin/clang++   -O0 -g -Wall -Wno-unused -Wno-sign-compare  -std=c++11 -Wold-style-cast -g    CMakeFiles/divine.ide.dir/main.cpp.o CMakeFiles/divine.ide.dir/qrc_main.cxx.o  -o ../divine.ide -rdynamic -L/nix/store/zm4bhsm8lprkzvrjgqr0klfkvr21als4-glibc-2.17/include ../baseIde/libbaseIDE.a ../baseTools/libbaseTools.a ../dv
20:14 mornfall snad spravený
20:14 mornfall jen Jiřík nám vytimeoutoval
20:23 xstill tak on si toho patche snad všimne
20:24 xstill jo máš patch ode mě
20:25 xstill hele náš trac posílá z adresy trac@fi.muni.cz, to by možná nemusal...
20:29 mornfall hh, to jsem si nevšim
20:30 mornfall smtp_from = trac@anna.fi.muni.cz
20:30 mornfall hm
20:30 mornfall on to možná relay přepisuje nebo něco
20:35 xstill to jsem nevěděl, že FI asi nechává některý lidem za zásluhy fungovat účty
20:35 xstill jinak máme ve skupině dost červených lidí
20:36 xstill ale to je asi Jiříkova starost
20:36 xstill (ten trac mě spíš přišel takový veselý, hlavně ta adresa nefunguje)
20:38 mornfall hm, ten info test je taky veselej
20:39 xstill je no
20:39 xstill ale projde
20:41 mornfall OK (nechce se mi to zase překládat s LLVM, takže tě beru za slovo)
20:42 xstill ono kdyby tam Milan neměl ty flagy ve stylu  --cflags="-std=c++11 < other flags >" tak by se daly i přímo použít a bylo to rozumnější
20:42 xstill možná by to měl anotovat povinnýma flagama
20:42 xstill nějak standardizovaně
20:42 mornfall mě se ten formát celkově nelíbí :-)
20:42 mornfall mně navíc
20:43 xstill jak bys to chtěl?
20:44 mornfall no, Name, Category, Standard jsou úplně zbytečně sekce
20:44 mornfall Elevator [controller, c++11] by úplně stačilo, jako hlavní nadpis
20:44 mornfall pod to short description bez dalšího nadpisu a pak long description jako L2 heading (----)
20:45 xstill hm, že je tam standard jsem si ani nevšim
20:45 mornfall Případně:
20:45 mornfall Elevator
20:45 mornfall ========
20:45 mornfall [controller, c++11] Variation on ...
20:47 mornfall Description
20:47 mornfall ------------
20:47 mornfall ...
20:47 mornfall etc :)
20:47 mornfall seznam tagů možná bez čárek, asi se to líp parsuje
20:47 xstill to bys skoro mohl dát Milanovi do tracu
20:48 xstill třeba to udělá
20:48 xstill a Jiřík by mohl vyhodit florána ze skupiny lab_paradise, nebo jestli si tam skladuje všechny lidi co mu prošly labem...
20:50 xstill a podle skupiny a ISu už Kriho úplně skončil
20:51 mornfall jakože už nemá ani přerušený studium?
20:52 xstill nemá aktivní účet na fakultě a IS u něj má jen BC studium
20:55 xstill co člověk všechno nezjistí ve fadminu...
20:55 xstill ale máme ještě relativně dobře udělaná práva oproti některým jiným skupinám
20:56 mornfall na cos přišel?
20:58 xstill ale tak třeba že pivník je napsaný v sybila-supp, lab_paradise obsahuje spoustu lidí co ani neznám, že někteří mají privilegia a FI jim nesmaže web a účet...
21:00 xstill z těch veřejných věcí jsem zjistil, že vidím které počítače v hale a B130 jsou online a tak
21:01 xstill máme rezervovaných dost IP adres pro pegasusXX, psyche jsou povětšinou mrtvé...
21:01 mornfall nevím, vidím leda tak Jirku Srbu a Janu, oba jsou vedení jako externisti na KTP
21:02 xstill aha, toho jsem si nevšiml, že jsou na KTP jako externisti
21:03 xstill potom je tam jedině florán kdo je aktivní a nemá s fakultou nic, asi ho ještě nestihli smazat
21:03 mornfall jo, to asi chvíli trvá
21:04 mornfall ad Erbureth, studium si v ISu můžeš schovat
21:04 mornfall takže počítám že tam má přerušený nebo zanechaný studium, jen je skrytý
21:04 mornfall co z toho můžem jen hádat :)
21:07 xstill to jsem nevěděl, že studium se dá schovat
21:07 xstill a je možný, že když přeruší tak mu deaktivují účet...
21:07 xstill takže vlastně víme kuloví
21:07 mornfall kulový
21:07 mornfall účet deaktivují skoro určitě
21:08 mornfall to by bylo aby sis přerušil studium a mohl klidně používat fakultní stroje :-)
21:10 xstill což o to, větší srandu si užijí ti studenti co jsou oficiálně přf, ale mají většinu předmětů na FI, těm ten účet zruší každého půl roku aby jim ho po 14 dnech zase aktivovali :-D

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