Skip to main content
SpringerLink
Log in

Automatic Verification of RMA Programs via Abstraction Extrapolation

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

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

  • 939 Accesses

Abstract

Remote Memory Access (RMA) networks are emerging as a promising basis for building performant large-scale systems such as MapReduce, scientific computing applications, and others. To achieve this performance, RMA networks exhibit relaxed memory consistency. This means the developer now must manually ensure that the additional relaxed behaviors are not harmful to their application – a task known to be difficult and error-prone. In this paper, we present a method and a system that can automatically address this task. Our approach consists of two ingredients: (i) a reduction where we reduce the task of verifying program P running on RMA to the problem of verifying a program \(\overline{P}\) on sequential consistency (where \(\overline{P}\) captures the required RMA behaviors), and (ii) abstraction extrapolation: a new method to automatically discover both, predicates (via predicate extrapolation) and abstract transformers (via boolean program extrapolation) for \(\overline{P}\). This enables us to automatically extrapolate the proof of P under sequential consistency (SC) to a proof of P under RMA. We implemented our method and showed it to be effective in automatically verifying, for the first time, several challenging concurrent algorithms under RMA.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. In: Desharnais, J., Jagadeesan, R. (eds.) 27th International Conference on Concurrency Theory, CONCUR 2016, Québec City, Canada, August 23–26, 2016. LIPIcs, vol. 59, pp. 5:1–5:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

  2. Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Automatic fence insertion in integer programs via predicate abstraction. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 164–180. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33125-1_13

    Chapter  Google Scholar 

  3. Alglave, J., Cousot, P.: Ogre and pythia: an invariance proof method for weak consistency models. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017, pp. 3–18. ACM (2017)

    Google Scholar 

  4. Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don’t sit on the fence: a static analysis approach to automatic fence insertion. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 508–524. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_33

    Google Scholar 

  5. 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). https://doi.org/10.1007/978-3-642-37036-6_28

    Chapter  Google Scholar 

  6. Allen, F., Almasi, G., Andreoni, W., Beece, D., Berne, B.J., Bright, A., Brunheroto, J., Cascaval, C., Castanos, J., Coteus, P., Crumley, P., Curioni, A., Denneau, M., Donath, W., Eleftheriou, M., Fitch, B., Fleischer, B., Georgiou, C.J., Germain, R., Giampapa, M., Gresh, D., Gupta, M., Haring, R., Ho, H., Hochschild, P., Hummel, S., Jonas, T., Lieber, D., Martyna, G., Maturu, K., Moreira, J., Newns, D., Newton, M., Philhower, R., Picunko, T., Pitera, J., Pitman, M., Rand, R., Royyuru, A., Salapura, V., Sanomiya, A., Shah, R., Sham, Y., Singh, S., Snir, M., Suits, F., Swetz, R., Swope, W.C., Vishnumurthy, N., Ward, T.J.C., Warren, H., Zhou, R.: Blue Gene: A vision for protein science using a petaflop supercomputer. IBM Syst. J. 40(2), 310–327 (2001)

    Article  Google Scholar 

  7. Alverson, R., Roweth, D., Kaplan, L.: The Gemini system interconnect. In: Proc. of the IEEE Symposium on High Performance Interconnects (HOTI 2010), pp. 83–87. IEEE Computer Society (2010)

    Google Scholar 

  8. Andrews, G.R.: Concurrent programming - principles and practice. Benjamin/Cummings (1991)

    Google Scholar 

  9. Arimilli, B., Arimilli, R., Chung, V., Clark, S., Denzel, W., Drerup, B., Hoefler, T., Joyner, J., Lewis, J., Li, J., Ni, N., Rajamony, R.: The PERCS high-performance interconnect. In: Proc. of the IEEE Symposium on High Performance Interconnects (HOTI 2010), pp. 75–82. IEEE Computer Society, August 2010

    Google Scholar 

  10. Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99–115. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_9

    Chapter  Google Scholar 

  11. Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Burke, M., Soffa, M.L. (eds.) Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20–22, 2001, pp. 203–213. ACM (2001)

    Google Scholar 

  12. Barrett, B.W., Brightwell, R.B., Pedretti, K.T.T., Wheeler, K.B., Hemmert, K.S., Riesen, R.E., Underwood, K.D., Maccabe, A.B., Hudson, T.B. :The Portals 4.0 network programming interface. Tech. rep., Sandia National Laboratories, SAND2012-10087 (2012)

    Google Scholar 

  13. Beck, M., Kagan, M.: Performance evaluation of the RDMA over Ethernet (RoCE) standard in enterprise data centers infrastructure. In: Proc. of the Workshop on Data Center - Converged and Virtual Ethernet Switching (DC-CaVES 2011), pp. 9–15. ITCP (2011)

    Google Scholar 

  14. Jeannet, B.: The ConcurInterproc Analyzer, September 2017. http://pop-art.inrialpes.fr/interproc/concurinterprocweb.cgi

  15. 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). https://doi.org/10.1007/978-3-642-37036-6_29

    Chapter  Google Scholar 

  16. 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). https://doi.org/10.1007/978-3-540-70545-1_12

    Chapter  Google Scholar 

  17. Calin, G., Derevenetc, E., Majumdar, R., Meyer, R.: A theory of partitioned global address spaces. In: Seth, A., Vishnoi, N.K. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2013, Guwahati, India, December 12–14, 2013. LIPIcs, vol. 24, pp. 127–139. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)

    Google Scholar 

  18. Cray Inc., Using the GNI and DMAPP APIs. Ver. S-2446-52, March 2014. http://docs.cray.com/

  19. Dan, A.M., Lam, P., Hoefler, T., Vechev, M.T.: Modeling and analysis of remote memory access programming. In: Visser, E., Smaragdakis, Y. (eds.) Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 – November 4, 2016, pp. 129–144. ACM (2016)

    Google Scholar 

  20. Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 84–104. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_7

    Chapter  Google Scholar 

  21. 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). https://doi.org/10.1007/978-3-662-46081-8_25

    Google Scholar 

  22. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  23. Dijkstra, E.: Cooperating sequential processes, TR EWD-123. Tech. rep., Technological University, Eindhoven (1965)

    Google Scholar 

  24. Donaldson, A.F., Kaiser, A., Kroening, D., Wahl, T.: Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: Gopalakrishnan and Qadeer [27], pp. 356–371

    Google Scholar 

  25. Faanes, G., Bataineh, A., Roweth, D., Court, T., Froese, E., Alverson, B., Johnson, T., Kopnick, J., Higgins, M., Reinhard, J.: Cray cascade: a scalable HPC system based on a dragonfly network. In: Proc. of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC 2012), pp. 103:1–103:9. IEEE Computer Society (2012)

    Google Scholar 

  26. Gerstenberger, R., Besta, M., Hoefler, T.: Enabling highly-scalable remote memory access programming with MPI-3 one sided. In: Proc. of the ACM/IEEE Supercomputing, SC 2013, pp. 53:1–53:12 (2013)

    Google Scholar 

  27. Gopalakrishnan, G., Qadeer, S. (eds.): CAV 2011. LNCS, vol. 6806, pp. 457–462. Springer, Heidelberg (2011)

    Book  Google Scholar 

  28. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10

    Chapter  Google Scholar 

  29. Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26–28, 2011 (2011), pp. 331–344. ACM

    Google Scholar 

  30. Gupta, A., Popeea, C., Rybalchenko, A.: Threader: a constraint-based verifier for multi-threaded programs. In: Gopalakrishnan and Qadeer [27], pp. 412–417

    Google Scholar 

  31. Hoefler, T., Dinan, J., Thakur, R., Barrett, B., Balaji, P., Gropp, W., Underwood, K.: Remote Memory Access Programming in MPI-3. ACM Transactions on Parallel Computing (TOPC), January 2015

    Google Scholar 

  32. Islam, N.S., Rahman, M.W., Jose, J., Rajachandrasekar, R., Wang, H., Subramoni, H., Murthy, C., Panda, D.K.: High performance RDMA-based design of HDFS over InfiniBand. In: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis (Los Alamitos, CA, USA, 2012), SC 2012, pp. 35:1–35:35. IEEE Computer Society Press (2012)

    Google Scholar 

  33. Kuperstein, M., Vechev, M.T., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4–8, 2011, pp. 187–198. ACM (2011)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  35. Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 212–226. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16164-3_16

    Chapter  Google Scholar 

  36. Meshman, Y., Dan, A., Vechev, M., Yahav, E.: Synthesis of memory fences via refinement propagation. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 237–252. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10936-7_15

    Google Scholar 

  37. OpenFabrics Alliance (OFA). OpenFabrics Enterprise Distribution (OFED) (2014). www.openfabrics.org

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

    Article  MATH  Google Scholar 

  39. de León, H.P., Furbach, F., Heljanko, K., Meyer, R.: Portability analysis for axiomatic memory models. PORTHOS: one tool for all models. CoRR abs/1702.06704 (2017)

    Google Scholar 

  40. Recio, R., Metzler, B., Culley, P., Hilland, J., Garcia, D.: A Remote Direct Memory Access Protocol Specification. RFC 5040, RFC Editor, October 2007

    Google Scholar 

  41. Schmid, P., Besta, M., Hoefler, T.: High-performance distributed RMA locks. In: Proceedings of the 25th Symposium on High-Performance Parallel and Distributed Computing (HPDC 2016), June 2016

    Google Scholar 

  42. Szymanski, B.K.: A simple solution to lamport’s concurrent programming problem with linear wait. In: International Conference on Supercomputing, pp. 621–626 (1988)

    Google Scholar 

  43. The InfiniBand Trade Association. Infiniband Architecture Spec, vol. 1, Rel. 1.2. InfiniBand Trade Association (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, ETH Zurich, Zürich, Switzerland

    Cedric Baumann, Andrei Marian Dan, Torsten Hoefler & Martin Vechev

  2. IMDEA Software Institute, Madrid, Spain

    Yuri Meshman

Authors
  1. Cedric Baumann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrei Marian Dan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yuri Meshman
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Torsten Hoefler
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Martin Vechev
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrei Marian Dan .

Editor information

Editors and Affiliations

  1. University of Texas , Austin, Texas, USA

    Isil Dillig

  2. University of California , Los Angeles, California, USA

    Jens Palsberg

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Baumann, C., Dan, A.M., Meshman, Y., Hoefler, T., Vechev, M. (2018). Automatic Verification of RMA Programs via Abstraction Extrapolation. In: Dillig, I., Palsberg, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2018. Lecture Notes in Computer Science(), vol 10747. Springer, Cham. https://doi.org/10.1007/978-3-319-73721-8_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-73721-8_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-73720-1

  • Online ISBN: 978-3-319-73721-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation