Microkernel Complexity

This is the seL4 microkernel. The picture shows the kernel's so-called function call graph. Each C function in the kernel is a dot. If function A calls function B, there is an arrow from A to B.

The graph shows that seL4 is highly complex software with strongly interconnected parts. This is typical for performance-optimised microkernels. Well engineered application level software would have groups or islands of strongly related dots connected by a small number of arrows bridging between the islands.

The proof analyses each of these function calls in all contexts it can occur.

The picture is a snapshot from early 2009. Green dots are the C functions we had verified at that time.