Establish sound worstcase bounds on the execution time of all seL4 kernel operations.
Hard realtime systems, including mixedcriticality 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 worstcase execution times (WCET).
Such a WCET analysis must be sound and complete, meaning guaranteed to not underestimate 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 controlflow 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) offline analysis.
The analysis tool produces a set of integer linear equations that are fed into an ILP solver, which then produces candiate worstcase 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 mutuallyexclusive 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 worstcase paths produced by the tool to determine the kernel state and systemcall 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 4way L1 cache with random replacement. A safe residency analysis needs to model this as a directmapped 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 infeasiblepaths refutations, using a sequence of tools (Sequoll, Trickle). This was only partially successful, due to the aboveexplained challenges with static analysis of binary code.
The final, and most successful, approach leverages our translation validation framework to formally link the semanticspoor binary (which is the subject to the WCET analysis) to the semanticsrich 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 highassurance fashion. Once those manual proofs are added, the rest of the analysis is fully automated. The resulting toolset, called graphtograph, can analyse the WCET of the complete seL4 kernel (and other software) without manually supplying extra information.
With the move to outoforder (OoO) processors with v7 of the architecture, Arm stopped publishing worstcase 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 RISCV 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 worstcase execution time of seL4 from here.
Past

Gernot Heiser, gernot@unsw.edu.au

Gernot Heiser The formally verified seL4 microkernel – a highassurance foundation for MCS Keynote at IEEE Conference on Embedded and RealTime Computing and Applications, August, 2020  
Thomas Sewell, Felix Kam and Gernot Heiser Highassurance timing analysis for a highassurance realtime OS RealTime Systems, Volume 53, Issue 5, pp. 812853, 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, highassurance determination of loop bounds and infeasible paths for WCET analysis IEEE RealTime 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 RealTime and Embedded Technology and Applications Symposium (RTAS), pp. 169–178, Berlin, Germany, April, 2014  
Bernard Blackham Towards verified microkernels for realtime mixedcriticality 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 RealTime 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 AsiaPacific 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 RealTime Systems Symposium, pp. 339–348, Vienna, Austria, November, 2011  
Bernard Blackham, Yao Shi and Gernot Heiser Protected hard realtime: The next frontier AsiaPacific 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 WorstCase ExecutionTime Analysis, pp. 5–11, Pisa, Italy, December, 2007 