X hits on this document





7 / 14

owned block at line 23 and consumes ownership (case 3 of consuming ownership). The method ends without any out- standing blocks and thus has no leaks.

To illustrate the kinds of errors that the verification will detect, suppose that the Main method calls Consume and Reverse in opposite order:




Reverse(vec );

The Sing# compiler emits the following error on that code.

(5,11): error CS6084: Accessing dangling reference ’Test.GetVector.returnValue’

The call to Consume consumes ownership of the block (since the formal parameter is annotated with [Claims]) and thus at the call to Reverse, the verification fails, since the argument pointer does not point to an owned block.

As another potential error, suppose we omit line 23 which deletes the vector in the Consume method. Sing# emits the following error in that case.

(24,1): error CS6095: Leaking owned reference ’vec’

To complete our discussion of the basic ownership checking, we need to address aliasing. If a method takes more than one tracked pointer, the assumption is that the pointers are distinct. The verification checks each call site to make sure no aliasing of parameters arises.

Also, ref and out parameters are handled in the obvious way. A ref parameter of tracked type requires ownership of the contents of the ref parameter on entry and returns ownership of the ptr in the ref parameter on exit of the method. For out parameters, no ownership transfer occurs on entry.

In practice, the verification needs to handle null specially, since no memory and thus no ownership is associated with such pointers. We use a “must-be-null” analysis before check- ing ownership in order to handle idioms such as:

1 2 3 4 5

void Consume([Claims] Tin ExHeap ptr) { if ( ptr != null ) { delete ptr ; }


The analysis needs to know that ptr is null on the control flow edge that skips the conditional block. This knowledge lets us determine at the merge point after the conditional (line 4) that no more resources are held.

3.1.2 Tracked pointers in the GC heap

The basic tracking is sufficient if all tracked pointers live on the stack. However, there are situations, in which one needs to escape the static checking of ownership or truly share some endpoint or other block in the exchange heap among multiple threads in the same process. To this end, Sing# provides a predefined class TCell<T> that is a GC wrapper for a tracked pointer. A TCell turns static verification of memory management into dynamic checking. Its interface is as follows:

class TCell<T> { TCell([ Claims] Tin ExHeap ptr); Tin ExHeap Acquire(); void Release ([Claims] Tin ExHeap ptr);


The semantics of a TCell is it can be either full (containing a tracked pointer) or empty. On construction, a cell consumes the argument pointer and thus starts out as full. An Acquire operation blocks until the cell is full and then returns the tracked pointer, leaving the cell empty. A Release blocks until the cell is empty and then stores the argument pointer in the cell, leaving it full. TCells can thus be used to pass ownership of a tracked block from one thread to another within the same process.

As mentioned above, static verification of memory man- agement is turned into dynamic checking by a TCell. For ex- ample, if a thread tries to acquire a cell twice and no other thread ever releases into the cell, then the thread blocks for- ever. Furthermore, TCells rely on the GC finalizer to delete the contained block if the cell becomes unreachable.

3.1.3 Tracked structs

So far we only have pointers from the stack and special cells into the exchange heap. But it is useful for pointers to link from the exchange heap to other blocks in the exchange heap as well. For example, the struct NetworkPacket used in the NicDevice contract contains a byte vector in a field. To verify code involving such fields we restrict how these fields are accessed: to access fields of tracked structs, the struct must be exposed using an expose statement as in the following example.


byte [] in ExHeap old = pktdata;


pktdata = new[ExHeap] byte[old.Length2];


delete old ;

1 2

void DoubleBufferSize(NetworkPacketin ExHeap pkt) { expose(pkt) {

6 7



In order to check this construct, the verification must track whether tracked structs are exposed or unexposed. An un- exposed struct pointer satisfies the invariant that it owns all memory blocks it points to. When the struct is ex- posed, ownership of the pointed-to blocks is transferred to the method context doing the expose. At the end of the expose block, ownership of the current pointers in the fields of the exposed struct is transferred from the method to the struct.

Thus, in the example above, at line 2, the method owns the block pointed to by pkt and it is unexposed. After line 2, the same block is now exposed and the method also owns the block pointed to by pktdata. After line 3, the method still owns the same blocks, but old points to the same block as pktdata. After line 4, the method owns three blocks pointed to by old, pkt, and pktdata. After line 5, ownership of old is consumed. At line 6, we unexpose the struct pointed to by pkt which consumes the contained pointer pktdata. Thus, at line 7, the method owns only the block pointed to by pkt, and its status is unexposed. Since ownerhips of this block passes back to the caller at this point, we managed to verify this method. If the delete statement were omitted, the checker would complain that the old byte vector is leaking.

3.2 Vectors of tracked data

The final extension we present here is supporting vectors of tracked data. The problem in this setting is that the verifier cannot track the ownership status of an unbounded number of elements in a vector. Thus, we restrict access to the vector to one element at a time, requiring an expose of the vector

Document info
Document views24
Page views24
Page last viewedTue Oct 25 10:50:31 UTC 2016