skip to main content
10.1145/2676726.2677008acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Succinct Representation of Concurrent Trace Sets

Published: 14 January 2015 Publication History

Abstract

We present a method and a tool for generating succinct representations of sets of concurrent traces. We focus on trace sets that contain all correct or all incorrect permutations of events from a given trace. We represent trace sets as HB-Formulas that are Boolean combinations of happens-before constraints between events. To generate a representation of incorrect interleavings, our method iteratively explores interleavings that violate the specification and gathers generalizations of the discovered interleavings into an HB-Formula; its complement yields a representation of correct interleavings.
We claim that our trace set representations can drive diverse verification, fault localization, repair, and synthesis techniques for concurrent programs. We demonstrate this by using our tool in three case studies involving synchronization synthesis, bug summarization, and abstraction refinement based verification. In each case study, our initial experimental results have been promising.
In the first case study, we present an algorithm for inferring missing synchronization from an HB-Formula representing correct interleavings of a given trace. The algorithm applies rules to rewrite specific patterns in the HB-Formula into locks, barriers, and wait-notify constructs. In the second case study, we use an HB-Formula representing incorrect interleavings for bug summarization. While the HB-Formula itself is a concise counterexample summary, we present additional inference rules to help identify specific concurrency bugs such as data races, define-use order violations, and two-stage access bugs. In the final case study, we present a novel predicate learning procedure that uses HB-Formulas representing abstract counterexamples to accelerate counterexample-guided abstraction refinement (CEGAR). In each iteration of the CEGAR loop, the procedure refines the abstraction to eliminate multiple spurious abstract counterexamples drawn from the HB-Formula.

Supplementary Material

MPG File (p433-sidebyside.mpg)

References

[1]
A. Albarghouthi and K. McMillan. Beautiful interpolants. In CAV, pages 313--329, 2013.
[2]
S. Basu, D. Saha, Y. Lin, and S. Smolka. Generation of all counter-examples for push-down systems. In FORTE, pages 79--94. 2003.
[3]
D. Beyer. Status report on software verification. In TACAS, pages 373--388. 2014. http://sv-comp.sosy-lab.org/.
[4]
D. Beyer, T. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In PLDI, pages 300--309, 2007.
[5]
D. Beyer and E. Keremoglu. CPACHECKER: A tool for configurable software verification. In CAV, pages 184--190, 2011. http://cpachecker.sosy-lab.org/.
[6]
P. Bjesse and J. Kukula. Using counter example guided abstraction refinement to find complex bugs. In DATE, pages 156--161, 2004.
[7]
N. Bjørner, K. McMillan, and A. Rybalchenko. On solving universally quantified horn clauses. In SAS, pages 105--125, 2013.
[8]
P. Černy, T. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach. Efficient synthesis for concurrency by semantics-preserving transformations. In CAV, pages 951--967, 2013.
[9]
P. Černy, T. Henzinger, A. Radhakrishna, L. Ryzhyk, and T. Tarrach. Regression-free synthesis for concurrency. In CAV, pages 568--584. 2014. https://github.com/thorstent/ConRepair.
[10]
S. Cherem, T. Chilimbi, and S. Gulwani. Inferring locks for atomic sections. In PLDI, pages 304--315, 2008.
[11]
E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS, pages 168--176, 2004. http://www.cprover.org/cbmc/.
[12]
E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. SATABS: SAT-based predicate abstraction for ANSI-C. In TACAS, pages 570--574, 2005.
[13]
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. Springer, 1982.
[14]
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, pages 154--169, 2000.
[15]
L. De Moura and N. Bjørner. Z3: An efficient smt solver. In CACAS, pages 337--340. 2008. http://z3.codeplex.com/.
[16]
A. Donaldson, A. Kaiser, D. Kroening, and T. Wahl. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In CAV, pages 356--371, 2011.
[17]
D. Engler and K. Ashcraft. Racerx: effective, static detection of race conditions and deadlocks. In SOSP, pages 237--252, 2003.
[18]
E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test them. In PDPS, page 7 pp., 2003.
[19]
A. Farzan, A. Holzer, N. Razavi, and H. Veith. Con2colic testing. In FSE, pages 37--47, 2013.
[20]
A. Farzan, Z. Kincaid, and A. Podelski. Inductive data flow graphs. In POPL, pages 129--142. 2013.
[21]
M. Glusman, G. Kamhi, S. Mador-Haim, R. Fraer, and M. Vardi. Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation. In TACAS, pages 176--191. 2003.
[22]
A. Gupta, C. Popeea, and A. Rybalchenko. Solving recursion-free horn clauses over li+uif. In APLAS, pages 188--203, 2011.
[23]
T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL, pages 232--244, 2004.
[24]
J. Huang, P. Meredith, and G. Roşu. Maximal sound predictive race detection with control flow abstraction. In PLDI, pages 337--348, 2014.
[25]
N. Jalbert and K. Sen. A trace simplification technique for effective debugging of concurrent programs. In FSE, pages 57--66, 2010.
[26]
G. Jin, W. Zhang, D. Deng, B. Liblit, and S. Lu. Automated Concurrency-Bug Fixing. In OSDI, pages 221--236. 2012.
[27]
V. Kahlon and C. Wang. Universal causality graphs: a precise happens- before model for detecting bugs in concurrent programs. In CAV, pages 434--449, 2010.
[28]
S. Kashyap and V. Garg. Producing short counterexamples using "crucial events". In CAV, pages 491--503. 2008.
[29]
S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In ASPLOS, pages 329--339, 2008.
[30]
Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. In TOPLAS, pages 68--93, 1984.
[31]
J. Morse, M. Ramalho, L. Cordeiro, D. Nicole, and B. Fischer. ES-BMC 1.22. In TACAS, pages 405--407. 2014. http://www.esbmc.org/.
[32]
M. Said, C. Wang, Z. Yang, and K. Sakallah. Generating data race witnesses by an smt-based analysis. In NASA Formal Methods, pages 313--327. 2011.
[33]
T. Sakunkonchak, S. Komatsu, and M. Fujita. Using counterexample analysis to minimize the number of predicates for predicate abstraction. In ATVA, pages 553--563. 2007.
[34]
S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. on Computer Systems (TOCS), pages 391--411, 1997.
[35]
K. Sen, G. Roşu, and G. Agha. Detecting errors in multithreaded programs by generalized predictive analysis of executions. In FMOODS, pages 211--226, 2005.
[36]
R. Sharma, A. V. Nori, and A. Aiken. Interpolants as classifiers. In CAV, pages 71--87, 2012.
[37]
N. Sinha and C. Wang. On Interference Abstractions. In POPL, pages 423--434, 2011.
[38]
Y. Smaragdakis, J. Evans, C. Sadowski, J. Yi, and C. Flanagan. Sound predictive race detection in polynomial time. ACM SIGPLAN Notices, pages 387--400, 2012.
[39]
M. Vechev, E. Yahav, and G. Yorsh. Abstraction-guided synthesis of synchronization. In POPL, pages 327--338, 2010.
[40]
M. T. Vechev, E. Yahav, and G. Yorsh. Inferring synchronization under limited observability. In TACAS, pages 139--154, 2009.
[41]
C. Wang, S. Kundu, M. Ganai, and A. Gupta. Symbolic predictive analysis for concurrent programs. In FM, pages 256--272. 2009.
[42]
C. Wang, B. Li, H. Jin, G. Hachtel, and F. Somenzi. Improving ariadne's bundle by following multiple threads in abstraction refinement. IEEE TCAD, pages 2297--2316, 2006.
[43]
C. Wang, R. Limaye, M. Ganai, and A. Gupta. Trace-based symbolic analysis for atomicity violations. In TACAS, pages 328--342. 2010.

