WCET: Worst-Case Execution-Time Analysis of seL4

Aim

Establish sound worst-case bounds on the execution time of all seL4 kernel operations.

Overview

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.

General Approach

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.

Main challenges:

Providing sound loop bounds (see above). Static analysis is generally unable to bound all loops, even where bounds exist. The core reason is that much of the original program semantics is lost in the compilation process, and cannot be recovered from just analysing the binary. A common cause is that the binary analysis cannot determined whether two pointers alias.
Refuting infeasible paths (see above). Similar to loop bounds, refuting all infeasible paths requires knowlege of program semantics that is not available in the binary.
Cache analysis. The latency of memory operations (loads, stores and instruction fetches) depends on whether a particular data item is resident in the cache. Without a residency analysis, the safe assumption is that each memory access results in a cache miss. This would result in massively pessimistic WCET bounds.
Scalability of the analysis. Most sound WCET analysis is conducted on small programs, such as the Mälardalen WCET benchmarks or unprotected RTOSes, all comprising a few 100s of SLOC. In contrast, the seL4 kernel is of the order of 10 kSLOC.

Our approach and results

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.

Status

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!

Downloads

Click here to download our tools used for computing the worst-case execution time of seL4 from here.

People

Past

Bernard Blackham
Chi Kam
Gernot Heiser
Thomas Sewell
Yao Shi

Contact

Gernot Heiser, gernot@unsw.edu.au

Publications

		Gernot Heiser 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
		Thomas Sewell 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
		Bernard Blackham 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

Trustworthy Systems