A Concurrency Framework for Priority-Aware Intercomponent Requests in CAmkES on seL4

This research work proposes a concurrency framework designed to handle priority-based intercomponent requests efficiently in CAmkES on seL4. The framework supports reentrant execution, locked critical sections over shared state using IPCP, NPCS, and PIP protocols. It requires minimal changes to component specifications and guarantees consistency over lock acquisition using priority semantics without additional atomic operations, minimizing RPC invocation overhead.

• Concurrency Framework
• Priority-Aware
• Intercomponent Requests
• CAmkES
• seL4

dennis23 Follow

Uploaded on May 11, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Priority-Based Concurrency and Shared Resource Access Mechanisms for Nested Intercomponent Requests in CAmkES Marion Sudvarg, Zhuoran Sun, Ao Li, Chris Gill, Ning Zhang Washington University in St. Louis St. Louis, Missouri, United States Work Accepted for Publication in Springer Real-Time Systems RTSS 2023 Funded by NSF grants CSR-1814739, CNS-17653503, and CNS-2229290, and NASA grant 80NSSC21K1741 1

2. seL4 Provides resilience for real-world platforms (e.g. the Boeing Unmanned Little Bird H-6U) Formally verified, capability-based, lightweight microkernel Supports real-time and mixed-criticality systems Image courtesy of Boeing: https://www.boeing.com/defense/unmanned-little-bird-h-6u/ RTCSA 2022 2

3. CAmkES: Components in seL4 Components encapsulate and isolate both state and functionality Example Component- Based System for Drone Set Speed Provide structure, modularity, and reusability Calibrate A component defines explicit interfaces for communication and control flow New Accelerometer Poll Diagram courtesy https://docs.sel4.systems/projects/camkes/visual-camkes/VisualCAmkES_Layout_Example.png RTCSA 2022 3

4. Real-Time Component-Based Systems A component might originate a real-time task Timer or Event- Based Tasks Components Shared Tasks may share common functionality or state, encapsulated by service components Camera L Record Event Camera R Object Detection Task execution begins in the originating component Proceeds via synchronous RPC invocations across shared components RTCSA 2022 4

5. Limitations of CAmkES Provides Component Procedure Interfaces (CPIs) for Remote Procedure Call (RPC) requests CPIs assigned a single thread that waits on an seL4 endpoint at a static priority specified at compile-time This is not well-suited to task execution that cross-cuts components Tasks of different priorities may concurrently send requests to the same CPI! RTCSA 2022 5

6. Our Original Solution Presented at RTCSA 2022: A Concurrency Framework for Priority-Aware Intercomponent Requests in CAmkES on seL4. Supports both reentrant execution and locked critical sections over shared state with the IPCP, NPCS, and PIP protocols Requires minimal changes to component specifications Bound overhead by using priority semantics to guarantee consistency over lock acquisition without additional atomic operations RPC invocation overhead is not significantly increased Did not support nested Priority Inheritance Protocol RTCSA 2022 6

7. This Work Extends the prior work to support nested priority inheritance Components coordinate to send priority updates to downstream components Individual components only need direct communication from incoming requestor Faster than Patina mutex service, which does not support nested locking RTCSA 2022 7

8. Thank You! Any questions? Full paper and code available from: https://www.sudvarg.com/priority-aware-camkes RTCSA 2022 8