NameDateSize

..25-Jul-201920

CreateIRQCaps_SI.thyH A D25-Jul-201918.8 KiB

CreateObjects_SI.thyH A D25-Jul-201978.5 KiB

DuplicateCaps_SI.thyH A D25-Jul-201915.7 KiB

ExampleSpec_SI.thyH A D25-Jul-201916.1 KiB

ExampleSpecIRQ_SI.thyH A D25-Jul-201937.7 KiB

InitCSpace_SI.thyH A D25-Jul-201990 KiB

InitIRQ_SI.thyH A D25-Jul-201914.2 KiB

InitTCB_SI.thyH A D25-Jul-201947.2 KiB

InitVSpace_SI.thyH A D25-Jul-201956.5 KiB

MakefileH A D25-Jul-2019441

ObjectInitialised_SI.thyH A D25-Jul-201965.6 KiB

Proof_SI.thyH A D25-Jul-201916.4 KiB

README.mdH A D25-Jul-20191.6 KiB

ROOTH A D25-Jul-2019519

RootTask_SI.thyH A D25-Jul-201940.4 KiB

StartThreads_SI.thyH A D25-Jul-20198.7 KiB

SysInit_SI.thyH A D25-Jul-201923.4 KiB

tests.xmlH A D25-Jul-2019666

WellFormed_SI.thyH A D25-Jul-201974 KiB

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