Vlákno názorů k článku HelenOS nikdy nebude dokončený, říká jeho autor Jakub Jermář od JaGa - Pěkný rozhovor. Jen mě zaujalo: ,,Když havaruje VFS, tak je...
-
A co takhle ten havarovaný modul zresetovat?
Ano, tohle je něco, co třeba lidé kolem MINIXu uvádějí jako univerzální všelék a opakují to téměř jako svou mantru :)
Samozřejmě restart spadlého serveru může krátkodobě pomoci, ale problém to ve skutečnosti neodstraní. Pokud je třeba ve VFS serveru nějaká chyba nebo neošetřený stav, tak je velmi pravděpodobné, že se po restartu projeví znovu — dříve či později.
V současné době v HelenOSu tedy spadlé servery nerestartujeme, i když jsme o tom už párkrát uvažovali alespoň jako o jakémsi prostředku poslední záchrany (potřebovali bychom k tomu zřejmě nějaký session manager, který zatím nemáme).
Chceme, aby VFS ani jiný esenciálně důležitý systémový server prostě nepadal, a toho se snažíme dosáhnout jak kvalitním kódem a správným "softwarově-inženýrským" přístupem, tak různými pokusy o formální verifikaci správnosti kódu.
-
Stav asi před rokem jsem popsal v tomto článku:
Martin Děcký: A Road to a Formally Verified General-Purpose Operating System, in Proceeding of the 1st International Symposium on Architecting Critical Systems (federated with CompArch 2010), LNCS 6150, Jun 2010
Aktuálně pracujeme na dvou dalších článcích s konkrétními výsledky. Vše je samozřejmě stále work-in-progress, ostatně jako celý HelenOS :)
-
M (neregistrovaný)
Největší problém je např. selhání komunikace se záznamovým HW, u kterého se kvůli poruše zařízení nebo rušení komunikační cesty prodlouží doba odezvy nebo sníží rychlost komunikace (zmetek USB kabel), uvolnění konektoru (častý případ u SATA a eSATA), rušení komunikace bezdrátovým vysílačem (WIFI, kabely (někdo přiskřípl kabel nebo ho přejel kolečkovou židlí),.. ).
To není dodnes ošetřené ani na Windows, ani na Linuxu, ani na MacOS,...
Řeší to jen tím, že když vyprší timeout, tak to zkusí znovu, třeba ještě párkrát a pak konec a data jsou nepřístupná, ty co se měly uložit většinou ztracená, program co je ukládal přestane komunikovat s OS a ten ho na timeout ukončí nebo dokonce spadne VFS nebo více částí OS apod.
Přitom uživatele vůbec neupozorní, že došlo k problému s komunikací se zařízením XY, nezeptají se zařízení na jeho aktuální SMART stav, nebo že došlo ke snížení přenosové rychlosti kvůli chybám a tak se začaly přenosy opakovat, ..
a nevypíšou ten stav a tu chybu na obrozaovku se zvýrazněním překročených nebo chybných parametrů.A uživatel marně čeká co se bude dít a doufá, že se to snad rozběhne, že jen nějakej proces zrovna zaměstnal víc procesor,...
Pak nastane chvíle, kdy na to zařízení má zapsat jinej proces nebo dokonce přímo z OS a výtuh a nebo zas jen zpomalené reakce.Uživatel po dlouhém čekání zvolí restart, a musí jak inspektor procházet logy co se stalo a když se ani ty logy neuložily, tak je nahranej a detektivka začíná. Přitom by stačilo napsat na obrazovku srozumitelnou řečí co se děje, proč se reakce systému zpomalily, co nastalo za chybu, případně to zkusit i odeslat třeba po síti nebo uložit na jinej HW v lokálním počítači nebo v síti(parametry serveru na chyby by byly přednastavené a uložené v paměti už od načítání OS),...
-
belzebub (neregistrovaný)
Obavam se ze pokud bude projekt psan v C/C++, tak "pokusy o formalni verifikaci spravnosti kodu" zustanou jenom pokusy.. (za predpokladu ze neplacam blbosti a stale pouzivate C/C++)
Neuvazovali jste treba o nejakem kulturnejsim (rekneme funkcionalnim) jazyku?
Osobne jsem presvedcen ze pokud je cilem spolehlivost a stabilita, funkcionalnim jazykum se nic nevyrovna
-
Obavam se ze pokud bude projekt psan v C/C++, tak "pokusy o formalni verifikaci spravnosti kodu" zustanou jenom pokusy
Problém není v programovacím jazyku, ale v množství abstrakce a sémantické informace, která je v kódu nějak implicitně nebo explicitně obsažena. Souhlasim, že lze asi s jistou básnickou licencí obecně říci, že Java se verifikuje snadněji než C a funkcionální jazyky se verifikuji snadnějí než imperativní jazyky, ale v praxi jde vždy o to, jaké vlastnosti a jakým způsobem chcete verifikovat, jak se poperete s nerozhodnutelností a state space explosion apod.
Nástroje pro formální verifikaci céčka existuji, např. Frama-C, VCC.
Neuvazovali jste treba o nejakem kulturnejsim (rekneme funkcionalnim) jazyku?
Nevidím na céčku nic nekulturního. Každý programovací jazyk lze používat kulturním i nekulturním způsobem.
Ovšem budoucímu použití nějakého funkcionálního jazyka nebo alespoň imperativního jazyka s funkcionálními prvky (typu Groovy) se rozhodně nebráníme. Až budeme umět chodit, můžeme se učit běhat :)
-
BostX (neregistrovaný)
Opakovane mam dojem ze ludia nechapu co je to 'reset' naco je to dobre a ako by to malo fungovat. Komplexne zariadenia a mechanizmy (ako napr. software) vzdy obsajuhu chyby, t.j padali, padaju a budu padat. Formalna verifikacia nezastavi tsunami co sa ruti na moj pocitac! To co pri operacnom systeme potrebujem je rychle a lacne error recovery, 100% formalna verifikacia je zbytocna.
Je _uplne_ jedno ci cakam 1 minutu na znovu-nacitanie konfiguracneho suboru (nap. defaultne nastavenie JBoss-su) a nasledne start/stop-nem databazovy sever, alebo ci rychlo vypnem/zapnem poistky. -
azmod (neregistrovaný)
nemate pravdu a vasa predstava je na urovni uzivatelskeho pohladu (nic v zlom)
ale pozrite si situaciu kedy si restart nemozete dovolit - napriklad pri riadeni kritickych systemov - tam pravidelny restart ala windows nieje jednoducho mozny a je nutna verifikacia - napriklad ak vase komponenty su vzajomne zavisle a maju zlozity vnutorny stav.
ČLÁNKY DO MAILU