JTC1/SC22/WG14 N927

WG14/N927

Another Formalism for Sequence Points
=====================================

D. Hugh Redelmeier
hugh@mimosa.com
2000 November 17

The current concept of sequence points in the C Standard is intended
to allow the description of certain race conditions in the evaluation
of expressions.  It seems to have failed to yield a precise
definition.  So here is a sketch of a different approach.

The original version of this was much simpler and cleaner.
Unfortunately, it did not capture several important details of C.  It
is not evident to me whether this version is simple and clean enough
to be useful.


The Problem
===========

There are two forms of race condition that yield undefined behaviour
in expression evaluation:

    If two settings of the same object cannot be proven to be disjoint
    in time, the evaluation is considered undefined.  Example:

            (x = 1) * (x = 2)

    If a fetch of an object cannot be proven to be before or after a
    setting of that object, the evaluation is considered undefined.
    Example:

            (x = 1) * x

There is a special rule for function calls that causes otherwise
undefined behaviour to be only unspecified:

    The execution of two functions is never interleaved.  Even if the
    order two function invocations is not specified, one will
    certainly complete before the other starts.

Whether the evaluation of an expression has a race condition is a
property that cannot always be determined without performing at least
parts of that evaluation -- it is not always a static property of the
expression.


The Approach
============

The process of determining whether an expression has a race condition
is fairly tricky to describe, so we fall back on a formal description.
We tie our analysis to an abstract syntax tree (AST) of the
expression.  In effect, our determination is a kind of evaluation of
the expression, but it yields something other that conventional
values.

There are three kinds of evaluation of C expressions (including
subexpressions).
- for a value (which may then be discarded!)
- for an lvalue
- for a sizeof (for now, we'll ignore this case; the only interesting
  issues involve VLAs)

