How-to guide for the seL4 C libraries

This guide provides links to tutorial solutions as quick references for the seL4 C prototyping libraries.

Initialisation & threading

• Obtain BootInfo
• Initialise simple
• Use simple to print BootInfo
• Initialise an allocator
• Obtain a generic allocation interface (vka)
• Find the CSpace root cap
• Find the VSpace root cap
• Allocate a TCB Object
• Configure the new TCB
• Name the new TCB
• Set the instruction pointer
• Set the stack pointer
• Write the registers
• Start the new thread
• Print

IPC

• Allocate an IPC buffer
• Allocate a page table
• Map a page table
• Map a page
• Allocate an endpoint
• Badge an endpoint
• Set a message register
• Send and wait for a reply
• Receive a reply
• Receive an IPC
• Validate a message
• Write the message registers
• Reply to a message

Processes & Elf loading

• Create a VSpace object
• Configure a process
• Get a CSpace path
• Badge a capability
• Spawn a process
• Receive a message
• Send a reply
• Initiate communications by using seL4_Call

Timer

• Allocate a notification object
• Initialise a timer
• Use a timer
• Handle an interrupt
• Destroy a timer