Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Abstract semantic diffing of evolving concurrent programs

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We present an approach for comparing two closely related concurrent programs, whose goal is to give feedback about interesting differences without relying on user-provided assertions. This approach compares two programs in terms of cross-thread interferences and data-flow, under a parametrized abstraction which can detect any difference in the limit. We introduce a partial order relation between these abstractions such that a program change that leads to a “smaller” abstraction is more likely to be regression-free from the perspective of concurrency. On the other hand, incomparable or bigger abstractions, which are an indication of introducing new, possibly undesired, behaviors, lead to succinct explanations of the semantic differences.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

Notes

  1. By configuration, we mean the tuple of thread-local states together with the state of the shared memory.

  2. Our framework is not bound to a specific set of program order constraints and statements to be preserved in the projected traces—they can be chosen arbitrarily.

  3. The synchronization statements are important only for defining the program semantics. As it will be clear in Sect. 4, the abstract traces are agnostic to the synchronization statements used in the program.

  4. Our framework can be extended such that the projection operator removes only a user-specified fragment of the program order.

  5. For a set A, \(\mathcal {P}(A)\) denotes the set of subsets of A.

  6. Therefore, so is a total order on writes to the same variable, and \( rf \) a total function from reads of a variable x to writes to x (according to Definition 1).

  7. The simple syntax we considered in Sect. 3 doesn’t include acquire/release actions, but they can be easily modeled using /.

  8. We denote by \(\cdot \) the concatenation operator.

  9. Recall that we consider programs without looping constructs and procedure calls.

  10. \(A/_\equiv \) is the quotient of the set (relation) A with respect to \(\equiv \).

  11. They are available at https://github.com/thorstent/ConcurrencySwapper and https://github.com/thorstent/Liss.

  12. Studies of concurrency errors, e.g.,  [6, 19], have reported that reordering statements for fixing bugs is very frequent (around 30% of the fixes are based on reorderings).

  13. We refer to the smallest value of k for which the buggy version is not a (V, k)-refinement of the fixed version.

