Flow Facts Specification & Transformation

The execution time of a program (on a given hardware) is largely determined by its control flow. Here, control flow means the execution order of instructions or basic blocks, as represented by a program's control flow graph. In typical programs, control flow is expressed using constructs like, e.g., loops or (conditional) branches.

In general, static WCET analysis is undecidable since it is undecidable to compute how many times a general loop iterates. Since loop iteration counts are crucial for a precise WCET analysis, and since they can not be computed for arbitrary loops in general, loop iteration counts need to be specified by the user of a WCET analyzer.

Besides loops known from high-level programming languages, any circle within a program's control flow graph needs to be annotated manually by the user. Any such user-provided annotations specifying the control flow are usually called flow facts. This page explains the mechanisms for flow facts specification and transformation within WCC:

According to related literature, flow facts give hints about the set of possible execution paths of a program. In general, a static WCET analyzer requires the following kinds of flow facts to perform WCET analysis:

  • Loop iteration counts
  • Recursion depths
  • Execution frequency of an instruction, relative to some other instruction

Specification of Flow Facts

The WCET analyzer requiring flow facts for static timing analysis operates on executable code as already discussed previously. Hence, all flow facts finally passed to aiT have to be formulated at machine code level. However, in the context of aiT being used within WCC, this is extremely cumbersome for a WCC user. For the compiler user, it is highly desirable to reason only about a piece of C source code, and not about the assembly-level code structures, WCC generates. Thus, it has to be possible to specify flow facts at the source code level.

WCC fully supports source-level flow facts by means of ANSI-C pragmas. Using WCC, the user can annotate C source codes using either Loop Bound or Flow Restriction flow facts.

Loop Bounds

Loop bounds allow to specify the minimum and maximum iteration counts for each loop and have the following structure:

  LOOPBOUND       |= loopbound min NUM max NUM
  NUM             |= Non-negative Integer

Loop bound flow facts provide an easy means to annotate regular for-, while do- and do while-loops having well-defined lower and upper bounds. For data-dependent loops having a variable iteration count, WCCs loop bound annotations allow to specify an interval of possible iteration counts.

For example, the following snippet of C code specifies that the shown loop body is executed exactly 100 times:

  _Pragma( "loopbound min 100 max 100" )
  for ( Index = 1; Index <= 100; Index++ )
    Array[ Index ] = Index * fact * KNOWN_VALUE;

Flow Restrictions

For irregular loops (e.g., non-rectangular loops, multi-entry loops, loops without explicit termination condition or loops formulated using labels and goto-statements), loop bound annotations are inapplicable. For such irregular control flow structures, WCC provides flow restriction annotations allowing to relate the execution frequency of one C statement with the execution frequency of another statement.

In order to use flow restrictions, some auxiliary annotations called markers are required which attach an identifying string to some source code statement:

  MARKER          |= marker NAME
  NAME            |= Identifier

For example, the following piece of code attaches the identifier outermarker for further use to a source code statement:

  _Pragma( "marker outermarker" )
  Statement A;

Using the identifiers specified by markers, complex flow restriction annotations can be defined according to the following EBNF syntax:

  FLOWRESTRICTION |= flowrestriction SIDE COMPARATOR SIDE
  COMPARATOR      |= >= | <= | =
  SIDE            |= SIDE + SIDE | NUM * REFERENCE
  REFERENCE       |= NAME | Function Name

Basically, flow restrictions allow to specify any linear dependency between an arbitrary amount of different positions in the C source code. For example, a flow restriction as shown below is useful to annotate a triangular loop:

  _Pragma( "marker outermarker" )
  Statement A;

  for ( i = 0; i < 10; i++ )
    for ( j = i; j < 10; j++ )
      _Pragma( "marker innermarker" )
      Statement B;

  _Pragma( "flowrestriction 1*innermarker <= 55*outermarker" );