A NICTA bejelentette a világ első, formális módszerekkel igazolt, általános célú kernelét

Kernel

A NICTA a napokban kutatási áttörésként jellemezte azt, hogy a világon elsőként befejezte egy általános célú operációs rendszer kernel géppel, formális módszerekkel igazolt, teljes ellenőrzését.

A Secure Embedded L4 (seL4) mikrokernelt valós felhasználási körülmények közé szánják, olyan helyekre - pl. repülőgépek, autók biztonsági berendezéseibe, védelmi megoldásokba -, ahol a beágyazott rendszerekben való hibamentes működés kritikus fontosságú.

seL4 mikrokernel
seL4 mikrokernel komplexitás¹

Lawrence C Paulson, a Cambridge Egyetem számítógépes laborjának számítási logikával foglalkozó egységének professzora elmondta, hogy az elért eredményeket nehéz közhelyek nélkül kommentálni, hiszen egy operációs rendszer kernelét alkotó 7 500 sornyi C forráskód helyességét igazolni egyedülálló teljesítménynek számít. A munka eredményeképpen pedig egy olyan megbízhatóságot kapnak a szoftvertől, amely eddig elképzelhetetlen volt.

Dr. Gerwin Klein - a NICTA vezető kutatója - elmondta, hogy kisebb kernelek meghatározott tulajdonságaira már történtek formális módszerekkel igazolt ellenőrzések, de olyan ellenőrzések, amelyeket ők végeztek, még soha, semmikor sem történtek ilyen méretű és bonyolultságú, valós felhasználásra szánt, nagy teljesítményű szoftveren.

Klein szerint az ellenőrzés azt is kimutatta, hogy számos ismert támadással szemben immunis a seL4 mikrokernel. Ilyen támadás például a puffer túlcsordulásos (buffer overflow) támadás.

A bejelentés 4 évnyi kutatás eredménye.

A bejelentés itt olvasható. A FAQ-ból kiderül, hogy a seL4 (ellenőrizetlen) x86-os portja már képes egy paravirtualizált Linux verzió futtatására. Tervebe van véve a Linux portolása a seL4 ellenőrzött ARM11 portjára.

¹ A seL4 mikrokernel. A kernel C függvényeit jelölik a pontok. Ha "A" függvény meghívja "B" függvényt, akkor "A"-ból "B"-be egy nyíl mutat. Az ábrából jól látható, hogy a seL4 komplex szoftver, szorosan összefüggő részekkel. A kép 2009 elején készült. A zöld pontok jelzik azokat a C függvényeket, amelyek akkor már átestek az ellenőrzésen.

( profeta | 2009. 08. 16., v – 18:38 )

7500 sor? Nem lesz az egy kicsit kevés?
Amúgy a formális helyességbizonyítás annyit igazol, hogy a szoftver megfelel a specifikációnak. A specifikáció ellen nem véd.

Igen, ezt le is írják itt:

"A cynic might say: proofs like this only show that every fault in the specification has been precisely implemented in C."

De azt is leírják, hogy szerintük miért van mégis értéke a munkának és hogy ez csak a kezdet. De ez kell ahhoz, hogy tovább léphessenek (ellenőrzött alkalmazások).

Mindenképpen érdekes viszont, hogy ha elfogadjuk a feltételezéseket, akkor az ellenőrzés implikálja, hogy egy rakás programozási hibától mentes a kernel:

* Buffer overflows: buffer overflows are a classic security attack against operating systems, trying to make the software crash or even to inject malicious code into the cycle. We have proved that no such attack can be successful on seL4.
* Null pointer dereferences: null pointer dereferences are another common issue in the C programming language. In applications they tend to lead to strange error messages and lost data. In operating systems they will usually crash the whole system. They do not occur in seL4.
* Pointer errors in general: in C it is possible to accidentally use a pointer to the wrong type of data. This is a common programming error. It does not happen in the seL4 kernel.
* Memory leaks: memory leaks occur when memory is requested, but never given back. The other direction is even worse: memory could be given back, even though it is still in use. Neither of these can happen in seL4.
* Arithmetic overflows and exceptions: humans and mathematics usually have a concept of numbers that can be arbitrarily big. Machines do not, they need to fit them into memory, usually into 32 or 64 bits worth of storage. Machines also generate exceptions when you attempt to do things that are undefined like dividing by zero. In the OS, such exceptions would typically crash the machine. This does not occur in seL4.

--
trey @ gépház

Szerintem egy monolitikus kernelre ezt eselytelen szinte megcsinalni, foleg annak merete miatt. A mikorkernel lehet eleg egyszeru ahhoz, hogy ezt meg lehet jatszani (az mas kerdes, hogy egy mikorkernel eseten ez csak a jeghegy csucsa, mert a felette futo dolgok meg mindig lehetnek kerdesesek, mikrokernel csak magaban sok mindenre nem jo ugye).

csak az utolsó részre ment a válasz, erre "mikrokernel csak magaban sok mindenre nem jo ugye".
mivel pl van már rá L4linux, mégiscsak jó sok mindenre:) ráadásul egy tökéletes L4 felett működő hibáktól hemzsegő linuxok így is jobbak, mint egy szimpla monolitikus linux a puszta vason;)

