adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/spec/cspec
History
Achim D. Brucker e59d6ad091 Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
..
AARCH64 aarch64 machine+aspec+cspec: pt_type ghost+table array sizes 2024-01-16 10:01:47 +11:00
ARM cspec: Kernel_C: hide numDomains, sync comments 2022-02-22 18:24:02 +11:00
ARM_HYP cspec: Kernel_C: hide numDomains, sync comments 2022-02-22 18:24:02 +11:00
RISCV64 cspec: Kernel_C: hide numDomains, sync comments 2022-02-22 18:24:02 +11:00
X64 cspec: Kernel_C: hide numDomains, sync comments 2022-02-22 18:24:02 +11:00
c Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
KernelInc_C.thy all: remove theory import path references 2020-11-02 10:16:17 +10:00
KernelState_C.thy Renamed Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. 2024-01-27 13:44:24 +00:00
README.md READMEs: use run_tests consistently in READMEs (#622) 2023-03-30 13:59:18 +11:00
Substitute.thy isabelle-2021: update CSpec 2021-09-30 16:53:17 +10:00
TypHeapLimits.thy all: adjust theory imports for TypHeapLib change 2023-01-25 10:13:45 +11:00
mk_umm_types.py isabelle2022 cspec: update mk_umm_types.py 2022-11-09 11:45:46 +11:00

README.md

The C Semantics of seL4

l4v/spec/cspec/

This directory contains the entry point for the automatic translation of the seL4 source code into Isabelle/HOL.

The C semantics of the kernel is produced by first configuring and preprocessing the C sources for a specific platform and then parsing it into Isabelle using the C parser in l4v/tools/c-parser.

To inspect the output of this translation, build the image CSpec and interactively inspect the constants the parser has defined.

Top-Level Theory

The top-level theory file for this module is Kernel_C for the bare translation of seL4 into Isabelle, and KernelInc_C for additional automatic proofs about generated bitfield functions.

Building

The corresponding Isabelle sessions for this module are CKernel and CSpec. CSpec contains CKernel plus automated bitfield proofs.

To build the image for the ARM architecture, run the corresponding session in directory l4v/, e.g.:

L4V_ARCH=ARM ./run_tests CSpec

This will also configure and preprocess the kernel sources.

Expect this build to take about 30 min on a modern machine and to require close to 4GB of memory. For further sessions building on top of CSpec, usually at least 16GB of main memory are required together with a 64-bit setup of Isabelle.

The target architecture may be specified by setting the L4V_ARCH environment variable. It determines both which configuration of seL4 is used, as well as indicating the architecture-specific definitions and proofs to use. The default architecture is ARM and will be selected if none is provided. See l4v/spec/cspec/c/Makefile for seL4 configuration details.

The build process has an option for providing a device tree overlay file if desired, which can customise the memory regions available to the kernel. See the README file in c/overlays/ for more details.

Remarks

To speed up interactive development, the bitfield code generator can be configured to skip the corresponding proofs and produce sorried (unproven) property statements only. To achieve this, set the environment variable SORRY_BITFIELD_PROOFS to TRUE.