Static Deadlock Detection for the SHIM Concurrent Language

10 years 1 months ago
Static Deadlock Detection for the SHIM Concurrent Language
Concurrent programming languages are becoming mandatory with the advent of multi-core processors. Two major concerns in any concurrent program are data races and deadlocks. Each are potentially subtle bugs that can be caused by non-deterministic scheduling choices in most concurrent formalisms. As an alternative, the SHIM concurrent language guarantees the absence of data races by eschewing shared memory, but a SHIM program may still deadlock if a program violates a communication protocol. We present a model-checking-based static deadlock detection technique for the SHIM language. Although SHIM is asynchronous, its semantics allow us to model it synchronously without losing precision, greatly reducing the state space that must be explored. This plus the obvious division between control and data in SHIM programs makes to construct concise abstractions. Experimentally, we find our procedure runs in only a few seconds for modest-sized programs, making it practical to use as part of a co...
Nalini Vasudevan, Stephen A. Edwards
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Authors Nalini Vasudevan, Stephen A. Edwards
Comments (0)