Skip to main content
SpringerLink
Log in

A Wide-Spectrum Language for Verification of Programs on Weak Memory Models

  • Conference paper
  • First Online:
Formal Methods (FM 2018)

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

Included in the following conference series:

Abstract

Modern processors deploy a variety of weak memory models, which for efficiency reasons may (appear to) execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be complex and subtle, and can impact on ensuring correctness. Previous work on the semantics of weak memory models has focussed on the behaviour of assembler-level programs. In this paper we utilise that work to extract some general principles underlying instruction reordering, and apply those principles to a wide-spectrum language encompassing abstract data types as well as low-level assembler code. The goal is to support reasoning about implementations of data structures for modern processors with respect to an abstract specification.

Specifically, we encode a weak memory model in a pair-wise reordering relation on instructions. Some architectures require an additional definition of the behaviour of the global storage system if it does not provide multi-copy atomicity. In this paper we use the reordering relation in an operational semantics. We derive some properties of program refinement under weak memory models, and encode the semantics in the rewriting engine Maude as a model-checking tool. The tool is used to validate the semantics against the behaviour of a set of litmus tests (small assembler programs) run on hardware, and also to model check implementations of data structures from the literature against their abstract specifications.

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 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.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

Notes

  1. 1.

    We adopt the term “forwarding” from ARM and POWER [3]. The equivalent effect is referred to as bypassing on TSO [8].

  2. 2.

    Different architectures may have different storage subsystems, however, and these need to be separately defined (see Sect. 3.2).

  3. 3.

    To focus on instruction reorderings we leave local variable declarations and process ids implicit, and assume a multi-copy atomic storage system (see Sect. 3.2).

  4. 4.

    In this straightforward model of shared state there is no global effect of fences, and we omit the straightforward promotion rule.

  5. 5.

    To handle the general case of an assignment , where e may contain more than one shared variable, the antecedents of the rules are combined, retrieving the value of each variable referenced in e individually and accumulating the changes to \(W\).

  6. 6.

    We have excluded address shifting, which creates address dependencies [3], as this does not affect the majority of high-level algorithms in which we are interested. However, address dependencies are accounted for in our tool as discussed in [11].

  7. 7.

    We simplified some of the syntax for clarity, in particular introducing a higher-level statement to model a jump command and implicit register (referenced by the compare () and branch-not-equal () instructions). We have also combined some commands, retaining dependencies, in a way that is not possible in the assembler language. The operator is exclusive-or; its use here artificially creates a data dependency [3] between the updates to \(r_0\) and z.

References

  1. Adve, S.V., Boehm, H.J.: Memory models: a case for rethinking parallel languages and hardware. Commun. ACM 53(8), 90–101 (2010)

    Article  Google Scholar 

  2. Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. SIGPLAN Not. 46(6), 175–186 (2011)

    Article  Google Scholar 

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

    Article  Google Scholar 

  4. Flur, S., Gray, K.E., Pulte, C., Sarkar, S., Sezgin, A., Maranget, L., Deacon, W., Sewell, P.: Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 608–621. ACM, New York (2016)

    Article  Google Scholar 

  5. Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Litmus: running tests against hardware. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 41–44. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_5

    Chapter  Google Scholar 

  6. Mador-Haim, S., Alur, R., Martin, M.M.K.: Generating litmus tests for contrasting memory consistency models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 273–287. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_26

    Chapter  Google Scholar 

  7. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)

    Article  MathSciNet  Google Scholar 

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

  9. Milner, R.: A Calculus of Communicating Systems. Springer, New York (1982). https://doi.org/10.1007/3-540-10235-3

    Book  MATH  Google Scholar 

  10. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall Inc., Upper Saddle River (1985)

    MATH  Google Scholar 

  11. Colvin, R.J., Smith, G.: A wide-spectrum language for verification of programs on weak memory models. CoRR abs/1802.04406 (2018)

    Google Scholar 

  12. Sorin, D.J., Hill, M.D., Wood, D.A.: A Primer on Memory Consistency and Cache Coherence, 1st edn. Morgan & Claypool Publishers, San Francisco (2011)

    Google Scholar 

  13. Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press (2018, to appear)

    Google Scholar 

  14. Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, New York (1994)

    MATH  Google Scholar 

  15. Back, R.J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, New York (1998). https://doi.org/10.1007/978-1-4612-1674-2

    Book  MATH  Google Scholar 

  16. Clavel, M., Duran, F., Eker, S., Lincoln, P., Marti-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285(2), 187–243 (2002)

    Article  MathSciNet  Google Scholar 

  17. Lê, N.M., Pop, A., Cohen, A., Nardelli, F.Z.: Correct and efficient work-stealing for weak memory models. In: Proceedings of the 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2013, pp. 69–80. ACM, New York (2013)

    Google Scholar 

  18. Chase, D., Lev, Y.: Dynamic circular work-stealing deque. In: SPAA 2005: Proceedings of the 17th Annual ACM Symposium on Parallelism in Algorithms and Architectures, pp. 21–28. ACM Press, New York (2005)

    Google Scholar 

  19. Mador-Haim, S., et al.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 495–512. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_36

    Chapter  Google Scholar 

  20. Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 175–189. ACM, New York (2017)

    Google Scholar 

  21. Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)

    Google Scholar 

  22. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5, 596–619 (1983)

    Article  Google Scholar 

  23. Hayes, I.J., Colvin, R.J., Meinicke, L.A., Winter, K., Velykis, A.: An algebra of synchronous atomic steps. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 352–369. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_22

    Chapter  Google Scholar 

  24. Colvin, R.J., Hayes, I.J., Meinicke, L.A.: Designing a semantic model for a wide-spectrum language with concurrency. Formal Aspects Comput. 29(5), 853–875 (2017)

    Article  MathSciNet  Google Scholar 

  25. Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst. 10, 403–419 (1988)

    Article  Google Scholar 

Download references

Acknowledgements

We thank Kirsten Winter, Ian Hayes, and the anonymous reviewers for feedback on this work. It was supported by Australian Research Council Discovery Grant DP160102457.

Author information

Authors and Affiliations

  1. School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, Australia

    Robert J. Colvin & Graeme Smith

Authors
  1. Robert J. Colvin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Graeme Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Graeme Smith .

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. University of Bremen, Bremen, Germany

    Jan Peleska

  3. University of Oxford, Oxford, United Kingdom

    Bill Roscoe

  4. Eindhoven University of Technology, Eindhoven, The Netherlands

    Erik de Vink

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Colvin, R.J., Smith, G. (2018). A Wide-Spectrum Language for Verification of Programs on Weak Memory Models. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95582-7_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95581-0

  • Online ISBN: 978-3-319-95582-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation