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 a 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.

File included from github repo edit