Trustworthy Systems

Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis

Authors

Thomas Sewell, Chi Kam and Gernot Heiser

NICTA

UNSW

Outstanding Paper award

Abstract

Worst-case execution time (WCET) analysis of real-time code needs to be performed on the executable binary code for soundness. Determination of loop bounds and elimination of infeasible paths, essential for obtaining tight bounds, frequently depends on program state that is difficult to extract from static analysis of the binary. Obtaining this information generally requires manual intervention, or compiler modifications to preserve more semantic information from the source program.

We propose an alternative approach, which leverages an existing translation-validation framework, to enable high-assurance, automatic determination of loop bounds and infeasible path. We show that this approach automatically determines all loop bounds as well as many (possibly all) infeasible paths in the seL4 microkernel, as well as in standard WCET benchmarks which are in the language subset of our C parser.

BibTeX Entry

  @inproceedings{Sewell_KH_16,
    address          = {Vienna, Austria},
    author           = {Sewell, Thomas and Kam, Felix and Heiser, Gernot},
    booktitle        = {IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)},
    keywords         = {wcet, sel4, real-time, translation validation},
    month            = apr,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/9118.pdf},
    title            = {Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for {WCET} Analysis},
    year             = {2016}
  }

Download