Sciweavers

CAV
2010
Springer

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

13 years 5 months ago
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 ...
Vineet Kahlon, Chao Wang
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2010
Where CAV
Authors Vineet Kahlon, Chao Wang
Comments (0)