Reply To: Inter-process Communication

Can you compare your ideas behind IPC to the seL4 operating system, which is the first operating system that comes with proofs of correctness (including proofs that the compiler correctly translated the code to assembly!). Awaiting features from CPU vendors, they are also on the cutting edge of doing time-dimension proofs. The feature that I see seems lacking on seL4 is futex(), with all its security coming from the page tables and seL4’s existing memory type system, but otherwise everything both you and seL4 seem to be talking about is properly utilizing the MMU to its full potential.