Progress guarantee for parallel programs via bounded lock-freedom

Parallel platforms are becoming ubiquitous with modern computing systems. Many parallel applications attempt to avoid locks in order to achieve high responsiveness, aid scalability, and avoid deadlocks and livelocks. However, avoiding the use of system locks does not guarantee that no locks are actually used, because progress inhibitors may occur in subtle ways through various program structures. Notions of progress guarantee such as lock-freedom, waitfreedom, and obstruction-freedom have been proposed in the literature to provide various levels of progress guarantees. In this paper we formalize the notions of progress guarantees using linear temporal logic (LTL). We concentrate on lock-freedom and propose a variant of it denoted bounded lock-freedom, which is more suitable for guaranteeing progress in practical systems. We use this formal definition to build a tool that checks if a concurrent program is bounded lock-free for a given bound. We then study the interaction between progr...

• Type: Conference
• Year: 2009
• Where: PLDI
• Authors: Erez Petrank, Madanlal Musuvathi, Bjarne Steensgaard
• Keywords: Many Parallel Applications, PLDI 2009, Progress Guarantees, Progress Inhibitors