[Tinyos-devel] Type safety for TinyOS

[John Regehr]

I just want to follow up David's message with a bit of cheerleading: type 
safety is really, really useful for TinyOS development.

As we all know, motes never core dump: array and pointer errors generally 
result in far worse problems like spurious reboots, RAM corruption, and 
even register corruption (AVR maps its registers into low RAM).  We have 
seen all of these problems in real TinyOS applications.  Debugging an 
instance of register corruption can be a life changing experience -- in a 
bad way.  In the field these problems are indistinguishable from other 
failure modes.

We are working to keep the cost of type safety extremely low for people 
who don't want/need it (just a bit of clutter in the code, which could 
easily be automatically hidden by Eclipse/emacs).  As David says the cost 
is also quite modest for people who do use it.

John




On Wed, 23 May 2007, David Gay wrote:

> 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
> _______________________________________________
> Tinyos-devel mailing list
> Tinyos-devel at Millennium.Berkeley.EDU
> https://mail.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-devel
>