Hi, 

I have been trying to figure out atomicity notion in VCC. For the following small example,

_(dynamic_owns) struct T {  int x;};

struct T *t;

void foo() 

_(requires \wrapped(t) ) 

_(writes \span(t)) 

_(requires t->x < INT_MAX) 

_(ensures t->x == \old(t->x) + 1)

{  _(unwrapping t)   // line 0 

t->x += 1; 

//line 1

// line 2

_(wrap t) // line 3

_(assert t->x == \old(t->x)+1 )

}

Verification of foo method succeeds

It would be great if you can help me to make the following points clear for me.

1.  'unwrapping' sets the ownership of object and its subfields to current thread. Is it something that includes implicit synchronization on object and its subfields, like implicit lock? If it is the case,   the block between _(unwrapping t) ... _(wrap t) can lead us to reason about the operations on t and its subfields performed atomically, right?  

2. However, I think point 1, atomicity issue, is not provided by these wrap and unwrap constructs. Because, _(assert t->x == \old(t->x)+1) or the reverse of this assertion always passes and I cant really understand why this happens. 

Conclusion and questions:

Does it mean that we need an expilicit synchronization objects like explicit lock modelling associated with object and use it before unwrapping and wrapping objects?

           _(lock t->lock)

                 _(unwrapping t)

                _(wrap t)

  _(unlock t->lock)

  If I can be sure about these notions , I can be going on different models , relaxations about these constructs.

THANKS IN ADVANCE!

Ismail

Hi Ismail,

  unwrap / wrap / unwrapping are constructs for sequential program verification in VCC. If a function has write access to a sequential ownership domain (_(requires \wrapped(x)) _(writes x)), it can update anything in that ownership domain, and no other thread / object can directly refer to this domain (this can should up as invariants not being admissible anymore). In a concurrent setting in VCC, you'd keep objects as closed, and would then be allowed to modify volatile fields inside of atomic statements, satisfying the transition / two-state invariants of the relevant objects. (Those fields and objects need not to be implementation objects, they may also be ghost). The VCC tutorial / papers should provide additional material on this.

  In the given code, there's an additional problem: the requires _(writes \span(t)) and _(requires \wrapped(t)) contradict each other. The former implies that the fields of t are writable, and thus t cannot be wrapped, as the second requirement requires. So, for your given example you can prove anything. (The /smoke switch can help to detect such cases).

  Hope this helps, Mark

Hi Mark,

This source code is taken from tutorials under VCC's source code and I used smoke and figured out the unreachable part of the code in the foo_method as you mentioned.  Thanks a lot.

As you mentioned , atomic block provides you to do one machine instruction to be done in atomic block but I do want to build bigger atomic blocks . I think to do this I have to use claims where if you can pass one claim then you can inherit the passed claim in new claim and create a new atomic block to build which you can integrate it to previous atomic block with passed claim.

My concern is whether there is any atomicity violation during these integration of atomic blocks. 

......

 atomic(c,a) {
    y = a->x;
    spec( c1 = claim(c, y <= a->x); )
  }
 
  if (y >= 0x7fffffff) {
      unclaim(c1,c);
      return;
  }
 
  atomic(c, c1, a) {
    // inlined InterlockedCompareAndExchange
    if (a->x == y) {
      a->x = y + 1;
    }
    spec( c2 = claim(c, y < a->x); )
  }
 
  atomic(c, c2, a) {
    z = a->x;
  }

.....

Thanks Mark

Ismail