[Tinyos Core WG] Safe TinyOS annotation format

[Vlado Handziski]

>From my side I can say that the proposal goes a long way towards addressing
my concerns about the syntax overload and my fear of giving even more
ammunition to the plain "C" admirers against TinyOS. Great work John and
David!.

Vlado

On Dec 16, 2007 10:58 PM, John Regehr <regehr at cs.utah.edu> wrote:

> Please look over the proposed annotation format for Safe TinyOS below,
> motivated by the discussion last Weds.
>
> The first issue is determining which modules should be compiled as safe
> code.  We propose two new nesC attributes that are used like this:
>
> module CC2420ActiveMessageP @safe() { ...
>
> module CC2420ActiveMessageP @unsafe() { ...
>
> If this attribute is omitted, the default (according to my understanding
> of the current consensus) is unsafe, meaning that pointer/array accesses
> in this module are unchecked.  This annotation applies only to modules,
> not configurations.
>
> Note that it will always be possible to override these module-level
> preferences by simply not invoking the Deputy compiler.  In that case no
> safety checks are added to an application; this is presumably useful for
> people who are more worried about code size than bugs.
>
> The second issue is reducing the cognitive load due to annotations in
> the TinyOS interface files.  Here we propose moving annotations into the
> comments that are parsed by nesdoc.  New nesdoc commands @deputyparam
> and @deputyreturn will serve two purposes.  First, the nesC compiler
> will translate these into regular Deputy annotations.  Second, it should
> be possible for nesdoc to translate annotations into human-readable
> documentation e.g. "the payload parameter is either NULL or refers to a
> memory region containing at least len bytes."
>
> Just to be clear, in this proposal there are two ways to express Deputy
> annotations: the original inline way and a new outline way.  By
> convention, TinyOS interface files would use the latter.
>
> interface Receive {
>
>   /**
>    * Receive a packet buffer, returning a buffer for the signaling
>    * component to use for the next reception. The return value
>    * can be the same as <tt>msg</tt>, as long as the handling
>    * component copies out the data it needs.
>    *
>    * <b>Note</b> that misuse of this interface is one of the most
>    * common bugs in TinyOS code. For example, if a component both calls a
>    * send on the passed message and returns it, then it is possible
>    * the buffer will be reused before the send occurs, overwriting
>    * the component's data. This would cause the mote to possibly
>    * instead send a packet it most recently received.
>    *
>    * @param        msg      the receied packet
>    * @deputyparam  "COUNT(len) payload"  a pointer to the packet's payload
>    * @param        len      the length of the data region pointed to by
> payload
>    * @return       a packet buffer for the stack to use for the next
>    *               received packet.
>    */
>   event message_t* receive(message_t* msg, void* payload, uint8_t len);
>
>   /**
>    * Return a pointer to a protocol's payload region if it is large
>    * enough to hold len bytes. Otherwise return NULL. This command
>    * behaves identically to <tt>Packet.getPayload</tt> and is included
>    * in this interface as a convenience.
>    *
>    * @param             msg      the packet
>    * @param             len   desired payload length
>    * @deputyreturn      "void * COUNT(len)" a pointer to the packet's
> data payload for this layer,
>    *    or NULL if the payload is smaller than len bytes
>    */
>   command void* getPayload(message_t* msg, uint8_t len);
>
>   /**
>    * Return the length of the payload of msg. This call is identical
>    * to <TT>Packet.payloadLength</TT>, and is included in Receive as a
>    * convenience.
>    *
>    * @param  msg      the packet
>    * @return          the length of the packet's payload
>    */
>   command uint8_t payloadLength(message_t* msg);
>
> }
>
> John Regehr et al.
>
> _______________________________________________
> Tinyos-2.0wg mailing list
> Tinyos-2.0wg at millennium.berkeley.edu
> https://www.millennium.berkeley.edu/cgi-bin/mailman/listinfo/tinyos-2.0wg
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://www.millennium.berkeley.edu/pipermail/tinyos-2.0wg/attachments/20071216/ecb1532e/attachment-0001.htm