How to use VCC to verify concurrent programs

Nov 16, 2012 at 12:09 PM
Edited Nov 16, 2012 at 12:12 PM

I want to verify the following program and obtain interleavings that cause the assertion to fail. However, VCC does not only complain about the assertion failure, but also about not thread-local variables.

"D:\Documents\1stRotation\driverConcurrency\examples\ex3-vcc.c(21,12) : error VC8512: Assertion 'IntrMask is thread local (accessing field data)' did not verify.

(and many more of these)

Can you tell how to make VCC infer these things automatically for such small examples and complain only about the assertion failure if it finds an interleaving that leads to it?

Thanks, Thorsten

Program:

#include <vcc.h>

int IntrMask;
int intr_mask;
int handled;

void thread1()
{
    while (IntrMask == 0);

    if (intr_mask == 1) {
        handled = 1;
    }
	
	_(assert (handled == 1))
}

void thread2() {
    IntrMask = 1;
    intr_mask = 1;
}
Editor
Nov 20, 2012 at 3:03 PM

Hi Thorsten,

The VCC methodology is based on reducing the verification of concurrent programs to local proof obligations. Unfortunately, this means that all reasoning is local, and that, as far as I know, you have to come up with invariants, even for simple programs (and indeed even for sequential programs) by yourself.

In particular, VCC never assumes that it was given the entire program, simply assuming that the (unknown) rest of the program fulfills the invariants it currently knows about. This means that, given the code shown above, VCC will simply assume that there is somewhere else a third thread that wreaks the worst possible havoc in your shared variables.

As far as I know, there is currently no tool, either inside VCC or outside, that analyzes a concurrent program, under the assumption that the whole program is given, and automatically infers local invariants as considered by VCC. In fact, I'm not sure there is an easy systematic way of turning rely/guarantee-style concurrent specs into VCC invariants.

Francois

Nov 20, 2012 at 3:08 PM

Hi Francois,

Thanks for your explanation.

As a matter of fact I found a tool that does exactly what we need: Poirot (http://research.microsoft.com/en-us/projects/poirot/). It seems to work on the small examples we fed it so far.

Thorsten