Consistency of value of volatile variable: parity.c

Mar 17, 2011 at 6:42 PM

In the file parity.c in directory Demo( in source code)

typedef struct vcc(claimable) _A {
 volatile int f;
 invariant(unchanged(f) || f == unchecked(old(f) + 2))
 // unchecked() used as work-around for issue 5883
} A;

int check_parity(A *a spec(out claim_t p))
 requires(wrapped(a))
 writes(a)
 ensures(wrapped(a) && ref_cnt(a) == old(ref_cnt(a)) + 1)
 ensures(wrapped(p) && claims(p, (a->f & 1) == result))
{
 int tmp;
 atomic (a) {
   tmp = a->f;
   bv_lemma(forall (int x; (x&1) == ((x+2) & 1)));
   spec(p = claim(a, (a->f & 1) == (tmp & 1));)

  assert( a->f== tmp);   // shouldn't it be false??

 }

 assert( a->f == tmp);  // shouldn't it be false???

assert(a->f >=tmp);     // true
   return (tmp & 1);
}

Why it verifies?

f is volatile, how can value a->f remains unchanged always?

Coordinator
Mar 22, 2011 at 9:33 AM

Hi George,

  VCC's treatment of concurrency is based on a reduction theorem by which other threads' interference (changes to volatile fields as above) needs only to be considered at a few points in the program, namely at the beginning of atomic blocks and across (most) functions calls. In other places (e.g., like the place of your asserts above) volatile fields seem to behave like sequential fields. Note that program code could not take advantage of that, since VCC enforces the use of atomic blocks for accesses to volatile fields of closed objects.

  More details on the reduction theorem are in http://research.microsoft.com/en-us/um/people/moskal/pdf/concurrency3.pdf, and on assertions in concurrent context are here http://vcc.codeplex.com/wikipage?title=Assertions%20in%20Concurrent%20Context&referringTitle=Documentation.

Hope that helps, Mark  

Developer
Apr 1, 2011 at 1:11 AM

Note also that

1) The assertion within the atomic statement should succeed, even without reduction considerations.

2) The implicit reduction has an effect of changing the meaning of assertions that mention volatile variables. The reason that your second assertion succeeds is that it is evaluated in a state that uses (for volatile variables) the values they had at the end of your atomic action. The reduction theorem guarantees that this pretense is invisible to programs, i.e. it doesn't effecdt "observable" (i.e. stable) aspects of program behavior (like crashing!).