The annotation language of TuBound v0.6

Introduction

TuBound [PSK08] is portable tool for high-level worst-case execution time (WCET) analysis of C++ programs developed at Vienna University of Technology. The design philosophy behind TuBound was to increase the productivity of the programmer by allowing for high-level annotations to be placed at the source code and by reducing the need for manual annotation through a strong support of static analysis.

Annotations in TuBound serve two purposes: At first, they provide a programmer-friendly user interface to support the timing analysis with domain-specific knowledge; secondly, they are a textual intermediate representation for automatically generated results generated by the static program analysis component. Since the result of the static analysis is attached to the program source code, the programmer can inspect it and then decide where to manually refine the annotations, thus keeping the amount of human intervention at a minimum.

Annotation syntax and source code integration

TuBound uses the #pragma-directive to embed annotations into C++ sources. With this mechanism, it is possible to place an annotation at each sequence point of the program. As of version 1.0, annotations comprise the following four types:

1. Loop bounds are the most basic type of annotation available in TuBound. For a successful timing analysis it is mandatory that every loop construct contains such an annotation. Loop bound annotations can be located anywhere inside the scope of the loop body and always refer to the loop construct that directly dominates the lexical scope containing the annotation.

   The annotation consists of a numerical expression that denotes an upper bound for the number of times a loop is executed in relation to the number of times the basic block that dominates the loop entry is executed. By convention, a special loop bound of -1 is used to indicate an endless (main-)loop.

2. Markers are a concept closely related to labels to identify addressable units in the program. A marker creates a symbolic name for a basic block that can be used in constraint specifications. A marker is always associated a scope, defaulting to the global scope.
3. Constraints are the most generic and powerful annotation concept supported by TuBound. They allow to express arbitrary relations between the execution counts of basic blocks, referred to via markers.
4. (Marker-)scopes declarations are syntactic sugar to reduce the amount of typing when doing manual annotation. Consider two basic blocks b₁,b₂ where b₁ dominates b₂: An incidence of a marker m_2loc ∈ b₂ with a scope of b₂ is equivalent to the expression m₂*m₁, where m₂ ∈ b₂ and m₁ ∈ b₁ are a global markers.

Figure 1 shows an example utilizing different types of annotation mechanisms to express the same fact that the loop construct is executed up to 42 times upon entering the parent scope. The formal EBNF-style grammar of annotation pragmas is given in Figure 2.

---

    { 
    # pragma wcet_marker(m1)
      do {
    #   pragma wcet_marker(m2)
    #   pragma wcet_marker(m3)
    #   pragma wcet_scope(m3)
     
    #   pragma wcet_constraint( m2 =< m1*42 ) // [1]
    #   pragma wcet_constraint( m3 =< 42 )    // [2]
    #   pragma wcet_loopbound(42)             // [3]
        ...
      } while (!done);
    }
  

Figure 1: Three annotations carrying the same information

---

---

Figure 2: Grammar of annotations

---

References

[PSK08]

Adrian Prantl, Markus Schordan, and Jens Knoop. TuBound – A Conceptually New Tool for Worst-Case Execution Time Analysis. In 8th International Workshop on Worst-Case Execution Time Analysis (WCET 2008), Prague, Czech Republic, 2008.

This document was translated from L^AT_EX by H^EV^EA.