Predicting serializability violations: SMT-based search vs. DPOR-based search

Arnab Sinha, Sharad Malik, Chao Wang, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationHardware and Software
Subtitle of host publicationVerification and Testing - 7th International Haifa Verification Conference, HVC 2011, Revised Selected Papers
Pages95-114
Number of pages20
DOIs
StatePublished - 2012
Event7th International Haifa Verification Conference, HVC 2011 - Haifa, Israel
Duration: Dec 6 2011Dec 8 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7261 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other7th International Haifa Verification Conference, HVC 2011
Country/TerritoryIsrael
CityHaifa
Period12/6/1112/8/11

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Predicting serializability violations: SMT-based search vs. DPOR-based search'. Together they form a unique fingerprint.

Cite this