Universal Causality Graphs: A Precise Happens-Before Model for Detecting Bugs in Concurrent Programs

Triggering errors in concurrent programs is a notoriously difficult task. A key reason for this is the behavioral complexity resulting from the large number of interleavings of operations of different threads. Efficient static techniques, therefore, play a critical role in restricting the set of interleavings that need be explored in greater depth. The goal here is to exploit scheduling constraints imposed by synchronization primitives to determine whether the property at hand can be violated and report schedules that may lead to such a violation. Towards that end, we propose the new notion of a Universal Causality Graph (UCG) that given a correctness property P, encodes the set of all (statically) feasible interleavings that may violate P. UCGs provide a unified happens-before model by capturing causality constraints imposed by the property at hand as well as scheduling constraints imposed by synchronization primitives as causality constraints. Embedding all these constraints into ...

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Vineet Kahlon, Chao Wang
• Keywords: Causality Constraints, CAV 2010, Hardware, Scheduling Constraints, Synchronization Primitives