Abstract
Worst-case execution time (WCET) estimation tools are complex pieces of software performing tasks such as computation on control flow graphs (CFGs) and bound calculation. In this paper, we present a formal verification (in Coq) of a loop bound estimation. It relies on program slicing and bound calculation.
The work has been integrated into the CompCert verified C compiler. Our verified analyses directly operate on non-structured CFGs. We extend the CompCert RTL intermediate language with a notion of loop nesting (a.k.a. weak topological ordering on CFGs) that is useful for reasoning on CFGs. The automatic extraction of our loop bound estimation into OCaml yields a program with competitive results, obtained from experiments on a reference benchmark for WCET bound estimation tools.
This work was supported by Agence Nationale de la Recherche, grant number ANR-11-INSE-003 Verasco.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Albert, E., Bubel, R., Genaim, S., Hähnle, R.: al. Verified resource guarantees using COSTA and KeY. In: PEPM 2011, pp. 73–76. ACM (2011)
Atkey, R.: Amortised resource analysis with separation logic. Logical Methods in Computer Science 7(2) (2011)
Ayache, N., Amadio, R.M., Régis-Gianas, Y.: Certifying and reasoning on cost annotations in C programs. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 32–46. Springer, Heidelberg (2012)
Barthe, G., Demange, D., Pichardie, D.: A formally verified SSA-based middle-end - Static Single Assignment meets CompCert. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 47–66. Springer, Heidelberg (2012)
Bedin França, R., Blazy, S., Favre-Felix, D., Leroy, X., et al.: Formally verified optimizing compilation in ACG-based flight control software. In: ERTS (2012)
Blackham, B., Shi, Y., Heiser, G.: Improving interrupt response time in a verifiable protected microkernel. In: Proc. of EuroSys, pp. 323–336. ACM (2012)
Blazy, S., Laporte, V., Maroneze, A., Pichardie, D.: Formal verification of a C value analysis based on abstract interpretation. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 324–344. Springer, Heidelberg (2013)
Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006, pp. 415–426. ACM Press (2006)
Ermedahl, A., Sandberg, C., Gustafsson, J., Bygde, S., Lisper, B.: Loop bound analysis based on a combination of program slicing, abstract interpretation, and invariant analysis. In: Workshop on WCET Analysis (2007)
Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Pottosin, I.V., Bjorner, D., Broy, M. (eds.) FMP&TA 1993. LNCS, vol. 735, pp. 128–141. Springer, Heidelberg (1993)
Gulwani, S.: SPEED: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 51–62. Springer, Heidelberg (2009)
Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The Mälardalen WCET benchmarks: Past, present and future. In: Proc. WCET 2010, pp. 137–147 (2010)
Gustafsson, J., Ermedahl, A.: Automatic derivation of path and loop annotations in object-oriented real-time programs. Scalable Computing: Practice and Experience 1(2) (1998)
Halbwachs, N., Henry, J.: When the decreasing sequence fails. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 198–213. Springer, Heidelberg (2012)
Heiser, G., Murray, T.C., Klein, G.: It’s time for trustworthy systems. IEEE Security & Privacy 10(2), 67–70 (2012)
Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107–115 (2009)
Ramalingam, G.: On loops, dominators, and dominance frontiers. ACM TOPLAS 24(5), 455–490 (2002)
Ranganath, V.P., Amtoft, T., Banerjee, A., Hatcliff, J., et al.: A new foundation for control dependence and slicing for modern program structures. ACM TOPLAS 29(5) (2007)
RTCA. DO-178C: Software considerations in airborne systems and equipment certification. Radio Technical Commission for Aeronautics Std. (2012)
Amtoft, T.: Slicing for modern program structures: a theory for eliminating irrelevant loops. Inf. Process. Lett. 106(2), 45–51 (2008)
Tristan, J.-B., Leroy, X.: A simple, verified validator for software pipelining. In: Proc. of POPL, pp. 83–92. ACM Press (2010)
Wasserrab, D., Lochbihler, A.: Formalizing a framework for dynamic slicing of program dependence graphs in Isabelle/HOL. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 294–309. Springer, Heidelberg (2008)
Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S.: al. The worst-case execution-time problem — overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7, 36:1–36:53 (2008)
Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blazy, S., Maroneze, A., Pichardie, D. (2014). Formal Verification of Loop Bound Estimation for WCET Analysis. In: Cohen, E., Rybalchenko, A. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2013. Lecture Notes in Computer Science, vol 8164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54108-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-54108-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54107-0
Online ISBN: 978-3-642-54108-7
eBook Packages: Computer ScienceComputer Science (R0)