RTOS as State Machine: Synthesis of Optimized Zephyr Embedded Systems with ARA

• Typ der Arbeit: Masterarbeit
• Status der Arbeit: in Planung
• Projekte: AHA
• Betreuer: Andreas Kässens, Daniel Lohmann

[Generated with AI]

Context

Within the AHA project, we focus on optimizing embedded systems by specialization of the OS itself. Using the Automatic Real-time Analyzer (ARA), we perform static analysis to find interactions between different tasks, resulting in a State Transition Graph (STG)¹. This information can be used to calculate effects of the system calls and tailor the implementation to the specific needs of the application. With the execution of Zephyr system calls on IR level during analysis, we are able to extract information about the OS objects before and after a system call. This allows specializing the RTOS interface to a state-machine, where system calls are transitions between global OS states.

Problem

The specialization of system calls is missing completely. The optimizer needs to generate a specialized system call implementation that can be compiled automatically into the Zephyr binary. Secondly, the correct specialized function must be called by the application.

Goal

In this thesis, the generation of specialized system calls shall be applied to the Zephyr RTOS. The student shall collect the effect of (all) system calls and generate specialized functions for each instance. The call-site must be rewritten to call this specialized function.

For example, if the application calls k_sem_take(sem_a, K_FOREVER) the generic RTOS implementation will modify at least the state on sem_a, and possibly the scheduler ready-queue. These effects can be detected statically and transformed into a very simple function, for example k_sem_take_bb42(), that will have exactly the same effect. Additionally, locking operations inside the kernel may need to be copied to match the behavior of the generic implementation. In the application IR code, the associated system call-site has to be replaced with a call to this new, specialized function.

To evaluate the results, the student shall compare the kernel overhead with an unmodified Zephyr build using benchmarks, e.g. the Thread Metric benchmark suite.

Topics: Zephyr, LLVM, Python, C, Static Analysis, Optimization

References

OSPERT Workshop B
IRx: RTOS-Aware Abstract Interpretation using an LLVM-based Interpreter

Andreas Kässens, Vitali Fendel, Daniel LohmannProceedings of the 19th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT '25)2025.
PDF [BibTex]

×

BibTex Entry

@inproceedings{kaessens:25:ospert,
author = {Andreas Kässens and Vitali Fendel and Daniel Lohmann},
booktitle = {Proceedings of the 19th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT '25)},
entrysubtype = {Workshop},
month = {July},
title = {{IRx}: {RTOS}-Aware Abstract Interpretation using an {LLVM}-based Interpreter},
venue = {Brussels, Belgium},
year = {2025},
}

Close

OSPERT Workshop B
Back to the Roots: Implementing the RTOS as a Specialized State Machine

Christian Dietrich, Martin Hoffmann, Daniel LohmannProceedings of the 11th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT '15)2015.
PDF [BibTex]

×

BibTex Entry

@inproceedings{dietrich:15:ospert,
author = {Dietrich, Christian and Hoffmann, Martin and Lohmann, Daniel},
booktitle = {Proceedings of the 11th Annual Workshop on Operating Systems Platforms for Embedded Real-Time Applications (OSPERT '15)},
entrysubtype = {Workshop},
month = {July},
pages = {7-12},
title = {Back to the Roots: Implementing the {RTOS} as a Specialized State Machine},
url = {http://www.mpi-sws.org/~bbb/events/ospert15/pdf/ospert15-p7.pdf},
venue = {Lund, Sweden},
year = {2015},
}

Close