Sound Automatic Lock Placement for Concurrent Programs with Pointers
Nicolas Waldburger, Florian Faissole, Ryo Okabe, Denis Cousineau
原文摘要
We propose a lightweight method for automatic lock placement in concurrent POSIX programs with explicit pointer manipulation, such as C programs. Given a program that lacks sufficient user-placed mutexes, or contains none at all, our method introduces new mutexes to prevent data races. The method is formally proven to guarantee the absence of data races and mainly consists of three steps. The first step performs lockset analysis and may-happen-in-parallel analysis. The second step conducts a concurrent points-to analysis derived from a Steensgaard-like procedural analysis, where per-thread points-to graphs are unified using a special completion rule. The final step places locks to prevent data races while respecting a lock ordering to avoid deadlocks. In addition, user-annotated critical sections are protected through insertion of dedicated locks. Since lock placement is a complex and error-prone task, our method aims at helping developers write correct concurrent programs.
cs.LO