How to: A quick solutions guide

This guide provides links to tutorial solutions as quick references for seL4 calls and methods.

The seL4 kernel

Capabilities

• Calculate the size of a CSpace
• Copy a capability between CSlots
• Delete a capability
• Suspend a thread

Untyped

• Create an untyped capability
• Create a TCB object
• Create an endpoint object
• Create a notification object
• Delete an object

Mapping

• Map a page directory
• Map a page table
• Remap a page
• Unmap a page

Threads

• Configure a TCB
• Change the priority of a thread
• Set initial register state
• Start the thread
• Set the arguments of a thread
• Resolve a fault

IPC

• Use capability transfer to send the badged capability
• Get a message
• Reply and wait
• Save a reply and store reply capabilities

Notifications

• Set up shared memory
• Signalling
• Differentiate signals

Interrupts

• Invoke IRQ control
• Set NTFN
• Acknowledge an interrupt

Fault handling

• Set up an endpoint for thread fault IPC messages
• Receive an IPC message from the kernel
• Get information about a thread fault
• Handle a thread fault
• Resume a faulting thread

MCS Extensions

• Set up a periodic thread
• Unbind a scheduling context
• Experiment with sporadic tasks
• Use passive servers
• Configure fault endpoints

Dynamic 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

CAmkES

A basic CAmkES application

• Define an instance in the composition section of the ADL
• Add a connection
• Define an interface
• Implement an RPC function
• Invoke a RPC function

Events in CAmkES

• Specify an events interface
• Add connections
• Wait for data to become available
• Signal that data is available
• Register a callback handler
• Specify dataport interfaces
• Specify dataport connections
• Copy strings to an untyped dataport
• Read the reply data from a typed dataport
• Send data using dataports
• Read data from an untyped dataport
• Put data into a typed dataport
• Read data from a typed dataport
• Set component priorities
• Restrict access to dataports
• Test the read and write permissions on the dataport

CAmkES Timer

• Instantiate a Timer and Timerbase
• Connect a timer driver component
• Configure a timer hardware component instance
• Call into a supplied driver to handle the interrupt
• Stop a timer
• Acknowledge an interrupt
• Get a timer handler
• Start a timer
• Implement an RPC interface
• Set a timer interrupt
• Instantiate a TimerDTB component
• Connect interfaces using the seL4DTBHardware connector
• Configure the TimerDTB component
• Handle the interrupt
• Stop the timer

CAmkES VM Linux

• Add a program
• Add a kernel module
• Create a hypercall

CAmkeES Cross VM Connectors

• Add modules to the guest
• Define interfaces in the VMM
• Define the component interface
• Instantiate the print server
• Implement the print server
• Implement the VMM side of the connection
• Update the build system
• Add interfaces to the Guest
• Create a process