Claims on globals, atomic blocks and 2-state invariants

Dec 2, 2010 at 7:37 PM

Hi all,

I am running in a bit of a snag when doing some atomic operations on a claimed global. In the following example, the first assertion fails, which prevents me from transposing the 2-state invariant preservation result to the whole function, which would be a nice bonus. However, I can't seem to figure out if this is a bug or expected behaviour. I cannot actually confirm whether this is specific to globals either (I'll check this tomorrow and let you know, I guess).

#include <vcc.h>

#define stable(_F)  old(_F) ==> _F

spec(typedef struct {
  int dummy;

  volatile bool isGood[mathint];
  invariant(forall(mathint m; stable(isGood[m])))

PRED pred;

struct vcc(claimable) _DATA_CONTAINER {
  int dummy;

} DataContainer;)

void testit(spec(mathint m) claimp(c))
always(c, closed(&DataContainer))
  spec(state_t s0,s1,s2;)
    s0 = current_state();
    atomic(c, &DataContainer, &pred)
      s1 = current_state();
      pred.isGood[m] = true;
    s2 = current_state();)

  assert(forall(mathint m; in_state(s0, pred.isGood[m]) ==> in_state(s1, pred.isGood[m])));
  assert(forall(mathint m; in_state(s1, pred.isGood[m]) ==> in_state(s2, pred.isGood[m])));
  assert(forall(mathint m; in_state(s0, pred.isGood[m]) ==> in_state(s2, pred.isGood[m])));

Dec 3, 2010 at 1:06 PM

Hi Francois,

  this is expected behavior (and not related to the use of globals): at the beginning of the atomic statement (between s0 and s1), VCC simulates the actions of other threads by havocing non-sequential state. This is an overapproximation, VCC wouldn't know or automatically apply that since &pred has to stay closed all the time while other threads interfere, that the transitive closure of the invariant holds (and indeed invariant are not required to be transitive in VCC). Instead, claim properties can be used to carry such knowledge, and stability is checked at claim creation time. Here you would need to construct a temporary claim (before the atomic statement) that states "when_claimed(pred.isGood[m]) ==> pred.isGood[m]". This should be sufficient to show the first assertion. (Passing in such a claim should also be possible but it shifts the responsibility of constructing such a claim to the caller.)

Hope that helps, Mark

Dec 3, 2010 at 2:06 PM

Hi Mark,

Thanks for the quick and indeed very useful reply. I figured this morning, after a night's sleep that one might write non transitive invariants for which this wouldn't hold, and was starting to think that there was simply no way around it, apart from assuming it was true, and justifying it offline by transitivity of my particular invariants.

Thanks again,