There are no malloc calls in the kernel — I think there is indeed no malloc routine in kernel space!
The main reason for this is that I wouldn’t know how to respond to a failure to get space.
This was an early design decision.
I was heavily influenced by the design of hardware caches that never failed to find room in the cache for new stuff.
The RAM of the machine was merely a cache of node and page stuff and this was motivation for the mantra that all state resides in nodes and pages — that way any stuff in RAM could be put back into pages and nodes and swapped out.
The kernel was never at the mercy of a user program to reach a state where it could be removed.
I assume some familiarity here with the caching style ideas about prepared nodes and involved keys and also prepared keys.
Those two general patterns are the heaviest use of adaptive formats in the Keykos kernel.
I want to consider here the top level view of kernel correctness theorems that one would aspire to in a full fledged code proof for the kernel.
By “code” I mean the machine code and not the assembler or C source.
This distinction is not relavant for most purposes, however.
Here is a lemma to the code proof is possible to complete that does not even involve the kernel’s semantics.
The kernel protects itself.
It does not shoot itself in the foot and also aranges to recapture control after launching user mode programs.
This comes in two parts:
- first, the kernel is type safe in the sense of recent languages.
This is easier to prove as there is no malloc that dynamically changes the type of a memory region, or a free that invalidates pointers to a freed region.
In the kernel a block of RAM that holds a node always will and always has held a node.
This expands the node concept for sometimes the block holds no node, and then holds nothing else either.
There are a few well discriminated unions.
There is no garbage collection logic to examine.
- second, I/O launched by the kernel will not write over itself or its data.
This can be proven with no attention to kernel semantics, just as a fancy compiler might achieve.
Memory Maps
When a domain program accesses its memory it is via the TLB which describes a subset of the memory mapping tables that are produced by the kernel and read by the hardware.
The mapping tables are constructed by reading segment nodes in item space and describe a subset of the access that the nodes describe.
The nodes in item space are a subset of the entire set of nodes in the system.
This logic is described in some detail here.
Here are some pot-shots on the practice of code proofs.