Isabelle/HOL
Abstract specification
Refinement proof
Executable specification
Haskell prototype
Refinement proof
Automatic
translation
High-performance C implementation
Otherwise, the data structures used in this abstract specification are high level—essentially sets, lists, trees, functions,
and records. We make use of nondeterminism in order to
leave implementation choices to lower levels: if there are
multiple correct results for an operation, this abstract layer
would return all of them and make clear that there is a choice.
The implementation is free to pick any one of them.
An example of this is scheduling. No scheduling policy is
defined at the abstract level. Instead, the scheduler is modelled as a function picking any runnable thread that is active
in the system or the idle thread. The Isabelle/HOL code for
this is shown in Figure 3. The function all_active_tcbs
returns the abstract set of all runnable threads in the system. Its implementation (not shown) is an abstract logical
predicate over the whole system. The select statement
picks any element of the set. The OR makes a nondeterministic choice between the first block and switch_to_idle_
thread. The executable specification makes this choice
more specific.
4. 2. executable specification
The purpose of the executable specification is to fill in the
details left open at the abstract level and to specify how the
kernel works (as opposed to what it does). While trying to
avoid the messy specifics of how data structures and code
are optimized in C, we reflect the fundamental restrictions
in size and code structure that we expect from the hardware
and the C implementation. For instance, we take care not to
use more than 64 bits to represent capabilities, exploiting
known alignment of pointers. We do not specify in which
way this limited information is laid out in C.
The executable specification is deterministic; the only
nondeterminism left is that of the underlying machine. All
figure 3. isabelle/hoL code for scheduler at abstract level.
schedule º do
threads ¬ all_active_tcbs;
thread ¬ select threads;
switch_to_thread thread
od OR switch_to_idle_thread
data structures are now explicit data types, records, and lists
with straightforward, efficient implementations in C. For
example the capability derivation tree of seL4, modelled as a
tree on the abstract level, is now modelled as a doubly linked
list with limited level information. It is manipulated explicitly with pointer-update operations.
Figure 4 shows part of the scheduler specification at this
level. The additional complexity becomes apparent in the
choose Thread function that is no longer merely a simple predicate, but rather an explicit search backed by data
structures for priority queues. The specification fixes the
behavior of the scheduler to a simple priority-based round-robin algorithm. It mentions that threads have time slices
and it clarifies when the idle thread will be scheduled. Note
that priority queues duplicate information that is already
available (in the form of thread states), in order to make it
available efficiently. They make it easy to find a runnable
thread of high priority. The optimization will require us to
prove that the duplicated information is consistent.
We have proved that the executable specification correctly implements the abstract specification. Because of
its extreme level of detail, this proof alone already provides
stronger design assurance than has been shown for any
other general-purpose OS kernel.
4. 3. c implementation
The most detailed layer in our verification is the C implementation. The translation from C into Isabelle is correct-ness-critical and we take great care to model the semantics
of our C subset precisely and foundationally. Precisely means
that we treat C semantics, types, and memory model as the
C99 standard4 prescribes, for instance, with architecture-dependent word size, padding of structs, type-unsafe casting
of pointers, and arithmetic on addresses. As kernel programmers do, we make assumptions about the compiler (GCC)
that go beyond the standard, and about the architecture
figure 4. haskell code for schedule.
schedule = do
action <- getSchedulerAction
case action of
ChooseNewThread -> do
chooseThread
setSchedulerAction ResumeCurrentThread
...
chooseThread = do
r <- findM chooseThread¢ (reverse [minBound ..
maxBound])
when (r == Nothing) switchToIdleThread
chooseThread¢ prio = do
q <- getQueue prio
liftM isJust findM chooseThread² q
chooseThread² thread = do
runnable <- isRunnable thread
if not runnable then do
tcbSchedDequeue thread
return False
else do
switchToThread thread
return True