azt irjak a programot megirtak haskell-ben is, ebbol a programbol automatikusan gyartottak a low-level specifikaciot, majd bebizonyitottak, hogy a c program megfelel ennek a specifikacionak. gondolom ebben a lepesben szurtek ki ezeknek a hibaknak egy nagy reszet - de kerem javitson ki aki jobban tudja ezt. na most ez akkor csak ugy lehet, hogy haskellben nem lehet ilyen hibakat veteni, tehat egy csomo erofeszitest megsporoltak volna ha a haskelles cuccot hasznaljak es nem is faradnak a c verzioval - tehat gyakorlatilag itt a munka lenyegi resze a manualis haskell->c konverzio es annak helyessegenek a bizonyitasa volt (amire mondjuk jobban belegondolva valoszinuleg tenyleg szukseg volt mert a haskell fordito bizonyara sokkal szarabb kodot gyart mint egy jo c programozo).

- Use the Source Luke ! -

na most ez akkor csak ugy lehet, hogy haskellben nem lehet ilyen hibakat veteni,

tevedtem. ugy tunik a haskell kodban emulaltak a pointereket is, es bebizonyitottak - ugyanugy mint azt, hogy az absztrakt specifikacionak megfelel a haskell modell - hogy nincs null pointer dereference, stb.

- Use the Source Luke ! -

Persze, rengeteg hibát ki lehet így szűrni, és megbízhatóbb szoftver születik. A cinizmus annak szólt, hogy ez a módszer meglehetősen régi, és azért nem alkalmazzák mert baromi hosszadalmas, és nem garancia semmire.
Az előnye az, hogy rákényszerít a dolgok végiggondolására. Ami mondjuk előrelépés lenne, ha írtak volna egy programot, ami segíti a specifikálást és a bizonyitást.
De ha már egyszer kötözködés, akkor kicsit még ragozzuk. (Nem biztos hogy jól tudom, a kutatási eredményeket nem ismerem)
1, A módszer csak struktúrált programozási nyelvekre működik (gondolom ki lehet terjeszteni, de az egy nehezebb probléma)
2, A helyességbizonyítás nem mond semmit a teljesítményről, és a memóriafogyasztásról. Mind a két dolog használhatatlanná tehet egy oprendszert.
3, Szerintem arra nincs módszer hogy általános esetben egy többszálú alkalmazásról belássuk, hogy soha nem fog deadlock-ot, vagy egyéb párhuzamos szoftvernél előforduló betegséget kapni. Ha egyszálú, akkor persze nincs ilyen gond, de az egy oprendszernél elég primitív megoldás.

"A módszer csak struktúrált programozási nyelvekre működik"
Mi másra szeretnéd még? (Funkcionális nyelvekre még automatikus bizonyító rendszer is létezik, gondolom ezért írták haskellben.)

"A helyességbizonyítás nem mond semmit a teljesítményről, és a memóriafogyasztásról."
Attól függ, mi van a specifikációban. :) Egyébként valószínűleg ezt is szem előtt tartották.

"Szerintem arra nincs módszer hogy általános esetben egy többszálú alkalmazásról belássuk, hogy soha nem fog deadlock-ot, vagy egyéb párhuzamos szoftvernél előforduló betegséget kapni."
De van rá módszer. De csakúgy mint programozni, helyességet bizonyítani is hatványozottan nehezebb mint egyszálú programnál.

"...handing C++ to the average programmer seems roughly comparable to handing a loaded .45 to a chimpanzee."
-- Ted Ts'o

"Mi másra szeretnéd még? (Funkcionális nyelvekre még automatikus bizonyító rendszer is létezik, gondolom ezért írták haskellben.)"
Mondjuk objektum-orientáltra, de tényleg lényegtelen.

"A helyességbizonyítás nem mond semmit a teljesítményről, és a memóriafogyasztásról.
Attól függ, mi van a specifikációban. :) Egyébként valószínűleg ezt is szem előtt tartották."
Nyilván, csak az külön tudomány, nem része a helyességbizonyításnak.

"Szerintem arra nincs módszer hogy általános esetben egy többszálú alkalmazásról belássuk, hogy soha nem fog deadlock-ot, vagy egyéb párhuzamos szoftvernél előforduló betegséget kapni.
De van rá módszer. De csakúgy mint programozni, helyességet bizonyítani is hatványozottan nehezebb mint egyszálú programnál."
Tényleg nem kötözködni akarok, de áruld már el a módszer nevét, vagy adj egy linket ...

Ennyire nem durva a dolog, az olyan utasításpárokra, melyek nem tartalmaznak közös változót, nem kell ellenőrizni. :)

Egyébként de, exponenciális. De hát ez a párhuzamos programozás már csak ilyen...

"...handing C++ to the average programmer seems roughly comparable to handing a loaded .45 to a chimpanzee."
-- Ted Ts'o

"Mondjuk objektum-orientáltra, de tényleg lényegtelen."
Arra is van...

"Tényleg nem kötözködni akarok, de áruld már el a módszer nevét, vagy adj egy linket ..."
De azt akarsz, de annyi baj legyen. :)
Magyarul itt olvashatsz módszerekről, mindhárom esetre: strukturált, objektum orientált, és párhuzamos programok.

"...handing C++ to the average programmer seems roughly comparable to handing a loaded .45 to a chimpanzee."
-- Ted Ts'o

Nade nem is azt írják, hogy egy teljes értékű rendszert futtatni képes kernelről lenne szó. Arról beszélnek, hogy hypervisora lehet mondjuk egy Linux-nak.

Üdv,
Dw.

"Jegyezze fel a vádhoz - utasította Metcalf őrnagy a tizedest, aki tudott gyorsírni. - Tiszteletlenül beszélt a feljebbvalójával, amikor nem pofázott közbe."

( Arbiter | 2009. 08. 16., v – 19:18 )

Ez nemcsak azért jó, mert a kernel bizonyos támadásokkal szemben jobban lesz védve, hanem talán kevesebb rosszul megtervezett program íródik majd rá.

Akárki akármit is mond, első lépésnek nagyon szép munka!

:) Igen, ez jó kérdés. Eszembe jutott egy ide illő sztori:

A Mercedesnek volt pár éve olyan gondja, hogy szoftverhiba miatt a vészfékező rendszer néha hibásan nem vette észre, hogy a kocsi előtt a ködben akadály van. Ha ha jól emlékszem pont a német Autobild munkatársa rongyolta össze emiatt az egyik tesztautót, amikor be akarták neki mutatni, hogy a tuti elektronika majd milyen szépen megállítja a kocsit, mert érzékeli a gépjármű előtti akadályt.

Nem. Abban az esetben tudták, hogy a rendszer nem képes teljesíteni azt, amit reklámoztak. Az Autobild (vagy nem tudom, micsoda) munkatársa meg azért törte össze a kocsit, mert a lécet, ami azt jelezte, hol kezdje a fékezést, valaki nem jó helyre tette le.

Egyébként azt mondták, hogy nyílt úton jól működne a rendszer, csak a promóciós kampányban a tesztet valami csarnokban végezték, és állítólag a csarnok fémszerkezete zavarta a radart... persze persze :-)

G

A furcsa jogi szabályozás miatt ilyen vészfékező rendszert nem építenek be az autógyártók. Ti. ha mégsem veszi az akadályt, akkor a vevő beperelheti az autógyártót. Ehelyett a rendszert úgy állítják be, hogy csak minimális ütközés következzen be, pl. lökhárító sérül maximum.

Nem értem pontosan mire gondolsz, de egyébként beépítenek. Az igaz, hogy a jogi szabályozás miatt nem lehet akármit, de azt a gondolatmanetet kell követni, hogy "a júzer helyett nem lehet vezetni". Elég komoly felelősségmegosztási hercehurcának tenné ki magát a gyártó, ha nem így tenne. Tehát, ha a júzer neki akar menni valaminek, akkor neki is fog. De nem mindegy hogyan.
Alapvetően két szituációt különböztethetünk meg:
1) veszélyhelyzet, de a baleset még elkerülhető:
a vezető figyelmeztetésétől kezdve a fékrendszer előkészítésén át, a csökkentett fékerővel megkezdett (önálló) fékezésig, ill. az ESP-vel/kormányzással történő korrigálásig (ha a vezető egyébként kitérő manőverbe kezdett).
2) a baleset már biztosan nem kerülhető el:
Ilyenkor minden mindegy alapon az autó átveheti bizonyos részrendszerek teljes irányítását, pl. teljesen "bele fog állni" a fékbe, ha a júzer ezt magától nem tenné meg. Ezen túl felkészíti a passzív biztonsági rendszereket: felhúzza az ablakokat, megfeszíti az öveket és igyekszik a meglehetősen puha humanoidokat olyan helyzetbe állítani, hogy a sérülésveszély lehetőleg minimális legyen.

Tehát, ha a júzer neki akar menni valaminek, akkor neki is fog. De nem mindegy hogyan.

Igen, arra gondoltam, hogy például ráfutásos baleset esetén, ha a vezető nem lép a fékre, akkor mindenféleképpen neki fog az előtte lévőnek. És ez nem technikai okok miatt van így, hanem az autógyártók nem vállalják a felelősséget, hogy az autó döntsön helyettünk.

És ezt meg tudja biztonságosan oldani a mai technológia? Kötve hiszem. Az európai utak nem olyan szögletesek, mint az amerikaiak. Bármikor történhet olyan eset, hogy a sofőr többet tudott a szituációról, mint a szenzorok és mégis el tudta volna kerülni az ütközést vagy úgy korrigálni, hogy kisebb legyen a kár (pl. az úttest megfelelő elhagyásával egy közeli földútra. Belehajt a bokrokba, amiket ismer és tudja, hogy nincs mögöttük fa vagy más veszély, azok lelassítják a kocsit és csak gittelni meg lakkozni kell. Mindaddig, amíg 1000 esetből egyben is jobban dönthet az ember, nagyon sokan elutasítják majd ezt az automatikát. Magamnak sokkal könnyebben megbocsátok olyan hibát, amiért egy helyettem rosszul döntő gépet örökre bezúzok. Ez van, tekerje a kormányt valaki más autójában a robot.
De mi köze is ennek egy mikrokernelhez?

Háát, ez nagyon naiv megközelítés :)
Itt az utolsó méterekről van szó. Itt már az automatika jobb mint _akármelyik_ ember. Arról van szó, hogy az ütközés _elkerülhetetlen_. Ennek a becslése is nyilván megfelelő biztonsági tartalékkal történik, tehát ott már nincs olyan, hogy "kisebb lesz a kár". Tudod, point of no return. Amúgymeg értem én, hogy itt kőkemény Schumacherek vannak, akik a fizika törvényei felett állnak, csak aztán nehogy kiderüljön, hogy egy ilyen esetben ők is csak becsukják a szemüket, elengedik a kormányt és sikítanak :P

