[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] threading

All,

I recently completed an analysis on some pthreads based C++ code using AT&T's SPIN. The code purported to implement a concurrent event queue in which a producer thread(s) would add events to a queue whilst consumer thread(s) removed events from that queue. It used a pthread condition instance to eliminate  a busy-wait-loop.

SPIN did a very good job at answering fundamental questions to include:

* did the code deadlock? (it did not)
* could any of the threads be starved for CPU cycles? (nope)
* were all states reachable? (no, some were not reachable.)
* did the producer thread(s) signal consumers only when data was there?
   (no it did not; bug)
* did the consumer thread(s) try to remove events only when data was
   in the queue? (no, there was a bug for two or more get threads)
* process of modeling code helped identify numerous other technical
   glitches and inefficiences.

All in all, a very good exercise.

How would one approach answering these same questions in PVS?

Shane Miller