Skip to main content
SpringerLink
Log in

Compiling Parameterized X86-TSO Concurrent Programs to Cubicle-\(\mathcal {W}\)

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10610))

Included in the following conference series:

Abstract

We present PMCx86, a compiler from x86 concurrent programs to Cubicle-\(\mathcal {W}\), a model checker for parameterized weak memory array-based transition systems. Our tool handles x86 concurrent programs designed to be executed for an arbitrary number of threads and under the TSO weak memory model. The correctness of our approach relies on a simulation result to show that the translation preserves x86-TSO semantics. To show the effectiveness of our translation scheme, we prove the safety of parameterized critical primitives found in operating systems like mutexes and synchronization barriers. To our knowledge, this is the first approach to prove safety of such parameterized x86-TSO programs.

The paper is supported by the French ANR project PARDI (DS0703).

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. Cubicle-W. https://www.lri.fr/~declerck/cubiclew/

  2. PMCX86. https://www.lri.fr/~declerck/pmcx86/

  3. Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 204–219. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_15

    Chapter  Google Scholar 

  4. Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Memorax, a precise and sound tool for automatic fence insertion under TSO. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 530–536. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_37

    Chapter  Google Scholar 

  5. Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721–736. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_56

    Chapter  Google Scholar 

  6. Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 145–157. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_17

    Chapter  Google Scholar 

  7. Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 512–532. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37036-6_28

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

  10. Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533–553. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37036-6_29

    Chapter  Google Scholar 

  11. Bouajjani, A., Meyer, R., Möhlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 428–440. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22012-8_34

    Chapter  Google Scholar 

  12. Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107–120. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70545-1_12

    Chapter  Google Scholar 

  13. Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 11–25. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_3

    Chapter  Google Scholar 

  14. Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: PODC 1986, NY, USA. ACM, New York (1986)

    Google Scholar 

  15. Conchon, S., Declerck, D., Zaïdi, F.: Compiling parameterized X86-TSO concurrent programs to cubicle-W. https://www.lri.fr/~declerck/pmcx86.pdf

  16. Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_55

    Chapter  Google Scholar 

  17. Dan, A., Meshman, Y., Vechev, M., Yahav, E.: Effective abstractions for verification under relaxed memory models. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 449–466. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46081-8_25

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  19. Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 22–29. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14203-1_3

    Chapter  Google Scholar 

  20. Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco (2008)

    Google Scholar 

  21. Intel Corporation: Intel 64 and IA-32 Architectures SDM, December 2016

    Google Scholar 

  22. Kuperstein, M., Vechev, M.T., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: PLDI, pp. 187–198 (2011)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  24. Linden, A., Wolper, P.: A verification-based approach to memory fence insertion in PSO memory systems. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 339–353. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_24

    Chapter  Google Scholar 

  25. 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, David Declerck & Fatiha Zaïdi

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

    Sylvain Conchon & 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 .

Editor information

Editors and Affiliations

  1. Xidian University, Xi’an, China

    Zhenhua Duan

  2. University of Oxford, Oxford, United Kingdom

    Luke Ong

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Conchon, S., Declerck, D., Zaïdi, F. (2017). Compiling Parameterized X86-TSO Concurrent Programs to Cubicle-\(\mathcal {W}\) . In: Duan, Z., Ong, L. (eds) Formal Methods and Software Engineering. ICFEM 2017. Lecture Notes in Computer Science(), vol 10610. Springer, Cham. https://doi.org/10.1007/978-3-319-68690-5_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68690-5_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68689-9

  • Online ISBN: 978-3-319-68690-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation