portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
seL4/haskell
History
Adrian Danis bddd804a6e x86: IOAPIC/MSI syscalls 
Restructure the x86 interrupt handling to allow for a more flexible
method of using IOAPIC and MSI interrupts. The essence of this change
is to allow for the user to pick, for both IOAPIC and MSIs, which
CPU vector to use. Additionally there is future support, in the API,
for seL4 to eventually protect MSI interrupts with the vt-d interrupt
routing tables.

API behaviour for legacy systems using the PIC is preserved

Part of SELFOUR-281
2016-02-02 15:58:18 +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 Release snapshot 2014-07-18 05:03:59 +10:00
src x86: IOAPIC/MSI syscalls 2016-02-02 15:58:18 +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 refactor haskell to allow for multiple architectures 2016-01-28 18:54:11 +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 refactor haskell to allow for multiple architectures 2016-01-28 18:54:11 +11:00
Setup.hs refactor haskell to allow for multiple architectures 2016-01-28 18:54:11 +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.