[Tinyos-devel] nesC concurrency semantics, volatiles, etc.

[David Gay]

On 8/11/06, John Regehr <regehr at cs.utah.edu> wrote:
> Many embedded programmers make sure that all of their async variables are
> declared as volatiles.  On the other hand, basically all TinyOS programs contain
> async variables that are not volatile.  In many cases this is harmless: since
> interrupts and tasks tend to be short, async values can only be cached in
> registers for a short period of time: they must be flushed to SRAM before the
> task or interrupt terminates.
>
> However, if there is interesting synchronization with interrupts then a
> non-volatile async can be a big mistake.  For an obvious example see the first
> question here:
>
>    http://www.nongnu.org/avr-libc/user-manual/FAQ.html
>
> It seems like the nesC semantics for atomic want to be updated to include some
> aspects of a memory barrier, where the results of an atomic section become
> visible to the rest of the program immediately after the atomic section ends.
>
> Has this issue been thought through?  Currently everything seems to be left up
> to the individual developer.  Issues with volatile are a notorious source of
> errors for programmers (and also for compiler writers!).  It seems like this is
> an area of embedded programming where nesC could add value instead of defaulting
> to the baseline C semantics.
>
> At the implementation level the nesC compiler could easily be changed to emit
> code where all async variables are volatile.  This inhibits some optimizations,
> but it's probably not a big deal in practice.  A more performant transformation
> would permit an async to be cached for the duration of an atomic section.  So if
> x is an async int, the compiler output would look like this:
>
>    nesc_atomic_start();
>    int x_tmp = x;
>    ... references to x replaced with x_tmp ...
>    x = x_tmp;
>    nesc_atomic_end();
>
> Of course the flush can be omitted if x is never stored to in a given atomic
> section.
>
> The context in which that has come up is in cXprop, our static analyzer for
> TinyOS programs.  We currently model async variables using the semantics in the
> code fragment above, in addition to making x volatile.  We noticed that these
> semantics are considerably stronger than those respected by the C compiler!

I think the reason we don't run into problems is that all atomic
sections start with a call to disable interrupts, which ends up being
something like:
   __asm volatile ("cli");}
which prevents rescheduling of instructions across the asm statement.
This probably further reduces any bad effects of optimisation on
atomic's...

If this were
   __asm volatile ("cli" : : : "memory");}
that would also tell gcc that memory may have changed (*), which
should be enough of a memory barrier, I think. It's also a simpler
change than rewriting all memory accesses as volatile (the async
variable detection is not conservative, so can't be used as a reliable
approach...).

A similar asm is probably needed at atomic section end.

Or, to summarise, my proposal would be to state that the
__nesc_atomic_start/end functions must contain the necessary stuff to
convince the compiler and hardware that there's a memory barrier.

FWIW, the approach so far has been to add volatile when we've run into
problems...

David Gay
*: I wouldn't be horribly surprised to learn that asm volatile
effectively causes memory to be included in the side effects...