Succinct representation of concurrent trace sets Conference Paper

Author(s): Gupta, Ashutosh; Henzinger, Thomas A; Radhakrishna, Arjun; Samanta, Roopsha; Tarrach, Thorsten
Title: Succinct representation of concurrent trace sets
Affiliation IST Austria
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.
Keywords: Trace Generalization; Concurrent Programs; Synchronization Synthesis; Bug Summarization; CEGAR
Conference Title: POPL: Principles of Programming Languages
Conference Dates: January 12 - January 18, 2015
Conference Location: Mumbai, India
Publisher: ACM  
Date Published: 2015-01-01
Start Page: 433
End Page: 444
DOI: 10.1145/2676726.2677008
Notes: The authors would like to thank Jyotirmoy Deshmukh, Roderick Bloem, and Bettina K├Ânighofer for enabling fruitful discussions. The authors would also like to thank the anonymous reviewers for their considerable, constructive feedback.
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Ashutosh Gupta
    16 Gupta
Related IST Austria Work