GNU Hurd 0.8, GNU Mach 1.7 a GNU MIG 1.7 (diskuse)

[BFU]

Verze 1.0 se blizi

[Ladislav Hagara]

GNU/Hurd 1.0.0 vydán

[Ruža Becelin]

Tyvole ja se snad doziju toho, ze vyjde verze 1.0!

[Honz]

Je tu spousta uživatelů z pouštních oblastí, které tomu nepřejí...

[Grunt]

Jesti dopadne jako Duke Nukem Forever tak snad i bude lepší když se toho nedožijem…

[koudy]

Já bych na to nespoléhal, po 0.9 následuje 0.10 ;)

[Michal Kubeček]

Tohle už se říkalo o openssl, wine, mplayeru… U všech nakonec verze 1.0 vyšla - a vlastně se nic zvláštního nestalo.

[pc2005]

Tak zrovna openssl by mělo IMO zůstat ještě dlouho jako 0.x .

[Bedňa]

git clone hurd

git tag -a v1.0 -m "version 1.0"

...

Tak a dožil si sa toho, čo aký to je pocit?

[xm]

Když už mikrojádro, tak proč ne raději seL4, které je formálně verifikované? Licencované je také pod GPL a bezpečností se mu žádný jiný kernel nemůže rovnat (pokud vím jiný formálně verifikovaný opensource kernel ani neexistuje, jen nějaké proprietární)

[xm]

Btw. seL4 je i přes jeho vysokou bezpečnost asi v současnosti nejvýkonnější mikrojádro. A může pod ním běžet Linux (pak plní seL4 úlohu hypervizoru).

[Michal Kubeček]

Co jsem si tak zatím zběžně přečetl, formální verifikace s vztahuje jen na jednu konkrétní konfiguraci na jednom ARMu - a např. také za předpokladu, že se nepoužívá DMA. A odpověď

On x86, seL4 can be configured to support multiple CPUs. Current multicore support is through a multikernel configuration where each booted CPU is given a portion of available memory. Cores can then communicate via limited shared memory and kernel supported IPIs. This configuration is highly experimental at the moment.

nezní v roce 2016 moc lákavě. Na nějaká malá a výkonově nenáročná embedded zařízení by to asi použít šlo (pokud tedy někdo dopíše drivery, které jsou PNJ). Ale už na nějaký router, firewall nebo fileserver to bude problém.

[xm]

Ano, formální verifikace je složitá věc Nejde to jen tak smahem vztáhnout na vše a neomezené DMA to zabíjí. Ale x86 verze by měla mít možnost používat DMA (pomocí VT-d) - zatím sice není verifikovaná, ale může v budoucnu být.

[Sid]

no tak to budu mat co robit hadam, specialne ked este ta validacia je robena vlastne napisanim mikrojadra v Haskell a potom neskor je to transformovane na C.

[pc2005]

Dneska prakticky jakákoliv periferie používá vlastní busmaster. A hádám, že žádná z nich nebude formálně verifikovaná .

[Jakub Jermář]

Když už mikrojádro, tak proč ne raději seL4, které je formálně verifikované?

Přísně vzato, Hurd není mikrojádro, ale multiserver, který běží nad mikrojádrem Mach. Zatím se Hurd nepodařilo naportovat na žádné jiné mikrojádro, a proto tedy nelze použít kombinaci Hurd nad seL4. Pak by tu ještě byla možnost použít mikrojádro seL4 bez Hurdu, ale tam by zase chyběla netriviální multiserverová vrstva (IMO to nejzajímavější na Hurdu), která řeší věci jako networking, souborové systémy, autentikaci, rozšiřitelnost atp.

Licencované je také pod GPL a bezpečností se mu žádný jiný kernel nemůže rovnat (pokud vím jiný formálně verifikovaný opensource kernel ani neexistuje, jen nějaké proprietární)

Viz microkernel.info a tam třeba heslo The Muen Separation Kernel.

[little.owl]

hyběla netriviální multiserverová vrstva (IMO to nejzajímavější na Hurdu),

+1

[x]

A o Minixu nikdo nic? Nebo obecne unikernel.org a konkretni priklad Erlang on Xen