CapDL initialiser for seL4

This repository contains the capDL initialiser for seL4.

The capDL initialiser is the root task for a seL4 system that takes a description of the state to be initialised using capDL, and starts the system in conformance with the specification.

The code is an implementation of the formal algorithm specified in Isabelle/HOL.

Repository overview

• src/main.c: The implementation of the initialiser
• include/capdl.h: The data structure for capDL.

Dependencies

The capDL loader uses capDL-tool to generate a data structure containing the capDL specification to be initialised.

Related papers

The formal model for the capDL initialiser is documented in ICFEM '13 paper and Andrew Boyton's PhD thesis.

License

The files in this repository are release under standard open source licenses. Please see individual file headers and the LICENSE_BSD2.txt file for details.