owner-approved fields cannot be encapsulated


The VCC framing discipline allows updates to the fields of an object o to he hidden in the contract of an operation that operates on a wrapped o, because opening up o gives the thread the right to write to all of its fields. A volatile, owner-approved field of an object should (from a framing perspective) behave like a sequential field; that is, an object of type T given by
typedef struct T {
    volatile int v;
    _(invariant \approves(\this->\owner, \this->v))
} T;
is morally like a sequential field from the framing perspective of its owner. However, there is an important difference: if a T is owned by an object s, opening s does not give the thread the right to update the v field of the T. Thus, the update of the v field has to be mentioned in the writes clauses of functions that operate on a wrapped s, even though they have to upwrap the s to do it. This makes owner-approved fields impossible to encapsulate properly.

The obvious solution is to extend the rules for writing, so that when opening an object o, the thread gets the right to update (volatily) the owner approved fields of objects owned by o.