Cited By

View all
  • (2022)Consistency-preserving propagation for SMT solving of concurrent program verificationProceedings of the ACM on Programming Languages10.1145/35633216:OOPSLA2(929-956)Online publication date: 31-Oct-2022
  • (2022)Automated Synthesis of AsynchronizationsStatic Analysis10.1007/978-3-031-22308-2_7(135-159)Online publication date: 5-Dec-2022
  • (2020)On Scheduling Constraint Abstraction for Multi-Threaded Program VerificationIEEE Transactions on Software Engineering10.1109/TSE.2018.286412246:5(549-565)Online publication date: 1-May-2020
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. bug summarization
  2. cegar
  3. concurrent programs
  4. synchronization synthesis
  5. trace generalization

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)8
  • Downloads (Last 6 weeks)0
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2022)Consistency-preserving propagation for SMT solving of concurrent program verificationProceedings of the ACM on Programming Languages10.1145/35633216:OOPSLA2(929-956)Online publication date: 31-Oct-2022
  • (2022)Automated Synthesis of AsynchronizationsStatic Analysis10.1007/978-3-031-22308-2_7(135-159)Online publication date: 5-Dec-2022
  • (2020)On Scheduling Constraint Abstraction for Multi-Threaded Program VerificationIEEE Transactions on Software Engineering10.1109/TSE.2018.286412246:5(549-565)Online publication date: 1-May-2020
  • (2020)Extracting safe thread schedules from incomplete model checking resultsInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00575-y22:5(565-581)Online publication date: 1-Oct-2020
  • (2020)Root Causing Linearizability ViolationsComputer Aided Verification10.1007/978-3-030-53288-8_17(350-375)Online publication date: 21-Jul-2020
  • (2019)Resource-guided program synthesisProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314602(253-268)Online publication date: 8-Jun-2019
  • (2019)Parallel refinement for multi-threaded program verificationProceedings of the 41st International Conference on Software Engineering10.1109/ICSE.2019.00074(643-653)Online publication date: 25-May-2019
  • (2019)Extracting Safe Thread Schedules from Incomplete Model Checking ResultsModel Checking Software10.1007/978-3-030-30923-7_9(153-171)Online publication date: 15-Jul-2019
  • (2018)Automatic Synchronization for GPU Kernels2018 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2018.8602999(1-9)Online publication date: Oct-2018
  • (2018)Scheduling constraint based abstraction refinement for weak memory modelsProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering10.1145/3238147.3238223(645-655)Online publication date: 3-Sep-2018
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media