Atomic block for concurrent program

Nov 22, 2010 at 2:53 AM

Hi,

I am new user of VCC.

In Concurrent C code I have these following two statements executing concurrently, 

x = x+1

//

x = x +2

In VCC can it implemented by following way in some function call myFunc? ,

void myFunc(struct A *num)

requires(wrapped(num))

writes(num)

ensures(wrapped(num))

{

atomic(num){

num->x = num->x +1

//check for the invariants.

}

atomic(num) {

num->x = num->x +2

//check for the invariants.

}

}

The code is not completed but I just wanted to know about the use of atomic block for the above two statements.

Looking for your suggestion.

 

Thanks.

Coordinator
Nov 25, 2010 at 9:02 AM

Hi,

  using atomic() {} for concurrent statement is the right way. Here are two comments, though:

  • VCC assumes that a function is run in a single thread. So, by putting both atomic statements into a single function, you are assuming that both statements are executed in a single thread. In general, you would place the different statements in separate functions.
  • Instead of the requirement that a concurrently accessed object is wrapped on function entry, in VCC we would typically pass in a (wrapped) claim stating that the object is closed. The former requirement is stronger, since there can be only a single / unique owner of an object at given time, while there can be many threads holding a claim on an object. Both requirements allow to derive that inside an atomic statement the object is closed after thread interference, which you need to know in order to be able to rely on the objects invariants and operate on it (VCC will check this condition).
  • As an aside, there are uses of passing in a concurrently accessed object as wrapped, e.g., during object destruction or when the object has thread-approved volatile fields. Thread-approved volatile fields are of the form "volatile f;" with an invariant "invariant(approves(owner(this),f))". These fields behave like  sequential fields to the owning thread, think of them as single-writer, multiple-readers fields.

Here is the more general pattern:

void add_one(struct A *num claimp(c))
  always(c, closed(num))
  // "always(c,e)" is logically equivalent to "maintains(wrapped(c)) requires(claims(c, e))"
{
  atomic (c, num) { // note the additional argument
     num->x = num->x + 1;
  }
}

void add_two(struct A *num claimp(c))
  always(c, closed(num))
{
  atomic (c, num) {
     num->x = num->x + 2;
  }
}

Hope this helps,

Mark