It's Time: OS Mechanisms for Enforcing Asymmetric Temporal Integrity

TL;DR

This paper introduces OS mechanisms for enforcing asymmetric temporal integrity in mixed-criticality systems, implemented in the seL4 microkernel to ensure high-criticality tasks meet deadlines during overloads.

Contribution

It proposes a novel approach for asymmetric temporal integrity and demonstrates its implementation in the high-assurance seL4 microkernel.

Findings

Effective enforcement of asymmetric temporal integrity in seL4

Improved deadline guarantees for high-criticality tasks

Enhanced resource management in mixed-criticality systems

Abstract

Mixed-criticality systems combine real-time components of different levels of criticality, i.e. severity of failure, on the same processor, in order to obtain good resource utilisation. They must guarantee deadlines of highly-critical tasks at the expense of lower-criticality ones in the case of overload. Present operating systems provide inadequate support for this kind of system, which is of growing importance in avionics and other verticals. We present an approach that provides the required asymmetric integrity and its implementation in the high-assurance seL4 microkernel.