2008 Articles
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 it easy 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 compilation chain.
Subjects
Files
-
vasudevan2008static.pdf application/pdf 96.2 KB Download File
Also Published In
- Title
- Proceedings, Sixth ACM & IEEE International Conference on Formal Methods and Models for Co-Design: MEMOCODE '08: June 5-7, 2008, Anaheim, CA, USA
- Publisher
- IEEE
- DOI
- https://doi.org/10.1109/MEMCOD.2008.4547686
More About This Work
- Academic Units
- Computer Science
- Published Here
- September 20, 2011