4a3d7a958c
As requested by verification, hypervisor registers are now an enumeration-indexed array rather than individual fields. This cleans up some of the proof. Additionally, we sweep some non-complexity under the machine op rug: vcpu_hw_write/read_reg_ccorres is as deep as we go, rather than specifying every operation and proving that vcpu_hw_write seL4_VCPUReg_REG calls set_REG for every REG I took this opportunity to clean up some arm-hyp definitions and proofs, so some whitespace cleanup got tangled in. |
||
|---|---|---|
| .. | ||
| include | ||
| src | ||
| .gitignore | ||
| Makefile | ||
| README.md | ||
| SEL4.cabal | ||
| Setup.hs | ||
| check-newlines.sh | ||
| configure | ||
| mkhsboot.pl | ||
| stack-path | ||
| stack.yaml | ||
README.md
The seL4 Haskell Model
The sources in this directory can be used to build a Haskell Cabal package containing an executable model of the seL4 kernel. The model cannot run stand-alone; it must be integrated into a simulator that can run user-level binaries and generate events that the kernel model can process.
To build it:
- install the Haskell build tool stack.
- run
make
The Makefile will use stack to fetch appropriate versions of ghc and
cabal-install.
After that, you can compile Haskell programs using the simulator by adding
-package SEL4 to the ghc command line. Note that the qemu target requires
some callback functions to be accessible via the FFI, so it is not possible to
load a model compiled for those targets in GHCi.
Currently, the simulator interface is out of date, so this model is currently only useful as documentation and as intermediate artefact in the seL4 correctness proof. The model itself is kept up to date with the C code, only the simulator interface is outdated.