Créer un compteSe connecter

Recherches récentes

Aucune recherche récente

Options de recherche

Disponible uniquement lorsque vous êtes connecté.
mastouille.fr est l'un des nombreux serveurs Mastodon indépendants que vous pouvez utiliser pour participer au fédiverse.
Mastouille est une instance Mastodon durable, ouverte, et hébergée en France.

Administré par :

Statistiques du serveur :

582
comptes actifs

mastouille.fr: À proposAnnuaire des profilsPolitique de confidentialité

Mastodon: À proposTélécharger l’applicationRaccourcis clavierVoir le code sourcev4.3.4

#microkernel

0 message0 participant0 message aujourd’hui
Public
Martin Děcký

In January, I've presented a lightning talk reviewing a few amazing events in the domain of microkernel-based operating systems in 2024. It was a great year and let's hope that 2025 will be even better. Did I miss anything important? #microkernel #operating #systems slideshare.net/slideshow/2024-

2024 in Microkernels (a year in review lightning talk)
SlideShare2024 in Microkernels (a year in review lightning talk)2024 in Microkernels (a year in review lightning talk) - Download as a PDF or view online for free
Suite du fil
Public
jhamby

I don't dare to make any sort of proclamations about whether a 32-byte message would be better for cache utilization, but I think we can agree that if you're going to need 34 bytes, you may as well go up to 64 bytes and add some new fields and increase the size of the one standard MINIX message type with chars from 14 bytes to a whopping 44 bytes.

Any #MINIX or #microkernel-related things you're interested in knowing about?

Public
Martin Děcký

Next time somebody tells you that that microkernels are useless, impractical and/or have poor performance, let them read this:

"We have deployed HM on tens of millions of devices, including smart routers, smart vehicles, and smartphones, which provides not only better security and reliability but also better performance than their Linux counterparts." [1]

[1] Haibo Chen et al.: Microkernel Goes General: Performance and Compatibility in the HongMeng Production Microkernel, in the Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation,
usenix.org/system/files/osdi24
#microkernel #osdi #osdi24

A répondu dans un fil de discussion
Public
blake shaw 🇵🇸

@lispi314 @cwebber I'm confused about this idea (and admittedly read the linked post quickly and haven't yet dug into Fare's argument)

The author seems to stress microkernels as a set of servers, but to me that seems to confuse the idea of microkernels (mach, zircon, se/L4) with microkernel operating systems (hurd, fuschia, minix [which defines both]).

A microkernel is best thought of as a "CPU driver"; a #microkernel ideally shouldn't define kernel space/ring0 to be any larger than the ISA's supervisor mode flag surface area. Its job is to ensure safe and fault tolerant execution of code and little more. Microkernels typically don't even define file systems, which usually also live in userspace.

But it seems like the author more or less ignores this, zooming in on the operating system-level services. But without a kernel, and only modules, every error should cause the the CPU to fail, with risks of serious corruption. What am I missing here?

Public *
blake shaw 🇵🇸

#Pancake: a new, verified Pascal-like #pl emphasizing formal verification over type safety for low-level systems programming, device drivers in particular.

"Pancake eschews complex type systems to make the language attractive to systems programmers, while at the same time aiming to ease the formal verification of code. We describe the design of the language and its verified compiler, and examine its usability, performance and current limitations through case studies of device drivers and related systems components for an #seL4-based #os."

trustworthy.systems/publicatio
#formalmethods #microkernel

while true { #tx_fifo_busy(tmp_c_uart, tmp_clen_uart, tmp_a_uart, tmp_alen_uart); tx_fifo_ret = ldb tmp_a_uart; if tx_fifo_ret <> 1 { strb c_arr_uart, tmp; #putchar_regs(c_arr_uart, clen_uart, a_arr_uart, alen_uart); break; } }
ExplorerFlux en direct
À propos