[Tinyos Core WG] Safe TinyOS

[John Regehr]

Hi folks-

I've put the safe version of TinyOS 2.0.2 here:

   http://www.cs.utah.edu/~regehr/safe-tinyos-2.0.2/

The interfaces are probably the most interesting code to look at.

To read the annotations consider this example:

   command void* COUNT(len) getPayload(message_t* SAFE msg, uint8_t len);

COUNT(len) is an annotation on the pointer returned by getPayload and 
specifies that this pointer will refer to a region containing at least 
len bytes (unless the pointer is NULL).  The SAFE annotation on msg 
means that msg is a pointer-to-singleton.

The full patch can be found here:

   http://www.cs.utah.edu/~regehr/safe-tinyos-2.0.2-patch.txt

For now please just use this patch for informational purposes, I haven't 
checked that it applies cleanly against a 2.0.2 install.  When looking 
over these changes keep in mind that:

   - SAFE annotations can be omitted, since SAFE is the default

   - the getPayload() changes have already been made in T2 CVS

   - there is some random cruft in the patch due to sloppy merging of 
our changes against TinyOS changes as we ported Safe TinyOS forwards to 
2.0.2

I will put together a distribution of our patched TinyOS and our 
toolchain but this will take a few days.

Finally the paper about Safe TinyOS is here:

   http://www.cs.utah.edu/~regehr/papers/coop-sensys07.pdf

John Regehr