Perl 6 - the future is here, just unevenly distributed

IRC log for #divine, 2017-01-12

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

All times shown according to UTC.

Time Nick Message
00:53 yaqwsx joined #divine
01:22 divine-buildbot Hey! build divine-nightly-release #45 is complete: Success [finished]
02:48 ilbot3 joined #divine
02:48 Topic for #divine is now DIVINE | http://divine.fi.muni.cz | http://irclog.perlgeek.de/divine/
02:53 divine-buildbot Hey! build divine-nightly-debug #48 is complete: Success [finished]
11:32 yaqwsx Jsou všechny věci ohledně LTL zarecordované? Nemůžu zbuildit testy: "error: use of undeclared identifier 'LTL'"
11:32 xstill_ yaqwsx: na arke?
11:33 yaqwsx xstill_: Ano
11:33 xstill_ asi obnovený bordel v adresáři s divine jak jsem obnovoval home ze zálohy
11:33 xstill_ darcs wh -l a budeš se muset zbavit toho co nejsou tvoje změny a je to přidané
11:34 yaqwsx Ok, díky.
11:35 xheno joined #divine
12:02 mornfall yaqwsx: už to vyrábí syntakticky správnej smtlib2 (zdá se)...
12:07 yaqwsx mornfall: Cool!
12:34 yaqwsx mornfall: Proč vlastně preferuješ includy ve stylu <dios/memory.h> před "memory.h"?
12:40 mornfall yaqwsx: ani nevim, ale většina jazyků má názvy modulů kvalifikovaný
12:54 yaqwsx mornfall: Mám dotaz ohledně spouštění divinu & konfiugrace DiOSu. Můžu přidat přepínač pro použítí reálného FS místo VFS, ale jak zabránit uživateli aby použil reálný FS i při verify? DiOS teď totiž není informován, jak je spouštěn.
12:56 mornfall yaqwsx: jo zatím bych spoléhal na to že uživatel ví co dělá
12:57 kkejstova joined #divine
12:58 yaqwsx Ok, dobře. Ale do budoucna bychom to myslím měli nějak vyřešit.
12:58 mornfall ano
12:59 kejsty joined #divine
13:02 xstill_ xheno: /home/xstill/DIVINE/sym/test/abstract/sym-subst-3.cpp
13:29 xstill_ yaqwsx: právě jsme zverifikovali první symbolický program
13:30 xstill_ (ten co jsem odkazoval Heňovi nahoře)
13:38 yaqwsx xstill_: Gratuluji! Takže jak jsme na tom časově? -50?
13:38 xstill_ yaqwsx: -43 +-1
13:39 xstill_ trochu smutný je, že když v tom programu je int tak běží asi 7x rychleji než s longem
13:42 yaqwsx Oukej, to je zajímavé.
13:42 yaqwsx mornfall: U mě je patch, který integruje VFS do DiOSu. Teď jdu sehnat něco na jídlo, pak bych se rád pobavil o monitorech - budeš mít chvíli?
14:21 yaqwsx mornfall: Abych si udělal jasno - monitor vnímám jako funkci, kterou si uživatel zaregistruje syscallem nebo přilartuje (možná lepší). Tato funkce by měla mít prototyp void f( __dios::Context ) a bude spouštěna při každém reschedulu. Flagy a další věci si bude předpokládám nastavovat sama přímo pomocí hypercallů.
14:23 xstill_ yaqwsx: mornfall se nám někam ztratil, ale mě to v principu příjde OK, (akorát si nejsem jistý, co myslíš při každém reschedule, asi mi dává větší smysl to pouštět než se scheduler vrátí)
14:24 yaqwsx xstill_: Tak jsem to myslel.
14:25 yaqwsx Přemýšlím, jesti má ale smysl mít monotr, který si drží stav.
14:25 yaqwsx A jestli přidávání monitorů za běhu nebude přinášet velký overhead
14:26 xstill_ monitor musí mít stav, pro LTL potřebuješ minimálně stav automatu
14:26 mornfall yaqwsx: už jsem tu
14:28 xstill_ otázka je, jestli bude stačit jeden monitor, nebo chceme umět i víc. Pokud jeden, tak by se to asi dalo udělat tak, že si zvětší stav a zapíše si svůj stav na konec (jestli je stav jen pole pointerů)
14:28 yaqwsx xstill_: Dává mi smysl více monitorů
14:30 xstill_ tam je otázka jak si ten monitor má zapamatovat, kde má stav aniž by na to potřeboval stav
14:35 yaqwsx Pokud by jsi monitory přilartovával, tak to asi není takový problém.
14:35 mornfall no úplná výhra to není ani tak
14:36 mornfall hlavně asi chceš aby si monitor mohl napsat obyčejnej smrtelník :-)
14:37 yaqwsx Ok, měl jsem na mysli, že monitor je něco jako struct MyMonitor { void monitor( const Context& );};
14:37 mornfall no tak se toho nebojme a udělejme tomu interface a linked list monitorů :-)
14:37 yaqwsx Ok, dobře. BTW: Potřebujeme linked list?
14:38 mornfall tak je to asi nejjednodušší ne?
14:38 yaqwsx Jo, už vidím proč linked list.
14:38 mornfall struct Monitor { virtual step() = 0; Monitor *next = nullptr; };
14:39 yaqwsx To vypadá nejrozumněji.
14:39 mornfall případně final run() { step(); if ( next ) next->run(); } nebo něco
14:40 mornfall a scheduler pak udělá if ( monitor ) monitor->run()
14:40 yaqwsx To se mi líbí.
14:52 yaqwsx Jedna věc: Jak si bude uživatel monitory přidávat? Je to C++ objekt, který v Cčku nezkonstruuje (pokud by se přidávaly z uživatelského programu)
14:54 xstill_ myslím, že chtít po uživateli aby pochopil C++ na úrovni jedné struktury s metodou step můžeme
14:54 yaqwsx O to mi nejde. Ale někde bude muset zavolat C++ API diosu. A to z Cčkového zdrojáku neudělá (např. aby v mainu přidal monitor)
14:55 mornfall yaqwsx: až ti to začne vadit, tak lehce stvoříš C API k tomu
14:56 yaqwsx mornfall: Dobře
14:57 mornfall CMonitor : Monitor { void *state; void (*_step)( void * ); step() { _step( state ); } }; extern "C" make_monitor( ... ) // dál už to určitě vymyslíš ;-)
14:57 yaqwsx Jop, beru.
15:05 yaqwsx Ale i tak. Abych mohl implementovat register_monitor, tak to musím implementovat jako syscall (abych se dostal k monitoru). Jenže to mi rozbije syscally v Cčkových programech (budu mít mezi syscally něco, co bere C++ strukturu). A předávat se mi to do syscallu jako void * moc nechce....
15:07 mornfall nepřijde to do syscallu beztak jako va_list?
15:07 xstill_ cčková funkce to může brát jako void * a hotovo
15:07 yaqwsx Problém je u generování syscallů z tabulky.
15:08 xstill_ cčková funkce = ten syscall wrapper
15:08 xstill_ až v kernelu si z toho vybereš Monitor *
15:09 yaqwsx Je to nejjednodušší, ale moc se mi to nelíbí.
15:10 mornfall yaqwsx: druhá možnost je #ifndef __cplusplus struct Monitor; #endif
15:10 mornfall teda _DiOS_Monitor nebo co
15:11 mornfall jinak typedef __dios::Monitor _DiOS_Monitor;
15:11 mornfall (tzn. __cplusplus)
15:11 xstill_ pravda, může to být opaque objekt
15:11 mornfall a extern "C" _DiOS_Monitor *make_monitor( ... )
16:36 mornfall yaqwsx: rozbil jsi testy
16:36 mornfall dokonce vlastní, test/dios/internal/sorted-storage-a.2.cpp:2:10: fatal error: 'dios/scheduling.hpp' file not found
16:59 divine-buildbot Hey! build divine-next-debug #344 is complete: Failure [finished]
17:34 divine-buildbot Hey! build divine-next-debug #347 is complete: Failure [finished]
18:21 divine-buildbot Hey! build divine-next-debug #345 is complete: Failure [finished]
18:32 yaqwsx Mám ammendnout?
18:32 yaqwsx A já si říkal, jestlimám nechat proběhnout všechny testy nebo polovina vypadá dobře.
18:33 mornfall yaqwsx: už jsem to asi opravil
18:33 mornfall yaqwsx: pak to zarecorduju
18:35 yaqwsx Ok
18:51 divine-buildbot Hey! build divine-next-debug #346 is complete: Failure [finished]
19:25 divine-buildbot Hey! build divine-next-debug #351 is complete: Failure [finished]
20:46 divine-buildbot Hey! build divine-next-debug #348 is complete: Failure [finished]
21:22 divine-buildbot Hey! build divine-next-debug #349 is complete: Failure [finished]
21:41 divine-buildbot Hey! build divine-next-debug #350 is complete: Failure [finished]
22:10 divine-buildbot Hey! build divine-next-debug #352 is complete: Failure [finished]
23:26 divine-buildbot Hey! build divine-next-debug #353 is complete: Success [finished]
23:40 yaqwsx mornfall: Kdy se teď děje interrupt? Jak moc máme dobrou tau redukci?
23:40 yaqwsx Jde mi o psaní testů pro monitory

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