In a previous post I described two extensions to CompCert’s memory model that I implemented during my visit at Gallium. Another thing I have been working on is non-determinism and sequence points in C. As some of you will know, the evaluation order of expressions is not specified by the C standard. This allows a compiler to pick its preferred evaluation strategy. To allow a compiler also to delay side-effects, and to interleave evaluation, the allowed non-determinism is slightly restricted.

Let us take a look at the following example.

int x = 0;
int main() {
  printf("%d ", (x = 3) + (x = 4));
  printf("%d\n", x);
  return 0;
}

By considering all possible evaluation paths, one would naively expect this program to print either 7 4 or 7 3, depending on whether x = 3 or x = 4 is evaluated first. However, the C standard does not allow an object to be modified more than once (or being read after being modified) between two sequence points. A sequence point occurs at the end ; of a full expression, before a function call, after the first operand of the conditional ? : operator, and in some other situations. Therefore, this program gives rise to a sequence point violation and exhibits undefined behavior. It thus may do literally anything, and indeed, gcc -O1 (version 4.7.2) prints 8 4 which does not correspond to one of the evaluation paths.

Notice that non-determinism in C is even more unrestrained than some may think. That the evaluation order in e1 + e2 is unspecified, does not mean that either e1 or e2 will be evaluated entirely before the other. Instead, it means that evaluation can be interleaved; first a part of e1 could be evaluated, then a part of e2, then another part of e1, … Hence, the following program is also allowed to print bac.

int main() {
  printf("a") + (printf("b") + printf("c"));
  return 0;
}

Dealing with sequence point violations

The executable C semantics by Chucky Ellison and Grigore Rosu provides a nice tool to explore non-deterministic behavior in C and is able to dynamically detect sequence point violations. Since CompCert also has an interpreter, I created an extension of CompCert that allows the interpreter to be used to detect sequence point violations as well.

As CompCert C already supports non-deterministism in expressions, it was fairly easy to extend Ellison and Rosu’s approach to sequence point violations to CompCert. I added a set L of locked locations to CompCert’s execution state. Whenever a write is performed, the address of that write is added to set L. If a read or write to an address contained in L is performed, it results in undefined behavior. At a sequence point, the set L is emptied.

Since CompCert picks a reduction strategy in one of its first compilation passes, and my extension removes the sequence point restriction quickly after, it did effect the rest of the compilation passes of CompCert. Since it remains an open (and not easy) question how CompCert could take advantage of sequence point violations to perform more aggressive optimizations, my extension is not part of the official CompCert code.

Many tools for verifying C programs also determinize programs in one of their first passes, and let the user verify the determinized program. When solely targeting a specific compiler (for example CompCert) for which the evaluation strategy is known, and which is known not to do any interleaving or delaying of side-effects, this approach works. But to claim something about the correctness of the program when being compiled with another compiler, this approach does not work, even if all possible evaluation paths are considered (see the counter example in gcc above).

Some tools will perform syntactical checks to exclude some sequence points violations. But as it is undecidable whether a sequence point violation may occur, determinization, possibly combined with such checks, is either unsound (slides 13 and 15 of Ellison and Rosu’s POPL 2012 talk present some examples in existing tools), or will exclude many valid C programs.

To indicate why this is undecidable, consider:

int* f() { \\ arbitrary code }
int x = 0;
int main() {
  int *p = f();
  printf("%d\n", (x = 3) + (*p = 10));
  return 0;
}

Deciding whether a sequence point violation occurs is equivalent to deciding whether f() returns a pointer equal to &x.

As I wish to use my own semantics not only to verify programs compiled by CompCert, having better means of reasoning about programs with non-determinism and sequence points is needed.

An axiomatic semantics

As a step towards taking non-determinism and sequence points seriously, I developed an axiomatic semantics for expressions that takes these issues into account. The key idea of my axiomatic semantics is that non-deterministic expression evaluation corresponds to (a weak form) of concurrency. Separation logic is well capable of dealing with concurrency, so my rule for the addition operator is based on the rule for parallel composition.

{ Pl } el { Ql }      { Pr } er { Qr }
--------------------------------------
    { Pl * Ql } el + er { Pr * Qr }

The idea is that, if the memory can be split up (using the separating conjunction *) into two disjoint parts, in which el respectively er can be evaluated safely, then el + er can be evaluated safely in the whole memory.

Obviously, as stated, this rule is too simple for the addition operator. First of all, expressions yield a result, so the post-condition should not just be an assertion, but should also tell something about the result. To that end, we let the post-condition Q be a function from values to assertions. Intuitively, { P } e { Q } means that if evaluation of e yields a value v, then the assertion Q v should hold afterward.

Second of all, we have to take care of undefined behavior by integer overflow. This gives rise to the following revised rule:

