This project is read-only.

Extension of a claimed property (dynamic claims)

Aug 6, 2009 at 11:54 AM

Let us consider the following scenario: a counter with a switch.
If switch is on, counter can be increased. Otherwise, the counter can only be decreased.
We also define a protector which restricts who can tun on/off the switch.
We define a structure S which implements this:

typedef struct vcc(claimable) S{

volatile bool on;
volatile int cnt;

Protector protector;
 
invariant(old(!on) ==> old(cnt) <= cnt)
invariant(old(closed(&protector)) ==> unchanged(on))

}


Now, we turn off the switch and create a claim A with the following properties (let s be of type S):
claims(A, !s->on)
claims_obj(A, s)
claims_obj(A, s-> protector)



Assume thread TH1 decreases the counter and it reaches zero. Assume also that TH1 can share this information with somebody else. Usually, we employ claims to do this.

Ideally, we only want to add an additional property to A:
  claims(A, !s->on && s->counter ==0)


Question: is it possible to have a vcc support for this scenario?


There are two naive workarounds (may be someone can suggest something more elegant?)
1) re-create the claim A
In this case it doesn't work because TH1 doesn't have write permissions for the protector.

2) we create a new claim on A with the desired property.
Main disadvantage: we have two claims instead of one.
* this is not nice because we increase (IMO unnecessarily)  number of specification constructs
* in my particular scenario moving two claims (i.e. two objects instead of one)  between threads does look really nasty and too ad-hoc.

Aug 6, 2009 at 3:12 PM

We do not support updating claims. With current axiomatization this would be unsound. This is because the translation of claims(A, P) is forall(S; closed(A)[S] ==> P[S]). Therefore, the property that you state in claims(...) holds always, in all states, not only in the ones after you assume claims(...).

The recommended way of doing this is 2), but I agree that this is somewhat annoying that you end up with two claims. We could possibly support a scenario, where you at exactly the same moment destroy the old claim and create a new one, without altering anyone’s reference counts. Thus, you would get a new claim, but the old claim would be gone.  I don’t think there is a soundness problem with it.

Would that work for you? [but I’m not saying you gonna get it this week :-]

Michal

Aug 7, 2009 at 9:17 AM

If for this destroy-create action I didn't need write permissions to the claimed objects, it works for me (this support is similar to  (1) ).

Aug 7, 2009 at 9:22 AM
MichalMoskal wrote:

We do not support updating claims. With current axiomatization this would be unsound. This is because the translation of claims(A, P) is forall(S; closed(A)[S] ==> P[S]). Therefore, the property that you state in claims(...) holds always, in all states, not only in the ones after you assume claims(...).

yes, that's basically my understanding as well. Just one question: "forall(S; closed(A)[S] ==> P[S])" means that the property it not guaranteed to be true in all states but only in those where the claim is closed, i.e., only after claim creation. So, would it help to assume that we get a new claim after the claim update, e.g., by guaranteeing fresh(A)?

Aug 7, 2009 at 3:49 PM
> Just one question: "forall(S; closed(A)[S] ==> P[S])" means that the property it not guaranteed to be true in all states but only in those where the claim is closed, i.e., only after claim creation. So, would it help to assume that we get a new claim after the claim update, e.g., by guaranteeing fresh(A)?

Yes, this is exactly the idea, you will get a new claim, and the old one will no longer be closed.
Aug 14, 2009 at 10:15 PM

I've created a work item 2439 to keep track of this.

 

Sep 11, 2009 at 10:15 AM

This is now implemented. See http://vcc.codeplex.com/Wiki/View.aspx?title=Deriving%20properties%20and%20upgrading%20claims

Please close http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=2439 once you make sure it works for you.