Detecting Concurrency Bugs in Higher-Order Programs through Abstract Interpretation

Manually detecting bugs in concurrent programs is hard due to the myriad of thread interleavings that needs to be accounted for. Higher-order programming features only exacerbate this difficulty. The need for tool support therefore increases as these features be-come more widespread. We investigate the P(CEK⋆)S abstract ma-chine as the foundation for tool support for detecting concurrency bugs. This abstract interpreter analyzes multi-threaded, higher-order programs with shared-store concurrency and a compare-and-swap synchronization primitive. In this paper, we evaluate two different approaches to reduce the size of the state space explored by the abstract interpreter. First, we integrate abstract garbage col-lection into the abstract interpreter, and we observe that it does not reduce the state space as expected. We then evaluate the im-pact of adding first-class support for locks on the machine’s client analyses. To this end, we compare a cas-based and a lock-based formulation of race condition and deadlock detection analyses. We show that adding first-class support for locks not only significantly reduces the number of abstract program states that need to be ex-plored, but also simplifies formulating the client analyses