Skip to main content
SpringerLink
Log in

Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10145))

Abstract

We present a static analysis by abstract interpretation of numeric properties in multi-threaded programs. The analysis is sound (assuming a sequentially consistent memory), parameterized by a choice of abstract domains and, in order to scale up, it is modular, in that it iterates over each thread individually (possibly several times) instead of iterating over their product. We build on previous work that formalized rely-guarantee verification methods as a concrete, fixpoint-based semantics, and then apply classic numeric abstractions to abstract independently thread states and thread interference. This results in a flexible algorithm allowing a wide range of precision versus cost trade-offs, and able to infer even flow-sensitive and relational thread interference. We implemented our method in an analyzer prototype for a simple language and experimented it on several classic mutual exclusion algorithms for two or more threads. Our prototype is instantiated with the polyhedra domain and employs simple control partitioning to distinguish critical sections from surrounding code. It relates the variables of all threads using polyhedra, which limits its scalability in the number of variables. Nevertheless, preliminary experiments and comparison with ConcurInterproc show that modularity enables scaling to a large number of thread instances, provided that the total number of variables stays small.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: POPL 2010, pp. 7–18. ACM, January 2010

    Google Scholar 

  2. Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. In: Infotech\(@\)Aerospace. AIAA, vol. 2010-3385, pp. 1–38. AIAA, April 2010

    Google Scholar 

  3. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI 2003, pp. 196–207. ACM, June 2003

    Google Scholar 

  4. Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: BjØrner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications, FMPA 1993. LNCS, vol. 735, pp. 128–141. Springer, Heidelberg (1993)

    Google Scholar 

  5. Carré, J.L., Hymans, C.: From single-thread to multithreaded: an efficient static analysis algorithm. Technical report. arXiv:0910.5833v1, EADS October 2009

  6. Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. Formal Methods Syst. Des. 34(2), 104–125 (2008)

    Article  MATH  Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252. ACM, January 1977

    Google Scholar 

  8. Cousot, P., Cousot, R.: Invariance proof methods and analysis techniques for parallel programs. In: Automatic Program Construction Techniques, Chap. 12, pp. 243–271. Macmillan, New York (1984)

    Google Scholar 

  9. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, pp. 84–97. ACM (1978)

    Google Scholar 

  10. Donaldson, A., Kaiser, A., Kroening, D., Tautschnig, M., Wahl, T.: Counterexample-guided abstraction refinement for symmetric concurrent programs. Formal Methods Syst. Des. 41(1), 25–44 (2012)

    Article  MATH  Google Scholar 

  11. Dwyer, M.B.: Modular flow analysis for concurrent software. In: ASE 1997, pp. 264–273. IEEE Computer Society (1997)

    Google Scholar 

  12. Farzan, A., Kincaid, Z.: Duet: static analysis for unbounded parallelism. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 191–196. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_12

    Chapter  Google Scholar 

  13. Godefroid, P.: Partial-order methods for the verification of concurrent systems - an approach to the state-explosion problem. Ph.D. thesis, University of Liege, Computer Science Department (1994)

    Google Scholar 

  14. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI 2012, pp. 405–416. ACM (2012)

    Google Scholar 

  15. Grunwald, D., Srinivasan, H.: Data flow equations for explicitly parallel programs. In: PPOPP 1993, pp. 159–168. ACM (1993)

    Google Scholar 

  16. Gupta, A., Popeea, C., Rybalchenko, A.: Threader: a constraint-based verifier for multi-threaded programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 412–417. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_32

    Chapter  Google Scholar 

  17. Jeannet, B.: BddApron. http://pop-art.inrialpes.fr/~bjeannet/bjeannet-forge/bddapron/bddapron.pdf

  18. Jeannet, B.: Relational interprocedural verification of concurrent programs. Softw. Syst. Model. 12(2), 285–306 (2013)

    Article  Google Scholar 

  19. Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_52

    Chapter  Google Scholar 

  20. Jones, C.B.: Development methods for computer programs including a notion of interference. Ph.D. thesis, Oxford University, June 1981

    Google Scholar 

  21. Kusano, M., Wang, C.: Flow-sensitive composition of thread-modular abstract interpretation. In: FSE 2016, pp. 799–809. ACM (2016)

    Google Scholar 

  22. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28, 690–691 (1979). IEEE Computer Society

    Article  MATH  Google Scholar 

  23. Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453–455 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  24. Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification is cartesian abstract interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 183–197. Springer, Heidelberg (2006). doi:10.1007/11921240_13

    Chapter  Google Scholar 

  25. Miné, A.: Static analysis of run-time errors in embedded critical parallel C programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 398–418. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19718-5_21

    Chapter  Google Scholar 

  26. Miné, A.: Static analysis by abstract interpretation of sequential and multi-thread programs. In: Proceedings of the 10th School of Modelling and Verifying Parallel Processes (MOVEP 2012), pp. 35–48, 3–7 December 2012

    Google Scholar 

  27. Miné, A.: Relational thread-modular static value analysis by abstract interpretation. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 39–58. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54013-4_3

    Chapter  Google Scholar 

  28. Miné, A.: Static analysis of run-time errors in embedded real-time parallel C programs. Logical Methods Comput. Sci. (LMCS) 8(26), 63 (2012)

    MathSciNet  MATH  Google Scholar 

  29. Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)

    Article  MATH  Google Scholar 

  30. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31980-1_7

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École Normale Supérieure de Lyon, Lyon, France

    Raphaël Monat

  2. École Normale Supérieure, Paris, France

    Raphaël Monat

  3. Sorbonnes Universités, UPMC Univ. Paris 6, Laboratoire d’informatique de Paris 6 (LIP6), 4, Pl. Jussieu, 75005, Paris, France

    Antoine Miné

Authors
  1. Raphaël Monat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Antoine Miné
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Antoine Miné .

Editor information

Editors and Affiliations

  1. IRIF, Université Paris Diderot, Paris, France

    Ahmed Bouajjani

  2. VERIMAG, CNRS & Université Grenoble Alpes, Grenoble, France

    David Monniaux

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Monat, R., Miné, A. (2017). Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-52234-0_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-52233-3

  • Online ISBN: 978-3-319-52234-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation