Reducing Deadlock and Livelock Freedom to Termination

ABSTRACT. In this paper we introduce a general method for proving deadlock and livelock freedom of concurrent programs with shared memory. Our goal in this work is to support programs which use locks stored in mutable data structures. The key to our technique is the observation that dependencies between locks can be abstracted using recursion and non-determinism in a sequential logic program such that termination of the abstraction implies deadlock and livelock freedom of the original program.