8d4a8eb238 | ||
---|---|---|
.. | ||
CreateIRQCaps_SI.thy | ||
CreateObjects_SI.thy | ||
DuplicateCaps_SI.thy | ||
ExampleSpecIRQ_SI.thy | ||
ExampleSpec_SI.thy | ||
InitCSpace_SI.thy | ||
InitIRQ_SI.thy | ||
InitTCB_SI.thy | ||
InitVSpace_SI.thy | ||
Makefile | ||
ObjectInitialised_SI.thy | ||
Proof_SI.thy | ||
README.md | ||
ROOT | ||
RootTask_SI.thy | ||
StartThreads_SI.thy | ||
SysInit_SI.thy | ||
WellFormed_SI.thy | ||
tests.xml |
README.md
CapDL User-level system initialiser
This contains a formalised algorithm and the proof of correctness of a user-level system initialiser that uses capDL to specify the state of the resultant system.
It builds on the CapDL API Proofs, and uses a separation logic defined for capDL.
The system initialiser and the proof are described in the ICFEM '13 paper and Andrew Boyton's PhD thesis.
Building
To build from the l4v/
directory, run:
make SysInit
To build the example capDL specifications, from the l4v/
directory, run:
make SysInitExamples
Important Theories
-
The specification for the algorithm of the system initialiser is in
SysInit_SI
. -
The top-level statement of the correctness of the system-initialiser is found in
Proof_SI
. -
The definition of what it means for an object to be initialised (
object_initialised
and (irq_initialised
) is found inObjectInitialised_SI
. -
Only "well-formed" capDL specifications can be initialised. The definition of well-formed is located in
WellFormed_SI
. -
Two example capDL specifications that are "well-formed" are found in
ExampleSpec_SI
andExampleSpecIRQ_SI
. The former is a simple capDL spec, and the latter a more complicated specifications with IRQ support.