Race checking by context inference

T.A. Henzinger, R. Jhala, R. Majumdar, in:, ACM, 2004, pp. 1–13.

Download
No fulltext has been uploaded. References only!

Conference Paper | Published
Author
; ;
Abstract
Software model checking has been successful for sequential programs, where predicate abstraction offers suitable models, and counterexample-guided abstraction refinement permits the automatic inference of models. When checking concurrent programs, we need to abstract threads as well as the contexts in which they execute. Stateless context models, such as predicates on global variables, prove insufficient for showing the absence of race conditions in many examples. We therefore use richer context models, which combine (1) predicates for abstracting data state, (2) control flow quotients for abstracting control state, and (3) counters for abstracting an unbounded number of threads. We infer suitable context models automatically by a combination of counterexample-guided abstraction refinement, bisimulation minimization, circular assume-guarantee reasoning, and parametric reasoning about an unbounded number of threads. This algorithm, called CIRC, has been implemented in BLAST and succeeds in checking many examples of NESC code for data races. In particular, BLAST proves the absence of races in several cases where previous race checkers give false positives.
Publishing Year
Date Published
2004-06-01
Page
1 - 13
Conference
PLDI: Programming Languages Design and Implementation
IST-REx-ID

Cite this

Henzinger TA, Jhala R, Majumdar R. Race checking by context inference. In: ACM; 2004:1-13. doi:10.1145/996841.996844
Henzinger, T. A., Jhala, R., & Majumdar, R. (2004). Race checking by context inference (pp. 1–13). Presented at the PLDI: Programming Languages Design and Implementation, ACM. https://doi.org/10.1145/996841.996844
Henzinger, Thomas A, Ranjit Jhala, and Ritankar Majumdar. “Race Checking by Context Inference,” 1–13. ACM, 2004. https://doi.org/10.1145/996841.996844.
T. A. Henzinger, R. Jhala, and R. Majumdar, “Race checking by context inference,” presented at the PLDI: Programming Languages Design and Implementation, 2004, pp. 1–13.
Henzinger TA, Jhala R, Majumdar R. 2004. Race checking by context inference. PLDI: Programming Languages Design and Implementation 1–13.
Henzinger, Thomas A., et al. Race Checking by Context Inference. ACM, 2004, pp. 1–13, doi:10.1145/996841.996844.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar