The annotation writes(p) on a function means that the function is "allowed" to write p. A function is also "allowed" to write any object that the function didn't own on function entry; as described below, this has the effect of allowing the function to write everything in p’s ownership domain.

We introduce a timestamp field defined on objects (typed pointers). There is also a global timestamp dependant on the state. We know (there is an axiom) that all the memory reachable at any given point has the timestamp not larger than the current global timestamp. Functions like malloc() increase the global timestamp and say the timestamp of the result is equal to the new current timestamp. The definition of is_fresh is:

function $is_fresh(M1:$state, M2:$state, p:$ptr) returns(bool)
  { $current_timestamp(M1) < $timestamp(M2, p) && $timestamp(M2, p) <= $current_timestamp(M2) }

where M1 and M2 refer to old($state) and $state. All functions get a free postcondition that they didn’t decrement global timestamp nor timestamp of any data.

We bump timestamps when doing unwrap, and the general proof obligation for writing is:

function $writable(S:$state, begin_time:int, p:$ptr) returns(bool)
  { ($in_writes_at(begin_time, p) || $timestamp(S, p) >= begin_time) && $mutable(S, p) }

where begin_time refers to the timestamp saved at the beginning of the function and $in_writes_at(...) to the writes clause specified on a function. So we check that the thing we’re writing to is mutable and that it was changed to mutable after the beginning of the current function (or it was listed in writes clause).

For example given the following function:

void g(A* p, A *q)
  writes(extent(p), q)
  p->x = 12;

we generate:

    var #wrTime^5: int;

    assume #wrTime^5 == $current_timestamp($meta);
    assume (forall #p: $ptr :: { $in_writes_at(#wrTime^5, #p) } $in_writes_at(#wrTime^5, #p) == ($set_in(#p, $extent(p)) || #p == q)));
    assert $writable($state, #wrTime^5, $dot(p, A.x));
    // *(p->x) = 12;
   call $write_int($dot(p, A.x)], 12);

As you can see, we put a definition of $in_writes_at() tailored at the specific begin time (this is because loops can also have writes clauses, so you might end up having several such definitions in a function). The ^5 refers to the line number.

We actually also generate the following, at the beginning of the function:

   assume (forall #p: $ptr :: { $st($s, #p) } { $ts($s, #p) } $set_in(#p, $struct_extent($ptr(^A, p))) ==> $mutable($s, #p));
   assume $thread_owned($s, $ptr(^A, q));

We can do that, because this is part of the proof obligation when calling g(...).

Last edited Mar 20, 2010 at 11:04 AM by erniecohen, version 3


No comments yet.