Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution. (English) Zbl 1356.68041

Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob

J. Symb. Comput. 80, Part 1, 101-124 (2017).

Summary: Embedded real-time software systems (ESS) play an important role in almost every aspect of our daily lives. We do rely on them to be functionally correct and to adhere to timing-constraints ensuring that their computational results are always delivered in time. Violations of the timing-constraints of a safety-critical ESS, such as an airplane or a medical control device, can have disastrous economic and social consequences. Identifying and correcting such violations is therefore an important and challenging research topic. In this article we address this challenge and describe a rigorous approach for the timing analysis of programs and for proving its results precise.
In practice most important is the worst-case execution time (WCET) of an ESS, that is, the maximal running time of the system on a specified hardware. A WCET analysis needs to provide a formal guarantee that a system meets its timing-constraints even in the worst case. This requires to compute a safe and tight bound for the execution time of a program. Existing WCET tools, however, are usually not able to guarantee that there is a feasible system trace that takes indeed as long as stated by the computed execution time bound: often, due to the employed abstractions during static analysis a computed WCET bound overestimates the actual WCET bound, since loop bounds and other timing-relevant program properties their computation is based on are computed for spurious infeasible system traces that can be ruled out by a path-sensitive program abstraction and analyzing program resources.
In this article we present an approach for inferring and proving WCET bounds precise. This approach guarantees that the WCET bound is computed for a feasible system trace. This is achieved by combining WCET computation with path-wise symbolic execution in an abstraction refinement loop. This way, symbolic execution can be targeted and limited to relevant program parts thereby taming and avoiding the usually prohibitive computational costs of symbolic execution with a full path coverage. Moreover, our approach improves the quality of the underlying WCET analysis, since it automatically tightens the bound until it is proven precise, thereby improving the precision of the initially computed WCET bound.
Our overall approach is an anytime algorithm, i.e., it can be stopped at any time without violating the soundness of its results. If run until termination, the WCET bound is proven precise, by automatically inferring additional constraints from spurious traces and using these constraints in the abstraction refinement. We implemented our approach in the \(r\)-TuBound WCET toolchain and tested it on challenging benchmarks from the WCET community. Our experimental results underline the advantage of using symbolic methods for proving WCET bounds precise, at a moderate cost.

MSC:

68N30	Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68W30	Symbolic computation and algebraic computation

Keywords:

worst-case execution time (WCET) analysis; static symbolic execution; symbolic computation

Software:

OTAWA; Smacc; r-TuBound; KLEE; LLVM; lp_solve; Stony Brook; STP; Boolector

References:

[1]	Ballabriga, C.; Casse, H.; Rochange, C.; Sainrat, P., OTAWA: an open toolbox for adaptive WCET analysis, (Proc. of IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems, SEUS, (October 2010), Springer Austria)
[2]	Bang, H. J.; Kim, T. H.; Cha, S. D., An iterative refinement framework for tighter worst-case execution time calculation, (Proc. of ISORC, (2007)), 365-372
[3]	Berkelaar, M.; Eikland, K.; Notebaert, P., Lp_solve. software, (2004)
[4]	Biere, A.; Knoop, J.; Kovács, L.; Zwirchmayr, J., Smacc: a retargetable symbolic execution engine, (Proc. of ATVA, (2013)) · Zbl 06314180
[5]	Boddy, M. S., Anytime problem solving using dynamic programming, (Proc. of AAAI, (1991)), 738-743
[6]	Bodík, R.; Gupta, R.; Soffa, M. L., Refining data flow information using infeasible paths, SIGSOFT Softw. Eng. Notes, 22, 6, 361-377, (Nov. 1997)
[7]	Brandner, F.; Jordan, A., Subgraph-based refinement of worst-case execution time bounds, (2014), Tech. Rep. hal-00978015 (version 1), ENSTA · Zbl 1308.68024
[8]	Brummayer, R.; Biere, A., Boolector: an efficient SMT solver for bit-vectors and arrays, Lecture Notes in Computer Science (LNCS), vol. 5505, 174-177, (2009), Springer, TACAS’09
[9]	Cadar, C.; Dunbar, D.; Engler, D. R., KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs, (OSDI, (2008)), 209-224
[10]	Cadar, C.; Ganesh, V.; Pawlowski, P. M.; Dill, D. L.; Engler, D. R., EXE: automatically generating inputs of death, (Proc. of CCS, (2006)), 322-335
[11]	Spitzer, Cary R., The avionics handbook, The Electrical Engineering Handbook Series, (2001), CRC Press Llc
[12]	Cassé, H.; Birée, F.; Sainrat, P., Multi-architecture value analysis for machine code, (Proc. of WCET, (2013)), 42-52
[13]	Cerny, P.; Henzinger, T.; Radhakrishna, A., Quantitative abstraction refinement, (Proc. of POPL, (2013)), 115-128 · Zbl 1301.68244
[14]	Chattopadhyay, S.; Roychoudhury, A., Scalable and precise refinement of cache timing analysis via model checking, (Proc. of RTSS, (2011)), 193-203
[15]	Chattopadhyay, S.; Roychoudhury, A., Scalable and precise refinement of cache timing analysis via path-sensitive verification, Real-Time Syst., 49, 4, 517-562, (2013) · Zbl 1291.68068
[16]	Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement, (Proc. of CAV, (2000)), 154-169 · Zbl 0974.68517
[17]	Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Proc. of POPL, (1977)), 238-252
[18]	The C++ front end, (1992)
[19]	Gustafsson, J., SWEET: swedish execution time tool, (2001)
[20]	Gustafsson, J., SWEET manual, (2013)
[21]	Gustafsson, J.; Betts, A.; Ermedahl, A.; Lisper, B., The Mälardalen WCET benchmarks: past, present and future, (Proc. of WCET, (2010)), 136-146
[22]	Kebbal, D.; Sainrat, P., Combining symbolic execution and path enumeration in worst-case execution time analysis, (Proc. of WCET, (2006))
[23]	Kirner, R., The WCET analysis tool calcwcet167, (Proc. of ISoLA (2), vol. 12, (2012)), 158-172
[24]	Knoop, J.; Kovács, L.; Zwirchmayr, J., Symbolic loop bound computation for WCET analysis, (Proc. of PSI, (2011)), 116-126
[25]	Knoop, J.; Kovács, L.; Zwirchmayr, J., R-tubound: loop bounds for WCET analysis, (Proc. of LPAR, LNCS, vol. 7180, (2012)), 435-444
[26]	Knoop, J.; Kovács, L.; Zwirchmayr, J., WCET squeezing: on-demand feasibility refinement for proven precise WCET-bounds, (Proc. of RTNS, (2013)), 161-170
[27]	Lattner, C.; Adve, V. S., LLVM: a compilation framework for lifelong program analysis & transformation, (Proc. of CGO, (2004)), 75-88
[28]	Li, Y.-T. S.; Malik, S.; Wolfe, A., Efficient microarchitecture modelling and path analysis for real-time software, (Proceedings of the 16th IEEE Real-Time Systems Symposium, (Dec. 1995)), 254-263
[29]	The rose compiler: an open source compiler infrastructure, (2000)
[30]	Milinkovich, M., ERTS 2014 keynote speech: what can industry learn from open source development, (Feb. 6th 2014), Last accessed: 2014-03-04
[31]	Muchnick, Steven S., Advanced compiler design and implementation, (1997), Morgan Kaufmann Publishers
[32]	Nielson, F.; Nielson, H. R.; Hankin, C., Principles of program analysis, (1999), Springer-Verlag New York, Inc., Secaucus, NJ, USA · Zbl 0932.68013
[33]	Prantl, A., The termite library, (2008)
[34]	Prantl, A.; Knoop, J.; Schordan, M.; Triska, M., Constraint solving for high-level WCET analysis, (2009), CoRR
[35]	Prantl, A.; Schordan, M.; Knoop, J., Tubound - a conceptually new tool for worst-case execution time analysis, (Proc. of WCET’08, vol. 8, (2008))
[36]	Puschner, P. P.; Schedl, A. V., Computing maximum task execution times - a graph-based approach, Real-Time Syst., 13, 1, 67-91, (July 1997)
[37]	Schordan, M.; Barany, G.; Prantl, A.; Pavlu, V., Satire - the static analysis tool integration engine, (2007)
[38]	Skiena, S. S., The algorithm design manual, (2008), Springer Publishing Company, Incorporated · Zbl 1149.68081
[39]	Souyris, J.; Pavec, E. L.; Himbert, G.; Jégu, V.; Borios, G., Computing the worst case execution time of an avionics program by abstract interpretation, (Proc. of WCET, (2005)), 21-24
[40]	Zolda, M.; Kirner, R., Compiler support for measurement-based timing analysis, (Proc. of WCET, (2011)), 62-71