Van, akinek volt már olyan balesete, ahol a technika mentette meg és van akinek még nem. Ez utóbbi csoportba tartozók szólnak fennen a technika ellen. De ez csak addig tart, amíg át nem kerülnek az első csoportba. Onnantól kezdve mély a csend.

Ave, Saabi.
(igen, engem már mentett meg az ABS)

mi köze is ennek egy mikrokernelhez?

lássunk egy példát. autó központi fedélzeti számítógép, monolitikus kernellel:)

#riasztás!
#riasztás!
#riasztás!
%kuss má! nem találok egy fájlt.
#riasztás!
#riasztás!
%picsába már, hogy nem áll be a szád! pedig itt kell lennie annak fájlnak valahol...
#RIASZTÁS! RIASZTÁS! RIASZTÁS!!!!!
%azt hiszem fájlrendszer ellenőrzést kell végeznem.
%na végre megvan a keresett fájl!
%mit is mondtál?
....
%ja megvan, riasztás volt valamiért.
%már megálltunk? khmm hmmm...
%gépkocsiban esett károk felmérése...
%keresem a kárfelmérést végző fájlt

általános célúnak még csak véletlenül sem neveznék egy olyan rendszert/kernelét, amelyre csak más pl windows vagy linux rendszeren lehet egyáltalán fejleszteni.
ilyen erővel lehet akár közvetlenül a vasra is fejleszteni az alkalmazást, memóriakezeléssel, perifériakezeléssel, fájlrendszerkezeléssel ha lesz benne olyan stb. csak több munkával jár.
a µkernel alapú rendszerek, alkalmasak lennének akár desktop/workstation akár server rendszernek is. Symbian, Qnx, fooTron stb rendszereknél, láthattunk is példát erre a múltban. az más kérdés, hogy a piac más termékekbe tereli őket, és természetesen a fejlesztések is ebbe az irányba történnek.
Vxworksből nem várható desktop, ws, vagy server rendszer a jövőben. jellemzően egy feladatot látnak el ezzel a rendszerrel működtetett eszközök, illetve gyárilag fejlesztve és beállítva pontosan meghatározott számú alkalmazás mehet rajtuk. nem véletlenül.

varjal te most ugy gondolod, hogy a kozponti fedelzeti szamitogep, amin pl. a belso homersekletet allitgatod (es amin esetleg a definiciod szerint altalanos celu os fut), hoz biztonsagkritikus donteseket egy beagyazott relative egyszeru nem altalanos celu os-t futtato ECU helyett?

- Use the Source Luke ! -

a mikrokernel tudtommal azert jo realtime OS-nek, mert a drivereket stb. is konnyen megtudja szakitani a fontosabb dologgal. akarcsak egy preemtable linux kernel. ezert nem ertem miert lenne elvi akadalya egy real-time monolitikus OS-nek - ami letezik is - vagy egy altalanos celu real-time monolitikus OS-nek - amit valahogy te kevertel ide, es amelynek kapcsan erdekelne, hogy egyaltalan milyen real-time altalanos celu OS-ek vannak, mert se monolitikus (RTLinux?) se microkerneles (QNX?) nem hiszem, hogy sok lenne.

- Use the Source Luke ! -

> A tananyagban (is) a mikrokernel kovetelmenyei cimszo alatt.

Értem. Akkor meséld el légyszi, hogy mi történik, ha egy mikrokernel nem teljesíti az alapfeltételt, mert nem fér be teljes egészében az L1-be. Elveszik tőle a mikrokernel megnevezést? Ezentúl makrokernelnek kell majd hívni, vagy mi?

az hogy eppen befer nem hiszem, hogy eleg lesz, leven az applikacionak is futnia kell es az is az L1 cachebe toltodik (es akkor bizony kitorlodik onnan a kernel amit aztan vissza kell tolteni) - sokkal kisebbnek kell lennie mint az L1 cache. viszont egy monolitikus kernel gyakran futo reszei miert ne lehetnenek ugyanugy megfeleloen kicsik mint a microkernel eseteben?

- Use the Source Luke ! -

Szép elvárás, csak ez bőven kevés ahhoz, hogy az L1 cache-ben is maradjon.

Egyébként is fenntartásokkal kezelek minden olyan spekulációt, mely garantálni akarja nekem, hogy a kernel az L1-ben marad egy mai processzoron (2-4-way asszociativitás, heurisztikák, out-of-order, stb.)

Illetve szerintem az még egy real-time kernel esetébn is régen rossz, ha a kernel maga foglalja el a futásidő nagyobb hányadát. Ha meg nem így van, miért is maradna az L1-ben?

"...handing C++ to the average programmer seems roughly comparable to handing a loaded .45 to a chimpanzee."
-- Ted Ts'o

Egyébként is fenntartásokkal kezelek minden olyan spekulációt, mely garantálni akarja nekem, hogy a kernel az L1-ben marad egy mai processzoron (2-4-way asszociativitás, heurisztikák, out-of-order, stb.)

