Modular verification of deadlock-freedom in the presence of condition variables

One of the common methods to synchronize threads in multithreaded programs is using condition variables, where calling the wait command for a condition variable blocks the caller thread and calling a signal command over that condition variable unblocks all the blocked threads waiting for that condition variable. One potential problem with these programs is that a waiting thread is not signaled and is blocked forever. In this paper a verification approach for deadlock-freedom of such programs is presented. In this approach a correspondence is established between a condition variable and a ghost variable, such that its value when a condition variable is created and a wait command for that variable is called is non-negative and non-positive, respectively. Calling a wait command for a condition variable requires a credit for that variable, where a credit for that condition variable can be achieved when another thread increments the corresponding ghost variable and also signals that condition variable if the old value is zero. We are now developing a Coq formalization to formally prove soundness of the presented approach.nrpages: 15status: publishe