Using atomic-statement with variables

Dec 14, 2011 at 3:00 PM

Hello,

I'm using VCC for some weeks now and I have a question regarding the atomic statement: Let's consider the following code snippet (which was my first attempt but did not work):

volatile unsigned int field;

void foo() 
_(writes &field) 
 {
        // variable "field" changed to 0 by another thread
	_(atomic &field) { // does not work
		field = 0;
	}
}
I know that this works, if "field" is within a struct, but is there a possibility to use a simple variable instead? I already tried \gemb(&field) but that didn't do the trick either.

Thanks!

Developer
Jan 13, 2012 at 6:20 PM

Using \gemb(&field) does work:

volatile unsigned int field;

void foo() 
_(requires \wrapped(\gemb(&field)))
_(writes (\gemb(&field))) 
{ 
  _(atomic \gemb(&field)) { 
    field = 0; 
    _(bump_volatile_version \gemb(&field)) 
  } 
}

Note that
- \gemb(&field) doesn't have to be wrapped, but you must be able to prove that it is closed to operate on its volatile fields in an atomic.
- By definition, the invariant of \gemb(&x) is \approves(\this->\owner, x), so an update to \gemb(&x) has to bump the volatile version. This also means that if the caller owns \gemb(&x), it has to list it in the writes clause.  The reason for using this invariant is that you will normally want to use the global as part of a larger object with a nontrivial invariant, so approval is needed to make this invariant admissible.
Jan 13, 2012 at 7:15 PM

Hi erniecohen,

thanks a lot, it works fine!

Jan 16, 2012 at 2:07 PM
Edited Jan 16, 2012 at 4:22 PM

Hi,

i'm sorry for posting again, but i have a question regarding your reply:

What exactly does \approves(...) stands for? I didn't find much about it in the documentation/papers, but i've read in a previous thread, that it is something like \unchanged(x) || inv2(\this->owner), where this->owner is a thread. I'm asking because I'm not sure why bump_volatile_version is needed, but obviously it is nedded to satisfy the invariant.

 

[Edit]

My plan is to use VCC to verify properties of embedded systems and therefore I need a way to simulate the behaviour of the environment. E.g. an input (of a microcontroller) is mapped to a variable "int temperature" and the value of the variable describes the currently measured temperature. Using VCC, the environment could be described by concurrent threads changing these variables.

For now, I use atomic statements to simulate the random change of those variables, for example:

unsigned int temperature;
...

// simulate random assignment of variable "temperature"
_(atomic \gemb(&temperature)) {}

if(_(atomic_read \gemb(&temperature)) temperature > 20) {
  // do something
}
else{
  // do something else
}

It doesn't produce any unreachable code, so I guess it works. Please let me know if you have any suggestions.

Regards