[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Per-Location Simulation

  • Conference paper
  • First Online:
NASA Formal Methods (NFM 2020)

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

Included in the following conference series:

  • 779 Accesses

Abstract

Simulation/bisimulation is one of the most widely used frameworks for proving program equivalence/semantic preservation. In this paper, we propose a new per-location simulation (PLS) relation that is simple and suitable for proving that a compiled program semantically preserves its original program under a CFG-based language with a real-world, C/C++ like, weak memory model. To the best of our knowledge, PLS is the first simulation framework weaker than the CompCert [26]/CompCertTSO [47] one that is used for proving compiler correctness. With a combination of PLS, the compiler proof-framework Morpheus [34], and a language semantics with a weak memory model, we are able to prove that programs are semantically preserved through a transformation. All the definitions and proofs have been implemented in Isabelle/HOL.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.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

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 51.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 64.99
Price includes VAT (United Kingdom)
  • 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

Similar content being viewed by others

References

  1. 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). https://doi.org/10.1145/2627752, http://doi.acm.org/10.1145/2627752

  2. Ballarin, C.: Tutorial to locales and locale interpretation. In: Contribuciones cientíÂficas en honor de Mirian Andrés Gómez, 1 Januray 2010, pp. 123–140 (2010). ISBN 978-84-96487-50-5

    Google Scholar 

  3. Batty, M., Donaldson, A.F., Wickerson, J.: Overhauling SC atomics in C11 and OpenCL. SIGPLAN Not. 51(1), 634–648 (2016)

    Article  Google Scholar 

  4. Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 283–307. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46669-8_12

    Chapter  Google Scholar 

  5. Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. SIGPLAN Not. 46(1), 55–66 (2011). https://doi.org/10.1145/1925844.1926394, http://doi.acm.org/10.1145/1925844.1926394

  6. van Benthem, J.: Exploring Logical Dynamics. Center for the Study of Language and Information, Stanford, CA, USA (1997)

    Google Scholar 

  7. Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263–288 (2009). https://doi.org/10.1007/s10817-009-9148-3

    Article  MathSciNet  MATH  Google Scholar 

  8. Boehm, H.J.: Memory Model Rationales. http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2007/n2176.html. Accessed 9 Mar 2007

  9. Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. SIGPLAN Not. 43(6), 68–78 (2008)

    Article  Google Scholar 

  10. Boehm, H.J., Demsky, B.: Outlawing ghosts: avoiding out-of-thin-air results. In: Proceedings of the Workshop on Memory Systems Performance and Correctness, MSPC 2014, pp. 7:1–7:6. ACM, New York, NY, USA (2014)

    Google Scholar 

  11. Burkart, O., Caucal, D., Steffen, B.: Bisimulation collapse and the process taxonomy. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 247–262. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61604-7_59

    Chapter  Google Scholar 

  12. Caucal, D.: On the regular structure of prefix rewriting. In: Arnold, A. (ed.) CAAP 1990. LNCS, vol. 431, pp. 87–102. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52590-4_42

    Chapter  Google Scholar 

  13. Caucal, D.: On infinite transition graphs having a decidable monadic theory. In: Meyer, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 194–205. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61440-0_128

    Chapter  Google Scholar 

  14. Chakraborty, S., Vafeiadis, V.: Formalizing the concurrency semantics of an LLVM fragment. In: Proceedings of the 2017 International Symposium on Code Generation and Optimization, CGO 2017, pp. 100–110. IEEE Press, Piscataway, NJ, USA (2017). http://dl.acm.org/citation.cfm?id=3049832.3049844

  15. Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. SIGPLAN Not. 42(6), 54–65 (2007)

    Article  Google Scholar 

  16. Chlipala, A.: A verified compiler for an impure functional language. SIGPLAN Not. 45(1), 93–106 (2010)

    Article  Google Scholar 

  17. Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28(6), 2–2 (2003)

    Article  Google Scholar 

  18. Dodds, M., Batty, M., Gotsman, A.: C/C++ causal cycles confound compositionality. TinyToCS 2 (2013). http://tinytocs.org/vol2/papers/tinytocs2-dodds.pdf

  19. Jeffrey, A., Riely, J.: On thin air reads towards an event structures model of relaxed memory. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pp. 759–767. ACM, New York (2016). https://doi.org/10.1145/2933575.2934536, http://doi.acm.org/10.1145/2933575.2934536

  20. Kalvala, S., Warburton, R., Lacey, D.: Program transformations using temporal logic side conditions. ACM Trans. Program. Lang. Syst. 31, 1–48 (2009). https://doi.org/10.1145/1516507.1516509

    Article  Google Scholar 

  21. Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. SIGPLAN Not. 52(1), 175–189 (2017). https://doi.org/10.1145/3093333.3009850, http://doi.acm.org/10.1145/3093333.3009850

  22. Lahav, O., Giannarakis, N., Vafeiadis, V.: Taming release-acquire consistency. SIGPLAN Not. 51(1), 649–662 (2016). https://doi.org/10.1145/2914770.2837643, http://doi.acm.org/10.1145/2914770.2837643

  23. Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for weak memory models. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 311–323. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47666-6_25

    Chapter  Google Scholar 

  24. Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in C/C++ 11. SIGPLAN Not. 52(6), 618–632 (2017). https://doi.org/10.1145/3140587.3062352, http://doi.acm.org/10.1145/3140587.3062352

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

    Article  Google Scholar 

  26. Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363–446 (2009). https://doi.org/10.1007/s10817-009-9155-4

    Article  MathSciNet  MATH  Google Scholar 

  27. Li, L., Gunter, E.: The axiomatic timed relaxed memory model (2019).https://github.com/liyili2/timed-relaxed-memory-model

  28. Li, L., Gunter, E.L.: Per-location simulation – appendix. Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign (2020). https://github.com/liyili2/timed-relaxed-memory-model/PLS

  29. Liang, H., Feng, X., Shao, Z.: Compositional verification of termination-preserving refinement of concurrent programs. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, pp. 65:1–65:10. ACM, New York (2014). https://doi.org/10.1145/2603088.2603123, http://doi.acm.org/10.1145/2603088.2603123

  30. Liu, X., Yu, T., Zhang, W.: Analyzing divergence in bisimulation semantics. SIGPLAN Not. 52(1), 735–747 (2017). https://doi.org/10.1145/3093333.3009870, http://doi.acm.org/10.1145/3093333.3009870

  31. Lochbihler, A.: Mechanising a type-safe model of multithreaded java with a verified compiler. J. Autom. Reason. 61(1), 243–332 (2018)

    Article  MathSciNet  Google Scholar 

  32. Mansky, W., Garbuzov, D., Zdancewic, S.: An axiomatic specification for sequential memory models. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 413–428. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21668-3_24

    Chapter  Google Scholar 

  33. Mansky, W., Gunter, E.: A framework for formal verification of compiler optimizations. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 371–386. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_26

    Chapter  Google Scholar 

  34. Mansky, W., Gunter, E.L., Griffith, D., Adams, M.D.: Specifying and executing optimizations for generalized control flow graphs. Sci. Comput. Program. 130, 2–23 (2016). https://doi.org/10.1016/j.scico.2016.06.003

    Article  Google Scholar 

  35. Manson, J., Pugh, W., Adve, S.V.: The java memory model. SIGPLAN Not. 40(1), 378–391 (2005). https://doi.org/10.1145/1047659.1040336

    Article  MATH  Google Scholar 

  36. Mccarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions, pp. 33–41. American Mathematical Society (1967)

    Google Scholar 

  37. Meshman, Y., Rinetzky, N., Yahav, E.: Pattern-based synthesis of synchronization for the C++ memory model. In: Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design. FMCAD 2015, pp. 120–127. FMCAD Inc., Austin, TX (2015)

    Google Scholar 

  38. Norris, B., Demsky, B.: Cdschecker: checking concurrent data structures written with C/C++ atomics. SIGPLAN Not. 48(10), 131–150 (2013)

    Article  Google Scholar 

  39. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). https://doi.org/10.1007/BFb0017309

    Chapter  Google Scholar 

  40. Pichon-Pharabod, J., Sewell, P.: A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. SIGPLAN Not. 51(1), 622–633 (2016)

    Article  Google Scholar 

  41. Podkopaev, A., Lahav, O., Vafeiadis, V.: Bridging the gap between programming languages and hardware weak memory models. Proc. ACM Program. Lang. 3(POPL), 69:1–69:31 (2019). https://doi.org/10.1145/3290382, http://doi.acm.org/10.1145/3290382

  42. Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Nardelli, F.Z.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15–17 January 2015, pp. 209–220. ACM (2015). https://doi.org/10.1145/2676726.2676995

  43. Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Zappa Nardelli, F.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. SIGPLAN Not. 50(1), 209–220 (2015). https://doi.org/10.1145/2775051.2676995, http://doi.acm.org/10.1145/2775051.2676995

  44. Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Zappa Nardelli, F.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. SIGPLAN Not. 50(1), 209–220 (2015)

    Article  Google Scholar 

  45. Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. SIGPLAN Not. 48(10), 867–884 (2013). https://doi.org/10.1145/2544173.2509532, http://doi.acm.org/10.1145/2544173.2509532

  46. Van Benthem, J.: Correspondence Theory, pp. 197–247. Springer, Netherlands (1984). https://doi.org/10.1007/978-94-009-6259-0_4

    Book  MATH  Google Scholar 

  47. Ševčík, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM 60(3), 22:1–22:50 (2013). https://doi.org/10.1145/2487241.2487248, http://doi.acm.org/10.1145/2487241.2487248

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois at Urbana-Champaign, Champaign, USA

    Liyi Li & Elsa L. Gunter

Authors
  1. Liyi Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Elsa L. Gunter
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Liyi Li or Elsa L. Gunter .

Editor information

Editors and Affiliations

  1. NASA Ames Research Center, Moffett Field, CA, USA

    Ritchie Lee

  2. SRI International, Menlo Park, CA, USA

    Susmit Jha

  3. KBR Inc., NASA Ames Research Center, Moffett Field, CA, USA

    Anastasia Mavridou

  4. NASA Ames Research Center, Moffett Field, CA, USA

    Dimitra Giannakopoulou

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Li, L., Gunter, E.L. (2020). Per-Location Simulation. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds) NASA Formal Methods. NFM 2020. Lecture Notes in Computer Science(), vol 12229. Springer, Cham. https://doi.org/10.1007/978-3-030-55754-6_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-55754-6_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-55753-9

  • Online ISBN: 978-3-030-55754-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation