[Tinyos-devel] Type safety for TinyOS

[David Gay]

Summary: By changing TinyOS a little, we can support Deputy, a
type-safety (array-bounds checks, etc) tool for C which should help
increase TinyOS reliability with very low overhead (~6% extra CPU
cycles).  Furthermore, you don't have to use Deputy (for 0% overhead
:-)).

Shortterm, this means changing one interface (Packet) and adding a few
annotations. Longterm, it means ensuring core TinyOS interfaces are
compatible with Deputy, and supporting Deputy as a standard (but
optionally used) element of the TinyOS toolchain.

Comments welcome.

--

Background: Deputy is a tool for ensuring that a C program is type
safe (don't access things with the wrong type,  don't access arrays or
other objects out of bounds). It works on mostly unchanged C code, but
does require some annotations to indicate what the bounds of various
pointers are, in terms of other program variables. For instance,

 void sum(int *x, int n); // A regular C function to sum an array of n elements
 void sum(int *LENGTH(n) x, int n); // The require deputy annotation for sum

See http://deputy.cs.berkeley.edu/ for lots more detail.

--

I applied Deputy to TinyOS a few months ago, which helped find a radio
stack bug (there's a very brief description in the ESOP paper on the
web site above). And Deputy would've caught (with a runtime error) a
nasty SPI bug that took several months to track down. More recently,
John Regehr&co at the University of Utah has extended this work,
reducing overhead, etc.

Using Deputy with TinyOS was mostly painless, except that Deputy
required one API change to the Packet/Send/Receive interfaces,
specifically the getPayload commands.

Proposed change (only getPayload changes, the other commands remain as is):
interface Packet {
 command void* getPayload(message_t* msg, uint8_t* len);
 ...
}

becomes
interface Packet {
 command void *getPayload(message_t *msg, uint8_t expectedLength);
 ...
}

The expectedLength is the number of bytes the caller requires for its
uses. If the implementation of getPayload (current protocol level)
cannot provide a payload that big, it must return NULL.

The Send and Receive interfaces change as follows:
- getPayload in both Send and Receive is now identical to getPayload in Packet

A typical code change. In Oscilloscope,
       if (!sendbusy && sizeof local <= call AMSend.maxPayloadLength())
         {
           memcpy(call AMSend.getPayload(&sendbuf), &local, sizeof local);
           If (call AMSend.send(AM_BROADCAST_ADDR, &sendbuf, sizeof
local) == SUCCESS)
             sendbusy = TRUE;
         }

becomes
 oscilloscope_t *buffer = call AMSend.getPayload(&sendbuf, sizeof local);
 if (!sendbusy && buffer)
   {
      *buffer = local;
       If (call AMSend.send(AM_BROADCAST_ADDR, &sendbuf, sizeof local)
== SUCCESS)
          sendbusy = TRUE;
   }


Advantages:
- I think the new interface is slightly cleaner in use
- the getPayload command is consistent across all interfaces
- we could more easily (optionally) apply Deputy to any TinyOS program

Disadvantages:
- we have to change a bunch of getPayload uses and implementations

David Gay