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. It has been updated to support nested Priority Inheritance Protocol.
More details on the design, implementation, and evaluation of this library are available in the following papers:
Marion Sudvarg, Zhuoran Sun, Ao Li, Ning Zhang, and Chris Gill. “Priority-Based Concurrency and Shared Resource Access Mechanisms for Nested Intercomponent Requests in CAmkES.” Real-Time Systems, Springer, 2023. (Accepted, to appear) [ preprint ]
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 | code | 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)