portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
seL4/haskell
History
Rafal Kolanski 5493f8c330 Move inline text block out of handleInterrupt and rephrase. 
Inline text blocks are not permitted without extra spacing in literate
Haskell files. This tweak makes the Haskell kernel build again.
2016-03-21 11:05:20 +11:00
..
doc SELFOUR-279: rename Wait -> Recv, add wrappers for seL4_Poll and seL4_Wait for notification objects. 2015-11-20 15:28:18 +11:00
include haskell: more fixes and pass sel4test on haskell-qemu-emulator 2016-02-16 10:21:50 +11:00
src Move inline text block out of handleInterrupt and rephrase. 2016-03-21 11:05:20 +11:00
.gitignore haskell: simpler build setup, so we can use cabal sandboxes 2015-05-22 15:19:36 +10:00
configure refactor haskell to allow for multiple architectures 2016-01-28 18:54:11 +11:00
Makefile haskell: Some fixes on kernel init and some progress on multi platform support 2016-02-16 10:21:49 +11:00
mkhsboot.pl refactor haskell to allow for multiple architectures 2016-01-28 18:54:11 +11:00
README.md haskell: simpler build setup, so we can use cabal sandboxes 2015-05-22 15:19:36 +10:00
SEL4.cabal l4v-proof-porting: make c-parser and haskell translator happy 2016-02-16 10:21:50 +11:00
Setup.hs move kernelBase to arch specific files 2016-02-16 10:21:50 +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.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.