History

Anna Lyons d9802d179f Add seL4_NBWait: non blocking wait for notifications and endpoints.		2015-10-21 13:43:39 +11:00
..
doc	haskell: build server complained about lack of scalable font	2015-05-22 22:02:38 +10:00
include	Release snapshot	2014-07-18 05:03:59 +10:00
src	Add seL4_NBWait: non blocking wait for notifications and endpoints.	2015-10-21 13:43:39 +11:00
.gitignore	haskell: simpler build setup, so we can use cabal sandboxes	2015-05-22 15:19:36 +10:00
Makefile	fix haskell kernel build	2015-10-09 16:00:29 +11:00
mkhsboot.pl	removed ancient arch tags	2014-07-19 10:48:49 +02:00
README.md	haskell: simpler build setup, so we can use cabal sandboxes	2015-05-22 15:19:36 +10:00
SEL4-ARM.cabal	haskell: simpler build setup, so we can use cabal sandboxes	2015-05-22 15:19:36 +10:00

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 GHC 7.8.x
install Cabal 1.20.x. This is usually included with GHC 7.8.
run make

After that, you can compile Haskell programs using the simulator by adding -package SEL4-ARM 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.