= Microkernel service failure isolation
Suppose the <user-space service> stops after receiving request `7`, before replying. Assume that its private <memory pages> are not writable mappings of the client's or an unrelated service's <computer memory>, and that it lacks <security capabilities> to change their <software threads>. A failed store in the service cannot directly overwrite that private state through ordinary <CPU> <address translation>. Those assumptions establish a particular isolation boundary, not a successful read.
\Image[/microkernel-service-failure-authority-boundaries.png]
{title=<Memory protection> and <security capabilities> limit a stopped service's reach; recovery needs an additional design}
The client can remain blocked waiting for request `7`. An unrelated runnable service may continue if <process scheduling> and resources permit, but clients that depend on the stopped service still lose access to its service. A separately authorized recovery manager would need to detect the failure, rebuild the service's state and arrange communication with its replacement. The <microkernel> architecture by itself supplies none of those application-specific recovery decisions.
A missing reply also does not reveal whether a service crashed, is delayed by <process scheduling>, or entered an infinite computation. For a read, retrying after recovery may be straightforward; for a modifying operation, absence of a reply does not prove that the modification never happened. Recovery must account for ambiguous completed operations and any required <file-system crash consistency>.
The boundary changes with authority. A deliberately shared writable <memory page> allows the service to change its shared contents; a <security capability> controlling another <software thread> permits the corresponding control operations. A <device driver> with uncontrolled <DMA> can bypass ordinary <CPU> <memory protection>. Thus service placement and actual permissions must be considered together. <What the Proofs Assume by seL4 Project>[What the Proofs Assume, The Assumptions: DMA and memory-mapped device registers]{ref}
Back to article page
