Under priority-based scheduling, inter-component control flow should be coupled with priority information, so that task execution can be prioritized appropriately end-to-end. However, the CAmkES component architecture for the seL4 microkernel does not adequately support priority propagation across intercomponent requests: component interfaces are bound to threads that execute at fixed priorities provided at compile-time in the component specification. This library provides CAmkES with a thread model that supports (1) multiple concurrent requests to the same component endpoint; (2) propagation and enforcement of priority metadata, such that those requests are appropriately prioritized; and (3) implementations of Non-Preemptive Critical Sections, the Immediate Priority Ceiling Protocol and the Priority Inheritance Protocol for components encapsulating critical sections of exclusive access to a shared resource.
More details on the design, implementation, and evaluation of this library are available in the following paper:
M. Sudvarg and C. Gill. A Concurrency Framework for Priority-Aware Intercomponent Requests in CAmkES on seL4. The 28th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA), August 2022. Best Paper. [ paper | slides | video ]
Instructions for using our library, as well as a more up-to-date discussion of our Notification Manager, are available in the README.
The TimeServer is a reusable component provided as part of the seL4 Foundation's CAmkES global components repository. We have added support for the Broadcom BCM2837 chip (which is used in the Raspberry Pi 3 Models B and B+, later models of the Raspberry Pi 2 Model B, and the Raspberry Pi Compute Module 3).
(Forked from https://github.com/seL4/global-components)