References

  1. Abadi M, Lamport L (1991) The existence of refinement mappings. Theor Comput Sci 82(2):253–284

    Article  MathSciNet  MATH  Google Scholar 

  2. Biere A, Bloem R (eds) (2014) Computer aided verification—CAV 2014, Vienna, Austria, 2014. Proceedings, volume 8559 of LNCS. Springer, Berlin

  3. Bouajjani A, Derevenetc E, Meyer R (2014) Robustness against relaxed memory models. In: Hasselbring W, Ehmke NC (eds) Software engineering, Kiel, Deutschland, volume 227 of LNI, pp 85–86

  4. Burckhardt S, Musuvathi M (2008) Effective program verification for relaxed memory models. In: CAV 2008, pp 107–120

  5. Cerný P, Clarke EM, Henzinger TA, Radhakrishna A, Ryzhyk L, Samanta R, Tarrach T (2017) From non-preemptive to preemptive scheduling using synchronization synthesis. Form Methods Syst Des 50(2–3):97–139

    Article  MATH  Google Scholar 

  6. Cerný P, Henzinger TA, Radhakrishna A, Ryzhyk L, Tarrach T (2013) Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina N, Veith H (eds) computer aided verification —CAV 2013, Saint Petersburg, 2013, volume 8044 of lecture notes in computer science. Springer, Berlin, pp 951–967

    Google Scholar 

  7. Cerný P, Henzinger TA, Arjun R, Leonid R, Thorsten T Regression-free synthesis for concurrency. In: Biere and Bloem [2], pp 568–584

  8. Chaki S, Gurfinkel A, Strichman O (2015) Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation). Form Methods Syst Des 47(3):287–301

    Article  MATH  Google Scholar 

  9. Clarke E, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Tools and algorithms for the construction and analysis of systems (TACAS 2004), volume 2988 of LNCS. Springer, Berlin, pp 168–176

    Google Scholar 

  10. Farzan A, Kincaid Z, Podelski A (2013) Inductive data flow graphs. In: Giacobazzi R, Cousot R (eds) The 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’13, Rome, Italy, 23–25 January 2013. ACM, pp 129–142

  11. Godlin B, Strichman O (2008) Inference rules for proving the equivalence of recursive procedures. Acta Inf 45(6):403–439

    Article  MathSciNet  MATH  Google Scholar 

  12. Inverso O, Nguyen TL, Fischer B, Torre La S, Parlato G (2015) Lazy-cseq: a context-bounded model checking tool for multi-threaded c-programs. In: Cohen MB, Grunske L, Whalen M (eds) 30th IEEE/ACM international conference on automated software engineering, ASE 2015, Lincoln, NE, USA, 9–13 Nov 2015. IEEE Computer Society, pp 807–812

  13. Inverso O, Tomasco E, Fischer B, Torre La S, Parlato G Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere and Bloem [2], pp 585–602

  14. Jackson D, Ladd DA (1994) Semantic diff: a tool for summarizing the effects of modifications. In: Proceedings of the international conference on software maintenance, ICSM 1994, Victoria, BC, Canada, Sept 1994. IEEE Computer Society, pp 243–252

  15. Joshi S, Lahiri SK, Lal A (2012) Underspecified harnesses and interleaved bugs. In: Field J, Hicks M (eds) Proceedings of the 39th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2012, Philadelphia, Pennsylvania, USA, 22–28 January 2012. ACM, pp 19–30

  16. Lahiri SK, Hawblitzel C, Kawaguchi M, Rebêlo H (2012) Symdiff: a language-agnostic semantic diff tool for imperative programs. In: Proceedings of the 24th international conference on computer aided verification, CAV’12

  17. Lahiri SK, McMillan KL, Sharma R, Hawblitzel C (2013) Differential assertion checking. In: Joint meeting of the european software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, 18–26 Aug 2013. ACM, pp 345–355

  18. Logozzo F, Lahiri SK, Fähndrich M, Blackshear S (2014) Verification modulo versions: towards usable verification. In: ACM SIGPLAN conference on programming language design and implementation, PLDI ’14, Edinburgh, United Kingdom, 09–11 June 2014. ACM, p 32

  19. Lu S, Park S, Seo E, Zhou Y (2008) Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: Eggers SJ, Larus JR (eds) Proceedings of the 13th international conference on architectural support for programming languages and operating systems, ASPLOS 2008, Seattle, WA, USA, 1–5 Mar 2008. ACM, pp 329–339

  20. Marinescu PD, Cadar C (2013) KATCH: high-coverage testing of software patches. In: Joint meeting of the european software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, 18–26 Aug 2013. ACM, pp 235–245

  21. Person S, Dwyer MB, Elbaum SG, Pasareanu CS (2008) Differential symbolic execution. In: Proceedings of the 16th ACM SIGSOFT international symposium on foundations of software engineering, 2008, Atlanta, Georgia, USA, 9–14 Nov 2008. ACM, pp 226–237

  22. Rosen BK, Wegman MN, Zadeck FK (1988) Global value numbers and redundant computations. In: Ferrante J, Mager P (eds) Conference record of the fifteenth annual ACM symposium on principles of programming languages, San Diego, California, USA, 10–13 Jan 1988. ACM Press, pp 12–27

  23. Shasha D, Snir M (1988) Efficient and correct execution of parallel programs that share memory. ACM Trans Program Lang Syst 10(2):282–312

    Article  Google Scholar 

Download references

Acknowledgements

This work is supported in part by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (Grant Agreement No. 678177).

Author information

Authors and Affiliations

  1. IRIF, Univ. Paris Diderot, Paris, France

    Ahmed Bouajjani & Constantin Enea

  2. Microsoft Research, Redmond, USA

    Shuvendu K. Lahiri

Authors
  1. Ahmed Bouajjani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Constantin Enea
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shuvendu K. Lahiri
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Constantin Enea.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bouajjani, A., Enea, C. & Lahiri, S.K. Abstract semantic diffing of evolving concurrent programs. Form Methods Syst Des 54, 4–26 (2019). https://doi.org/10.1007/s10703-018-0322-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-018-0322-2

Keywords

Search

Navigation