Nem tudja garantalni semmi ha nincs hozza a hardverben tamogatas, de nem is feltetel, h ott maradjon. De ha jobban belegondolsz, a mikrokernel azon resze amire ez fent all, eleg surun jut szohoz (foleg a multitasking/megszakitas kezeles/etc miatt) ahhoz, h nagyjabol az L1/L2/L3-ban elje le az eletet.

---
pontscho / fresh!mindworkz

Nem tudja garantalni semmi ha nincs hozza a hardverben tamogatas

milyen hardverben van ilyen tamogatas? komolyan erdekelne, mert csak olyanrol hallottam eddig, hogy invaldialni/flusholni lehet a cache-t, meg meg lehet mondani, hogy valami ne keruljon be a cachebe - de ilyenrol, hogy valami maradjon az L1 cacheban meg nem.

- Use the Source Luke ! -

ez a feladattól függ. egy csillogó flash weblapot lehetséges, hogy jobban el tud készíteni, egy olyan autodidakta, akinek nagy gyakorlata van ebben. kernelekkel és azok fejlesztésénél viszont jelentős szerepe van annak a háttértudásnak, amit egyetemek sokkal inkább megadnak, mint az önfejlesztés wikipediából linux doksiból howtokból stb. egyébként nem pont erre utaltam, hanem azokra akik csak olvassák a híreket a témában, ebben a kérdésben pedig az fent írt Tanenbaum Torvalds vitára alapozzák a véleményüket. annak is egyfajta leegyszerűsítésére, Linus szerényen magáról elnevezett kernele sokkal elterjedtebb lett mára mint Tanenbaum minixe, ergo monolitikus kernel jobb, és jó minden feladatra.
ahhoz, hogy valaki belássa a µkernel előnyeit szükséges bizonyos alapképzettség. bár a kiindulásul szolgáló vicces példám mindenki számára érthetően emeli ki a különbség lényegét. legalábbis ezt feltételeztem. hát mégsem mindenki számára érthető sajnos.

> Linus szerényen magáról elnevezett kernele

Ha nem tudsz valamit, nézz utána nyugodtan: http://en.wikipedia.org/wiki/History_of_Linux#The_name

> ahhoz, hogy valaki belássa a µkernel előnyeit szükséges bizonyos alapképzettség.

Meg a hátrányaihoz is.

> hát mégsem mindenki számára érthető sajnos.

Tán mert troll-stílusban írsz.

bár a kiindulásul szolgáló vicces példám mindenki számára érthetően emeli ki a különbség lényegét. legalábbis ezt feltételeztem. hát mégsem mindenki számára érthető sajnos.

ha nem lennenek preemtable - sok esetben real-time (pl. a mar emlitett microC/OS-II) - monolitikus kernelek akkor igazad lenne. amugy hol szerezted a diplomad, hogy ekkora nagy embernek gondolod magad tole (nekem is van amugy, az ELTE IK-rol - csak a tisztanlatas vegett)?

- Use the Source Luke ! -

nekem ugyanonnan. így neked is tudnod kellene, miért jobbak a µkernelek rt feladatra, általános felhasználású rendszer magjaként.

add össze a precesszeid cpuidő felhasználását, akkor ha pl a kernel el van foglalva pl a fájlrendszerrel. nem fog kijönni a 100%, az idlevel együtt. a rendszer a saját kernelének a procidőfogyasztását nem látja, és nem is számolhat vele. az rt feltétele, hogy egy folyamat/számítás eredményei adott időre rendelkezésre álljanak. egy rendszer tervezésekor számolni kell a cpu számítási kapacitásával is természetesen, az adott folyamat nem igényelhet nagyobb számítási kapacitást. mivel a számítási folyamat egy szoftveres környezet keretei között működik, számolni kell ennek a szoftveres környezetnek a saját számítási szükségletével, azaz cpu igényével. hasonló probléma a fizikában az, hogy egy mérési folyamatban részt vesznek maguk a mérőeszközök is, így azokat is számításba kell venni.
általános feladat esetében egy folyamatot nem szokás kernel szinten kezelni. a kernelek eddig a saját cpu fogyasztásukat nem tudják szabályozni, így egy komplex, sok feladatot ellátó nagy kernel esetében nem garantálható, hogy ne vegye el a szükséges számítási kapacitást egy rt folyamattól. ha a kernel a lehető legkisebb, és minden egyéb folyamat felette fut, akkor ennek veszélye kizárható. így nem lehetséges, hogy pl a néha cpu igényes fájlrendszer kezelés/javítás elvegye a szükséges cpu időt egy rt feladattól.
a hardver jó ideje fejlődésben lelépi a szoftvereket, így mára már sok feladatra nagyságrendnyivel több számítási kapacitás áll rendelkezésre a szükségesnél. pláne, ha ismert rt feladatra terveznek egy komplett rendszert, fel lehet készíteni az adott folyamat kernel szintű támogatására, amivel egy monolitikus rendszer is RT képességekkel bír. most elég sok munkájába kerül a linux fejlesztőknek, hogy közvetlen gsm/3G/mobil támogatás kapjon. nagy szövetségek jöttek létre erre mostanában neves szereplőkkel. a mobil kommunikációs hardver vezérlése rt igényű feladat. kernel szinten lesz megoldva természetesen. egyébként is driver terület, de userspace szinten gnu/linuxon nem lehetne megbízhatóan megoldani.
ha az rt folyamat sokkal, nagyságrendnyivel kisebb számítási kapacitást igényel, mint a rendelkezésre álló cpu/cpuk kapacitása, akkor kerneltámogatás nélkül is megoldható monolitikus kernel mellett is, hogy rendelkezésre álljon minden eredmény adott időre, mert "bőven van idő rá".