{ Pl } el { Ql }   { Pr } er { Qr }   ∀ vl vr, (Ql vl * Qr vr) → (vl + vr ⇓-)
-----------------------------------------------------------------------------
    { Pl * Pr } el + er { λ v', ∃ vl vr, vl + vr ⇓ v' ∧ (Ql vl * Qr vr) }

Here, the assertion vl + vr ⇓- ensures that adding vl to vr does not overflow, and the assertion vl + vr ⇓ v' states that v' is the result of adding vl to vr.

In order to make this rule sufficiently powerful, a strong version of the separating conjunction * is needed. After all, it should be possible to prove the correctness of programs like x = x + x. Fractional permissions allow memory cells that are solely used for reading to be used in both operands of the separating conjunction *.

To take care of sequence point violations, we include a special locked permission. In order to perform a write or a read, one has to prove that the permission of the location to be written to (respectively read from) is not locked. This is captured by the following rule for assignments.

                                      Write ⊆ perm_kind γ
{ Pl } el { Ql }   { Pr } er { Qr }   ∀ a v, (Ql a * Qr v) → (a ↦{γ} - * R a v)
-------------------------------------------------------------------------------
          { Pl * Pr } el ::= er { λ v, ∃ a, a ↦{lock γ} v * R a v }

As standard in separation logic with permissions, the assertion of a singleton memory e1 ↦ e2 is extended with its permission γ, resulting in e1 ↦{γ} e2. Hence, this rule requires the permission of the memory cell to be sufficient before the write, and will lock the memory cell after.

In the operational semantics, a sequence point results in the set of locked locations being emptied. Xavier Leroy helpfully remarked to me that “a sequence point is just an assignment to the dummy variable of locked locations”. This is captured by the following rule.

{ P } e { λ v, P' v ▷ }    { is_true P' } el { Q }   { is_false P' } er { Q }
-----------------------------------------------------------------------------
                       { P } e ? el : er {{ Q }}

Here the assertion R ▷ empties the set of locked locations, and its semantic interpretation is basically an assignment of the empty set to the set of locked locations.

Adapting the operational semantics

Unfortunately, the way my axiomatic semantics deals with sequence point violations does not correspond well to the operational semantics. In the operational semantics, a sequence point results into the set of locked locations being emptied globally, whereas the axiomatic semantics only talks about a local part of the memory.

Hence, I defined another operational semantics that make sequence points local. Instead of unlocking all locations at a sequence point, it only unlocks locations that have been locked in subexpressions of the expression where the sequence point occurred. To achieve this, values val@{Ω} v of the expression syntax are annotated with a set of locked locations Ω. Initially, all values in the program should have the empty set of locked locations. Whenever a write occurs, not only is the written location locked in memory, it is also added to set Ω of the specific subexpression where the write occurred. On a sequence point, just the annotated locations Ω in the specific subexpression where the sequence point occurred are unlocked. Connectives without a sequence point just take the union of the locked locations of their children.

For example, my operational semantics contains the following rules

ptr@{Ωl} b := val@{Ωr} v, m ⇒ val@{ {[b]} ∪ Ωl ∪ Ωr} v, lock b (<[b:=v]>m)
   provided that is_writable m b

val@{Ω} v ? el : er, m ⇒ er, unlock Ω m
   provided that value_false v

As one can see here, the rule for the assignment not only locks the location b, it also adds it to the locations to be unlocked in the expression. Notice that the predicate is_writable m b also ensures that b is not locked.

This way of dealing with sequence points is more restrictive than Ellison/Rosu’s approach. For example, my semantics makes

int x, y, *p = &y;
int f() { if (x) { p = &x; } return 0; }

int main() {
  int r = (x = 1) + (*p = 2) + f();
}

undefined. The path that leads to undefined behavior is 1.) x = 1 2.) call f which changes p to &x, 3.) *p = 1. Here, the lock of &x survives the function call. In the semantics of Ellison/Rosu, this program has defined behavior, as the sequence point before the function call destroys all locks, so also the lock of &x.

I am still wondering whether my semantics excludes any non artificial programs. Keep in mind that the following program has defined (but non-deterministic) behavior in my operational semantics (as one would expect).

int x;
int f(int y) { return (x = y); }
int main(void) {
  printf("%d\n", f(3) + f(4));
  return 0;
}

Future work

Currently I have two versions of an operational semantics for sequence points: one as an extension of CompCert, and a more restrictive version as part of my own development. For the last one I also have an axiomatic semantics (and a formally verified soundness proof).

I intend to prove that CompCert is an instance of my semantics in future work. In my previous post I described two extensions of CompCert that will be needed for this correspondence.

An important next step is to make the axiomatic more suitable to be used for a verification condition generator.

Sources

The sources of my extensions to CompCert can be found at my github repository, and the sources and documentation of my axiomatic semantics can be found here.