Deriving properties and upgrading claims

claims_claim(...)

Sometimes, you have a claim to an object, say struct T, which owns a claim on something else, say a spinlock:

struct T {
  struct S s;
  RTL_SPIN_LOCK L;
  spec(claim_t Claim;)

  invariant(keeps(Claim))
  invariant(claims(Claim, closed(&L) && L.protected_obj == &s))
};


The function acquiring the spinlock wants the inner claim (a claim on the spinlock).

void RtlAcquireSpinLock(PRTL_SPIN_LOCK SpinLock claimp(c))
    always(c,closed(SpinLock) && SpinLock->protected_obj != NULL)
    // ...
    ;


You cannot supply the inner claim, as it needs to be wrapped. However, because you have the claim on something that owns the inner claim, it should be good enough. The verifier however needs some guidance, which claim do you actually need. This is done with claims_claim(c1, c2) assertion:

void foo(struct T *p claimp(c))
  always(c, closed(p))
{
  assert(claims_claim(c, p->Claim));
  RtlAcquireSpinLock(&p->L spec(c));
}


The meaning of claims_claim(c1, c2) is that in every state where c1 is valid, c2 is closed. It is a state-independent predicate. Thus the example above works only because we know p->Claim is not going to change as long as c remains closed. In other words, the compiler uses:

  assert(claims_claim(c, by_claim(c, p->Claim)));

Upgrading Claims

If you learn a new fact F about the state, on which you hold a claim c, you may want to include this new information in the claim.

However, claims(c, P) means that forall(S; closed(S, c) ==> P(S), which means that it holds in any state, also in previous states, before you learned F. Therefore, just assuming claims(c, P && F) would be unsound.

Instead we allow for constructing a new claim, while simultaneously destroying the old one. The new claim, c2, will claims(c2, P && F), and will claim all the objects that c used to claim. Therefore, you will get the reference counts back when destroying c2. This does not require any write access to objects claimed by c, but it does require write access to c itself. (As in unclaim operations, the claim c is also considered not closed after upgrading).

#include <vcc.h>

struct vcc(claimable) Counter {
  volatile int count;
  invariant( unchanged(count) || count == old(count) + 1 )
};

int foo(struct Counter *cnt spec(claim_t cl) spec(out claim_t res))
  writes(cl)
  requires(wrapped0(cl) && claims_obj(cl, cnt))
  ensures(wrapped(res) && claims(res, cnt->count >= result - 1 ) && claims_obj(res, cnt) && is_fresh(res))
{
  int y;
  spec( claim_t x; )

  atomic(cl,cnt) {
    y = cnt->count;
    spec( res = upgrade_claim(cl, cnt->count >= y);)
  }

  return y;
}


Note that there exists a risk of loosing reference counts in this manner. If we forgot the claims_obj(res, cnt) postcondition, the caller would be never able to open cnt. This is the same as with usual claim creation.

One can also combine knowledge from several claims into one. For example:

void two(struct Counter *cnt1, struct Counter *cnt2 spec(claim_t cl1) spec(claim_t cl2) spec(out claim_t res))
  writes(cl1,cl2)
  requires(wrapped0(cl1) && claims_obj(cl1, cnt1) && claims(cl1, cnt1->count >= 0))
  requires(wrapped0(cl2) && claims_obj(cl2, cnt2) && claims(cl2, cnt2->count >= 0))
  ensures(wrapped0(res) && claims(res, cnt1->count + cnt2->count >= 0) && claims_obj(res, cnt1) && claims_obj(res, cnt2) && is_fresh(res))
{
  int y;
  spec( claim_t x; )

  spec( res = upgrade_claim(cl1, cl2, cnt1->count + cnt2->count >= 0);)
}


Note that you get only one claim out of the process, and you loose both input claims. The output claim however claims all the objects that the input claim used to claim.

There is a drawback though: if both input claims claim the same object, you will loose a reference count.

Using Guaranteed Properties in Upgraded Claims

The upgraded claims are valid just before the upgrade. Therefore, if claims(c, P) and one does c2 = upgrade_claim(c, P && F), then proving P initially is not a problem. However, to when upgrading the claim one still needs to prove stability of P. Stability of P for c2 does not directly follows from stability of P for c. For example here it would be unsound to allow for claim upgrade:

struct A {
  spec(claim_t c;)
  spec(volatile int x;)
  invariant(closed(c) ==> unchanged(x))
};

void foo(struct A *a claimp(c))
  writes(c)
  requires(claims(c, a->c == c && a->x == 20))
{
  ...
  c2 = upgrade_claim(c, a->x == 20);
  ...
}


This might be somewhat cumbersome, for example, if you replace the precondition:
  requires(wrapped0(cl) && claims_obj(cl, cnt))

with:
  requires(wrapped0(cl) && claims(cl, closed(cnt)))

on the foo function defined before, the claim stability test will fail, because there is no way of knowing if closed(cnt) is stable.

Last edited Feb 11, 2011 at 7:00 PM by MarkHillebrand, version 6

Comments

No comments yet.