végül annyit tennék hozzá, nem a linuxot vagy a fosst általában kívántam "fikázni". egyszerűen vannak feladatok, amikre nem egy monolitikus kernel alapú rendszer az ideális. imho érzelmi szálakat kavar még ma is a témába az egykori linux minix vita.
volt példa sikeres µkerneles unixokra is, pl a jó öreg Digital Unix a Mach µkernellel.
a µkernel hátránya egyébként a hagyományos szerver szolgáltatások esetében tapasztalható rosszabb teljesítmény monolitikus társaihoz képest. nem meglepő, hogy a linux sikerében pont ezek játszottak jelentős szerepet.
a 80as években és a 90es elején, a mikroprocesszorok gyakran éppen elégségesek voltak a szükséges feladatok elvégzésére, ezért nagyobb volt a jelentősége a µkerneleknek, és a mainál inkább felszínen volt tartva a téma.

kossz a kimerito valaszt.
elgondolkodtam azon amit irtal es szerintem igazad van (halleluja :) ). az en ertelmezeseben (amit nem az ujjambol szoptam, hanem tobbek kozott innen, 4.7 es 3.6 pont) arra celzol, hogy az a problema, hogy egy preemtable monolitikus kernelben a driverek barhol letilthatjak az interruptokat meg a preemption-t, tovabba a preemption pointok is relative ritkan vannak, es ez nem tesz jot a real-time latencynek. ezzel szemben ha a driverek userspacebeli taskok egy mikrokernel alatt, akkor azok kozott igazsagosabban/jobban tud kapcsolgatni a mikrokernel, mert se az interruptot nem tiltjak le a driverek, se explicit preemption point nem kell mert barhol megszakithatoak (mert ahogy irod, a userspace process-t azt teljesen tudja kontrollalni a kernel, szemben a sajat eroforras felhasznalasaval, lasd elozo mondatom) - es igy a fix alacsony latency sokkal konnyebben garantalhato.

vegulis lehet csinalni monolitikus kernelbol is jo real-time viselkedesut, csak nagyon sok mindenre kell figyelni (egy rossz sor egy rossz driverben hazavag(hat)ja az egeszet), es ez pl. egy altalad emlitett komplex altalanos celu OS eseten mar valoszinuleg lehetetlen feladat (illetve meglatjuk pl. a linux meddig tud eljutni).

végül annyit tennék hozzá, nem a linuxot vagy a fosst általában kívántam "fikázni". egyszerűen vannak feladatok, amikre nem egy monolitikus kernel alapú rendszer az ideális. imho érzelmi szálakat kavar még ma is a témába az egykori linux minix vita.

erzelmileg nem kavart fel a kerdes. persze orulok, hogy nem a linuxot akartad fikazni, de a jogos kritikanak van helye.

- Use the Source Luke ! -

helyreigazitas a torteneszek kedveert akik az archivumot kutatjak:
a microkernel megbizhatosag teren jobb. viszont tisztan realtime szempontbol egy epeszuen megirt realtime monolitikus kernel legalabb olyan jo ha nem jobb tud lenni (ami a preemption pointokat illeti, ez a linuxban letezik, de egy igazi realtime monolitikus kernelben nem szuksegszeru, elvileg szinte barhol preemptalhato lehet az OS ha bizonyos szabalyokat betartva, jol van megirva).
Jo realtime monolitikus kerneleket - de ezek nem altalanos celo OS-ek - a gyakorlatban is sok helyen hasznalnak, pl. olyan kornyezetben is ahol nincsen MMU, igy egy microkernel eleve nem lenne ertelmes alternativa.
Egyebkent a linuxhoz is van realtime patch, PREEMPT_RT neven, ezzel allitolag (es en hiszek nekik) tokeletes hard-realtime viselkedes erheto el - persze ekkor is megmarad a microkernelekkel szemben az a hatrany, hogy egy kernel hiba magaval ranthatja az egesz OS-t.

- Use the Source Luke ! -

de. egyébként központiról. egy vicces példa volt arra, miben más/jobb a µkernel mint a monolitikus, ill az arra épülő rendszer.
nyilván ha egyetlen feladatot ellátó célrendszerről van szó, esetleg nincs is szükség fájlkezelésre. ahogy egyre komplexebbé válnak ezek a rendszerek, felmerül az integráció szükségessége, és egye komolyabb hátrányba kerülnek a monolitikus rendszerek. ahol valódi realtimera van szükség µkernel a megoldás.

a nem igazán megfelelő szó ide az ortogonális, de mind1. amire gondolsz az nem igaz. általános célú kernelről volt szó. ott pedig realtime képességgel csak a µkernel alapú rendszer bír. természetesen hihetetlen mértékben fejlődött az it marketing az utóbbi évtizedekben, pár év múlva egy kiváló pr csapat azt is el fogja tudni hitetni, hogy az ultimate os, a jó öreg DOS:)

