I think that software verification techniques will pay off sometime and they are indeed a worthy research goal. I hope they do not excessively delay the system.
I am very pleased that plans currently include persistence. The NCSC people were enthusiastic about not having to consider how to recover an evolved secure state.
Indeed Keykos has nodes with 16 slots for 16 capabilities. 16 was a somewhat magic number in the 370 architecture. log2log216 is an integer too. The cleavage points in the virtual address were on 4 bit nibbles. Wimpy arguments all; most of them receded on subsequent architectures.
The wrapper function of the Keykos red segment was a discovered pattern. Coyotos has rationalized this pattern.
Overuse of nodes was considered a virtue. It allowed the mantra “All state is in pages and nodes.”. The several uses of nodes known to the kernel added some hair as those nodes were prepared for their special functions. It was an abstraction within an abstraction. This was indeed extra TCB hair but infrequently executed. The extra hair was somewhat counterbalanced by simplicity in:
The note about Size Partitioning is certainly correct. I was enthusiastic about the speed at which one could find and modify all Keykos capabilities on the occasion of new kernel that required a new real key format. This was fast for they were in contiguous disk cylinders. One might take some applications out of service for only a few seconds to remap the world. We never did this, nor needed to.
That the height of a node should be an attribute of the node instead of an attribute of the capability naming the node caused us to invent the red segment node. That was a hack but it was also efficient considering the way we built memory trees. I am enthusiastic about powers of 2 for height.
The PATT seems like a sound idea. It is like a special user mode instruction that is available in the AS/400 architecture and I think came from the System/38 where it was used to accelerate access to balanced tries as used in data base systems. The key to such trees were bit strings and the hardware ran down the tree comparing and skipping parts of the key that were common to adjacent parts of the tree. I vaguely recall that each trie node was binary.
Keykos has the external migrator as an Out of Kernel Helper. The migrator could not foul the logic of other domain code but most migrator bugs would cause the system to hang and fail to make progress. We had also designed but not implemented an external decongester. I have no fundamental objection to trusted code outside the kernel. One must cope with the necessity to get zot to run in order to get zot to run. It is often more difficult to argue correctness than to be correct.
The Keykos kernel had the great good fortune of being born in a virtual machine where it can be debugged. IBM’s VM/370 had debugging hooks cruder that gdb but superior to the tools for debugging privileged x86 code that I am familiar with.
Capability Address Spaces seem like a good idea. The Keykos general key registers are dual to the general (data) registers. The Capability Address Spaces may win. There were quite a few programs that did awkward things to duck the 16 key limit. A few programs resorted to a key cache to manage the 16 general key slots. The cache overhead was poor.
The Virtual Registers seem like a good idea. Keykos has virtual registers but they were stumbled upon rather that invented. We did not think of using them as a technique to send and receive messages. There may be literally no code in the Keykos kernel to implement virtual registers. The only change was to modify domain service key orders on where the limits of the register save area was within a domain. Perhaps more kernel function is necessary to make them useful. It would be necessary to make it faster for a domain to access its own virtual registers, than was the case in Keykos.
Keykos did not provide different service classes but there was a plan to allow a domain to declare a threshold in the entry block. Start keys with data bytes above this threshold would go to the front of the stall queue. Neither did Keykos dispatch or distribute requests in the kernel. We had a tentative plan for the kernel to contemplate a node full of start keys to fungible server domains. I suspect that the Coyotos plan may be more efficient.
I will be curious to see how the GC plan works.
The folks at the NASA wind tunnel liked many of the Keykos features. They have hard real-time problems. They suggested canceling checkpoints during tests. Concomitantly certain programs would be blocked from running. This is not a general solution to the hard real-time problem.