Establish sound worst-case bounds on the execution time of all seL4 kernel operations.
Hard real-time systems, including mixed-criticality systems (MCS) require schedulability analysis. This in turn requires hard upper bounds on execution times, including those of the OS. In order to make seL4 a suitable base for protected real time, we need to conduct an analysis of its worst-case execution times (WCET).
Such a WCET analysis must be sound and complete, meaning guaranteed to not under-estimate the true WCET.
Such a sound analysis is possible using static analysis of the code. In order to avoid making (unsound) assumptions on the compiler, the analysis must be conducted on the executable binary code.
The figure above shows a typical WCET analysis pipeline. A tool extracts the control-flow graph (CFG) from the binary. This is fed into an analysis tool that contains a model of the processor's microarchitecture, including (upper bounds of) individual instruction latencies, as well as a model of caches etc.
For any loops that do not have a fixed iteration count, loop bounds must also be supplied to the tool. They are usually determined by an (frequently informal) off-line analysis.
The analysis tool produces a set of integer linear equations that are fed into an ILP solver, which then produces candiate worst-case execution paths and their latencies; these are candidate WCETs.
In practice, many of the candidate WCET paths are infeasible, leading to a (potentially massive) overestimate of the WCET. Typically this happens for code paths guarded by mutually-exclusive conditions. As these conditions tend to depend on input data, the static analysis performed by the analysis tool is generally unable to detect those, so they need to be supplied from external analysis, similar to loop bounds.
We succeeded in performing a complete and sound WCET analysis of the seL4 microkernel on the ARM11 microarchitecture, including a cache analysis. This used a toolchain based on the NUS Chronos tool. We used manual (informal) analysis to determine loop bounds and infeasible paths. We used the worst-case paths produced by the tool to determine the kernel state and system-call parameters that would trigger these paths, and measured execution times, resulting in the execution times shown in the figure.
We can see that the safe bound is about four times the worst observed time. Much of this latency arises from the cache analysis: The ARM11 has a 4-way L1 cache with random replacement. A safe residency analysis needs to model this as a direct-mapped cache of 1/4 capacity, an obviously pessimistic scenario. We can assume that the true WCET is much closer to the observed that the calculated safe bound (but there's no proof of that).
We used this toolchain to optimise several of seL4's code paths and data structures to arrive at the above overall WCET.
We then worked on automatically determining sound loop bounds and infeasible-paths refutations, using a sequence of tools (Sequoll, Trickle). This was only partially successful, due to the above-explained challenges with static analysis of binary code.
The final, and most successful, approach leverages our translation validation framework to formally link the semantics-poor binary (which is the subject to the WCET analysis) to the semantics-rich C environment and all the theorems and invariants we have proved about the C code in the context of the functional correctness proof of seL4.
This allows us to add proofs of difficult loop bounds in the existing verification framework, and link those proofs to the binary in a high-assurance fashion. Once those manual proofs are added, the rest of the analysis is fully automated. The resulting toolset, called graph-to-graph, can analyse the WCET of the complete seL4 kernel (and other software) without manually supplying extra information.
With the move to out-of-order (OoO) processors with v7 of the architecture, Arm stopped publishing worst-case instruction latencies, and we could therefore no longer perform the analysis on recent Arm cores. This project is therefore archived (for now).
However, there is hope, in the form of open implementations of the RISC-V architecture, where all latency information can be obtained. An example is the CVA6 RV64 core (aka Ariane) developed by ETH Zurich. In principle, our WCET analysis can be resurrected for such cores. We are looking for funding for doing this!
Click here to download our tools used for computing the worst-case execution time of seL4 from here.
Gernot Heiser, firstname.lastname@example.org
The formally verified seL4 microkernel – a high-assurance foundation for MCS
Keynote at IEEE Conference on Embedded and Real-Time Computing and Applications, August, 2020
|Thomas Sewell, Felix Kam and Gernot Heiser|
High-assurance timing analysis for a high-assurance real-time OS
Real-Time Systems, Volume 53, Issue 5, pp. 812-853, September, 2017
Translation validation for verified, efficient and timely operating systems
PhD Thesis, UNSW, Sydney, Australia, 2017
|Thomas Sewell, Chi Kam and Gernot Heiser|
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
||Bernard Blackham, Mark Liffiton and Gernot Heiser|
Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 169–178, Berlin, Germany, April, 2014
Towards verified microkernels for real-time mixed-criticality systems
PhD Thesis, UNSW, Sydney, Australia, October, 2013
2013 ACM SIGBED Paul Caspi Memorial Dissertation Award and John Makepeace Bennett Award for Australasian Distinguished Doctoral Dissertation
||Bernard Blackham and Gernot Heiser|
Sequoll: A framework for model checking binaries
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), pp. 97–106, Philadelphia, USA, April, 2013
Best Paper Award
||Bernard Blackham, Vernon Tang and Gernot Heiser|
To preempt or not to preempt, that is the question
Asia-Pacific Workshop on Systems (APSys), pp. 7, Seoul, Korea, July, 2012
||Bernard Blackham, Yao Shi and Gernot Heiser|
Improving interrupt response time in a verifiable protected microkernel
EuroSys Conference, pp. 323–336, Bern, Switzerland, April, 2012
|Bernard Blackham, Yao Shi, Sudipta Chattopadhyay, Abhik Roychoudhury and Gernot Heiser|
Timing analysis of a protected operating system kernel
IEEE Real-Time Systems Symposium, pp. 339–348, Vienna, Austria, November, 2011
|Bernard Blackham, Yao Shi and Gernot Heiser|
Protected hard real-time: The next frontier
Asia-Pacific Workshop on Systems (APSys), pp. 5, Shanghai, China, July, 2011
|Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters|
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007
|Stefan M. Petters, Patryk Zadarnowski and Gernot Heiser|
Measurements or static analysis or both?
Workshop on Worst-Case Execution-Time Analysis, pp. 5–11, Pisa, Italy, December, 2007