Using VCC to detect situations like starvation or deadlocks

Apr 20, 2011 at 1:42 PM

In case of concurrent verification can we use VCC to detect cases like deadlocks or starvations or liveliness etc..


For e.g. the implementation of Reader-Writer code does not ensures that some reader or writer will eventually get its turn, leading to starvation.

Can VCC be used to detect this situation, something like VCC tries to prove that 'eventually(reader gets to read the object)'.

Apr 24, 2011 at 9:20 AM

I am sorry, is my doubt irreverent or i didn't pose it clearly?

Apr 24, 2011 at 9:51 AM

No, your doubts are fine, I think it's just that it's a long weekend :)

As far as I know, VCC cannot be used to prove liveness properties, and I do not think it can be adapted, as the whole point of VCC is to prove properties of arbitrary parallel compositions of threads by proving local properties of single threads. This modularity cannot, a priori, work for liveness property, since you could always add a thread that never releases its locks and break liveness properties of already verified code.

However, you may be able to find invariants on your synchronisation structures (locks, semaphores...), to ensure, for example, that they are released whenever they are not being actively used. A "simple" paper proof on the side could then convince you (and perhaps others) that your program is indeed deadlock-free.

If those liveness properties are really important to you, I would advise looking into more specific tools (a quick Google gave me this paper, but I am not an expert in liveness, and it is possible that some other temporal logic tools exist for C code).