README.md
1CapDL User-level system initialiser
2===================================
3
4This contains a formalised algorithm and the proof of correctness of
5a user-level system initialiser that uses [capDL](../spec/capDL/) to
6specify the state of the resultant system.
7
8It builds on the [CapDL API Proofs](../spec/capDL-api/), and uses
9a [separation logic defined for capDL](../spec/sep-capDL/).
10
11The system initialiser and the proof are described in the
12[ICFEM '13 paper][Boyton_13] and Andrew Boyton's PhD thesis.
13
14 [Boyton_13]: http://www.nicta.com.au/pub?id=7047 "Formally Verified System Initialisation"
15
16Building
17--------
18
19To build from the `l4v/` directory, run:
20
21 make SysInit
22
23To build the example capDL specifications, from the `l4v/` directory, run:
24
25 make SysInitExamples
26
27
28Important Theories
29------------------
30
31* The specification for the algorithm of the system initialiser is in
32 [`SysInit_SI`](SysInit_SI.thy).
33
34* The top-level statement of the correctness of the system-initialiser
35 is found in [`Proof_SI`](Proof_SI.thy).
36
37* The definition of what it means for an object to be initialised
38 (`object_initialised` and (`irq_initialised`) is found in
39 [`ObjectInitialised_SI`](ObjectInitialised_SI.thy).
40
41* Only "well-formed" capDL specifications can be initialised. The
42 definition of well-formed is located in
43 [`WellFormed_SI`](WellFormed_SI.thy).
44
45* Two example capDL specifications that are "well-formed" are found in
46 [`ExampleSpec_SI`](ExampleSpec_SI.thy) and
47 [`ExampleSpecIRQ_SI`](ExampleSpecIRQ_SI.thy). The former is a simple
48 capDL spec, and the latter a more complicated specifications with IRQ
49 support.
50
51