Skip to main content

Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search

Author(s): Sinha, Arnab; Malik, Sharad; Wang, Chao; Gupta, Aarti

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1r83k
Abstract: In our recent work, we addressed the problem of detecting serializability violations in a concurrent program using predictive analysis, where we used a graph-based method to derive a predictive model from a given test execution. The exploration of the predictive model to check alternate interleavings of events in the execution was performed explicitly, based on stateless model checking using dynamic partial order reduction (DPOR). Although this was effective on some benchmarks, the explicit enumeration was too expensive on other examples. This motivated us to examine alternatives based on symbolic exploration using SMT solvers. In this paper, we propose an SMT-based encoding for detecting serializability violations in our predictive model. SMT-based encodings for detecting simpler atomicity violations (with two threads and a single variable) have been used before, but to our knowledge, our work is the first to use them for serializability violations with any number of threads and variables. We also describe details of our DPOR-based explicit search and pruning, and present an experimental evaluation comparing the two search techniques. This provides some insight into the characteristics of the instances when one of these is superior to the other. These characteristics can then be used to predict the preferred technique for a given instance.
Publication Date: 2012
Citation: Sinha, Arnab, Sharad Malik, Chao Wang, and Aarti Gupta. "Predicting Serializability Violations: SMT-Based Search vs. DPOR-Based Search." In Haifa Verification Conference (2012): pp. 95-114. doi:10.1007/978-3-642-34188-5_11
DOI: 10.1007/978-3-642-34188-5_11
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 95 - 114
Type of Material: Conference Article
Journal/Proceeding Title: Haifa Verification Conference
Version: Author's manuscript



Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.