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

Parameterized Model Checking on the TSO Weak Memory Model

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

We present an extended version of the model checking modulo theories framework for verifying parameterized systems under the TSO weak memory model. Our extension relies on three main ingredients: (1) an axiomatic theory of the TSO memory model based on relations over (read, write) events, (2) a TSO-specific backward reachability algorithm and (3) an SMT solver for reasoning about TSO formulas. One of the main originality of our work is a partial order reduction technique that exploits specificities of the TSO memory model. We have implemented this framework in a new version of the Cubicle model checker called Cubicle-\(\mathscr {W}\). Our experiments show that Cubicle-\(\mathscr {W}\) is expressive and efficient enough to automatically prove safety of concurrent algorithms, for an arbitrary number of processes, ranging from mutual exclusion to synchronization barriers translated from actual x86-TSO implementations.

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

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. By variable, we mean a distinct memory location.

  2. e = external, i = internal.

References

  1. Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. In: 27th International Conference on Concurrency Theory, CONCUR 2016, August 23–26, 2016, Québec City, Canada, pp. 5:1–5:15 (2016)

  2. Abdulla, P.A., Atig, M.F., Chen, Y., Leonardsson, C., Rezine, A.: Memorax, a precise and sound tool for automatic fence insertion under TSO. In: 19th International Conference Tools and Algorithms for the Construction and Analysis of Systems—TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings, pp. 530–536 (2013)

  3. Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: 13th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24–April 1, 2007, Proceedings, pp. 721–736 (2007)

  4. Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: 19th International Conference on Computer Aided Verification, CAV 2007, Berlin, Germany, July 3–7, 2007, Proceedings, pp. 145–157 (2007)

  5. Alglave, J.: A Shared Memory Poetics. Ph.D. thesis, University of Paris 7 - Denis Diderot, Paris, France (2010)

  6. Alglave, J., Fox, A.C.J., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and ARM multiprocessor machine code. In: Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, DAMP 2009, Savannah, GA, USA, January 20, 2009, pp. 13–24 (2009)

  7. Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Programming Languages and Systems—22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, pp. 512–532 (2013)

  8. Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: 25th International Conference on Computer Aided Verification—CAV 2013, Saint Petersburg, Russia, July 13–19, 2013. Proceedings, pp. 141–157 (2013)

  9. Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1–7:74 (2014)

    Article  Google Scholar 

  10. Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)

    Article  MathSciNet  Google Scholar 

  11. Bouajjani, A., Calin, G., Derevenetc, E., Meyer, R.: Lazy TSO reachability. In: Fundamental Approaches to Software Engineering—18th International Conference, FASE 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings, pp. 267–282 (2015)

  12. Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Programming Languages and Systems—22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings, pp. 533–553 (2013)

  13. Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing, Calgary, Alberta, Canada, August 11–13, 1986, pp. 240–248 (1986)

  14. Conchon, S., Declerck, D., Zaïdi, F.: Cubicle-\(\cal{W}\): parameterized model checking on weak memory. In: 9th International Joint Conference System Descriptions—IJCAR 2018, Oxford, United Kingdom, July 14–17, 2018, Proceedings (2018)

  15. Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Invariants for finite instances and beyond. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20–23, 2013, pp. 61–68 (2013)

  16. Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems—tool paper. In: 24th International Conference on Computer Aided Verification, CAV 2012, Berkeley, CA, USA, July 7–13, 2012 Proceedings, pp. 718–724 (2012)

  17. Conchon, S., Mebsout, A., Zaïdi, F.: Certificates for parameterized model checking. In: FM 2015: Formal Methods in 20th International Symposium, Oslo, Norway, June 24–26, 2015, Proceedings, pp. 126–142 (2015)

  18. Cubicle-\(\cal W\it \). http://cubicle.lri.fr/cubiclew/

  19. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675–735 (1992)

    Article  MathSciNet  Google Scholar 

  20. Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. LMCS 6(4) (2010)

  21. Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: 5th International Joint Conference Automated Reasoning, IJCAR 2010, Edinburgh, UK, July 16–19, 2010. Proceedings, pp. 22–29 (2010)

  22. Goeman, H.J.M.: The arbiter: an active system component for implementing synchronizing primitives. Fundam. Inform. 4, 517–530 (1981)

    MathSciNet  MATH  Google Scholar 

  23. Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, Burlington (2008)

    Google Scholar 

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

    Article  Google Scholar 

  25. Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: 22nd International Conference Theorem Proving in Higher Order Logics, TPHOLs 2009, Munich, Germany, August 17–20, 2009. Proceedings, pp. 391–407 (2009)

  26. Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LRI (CNRS & Univ. Paris-Sud), Université Paris-Saclay, 91405, Orsay, France

    Sylvain Conchon & Fatiha Zaïdi

  2. Inria, Université Paris-Saclay, 91120, Palaiseau, France

    Sylvain Conchon

  3. OCamlPro, 91190, Gif-sur-Yvette, France

    David Declerck

Authors
  1. Sylvain Conchon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Declerck
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Fatiha Zaïdi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David Declerck.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Work supported by the French ANR Project PARDI (ANR-16-CE25-0006).

Appendix: Axiomatic Memory Model (with ppo Instantiated for TSO)

Appendix: Axiomatic Memory Model (with ppo Instantiated for TSO)

figure aa

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Conchon, S., Declerck, D. & Zaïdi, F. Parameterized Model Checking on the TSO Weak Memory Model. J Autom Reasoning 64, 1307–1330 (2020). https://doi.org/10.1007/s10817-020-09565-w

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-020-09565-w

Keywords

Search

Navigation