Ownership model in VCC is based on the one used in Spec#: each object has a special owner field that links to object “controlling” the current object. This can be either an ordinary object or a thread (threads are also considered to be objects). When reasoning about concurrent code, we are reasoning about just one thread in separation, called the current thread, or me() in VCC.

Objects that are closed and owned by me are called wrapped, whereas object that are open and owned by me are called mutable. Modification of non-volatile fields is only allowed for mutable objects.

Closing an object that is owned by me (it is impossible otherwise), is called wrapping it, whereas the opposite operation is called unwrapping it.

To control ownership transfer when wrapping and unwrapping an object, VCC uses the owns set. It behaves like an ordinary field, when the object in mutable, it can be changed using set_owns(...) function. It represents the set of objects that we want the current object to own, at the time it is wrapped.

Indeed, just before wrapping an object, we require me to own everything in the owns set, and at the time of wrapping, we transfer ownership of everything in the owns set to the wrapped object.

Once the object is closed, it is a system invariant, that everything it lists in its owns set has the owner field set to the object and vice versa.

When we unwrap the object, everything in the owns set (and by the aforementioned system invariant of everything that has the owner field set to the unwrapped object) has its ownership transferred to me.

The owns set of the unwrapped object, however, stays unchanged. This means that if you do not want to add or remove any objects from the ownership domain of the unwrapped object, you can just wrap it back, without touching the owns set.

The typical way to state ownership is in invariants of types. It is done using set_in(ownee, owns(this)).

Keeps

It is usually the case that an object owns a fixed, small number of other objects. For example:

#include <vcc.h>

struct vcc(dynamic_owns) A {
  struct B *by_ptr;
  struct C by_emb;

  invariant(set_in(by_ptr, owns(this)))
  invariant(set_in(&by_emb, owns(this)))
};

However this invariant doesn’t talk about other objects that could possibly be in the owns set of A. Therefore in the following code:

  struct A *a;
  ...
  unwrap(a);
  foo(a->by_ptr);
  wrap(a);

VCC will need to reason about changes to those possible objects when wrapping a back. This slows down the prover. Additionally when wrapping a for the first time, you will need to set the owns set to those two objects, that the invariant requires.

This is why, recently (12/12/2008) we have switched to a more restricted model, which is used by default. Instead of using:

  invariant(set_in(by_ptr, owns(this)))
  invariant(set_in(&by_emb, owns(this)))

we can now say:

  invariant(keeps(by_ptr, &by_emb))

This new invariant means that the object will own those two objects only. Additionally, just before wrapping the object, VCC will set the owns set accordingly (so you no longer need to use set_owns(...) or set_owner(...)). It is also possible to have conditional ownership, as in:

#include <vcc.h>
#include <stdlib.h>

struct A {
  struct B *by_ptr;
  invariant(by_ptr != NULL <==> keeps(by_ptr))
};

This is however only possible when the condition is of the form cond <==> keeps(o1) [ && something else ] (there need to be equivalence, implication is not enough).

keeps(o) implies set_in(o, owns(this)) and old(o) == o. The second condition might fail during admissibility check, when you for example want to own something pointed to by a field of a different object.

Limitations: When you need to own an unbounded number of objects (like for example the list manager, or when dealing with arrays), you need to disable that new feature. This is done by placing vcc(dynamic_owns) on the type definition. Also when a type is marked with vcc(volatile_owns), this feature is disabled.

By default, when there are no vcc(dynamic_owns) nor vcc(volatile_owns) on the type, VCC will not allow explicit reference to the owns-set of a type. Instead, keeps must be used to specify the elements in owns(this). In the absence of any keeps annotation, VCC will generate an invariant stating that the owns(this) is empty.

The bottom line
  • when you want to own unbounded number of objects, you still use set_owns(...) and mark the type with vcc(dynamic_owns)
  • otherwise, you can use the new shorted keeps(...) notation, and don’t have to use set_owns(...) at all (it will be overwritten when wrapping the object anyhow)
  • it does not affect types with vcc(volatile_owns)

Last edited Nov 13, 2009 at 12:00 PM by stobies, version 6

Comments

No comments yet.