X hits on this document

54 views

0 shares

0 downloads

0 comments

6 / 14

3.1 Tracked Data

In order to make the static verification of block ownership tractable, we segregate data on the GC heap from data on the exchange heap. This segregation is explicit at the type level, where pointers into the exchange heap always have the form Rin ExHeap or R [] in ExHeap. Any other type is either a scalar or must live in the GC heap. We use the term tracked pointer to refer to pointers (including vectors) to the exchange heap because the verification tracks ownership of such pointers precisely at compile time. Pointers into the GC’ed heap need not be tracked generally, since the lack of explicit freeing and presence of garbage collection guarantee memory safety for those objects.

In the following sections, we first present a very restricted, but simple method of tracking ownership, and then gradu- ally relax it to allow more programming idioms to be ex- pressed and verified.

3.1.1 Basic tracking

The simplest form of ownership tracking restricts tracked pointers to appear only on the stack (i.e., as method pa-

rameters, return values, and local variables).

The com-

piler simply rejects tracked pointer types in any other po- sition. With these restrictions, GC’ed objects never point to tracked blocks, and tracked blocks themselves only con- tain scalars. Now it is fairly easy to classify which pointers are owned within the context of a method by considering how ownership is acquired and is lost. There are three ways ownership of a tracked block is acquired by a method:

1. A pointer to the block is passed in as a parameter

  • 2.

    A pointer to the block is the result of a method call

  • 3.

    A pointer to the block is the result of new operation

Similarly, there are three ways a method can lose ownership of a tracked block:

1. A pointer to the block is passed as an actual parameter in a call

2. A pointer to the block is a result of the method

3. A pointer to the block is the argument to delete

Let’s look more closely at how ownership of blocks is trans- ferred from a caller to a callee. There are two common cases when passing a tracked pointer to a method:

The ownership of the block pointed to by the parame-

ter is turn,

passed to the callee temporarily, i.e., upon re-

ownership

reverts

back

to

the

caller.

In

the

classification

above, we consider that as two transfers:

from caller to implicit result

callee as a parameter, and then as an from callee to caller upon return. We

consider this the (including this).

default

case

for

method

parameters

  • The ownership of the block pointed to by the parame- ter is passed to the callee permanently (e.g., arguments to Send methods). We say that ownership of such pa- rameters is claimed and use the annotation [Claims] on such parameters.

With these insights, it is simple to track the status of each pointer value at each program point of the method, via a data-flow analysis, to determine whether a pointer is defi- nitely owned. A complication is that the analysis must keep track of local aliases. This issue can be dealt with using alias types [34, 15] and we won’t comment on it further. Below is a well-typed example.

11

}

12

13

static void Reverse( int [] in ExHeap vec) {

9

int [] in ExHeap vec = new[ExHeap] int[512];

10

return vec;

2

int [] in ExHeap vec = GetVector();

3

for ( int i=0; i<vec.Length; i++) { vec[i] = i ; }

4

Reverse(vec );

5

Consume(vec);

20

}

21

22

static void Consume([Claims] int [] in ExHeap vec) {

1

static void Main() {

6

}

7

8

static int [] in ExHeap GetVector() {

15

int peer = vec.Length1i;

16

int tmp = vec[i ];

17

vec[ i ] = vec[peer ];

18

vec[peer] = tmp;

14

for ( int i=0; i<(vec.Length+1)/2; i++) {

19

}

23

delete vec;

24

}

Let’s consider the ownership information inferred by the ver- ification at each program point of the above program. At line 1 no blocks are owned since Main has no parameters. Af- ter line 2, the method owns the block pointed to by vec (case 2 of acquiring ownership). On line 3, the checker can cor- rectly verify that the method owns the vector being indexed. At line 4, we check that the method owns the argument to the call, since that is what the method Reverse assumes of its parameter. This check passes. After the call to Reverse, the method still owns the block pointed to by vec, since Reverse only took temporary ownership of its parameter. Thus at line 5, we can verify that the method owns the argument to Consume. Since the parameter of Consume is claimed, the method does not own any more blocks at line 6. We have reached the return point of the method without any owned blocks and can thus conclude that Main does not leak any blocks.

Method GetVector starts out without any owned blocks (it has no tracked parameters). After line 9, the method owns the newly allocated block pointed to by vec (case 3 of acquiring ownership). At line 10, ownership of this block is consumed by virtue of returning it from the method (case 2 of consumption). After that, no more blocks are owned and thus no leaks are present.

The reasoning for Reverse is very simple. On entry, the method owns the block pointed to by vec. We can thus verify that all index operations act on an owned vector in lines 14–18. At the return of Reverse, the method must still own the block that was pointed to by vec on entry (since it is obliged to return ownership to the caller). It does, so ownership is reclaimed, leaving the method with no more owned blocks and thus proving that Reverse does not leak.

Finally, on entry, method Consume owns the block pointed to by parameter vec. The delete correctly operates on an

Document info
Document views54
Page views54
Page last viewedMon Jan 23 02:28:58 UTC 2017
Pages14
Paragraphs544
Words12418

Comments