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

[John Regehr]

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!

John