2014-07-28 01:59:57 +00:00
|
|
|
The Executable Design Specification of seL4
|
|
|
|
|
===========================================
|
2014-07-22 23:11:43 +00:00
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
l4v/spec/design/
|
2014-07-22 23:11:43 +00:00
|
|
|
|
|
|
|
|
This directory contains the Isabelle sources of the executable design
|
2014-07-28 01:59:57 +00:00
|
|
|
specification for seL4.
|
2014-07-22 23:11:43 +00:00
|
|
|
|
|
|
|
|
Most theory files in this directory are tool-generated, do not edit!
|
|
|
|
|
|
|
|
|
|
The files here are also not particularly well suited for human consumption, it
|
|
|
|
|
is recommended to directly read the corresponding Haskell code in
|
|
|
|
|
`seL4/haskell` instead.
|
|
|
|
|
|
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
Top-Level Theory
|
|
|
|
|
----------------
|
2014-07-22 23:11:43 +00:00
|
|
|
|
|
|
|
|
The top-level theory file that draws the whole specification together is
|
|
|
|
|
`API_H`, the top-level function in that theory is `callKernel`.
|
|
|
|
|
|
|
|
|
|
Similarly to the abstract specification, this top-level function is later in
|
|
|
|
|
the proofs further wrapped in an automaton that describes system behaviour on
|
|
|
|
|
this level of abstraction.
|
|
|
|
|
|
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
Building
|
|
|
|
|
--------
|
2014-07-22 23:11:43 +00:00
|
|
|
|
|
|
|
|
The corresponding Isabelle session is `ExecSpec`. Build in `l4v/spec/` with
|
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
make ExecSpec
|
2014-07-22 23:11:43 +00:00
|
|
|
|
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
Remarks
|
|
|
|
|
-------
|
2014-07-22 23:11:43 +00:00
|
|
|
|
|
|
|
|
* for regenerating the design spec from Haskell sources, go to directory
|
|
|
|
|
`l4v/tools/haskell-translator` and run
|
|
|
|
|
|
2014-07-28 01:59:57 +00:00
|
|
|
./make_spec.sh
|
2014-07-22 23:11:43 +00:00
|
|
|
|
|
|
|
|
* skeleton files that define which parts of which Haskell files get mapped
|
|
|
|
|
to which Isabelle theories are found in the sub directories `skel` and
|
|
|
|
|
`m-skel` for `design` and `machine` respectively.
|
2014-07-28 01:59:57 +00:00
|
|
|
|
