Ownership annotations

ptrset span(void* p)

Expresses the set of primitive field in the struct pointed to by p. The span includes both volatile and non-volatile primitive fields of a struct.

ptrset extent(void* p)

Expresses the union of the span of p, and the extents of all embedded structs within the given struct p.
The extent of a union only covers one option.

ptrset full_extent(void* p)

Expresses the union of the span of p, and the full extents of all embedded structs within the given struct p.
The full extent of a union covers all options.

void* owner(void* p)

Returns the owner of p. The result is either another object or a thread.
The owner of an object is set when wrapping/unwrapping the owner. During the wrap, the owner of every object in its owner set gets updated from the local thread (i.e. me()) to the owner. During the unwrap() of the owner, the owner of every object in the owner set of the owner is updated from the owner to the local thread (i.e. me()).
The functions giveup_owner() and set_owner() do not change the return value of owner, but only update the owns set. The update occurs only during wrapping.

bool closed(void* p)

Expresses the fact that p is closed. If p is closed, then p is either wrapped (i.e. owned by the local thread), or nested (owned by another object). When an object is closed, we know that its invariant holds (i.e. inv(p)).
Volatile fields of an object can only be read/written in a volatile way if the object is closed, or if the object is thread_local.
Asserting that an object is closed is usually done by specifying that p is in the ownership domain of a closed object (i.e. in_domain(p,q) && wrapped(q)), or you have a handle that expresses that p is closed.

thread_id me()

Represents the local thread. This local thread owns the wrapped and mutable objects. Typically, we don?t need to use this annotation, but we should rather use wrapped or mutable.

bool inv(void* p)

Expresses the fact that the (1-state) invariant of p holds.
This predicate is typically a post-condition of unwrapping an object, or asserting the fact that p is closed (i.e. wrapped or nested). This latter condition can be asserted by specifying that p is in the ownership domain of a closed object (i.e. in_domain(p,q) && wrapped(q)).

set_owner(void* p, void* o)

This statement updates the owns set of the object o: the owns set of o is the union of the old owns set and the singleton p.
Nevertheless, the owner(p) is not changed until o is wrapped. Typically, the set_owner() statement is combined with a giveup_owner() statement on the old owner, and the wrapping of o. Moreover, an object can be in the owns set of multiple objects, but at most in one wrapped object.

giveup_owner(void* p, void* o)

The statement updates the owns set of the object o: the owns set of o is the difference of the old owns set and the singleton p.
Nevertheless, the owner(p) is not changed until o is wrapped. Typically, the giveup_owner() statement is combined with a set_owner() statement on the new owner, and the wrapping of the new owner.

set_owns(void* o, ptrset X)

This statement updates the owner set of o to the pointer set X. This operation only changes ownerships when o gets wrapped (cf. set_owner() and giveup_owner()).
The set_owner() and giveup_owner() statements are internally translated to a set_owns() operation:
  • set_owner(p, owner) : set_owns(owner, set_union(set_singleton(p), owns(owner)))
  • giveup_owner(p, owner) : set_owns(owner, set_difference(owns(owner), set_singleton(p)))

in_domain(void* p, void* q)

Expresses, that p is in the transitive ownership domain of q and the invariant of p holds. in_domain() additionally specifies, that p is closed. This clause is required to trigger the owner ship relation between the objects p and q in the prover. It is required, that q is wrapped, since it needs to be the root of the ownershop domain. Currently in_domain() is not supported for a closed() and thread_local() object as root of the ownership domain. The reason being, that only wrapped objects can ensure, that the ownership domain that is triggered by in_domain() is not written to unnoticed.

wrap(void* p)

This statement wraps the object p.
In order to wrap an object p, you have to fulfill the following preconditions:
  • p is typed, but not a primitive type
  • p is owned by the current thread
  • p is not closed
  • every object in the owns set of p is wrapped (i.e. closed and owned by the current thread)
  • the invariant of p holds
The side-effects of wrapping p are that:
  • very object in the owns set of p is now nested (i.e. closed and owned by p)
    • More specific, wrapping p transfers ownership of the objects in the owns set from the local thread to p.
  • p is wrapped, i.e. closed and still owned by the current thread

bool wrapped(void* p)

Expresses the the fact that p is typed, closed and owned by the current thread. Once wrapped, the object p is the owner of all objects in its owns set. All those objects are typed, non-primitive and closed.
Only non-primitive types can be wrapped.
If p is wrapped, it means that it is also closed, and therefore its invariant holds.

unwrap(void* p)

This statement unwraps the object p. In order to unwrap an object p, p has to be wrapped.
The side effects of unwrapping p are that:
  • the invariant of p holds
  • p is owned by the local thread
  • p is mutable (i.e. owned by the local thread and not closed)
  • every object in the owns set of p is wrapped (i.e. closed and owned by the current thread) and we also know that these objects were nested before the unwrap

bool nested(void *p)

The object represented by p is closed and nested in the owner ship domain of another object, i.e. it is owned by another object.

bool thread_local(void *p)

Expressed that the object pointed to by p is typed. If p is non volatile, p must either be directly or transitively owned by the current thread. If p is volatile it must be directly owned by the current thread and must not be closed.

bool mutable(void* p)

Expresses that p is not closed, and is owned by the current thread. Typically this is necessary to update its state, next to the fact that it is allowed by the writes clause of the function.

bool depends(void *p, void* q)

This clause is usually being used in invariants of types to express, that the invariant of object p depends on object q. This usually involves, that the invariant of p needs to be rechecked, if q changed either in meta or in state.
This means, that on wrapping the object q the invariant of the closed object p is also checked if q has been changed.

Last edited Jul 1, 2009 at 8:45 PM by DirkLeinenbach, version 2

Comments

No comments yet.