[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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?