Lock Allocation

Michael Emmi, Jeff Fischer, Ranjit Jhala and Rupak Majumdar

We introduce lock allocation, an automatic technique that takes a multithreaded program annotated with atomic sections (that must be executed atomically), and infers a lock assignment from global variables to locks and a lock instrumentation that determines where each lock should be acquired and released such that the resulting instrumented program is guaranteed to preserve atomicity and deadlock freedom (provided all shared state is accessed only within atomic sections). Our algorithm works in the presence of pointers and procedures, and sets up the lock allocation problem as a 0-1 ILP which minimizes the conflict cost between atomic sections and simultaneously minimizes the number of locks. We have implemented our algorithm for both C with pthreads and Java, and have applied it to infer locks in 15K lines of AOLserver code. Our automatic allocation produces the same results as hand annotations for most of this code, while solving the optimization instances within a second for most programs.

Proceedings of the 34th Annual ACM Symposium on the Principles of Programming Languages, 2007. (POPL), 2007 (to appear).

PDF PostScript © 2007.