Our determination procedure will calculate, for each subtree in the AST,
properties of the usage of each object.  We chose to represent these
properties by membership in sets (this isn't the only possible way).

The goal is to determine what objects have bad properties (i.e. are
involved in race conditions).


Properties of Object Usage
==========================

There are only two properties we are interested in (Undefined and
Unspecified), but our calculation will require the use of a number of
other properties.

The sets that represent properties will have objects as members.
Since C allows objects to overlap in interesting ways, we actually
need to have each byte of each object be separately included.  This
may not be enough for bitfields -- it may be necessary to go down to
the bit level.  For our purposes, a register can be considered a
(possibly large) single byte object.

The sets we need to know for each subtree include:
    Race: (the set of bytes of) objects for which the expression has a race
    Set: objects set by the evaluation
    Fetched: objects fetched by the evaluation

For subtrees that are evaluated for an lvalue, we also need:
    Obj: (the set of bytes of) the object designated by the lvalue

These properties are not mutually exclusive, so an object can be in
any or all of the sets at the same time.

Unfortunately, the properties listed above turn out to be too
simplistic.  We need to keep track of more detailed information.

Instead of Race, we need Unspecified and Undefined to distinguish the
two kinds of race condition.  Furthermore, we need to distinguish Set
and Fetched done within a function and done outside a function.  So we
essentially double the number of sets needed.

Based on an example of Martin Riordan, I think that further refinement
is needed.  The example (simplified):

    *(x = 2, &x) = 7

Compare this with the expression:

    *(&x + (x = 0)) = 7

In the original, the inner assignment to x must occur before the
outermost assignment.  Since the two assignments are separated by a
sequence point, the result is well defined.

In the second example, there is no sequence point, so the result will
be undefined.

To perform this analysis, we need to distinguish between setting done
before a sequence point, and setting done since the last sequence
point.

Perhaps surprisingly, without rather contrived examples like this one,
sequence point semantics could be handled without additional
properties -- only careful specification of the rules for computing
the existing properties.  It is tempting to think that C should be
changed to eliminate this complexity.

Finally, setting a floating point status flag is "sticky".  Although a
flag can be modelled as a variable, it has an additional property:
certain ways of setting the flag to 1 can be done several times is
well defined, even without a separating sequence point.  Unlike other
variables, the floating point flags can be implicitly set to 1 by many
floating point operators.  This requires that we keep a separate set
Set1flag for each Set set.

I don't know how to handle the sticky bit correctly and concisely.  A
naive approach leads to combinatorial explosion.  Here is an example.
Let F be a sticky bit.
    x + y + F
If F is already set (not a well defined term in itself), there is no
problem.  Otherwise, if the leftmost addition would set F, the
expression is undefined (I think).  This does not match the ordinary
semantics of assignment -- in the analogous case, the computation
would always be undefined.  So the sticky bit appears to require a
parallel set of somewhat distinct machinery.

Simply pretending each setting of the sticky bit involves a
conditional to only set it if it is unset leaves the problem that the
test in this conditional can yield race conditions.

I will leave description of the sticky bit out of this discussion.  It
may be that the standard constrains sticky bits in a way that reduces
the problems I perceive.  For example, if the only way to fetch a
sticky bit involves a subroutine, and the only way to set it other
than as the side effect of a floating point operation involves a
subroutine, perhaps the interactions are tamed by the sequence points.

So the sets we need to compute, for each node, are now:
    Undefined
    Unspecified
    FetchedDirect
    FetchedSub (Fetched within a subroutine evaluation)
    Set x {now, before seq. pt.} x {direct, sub}

This last line represents 4 sets all by itself:
    SetNowDirect
    SetNowSub
    SetBeforeDirect
    SetBeforeSub
Anything done inside a subroutine is before a sequence point.  So
SetNowSub should be empty.  We can therefore eliminate it.

It turns out that certain composite properties are useful.  The
corresponding sets are purely a combination of the sets described
above.  Think of this as a kind of common subexpression elimination in
our presentation:
    SetDirect = SetNowDirect | SetBeforeDirect
    Set = SetDirect | SetBeforeSub
    Direct = FetchedDirect | SetDirect
    Sub = FetchedSub | SetBeforeSub
    Fetched = FetchedDirect | FetchedSub


Calculating Properties
======================

We calculate properties of subtrees.  The properties of a subtree are
calculated based on properties of its subtrees and the nature of the
operator at the root of the subtree.

For each set described previously, we introduce a function of the same
name.  The function maps a subtree into the set value for that
subtree.  Thus SetNowDirect("x = 1") would yield the set of byte objects
that makes up the variable x.

To make the distinction between evaluation for lvalue and evaluation
for value clear in the AST, we add an explicit operator to convert
from lvalue to value.  We will denote this by @.  Any subtree that
could be evaluated for lvalue is.

Now that we have those details out of the way, we can start specifying
the rules.


==> For an expression x of the form "left op right", where op is +, -,
*, <<, ... (ordinary binary operators):

    FetchedDirect(x) = FetchedDirect(left) | FetchedDirect(right)
    FetchedSub = FetchedSub(left) | FetchedSub(right)
    SetNowDirect(x) = SetNowDirect(left) | SetNowDirect(right)
    SetBeforeDirect(x) = SetBeforeDirect(left) | SetBeforeDirect(right)
    SetBeforeSub(x) = SetBeforeSub(left) | SetBeforeSub(right)

    Undefined(x) = Undefined(left)
                 | Undefined(right)
                 | Direct(left) & Set(right)
                 | Set(left) & Direct(right)
                 | SetDirect(left) & Fetched(right)
                 | Fetched(left) & SetDirect(right)

    Unspecified(x) = Unspecified(left) | Unspecified(right)
                   | Sub(left) & SetSub(right)
                   | SetSub(left) & Sub(right)

Let's study these rules.

The first five are very simple: the properties simply flow from the
operands.  Pretty simple.  Too bad the notation is a bit cluttered.

The definition of Undefined is quite intricate.  Half the lines can be
understood as mirror images of the other lines due to the symmetry of
these operators.  That still leaves three cases to understand.  The
first case is that if anything undefined in an operand is undefined in
the whole subexpression (for these operators).  The second case is
that if anything directly references or sets an object, this clashes
with a subroutine's setting it.  The third case is that a direct
setting conflicts with a subroutine's fetch.  Notice that these cases
are not always distinct.

Care has been taken to exclude the Unspecified case from Undefined.
This cannot be handled by set subtraction because cases sometimes
overlap.  Thus the last four lines are needed where two would
otherwise have been sufficient.

The definition of Unspecified has one interesting rule, and a copy of
it induced by symmetry.

[Before we added all the distinctions to handle Unspecified vs
Undefined and to handle Martin Riordan's example, the rules were much
simpler:

        Race(x) = Race(left) | Race(right)
                | Set(left) & Fetched(right)
                | Fetched(left) & Set(right)
                | Set(left) & Set(right)

        Set(x) = Set(left) | Set(right)

        Fetched(x) = Fetched(left) | Fetched(right)

Personally, I think much of the appeal of this approach is lost in the
resulting complexity.]


==> For an expression x of the form "op opand" where op is +, -, !,
...  (ordinary unary operator), all the definitions simply pass
through the results from the operand:

    FetchedDirect(x) = FetchedDirect(opand)
    FetchedSub(x) = FetchedSub(opand)
    SetNowDirect(x) = SetNowDirect(opand)
    SetBeforeDirect(x) = SetBeforeDirect(opand)
    SetBeforeSub(x) = SetBeforeSub(opand)
    Undefined(x) = Undefined(opand)
    Unspecified(x) = Unspecified(opand)

[Just a pass-through -- pretty boring.]


==> For an expression x of the form "obj = val":

    FetchedDirect(x) = FetchedDirect(obj) | FetchedDirect(val)
    FetchedSub(x) = FetchedSub(obj) | FetchedSub(val)
    SetNowDirect(x) = SetNowDirect(obj) | SetNowDirect(val) | Obj(obj)
    SetBeforeDirect(x) = SetBeforeDirect(obj) | SetBeforeDirect(val)
    SetBeforeSub(x) = SetBeforeSub(obj) | SetBeforeSub(val)

    Undefined(x) = Undefined(obj)
                 | Undefined(val)
                 | Direct(obj) & Set(val)
                 | Set(obj) & Direct(val)
                 | SetDirect(obj) & Fetched(val)
                 | Fetched(obj) & SetDirect(val)
                 | Obj(obj) & (SetNowDirect(obj) | SetNowDirect(val))

    Unspecified(x) = Unspecified(obj) | Unspecified(val)
                   | Sub(obj) & SetSub(val)
                   | SetSub(obj) & Sub(val)

Although assignment is clearly a key operator, the definitions are
very little different from those for an ordinary binary operator.  The
first difference is another term in the definition of SetNowDirect --
a pretty obvious one.  The second is the last line of Undefined.

This last line of Undefined says that there is a problem if we are
assigning to an object that was assigned while evaluating an operand
and not separated by a sequence point.

It is a bit disturbing that there are so many lines of definition
where only two are "interesting".


==> For an expression x of the form "obj op= val":

    FetchedDirect(x) = FetchedDirect(obj) | FetchedDirect(val) | Obj(obj)
    FetchedSub(x) = FetchedSub(obj) | FetchedSub(val)
    SetNowDirect(x) = SetNowDirect(obj) | SetNowDirect(val) | Obj(obj)
    SetBeforeDirect(x) = SetBeforeDirect(obj) | SetBeforeDirect(val)
    SetBeforeSub(x) = SetBeforeSub(obj) | SetBeforeSub(val)

    Undefined(x) = Undefined(obj)
                 | Undefined(val)
                 | Direct(obj) & Set(val)
                 | Set(obj) & Direct(val)
                 | SetDirect(obj) & Fetched(val)
                 | Fetched(obj) & SetDirect(val)
                 | Obj(obj) & (SetNowDirect(obj) | SetNowDirect(val))
                 | Obj(obj) & Set(val)

    Unspecified(x) = Unspecified(obj) | Unspecified(val)
                   | Sub(obj) & SetSub(val)
                   | SetSub(obj) & Sub(val)

This is very close to the definitions for "obj = val".  FetchedDirect
is different in the obvious way.  A new line has been added to the end
of Undefined: any setting by val is unordered with respect to the
fetching of obj.


==> For an expression x of the form "obj++", "obj--", "++obj", or
"--obj":

    FetchedDirect(x) = FetchedDirect(obj) | Obj(obj)
    FetchedSub(x) = FetchedSub(obj)
    SetNowDirect(x) = SetNowDirect(obj) | Obj(obj)
    SetBeforeDirect(x) = SetBeforeDirect(obj)
    SetBeforeSub(x) = SetBeforeSub(obj)

    Undefined(x) = Undefined(obj)
                 | Obj(obj) & SetNowDirect(obj)

    Unspecified(x) = Unspecified(obj)

This is essentially the same as "obj += 0".  Every term involving the
right operand has been replaced by the empty set, and the results
simplified.

Compare these definitions with those for "op opand" -- this one is
more than a simple pass-through.


==> For an expression x of the form "var" (a variable) evaluated for
its lvalue:

    Obj(var) = bytes of object designated by var
    FetchedDirect(x) = {}
    FetchedSub(x) = {}
    SetNowDirect(x) = {}
    SetBeforeDirect(x) = {}
    SetBeforeSub(x) = {}
    Undefined(x) = {}
    Unspecified(x) = {}

In other words, all property sets are empty, but Obj contains the
variable.


==> For an expression x of the form "@ lval" (an lvalue being
explicitly converted to a value):

    FetchedDirect(x) = FetchedDirect(lval) | Obj(lval)
    FetchedSub(x) = FetchedSub(lval)
    SetNowDirect(x) = SetNowDirect(lval)
    SetBeforeDirect(x) = SetBeforeDirect(lval)
    SetBeforeSub(x) = SetBeforeSub(lval)
    Undefined(x) = Undefined(lval)
                 | Obj(lval) & SetNowDirect(lval)
    Unspecified(x) = Unspecified(lval)

This is almost a straight pass-through.  There is an additional term
in FetchedDirect.  Undefined can actually occur due to the fetch.
Consider the following example:
        (&x)[x = 0]


==> For an expression x that is a manifest constant (for example,
"42"):

    FetchedDirect(x) = {}
    FetchedSub(x) = {}
    SetNowDirect(x) = {}
    SetBeforeDirect(x) = {}
    SetBeforeSub(x) = {}
    Undefined(x) = {}
    Unspecified(x) = {}


==> For an expression x of the form "* val", evaluated for lvalue.
Let ob designate the bytes of the object that val points to:

    Obj(x) = bytes of object that Val(val) points to
    FetchedDirect(x) = FetchedDirect(val)
    FetchedSub(x) = FetchedSub(val)
    SetNowDirect(x) = SetNowDirect(val)
    SetBeforeDirect(x) = SetBeforeDirect(val)
    SetBeforeSub(x) = SetBeforeSub(val)
    Undefined(x) = Undefined(val)
    Unspecified(x) = Unspecified(val)

Except for the definition of Obj, this is a simple pass-through.

[&*x not treated specially.  I think it just works.]


==> For an expression x of the form "& lval":

    FetchedDirect(x) = FetchedDirect(lval)
    FetchedSub(x) = FetchedSub(lval)
    SetNowDirect(x) = SetNowDirect(lval)
    SetBeforeDirect(x) = SetBeforeDirect(lval)
    SetBeforeSub(x) = SetBeforeSub(lval)
    Undefined(x) = Undefined(lval)
    Unspecified(x) = Unspecified(lval)

This is a pass-through.  Nothing interesting is happening, which is
interesting.


==> For an expression x of the form "s.member", evaluated for lvalue:

    Obj(x) = the subset of Obj(s) that contains .member
    FetchedDirect(x) = FetchedDirect(s)
    FetchedSub(x) = FetchedSub(s)
    SetNowDirect(x) = SetNowDirect(s)
    SetBeforeDirect(x) = SetBeforeDirect(s)
    SetBeforeSub(x) = SetBeforeSub(s)
    Undefined(x) = Undefined(s)
    Unspecified(x) = Unspecified(s)

This is close to a pass-through.  

If the struct were instead being returned by a function, it ought to
be a pure value, with no lvalue, so there should be no race
conditions.  I vaguely remembered that the committee may have fudged
some aspects (for example, if a struct returned by a function has an
array member, does selecting that array member yield a pointer into
the value?).


==> For an expression x of the form "f(arglist)":

We consider the argument list comma to be a regular binary operator
(but not the normal comma operator!).  This means that we need not do
a separate induction over the argument list in this rule.

    FetchedDirect(x) = FetchedDirect(f) | FetchedDirect(arglist)
    FetchedSub = FetchedSub(f) | FetchedSub(arglist)
               | fetched by execution of subroutine
    SetNowDirect(x) = {}
    SetBeforeDirect(x) = SetBeforeDirect(f) | SetBeforeDirect(arglist)
                       | SetNowDirect(f) | SetNowDirect(arglist)
    SetBeforeSub(x) = SetBeforeSub(f) | SetBeforeSub(arglist)
                    | set by execution of subroutine

    Undefined(x) = Undefined(f)
                 | Undefined(arglist)
                 | Direct(f) & Set(arglist)
                 | Set(f) & Direct(arglist)
                 | SetDirect(f) & Fetched(arglist)
                 | Fetched(f) & SetDirect(arglist)

    Unspecified(x) = Unspecified(f) | Unspecified(arglist)
                   | Sub(f) & SetSub(arglist)
                   | SetSub(f) & Sub(arglist)

Much of this is like an ordinary binary operator, but there are key
differences.  Surprisingly, Undefined and Unspecified are unchanged:
they are all about evaluation of the argument list and function
pointer before the call.

Everything set is Before because the function contains sequence points
(this may not actually be true of library routines; what are the
consequences?).

Things set or fetched in the subroutine are recorded in FetchedSub and
SetBeforeSub.


==> For an expression x of the form "left , right" (the sequencing
comma, not the argument list comma):

    FetchedDirect(x) = FetchedDirect(left) | FetchedDirect(right)
    FetchedSub = FetchedSub(left) | FetchedSub(right)
    SetNowDirect(x) = SetNowDirect(right)
    SetBeforeDirect(x) = SetBeforeDirect(left) | SetNowDirect(left)
                       | SetBeforeDirect(right)
    SetBeforeSub(x) = SetBeforeSub(left) | SetBeforeSub(right)

    Undefined(x) = Undefined(left) | Undefined(right)
    Unspecified(x) = Unspecified(left) | Unspecified(right)

These definitions are similar to those for a plain binary operator,
but with some key differences.  SetNowDirect does not pass through the
left's SetNowDirect -- that is instead contributed to SetBeforeDirect
because it is now before a sequence point.  Undefined and Unspecified
are simple pass-throughs.


==> For an expression x of the form "test ? tex : fex":

If the value of test is true, the definitions are identical to those
for "test , tex".

Otherwise, the definitions are identical to those for "test , fex".


==> For an expression x of the form "left || right:

The definitions are identical to those for "left ? 1 : right"


==> For an expression x of the form "left && right:

The definitions are identical to those for "left ? right : 0"


We're done
==========

The results we actually care about are Undefined and Unspecified for
the whole expression.  If Undefined is non-empty, the program has
strayed into Undefined territory.  If Unspecified is non-empty, the
values of those objects is not specified (it is constrained, but we
have not computed the constraints).

This mechanism might be useful for other issues.  For example,
understanding volatile.  In that case, sets might be the wrong
tool to use.

The description could be tightened up, with a possible loss of
clarity, by eliminating all "For an expression x of the form"
preambles and eliminating x from the definitions.  An example:

    SetNowDirect(left op right) = SetNowDirect(left) | SetNowDirect(right)
        where op is +, -, *, <<, ...

A lot of rules are similar.  Exploiting this might make the result
less readable, or it might not.


Questions to be answered
========================

- is this approach sufficiently precise?

- is this description accurate (or can it be made accurate)?

- how can we satisfy ourselves that what is specified this way matches
  what is specified in the current Standard?

- Are there any surprises uncovered by this process?  Some are noted
  along the way.

- for what purpose(s) could a description of this style be useful to
  WG24?

- is this formalization more useful for some purposes than the others
  WG24 has?

- is the terminology acceptable?  Can it be improved?

- how can the unformalized bits be tightened up (eg. how to
  appear formal and be accurate about the object representation)?

- is it acceptable to leave the analysis of called functions out (we
  presume that the analysis is handed to us)?

- Are "bytes of objects" the right granularity for analysis?

- what can and what should be said about volatile?

- can we say anything interesting about union member access?

- these analyses can be recast as static, but must then be only
  approximate.  Would the resulting analyses be useful (for example,
  for generating compile-time diagnostics)?  An extreme case: would
  they allow the committee to mandate compile-time diagnostics?