Trustworthy Systems

Protected hard real-time: The next frontier

Authors

Bernard Blackham, Yao Shi and Gernot Heiser

NICTA

UNSW

Abstract

Hard real-time systems are typically written to execute either on bare metal or on a small real-time executive that offers no memory protection. This model scales poorly as systems become more complex and integrated, as is the trend in industry today. Designing hard real-time systems on a protected OS is often avoided due to the difficulty in predicting its response time. Hard real-time systems with full virtual memory and memory protection have been proposed previously. However, to our knowledge, no such system has determined safe upper bounds on the latency introduced by this protection. This paper proposes that hard real-time systems can be constructed confidently and cost-effectively using an operating system providing full memory protection and virtual memory. We contend that a carefully written microkernel providing these mechanisms has the ability to be used in a hard real-time system without overly pessimistic response time guarantees. We use the seL4 microkernel as a case study, investigating how the features of seL4’s design enable a highly accurate WCET analysis.

BibTeX Entry

  @inproceedings{Blackham_SH_11,
    address          = {Shanghai, China},
    author           = {Blackham, Bernard and Shi, Yao and Heiser, Gernot},
    booktitle        = {Asia-Pacific Workshop on Systems (APSys)},
    keywords         = {wcet, microkernels, trusted systems, real-time systems},
    month            = jul,
    pages            = {5},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4862.pdf},
    publisher        = {ACM},
    title            = {Protected Hard Real-time: The Next Frontier},
    year             = {2011}
  }

Download