tudom jól. csak egy példa, ráadásul vicces példa volt, és az autó ebben teljesen mellékszereplő. ennyi erővel Emmett Brown doki jövőben repülésre állított szürke De Loreanjének központi számítógépét is írhattam volna. de akkor meg a sok bikeshed festő azzal jött volna, hogy az nem is szürke, hanem metál színű:)

"...egy Volvo V70-es ESP-hez szokott tulaja..."

Nem akarom látatlanban minősíteni az ismerősödet, de ha "hozzá volt szokva" az ESP-hez (fogadjuk el, amit írtál), akkor az a "szokott tempó" valószínűleg messze kimerítette a relatív, az abszolút gyorshajtás, ill. az útviszonyoknak nem megfelelő közlekedés fogalomkörét, lévén, hogy normális vezetés mellett alig-alig lehet találkozni az ESP működésével.
Szóval, ha valaki annyira rendszeresen "működteti", hogy "hozzászokik", hááát... ööö... azellen nem véd...

a relatív gyorshajtás = út és látási viszonyoknak nem megfelelő sebességgel haladás.
Az abszolút gyorshajtásról fogalmunk se lehet.

Magát az esetet viszont nem nagyon tudom elképzelni. Egyenes szakaszon hogy kerül valaki az árokba jegesedéstől vagy huppanótól? Esetleg nem tud megállni a jégen, vagy esetleg repül egy kicsit az autó... gondolnám én.

Hacsak nem az volt mondjuk, hogy a huppanó külső fele jegesedett, és a külső kerekek nem tapadtak... bár ha kipörög, akkor meg a belsőre se jut nyomaték, ami kitolhatná a kocsi orrát.
Esetleg belül volt jég, kipörgött a kerék, a csóka ráfékezett, és ABS nélkül csak az egy féloldali kerekek fogtak, és ez térítette el irányból...

Ja, és az ESP és társai nem feltétlenül nagy sebességnél avatkozik közbe, hanem pl. csúszós (váratlanul jeges) úton is.

Egyszer pl. a ladámmal haladtam Székesfehérvárott, és jobb kanyarban azt vettem észre, hogy előttem egy teherautó áll félig a sávomban. Fékeztem, de a két belső kerekem a teherautóból kifolyt valami folyadékon csúszott, mint a fene.
Azt várnám, hogy egy ESP ilyenkor közbelép, és a fékerő szabályzásával egyenesben tartaná az autót.
A Ladát meg nekem kellett a kormánnyal irányban tartani, mert nem akartam a mellettem haladó kamion pótkocsija alá futni oldalról.

G

"Az abszolút gyorshajtásról fogalmunk se lehet."

Annak ellenére, hogy a KRESZ ezt így nem nevesíti, én az adott útszakaszra megengedett sebesség túllépését értettem alatta.

"Ja, és az ESP és társai nem feltétlenül nagy sebességnél avatkozik közbe..."

Ilyet én nem is állítottam, csak azt, hogy az említett esetben valószínűleg a sebesség helytelen megválasztása alaposan benne volt abban, hogy elszállt.

amúgy +1 :)

"Az abszolút gyorshajtásról fogalmunk se lehet."
Annak ellenére, hogy a KRESZ ezt így nem nevesíti, én az adott útszakaszra megengedett sebesség túllépését értettem alatta.

Ez pontosan ezt jelenti. Én csak arra akartam utalni, hogy nem tudjuk, hogy a baleset bekövetkeztekor az adott útszakaszra engedélyezett sebességhatárt túllépte-e, ugyanis ez nem derül ki az eredeti történetből.

A sebesség helytelen megválasztása bizonyára, bár néhány esetben nehéz... pl. ha úgy van jegesedés, hogy erre semmi nem utal korábban.

Sajnos én is törtem már úgy össze autót, hogy több száz kilométer vezetés után sikerült az autópályán egy olyan részre érnem, ahol láthatatlan jégréteg fedte az aszfaltot. Jött a kanyar, én meg csak azt vettem észre, hogy az autó nem követi a kormánymozdulatot...

"Hacsak nem az volt mondjuk, hogy a huppanó külső fele jegesedett, és a külső kerekek nem tapadtak..."

Ennyire hup-fan még nem vagyok, hogy bukkanó helyett huppanót írjak :)
Enyhe dombocska volt és sztem az emberünk egy pillanatra repült az autóval. Legalábbis ilyesmit meséltek. Szerencsére nem voltam közvetlen tanúja az ügynek.

( Yorirou | 2009. 08. 16., v – 19:22 )

Én ilyen OS-t és programokat szeretnék egy szép napon :)

Ezt meg honnan szedted? Egyebkent *nem* resze.

"
What we assume
[..]
Compiler/linker: we assume that the compiler has translated this specific program (seL4) correctly into ARM11 assembly code (according to our formalisation of C and the C standard) and that the linker lays out this code correctly in memory."

http://ertos.nicta.com.au/research/l4.verified/proof.pml

Nem emlékszem, hogy ki lettetek volna röhögve, inkább csak a szokásos "mikro-/monolitikus kernel a jobb" vita folyt le ezredszer. (Engem nem kell meggyőzni, hogy Tannenbaumnak volt igaza, és szerintem vannak még itt páran akiket nem.) Trey ezen cikke pedig nem általában az L4 mikrokernelről szól, hanem annak az seL4 változatának bejelentéséről, meg egyáltalán egy kernel formális módszerekkel történő ellenőrzéséről.

