11 Control Flow Constraints

The control flow constraints have for goal to bind the control flow to some axiomatic rules in order to better approximize the real sets of execution paths of the application (this problem is also called "infeasible paths").

11.1 Issues

Basically, a control constraint is an equation between the execution counts in WCET of different part of the code. This simple definition induces two issues:

1. the way the equations are implemented (some solver as ILP often used in WCET computation only linear equations): a straight-forward answer is to ignore too complex equations as it does only worsen the WCET approximation,

2. the semantics of the equations: what is the meaning of an equation whose the execution count are parts of code duplicated in different contexts ?

Another definition of control flow equations would include data in the variable of the equation. Such an extension is currently considered as too complex and is not covered by the current document.

11.2 Execution Count in Different Contexts

Le's take a simple example in C:

int t = 0;
void f(int n) {
  for(int i = 0; i < n; i++)
    /* block 1 */
  for(int i = 0; i < n && t < 100; i++) {
    /* block 2 */
    t = t + 1;
  }
}

int main(void) {
  ...
  f(80);  // call 1
  ...
  f(80); // call 2
  ...
}

And lets take the following constrains on the execution count of block 1 and block 2 (x_i is the number of times the block i is executed):

x_1 <= 80   // eq. (1)
x_2 <= 100 // eq. (2)

The questions is now: does eq. (1) means that throughout the whole execution of the program, the block 1 is executed a total of 80 times or the block is executed 80 times each time the function f is called? In this case, the latter interpretation is the right one. Conversely, the eq. (2) must be interpreted according to the first assertion.

A way is required to disambiguate the interpretation of the equation. FFX proposes to interpret the equation according to its context of definition. For example, eq. (1) must be put in the definition of function f as it has to be instantiated for each invocation of f:

<flowfacts>
  ...
  <function name="f">
    <control-constraint><le><count id="block-1"/><const int="80"/></le></control-constraint>
  </function>
  ...
</flowfacts>

The eq. (2) must be put in the entry point of the task, main, to takes into account it applies on all invocation of f:

<flowfacts>
  ...
  <function name="main">
    <control-constraint><le><count id="block-2"/><const int="100"/></le>    
  </function>
</flowfacts>

In the case of analysis with duplication of function f used to improve the precision of the WCET, we get two instances of f and two instances of block 1, 1a and 1b, and of block 2, 2a and 2b. The equations will become:

x_1a <= 80
x_1b <= 80
(x_2a + x_2b) <= 100

This is exactly the semantics supported by the initial equations.

11.3 Syntax

The syntax of control flow constraints is displayed below:

CONTROL-CONSTRAINT ::=
  <control-constraint> CONTROL-PREDICATE </control-constraint>

A control predicate is either a relation, or the composition of equations by AND and OR.

CONTROL-PREDICATE ::=
  | CONTROL-RELATION
  | <and> CONTROL-RELATION+ </and>
  | <or> CONTROL-RELATION+ </or>

A control relation is a comparison between two formulas whose variables represents the execution count of some part of the code in the case of the WCET.

CONTROL-RELATION ::=
  | <eq> CONTROL-FORMULA CONTROL-FORMULA </eq>
  | <ne> CONTROL-FORMULA CONTROL-FORMULA </ne>
  | <lt> CONTROL-FORMULA CONTROL-FORMULA </lt>
  | <le> CONTROL-FORMULA CONTROL-FORMULA </le>
  | <gt> CONTROL-FORMULA CONTROL-FORMULA </gt>
  | <ge> CONTROL-FORMULA CONTROL-FORMULA </ge>

The control formula are usual mathematics formula supporting variables representing execution count.

CONTROL-FORMULA ::=
  | <int>INT</int>
  | <count ref="TEXT"/>
  | <neg> CONTROL-FORMULA </neg>
  | <add> CONTROL-FORMULA CONTROL-FORMULA </add>
  | <sub> CONTROL-FORMULA CONTROL-FORMULA </sub>
  | <mul> CONTROL-FORMULA CONTROL-FORMULA </mul>
  | <div> CONTROL-FORMULA CONTROL-FORMULA </div>

The formulas may be integer constants, execution count (describes below), negation with one formula operand or binary operators with two operands (respectively addition, subtraction, multiplication or division).

The count identifies a part of code and, more exactly, the number of times this part is executed. It references a block defined in the activated context tree or at the top level.

Notice that the formulation computation is only performed in the integer domain.

11.4 Building of Constraints

From the analyses of paragraph 1, it results that a constraint is duplicated as many as its context is duplicated by the WCET analysis. It remains to precise how the duplication of the constrains are instantiated according to their context.

Lets define a block identification by its block identifier i and its context path, p. Lets the path of the constraint be q. The constraint may be viewed as a function f(x1, x2, ⋯) where is a count variable. The problem is to match the with the variables produces by the WCET analyses and computation. According to the instanciation of each block, the variable may remain unique or duplicated in versions. In the latter case, the variable is simply replaced by the sum of :

But not all instances of needs to be involved according to the position of block i and its contextual path p. If q is a prefix of p, that is the block i a sub-block of the context containing the constraint, only the execution count that are called from the context containing the constant are used.

If q is not a prefix of p, then any matching the contextual path p in the program is used.