[Tinyos Core WG] Safe TinyOS annotation format

[Kevin Klues]

I think this sounds great.  I definitely like the annotations outside of the
function declarations themselves.  And seeing the explicit keyword @safe at
the beginning of a module will help people understand why they see "weird"
annotations strewn throughout the code contained within it.

Kevin

On Dec 16, 2007 1: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
>



-- 
~Kevin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://www.millennium.berkeley.edu/pipermail/tinyos-2.0wg/attachments/20071216/db6f67e3/attachment.html