init();

Úgy van, nem is találgattam:

"...dehát minden szentnek maga felé hajlik a keze, hát még neki. /me pets Linus..."
"lássuk hogy is lehet ezt összetákolni @ home."
"nem jár több szopással mint egyéb F/OSS komponensek összeizgatása, tehát full szopás)"

Korrekt magyar mondatok, tényleg címlapra való (félre ne érts, hozzászólásban ez még talán elmegy, de ne rakjunk már ki ilyeneket egy cikkbe).

init();

látom még sosem olvastál ÉSt, nem is szólva a Magyar Narancsról. nem mintha kedvelném ezeket a lapokat, de ezekben rengeteg hasonló stílusú cikk olvasható. sőt még támogatja is őket a magyar kormány a te adóforintodból is, már ha itt adózol:) szólva 2009ben azt állítani, hogy ezek a mondatok nem valók címlapra, hmm minimum valóságtól elrugaszkodott kijelentésnek tekinthető:)

ez meglep. általában pont az idősebb műszaki szakik azok, akiknek minden 3ik szavuk trágár szó. szinte egységes stílusjegyük ez a káromkodó beszédstílus. analóg technikában profi műszerészek, nyáktervező villanymérnökök a fő képviselők. legalábbis akiket ismerek ilyenek. a fiatalabbakra már nem jellemző a folytonos bazmegelés.

Nem azt mondtam, hogy az én számból állandóan matyó hímzés bújik ki, mint a Magyar Népmesék főcímében a galambok csőréből, csak azt, hogy legalább szakmai cikkekben kerüljük a magyartalan, vagy trágár kifejezéseket. Nem láttam még PC World-ben, Chip magazinban, Világgazdaságban, HVG-ben stb. káromkodást. (Irodalom, publicisztika, film, színház más téma, ott ez elfogadható, ha dramaturgiailag szerepe van - cél nélkül még ott sem.)

init();

Úgy emlékeztem, hogy beküldte a cikket Trey-nek, akinél elszakadt a cérna, hogy megint neki kell kijavítania másvalaki rosszul fogalmazott, magyartalan stb. cikkét. Szólt neki, hogy javítsa, majd miután a srác felszólítás után sem volt hajlandó javítani, Trey nem rakta ki az írást hup-ra. Ezután a srác itt háborgott egy ideig, majd az írását kitette a saját blogjára, Trey meg a szűrét. :)

init();

( prygme | 2009. 08. 16., v – 21:57 )

ez az általános célú µkernel, az L4, már jó régóta létezik. az újdonság csak ennek az "ellenőrzésnek" az elvégzése volt. a linux kernel már sok év óta működik az L4en, bár az nicta saját seL4 változatán eddig lehet, hogy nem ment. egyébként gratulálok a meleg víz újbóli felfedezéséhez:D

( skylooker | 2009. 08. 16., v – 22:46 )

A Fraunhoffer-intézetben is készült egy kernel, kb. 3000 sor a forrás (C), ebben már van vmi self-healing-szerű huncutság is.
Tűz, víz és saválló.

( tomaza | 2009. 08. 17., h – 10:25 )

próbáltam bugreportot küldeni: nem találtam az oldalon bugreportot

a rendszerben _van_* bug (mint ahogy a nap is felkel holnap, ha nem is ezen a bolygón, ha nem is ebben a naprendszerben, de _biztos_), például hogy nincs bugreportlehetőség :)
amire te gondolsz az az, hogy a specifikációnak az implementáció megfelel, most nem egy világmegváltásról, vagy akárcsak valami első nagyobbacska lépésről van szó, eddig is volt rengeteg helyen, sőt sokkal nagyobb rendszereknél is formális bizonyítás, és még csak nem is arról hogy valaha is mondjuk egy oprendszer(a tágabb értelemben véve) ellenőrizve lesz

((fentebbi optimista linux meg 1000 év "extrapolációhoz": nem kétszer annyi kódsornál lesz kétszer annyi idő az ellenőrzés, hanem minden egyes plusz sornál!))

*: a legtriálisabbakat ők is megírják a faqban, feature-nek fogalmazva:)

( mchalls | 2009. 08. 19., sze – 12:30 )

Mar csak azt kell bizonyitani hogy a bizonyitas helyes =)

Van itt még több feladat is ;)

1. elkészíteni a C nyelv szemantikájának formális leírását (mert bizonyításokban elég nehéz dolgozni a jelenleg létező angol nyelvű szöveges szabvánnyal)

2. Írni egy C fordítót is ami bizonyíthatóan megfelel az 1.-nek.

3. És azzal a C fordítóval lefordítani, egy formális módszerekkel szintén végigellenőrzött architektúrára

a bizonyitast geppel ellenoriztek, mert a gep el tudja donteni a bizonyitas minden lepeserol, hogy helyes/megengedett-e - az meg egyertelmu, hogy mibol (kesz program) mit (specifikacio) akarunk bizonyitani. mondjuk az ellenorzo program nincs bizonyitva, hogy helyes, de azt mondjak valoszinu helyes.

- Use the Source Luke ! -