Sciweavers

EMSOFT
2009
Springer

Compositional deadlock detection for rendezvous communication

14 years 5 months ago
Compositional deadlock detection for rendezvous communication
Concurrent programming languages are growing in importance with the advent of multi-core systems. However, concurrent programs suffer from problems, such as data races and deadlock, absent from sequential programs. Unfortunately, traditional race and deadlock detection techniques fail on both large programs and small programs with complex behaviors. In this paper, we present a compositional deadlock detection technique for a concurrent language—SHIM—in which tasks run asynchronously and communicate using synchronous CSP-style rendezvous. Although SHIM guarantees the absence of data races, a SHIM program may still deadlock if the communication protocol is violated. Our previous work used NuSMV, a symbolic model checker, to detect deadlock in a SHIM program, but it did not scale well with the size of the problem. In this work, we take an incremental, divide-and-conquer approach to deadlock detection. In practice, we find our procedure is faster and uses less memory than the existin...
Baolin Shao, Nalini Vasudevan, Stephen A. Edwards
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where EMSOFT
Authors Baolin Shao, Nalini Vasudevan, Stephen A. Edwards
Comments (0)