History

Gerwin Klein 212ab3f3fd updated INSTALL file; renamed		2014-11-23 15:30:19 +11:00
..
doc	Retire old dft package; resurrect Haskell manual.	2014-07-19 15:55:06 +02:00
include	Release snapshot	2014-07-18 05:03:59 +10:00
src	changes for warning-free build with GHC 7.8.3	2014-11-23 15:30:19 +11:00
build	Release snapshot	2014-07-18 05:03:59 +10:00
mkhsboot.pl	removed ancient arch tags	2014-07-19 10:48:49 +02:00
README.md	updated INSTALL file; renamed	2014-11-23 15:30:19 +11:00
SEL4.cabal	changes for warning-free build with GHC 7.8.3	2014-11-23 15:30:19 +11:00
Setup.hs	changes for warning-free build with GHC 7.8.3	2014-11-23 15:30:19 +11: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 or later
install Cabal 1.18 or later. This is included with GHC 7.8.
configure the sources:
```
runhaskell Setup.hs configure --with-target=<arch>-<platform>
```
Valid target options are: arm-qemu, arm-lyrebird
build the library:
```
runhaskell Setup.hs build
```
install:
```
runhaskell Setup.hs install --user
```

After that, you can compile Haskell programs using the simulator by adding -package SEL4 to the ghc command line. Note that the qemu and lyrebird targets require 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.