Most previous work on race condition detection and inference of synchronization disciplines (methods of synchronizing access to shared data in concurrent programs) has focused on the lockset model, using both static and dynamic analyses. However, the lockset model is restrictive and is not sufficiently expressive to capture synchronization disciplines other than mutual exclusion locks. We present the Grits synchronization discipline specification language, an expressive model for ensuring race-freedom in concurrent programs. We also present Hominy, an accompanying synchronization discipline specification inference tool for the Grits specification language. Our experience shows that Grits and Hominy are sufficiently expressive to capture nearly all synchronization disciplines.
PDF (645KB)