Advertisement

Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)

  • Parosh Aziz AbdullaEmail author
  • Mohamed Faouzi Atig
  • Bengt Jonsson
  • Tuan Phong Ngo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11704)

Abstract

We describe at a high-level the main concepts in the Release-Acquire (RA) semantics that is part of the C11 language. Furthermore, we describe the ideas behind an optimal dynamic partial order reduction technique that can be used for systematic analysis of concurrent programs running under RA.

This tutorial is based on the material presented in [5], which also contains the formal definitions of all the models, concepts, and algorithms .

References

  1. 1.
    Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353–367. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_28CrossRefzbMATHGoogle Scholar
  2. 2.
    Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Symposium on Principles of Programming Languages, (POPL), pp. 373–384. ACM, San Diego (2014)Google Scholar
  3. 3.
    Abdulla, P.A., Aronis, S., Jonsson, B., Sagonas, K.: Source sets: a foundation for optimal dynamic partial order reduction. J. ACM 64(4), 25:1–25:49 (2017).  https://doi.org/10.1145/3073408MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 134–156. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_8CrossRefGoogle Scholar
  5. 5.
    Abdulla, P.A., Atig, M.F., Jonsson, B., Ngo, T.P.: Optimal stateless model checking under the release-acquire semantics. PACMPL 2(OOPSLA), 135:1–135:29 (2018).  https://doi.org/10.1145/3276505CrossRefGoogle Scholar
  6. 6.
    Abdulla, P.A., Bertrand, N., Rabinovich, A.M., Schnoebelen, P.: Verification of probabilistic systems with faulty communication. Inf. Comput. 202(2), 141–165 (2005).  https://doi.org/10.1016/j.ic.2005.05.008MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Abdulla, P.A., Bouajjani, A., Cederberg, J., Haziza, F., Rezine, A.: Monotonic abstraction for programs with dynamic memory heaps. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 341–354. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70545-1_33CrossRefGoogle Scholar
  8. 8.
    Abdulla, P.A., Bouajjani, A., d’Orso, J.: Deciding monotonic games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 1–14. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45220-1_1CrossRefGoogle Scholar
  9. 9.
    Abdulla, P.A., Deneux, J., Mahata, P.: Multi-clock timed networks. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14–17 July 2004, Turku, Finland, Proceedings, pp. 345–354. IEEE Computer Society (2004). https://doi.org/10.1109/LICS.2004.1319629
  10. 10.
    Abdulla, P.A., Haziza, F., Holík, L., Jonsson, B., Rezine, A.: An integrated specification and verification technique for highly concurrent data structures. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 324–338. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_23CrossRefzbMATHGoogle Scholar
  11. 11.
    Abdulla, P.A., Jonsson, B., Kindahl, M., Peled, D.: A general approach to partial order reductions in symbolic verification. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 379–390. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0028760CrossRefGoogle Scholar
  12. 12.
    Abdulla, P.A., Kindahl, M., Peled, D.A.: An improved search strategy for lossy channel systems. In: Togashi, A., Mizuno, T., Shiratori, N., Higashino, T. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE X / PSTV XVII’97, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE X) and Protocol Specification, Testing and Verification (PSTV XVII), 18–21 November 1997, Osaka, Japan, IFIP Conference Proceedings, vol. 107, pp. 251–264. Chapman & Hall (1997)Google Scholar
  13. 13.
    Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., Vaidya, K.: Data-centric dynamic partial order reduction. Proc. ACM Program. Lang. 2(POPL), 31:1–31:30 (2017).  https://doi.org/10.1145/3158119CrossRefGoogle Scholar
  14. 14.
    Christakis, M., Gotovos, A., Sagonas, K.: Systematic testing for detecting concurrency errors in Erlang programs. In: International Conference on Software Testing. Verification and Validation, (ICST), pp. 154–163. IEEE, Luxembourg (2013)Google Scholar
  15. 15.
    Clarke, E.M., Grumberg, O., Minea, M., Peled, D.A.: State space reduction using partial order techniques. STTT 2(3), 279–287 (1999)CrossRefGoogle Scholar
  16. 16.
    Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8CrossRefzbMATHGoogle Scholar
  17. 17.
    Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. The MIT Press, Cambridge (2009)zbMATHGoogle Scholar
  18. 18.
    Demsky, B., Lam, P.: Satcheck: Sat-directed stateless model checking for SC and TSO. In: Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA), pp. 20–36. ACM, Pittsburgh (2015)Google Scholar
  19. 19.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Principles of Programming Languages, POPL, pp. 110–121. ACM, Long Beach (2005)Google Scholar
  20. 20.
    Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Ph.D. thesis, University of Liége (1996). Also, volume 1032 of LNCS, SpringerGoogle Scholar
  21. 21.
    Godefroid, P.: Model checking for programming languages using VeriSoft. In: Principles of Programming Languages, POPL, pp. 174–186. ACM Press, Paris (1997)Google Scholar
  22. 22.
    Godefroid, P., Hammer, B., Jagadeesan, L.: Model checking without a model: an analysis of the heart-beat monitor of a telephone switch using VeriSoft. In: Proceedings of ACM SIGSOFT International Symposium on Software Testing and Analysis. pp. 124–133 (1998)Google Scholar
  23. 23.
    Godefroid, P.: Software model checking: the VeriSoft approach. Formal Methods Syst. Des. 26(2), 77–101 (2005)CrossRefGoogle Scholar
  24. 24.
    Huang, J.: Stateless model checking concurrent programs with maximal causality reduction. In: Programming Language Design and Implementation, PLDI, pp. 165–174. ACM, Portland (2015)Google Scholar
  25. 25.
    Huang, S., Huang, J.: Maximal causality reduction for TSO and PSO. In: Object-Oriented Programming, Systems, Languages, and Applications, (OOPSLA), pp. 447–461. ACM, Amsterdam (2016)Google Scholar
  26. 26.
    Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C/C++ concurrency. In: POPL (2018, to appear). http://plv.mpi-sws.org/rcmc/
  27. 27.
    Kokologiannakis, M., Sagonas, K.: Stateless model checking of the linux kernel’s hierarchical read-copy-update (tree RCU). In: Symposium on Model Checking of Software, SPIN, pp. 172–181. ACM, Santa Barbara (2017)Google Scholar
  28. 28.
    Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20–22 January 2016, pp. 649–662. ACM (2016)Google Scholar
  29. 29.
    Mazurkiewicz, A.: Trace theory. In: Advances in Petri Nets (1986)Google Scholar
  30. 30.
    Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: OSDI, pp. 267–280. USENIX Association (2008)Google Scholar
  31. 31.
    Norris, B., Demsky, B.: A practical approach for model checking C/C++11 code. ACM Trans. Program. Lang. Syst. 38(3), 10:1–10:51 (2016)CrossRefGoogle Scholar
  32. 32.
    Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-56922-7_34CrossRefGoogle Scholar
  33. 33.
    Rodríguez, C., Sousa, M., Sharma, S., Kroening, D.: Unfolding-based partial order reduction. In: CONCUR 2015, pp. 456–469 (2015)Google Scholar
  34. 34.
    Saarikivi, O., Kähkönen, K., Heljanko, K.: Improving dynamic partial order reductions for concolic testing. In: Application of Concurrency to System Design, ACSD, pp. 132–141. IEEE, Hamburg (2012)Google Scholar
  35. 35.
    Sen, K., Agha, G.: A race-detection and flipping algorithm for automated testing of multi-threaded programs. In: Haifa Verification Conference. pp. 166–182 (2007), lNCS 4383Google Scholar
  36. 36.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991).  https://doi.org/10.1007/3-540-53863-1_36CrossRefGoogle Scholar
  37. 37.
    Zhang, N., Kusano, M., Wang, C.: Dynamic partial order reduction for relaxed memory models. In: Programming Language Design and Implementation (PLDI), pp. 250–259. ACM, Portland (2015)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Parosh Aziz Abdulla
    • 1
    Email author
  • Mohamed Faouzi Atig
    • 1
  • Bengt Jonsson
    • 1
  • Tuan Phong Ngo
    • 1
  1. 1.Uppsala UniversityUppsalaSweden

Personalised recommendations