Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Owicki-Gries Reasoning for Weak Memory Models

  • Conference paper
  • First Online:
Automata, Languages, and Programming (ICALP 2015)

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

Included in the following conference series:

Abstract

We show that even in the absence of auxiliary variables, the well-known Owicki-Gries method for verifying concurrent programs is unsound for weak memory models. By strengthening its non-interference check, however, we obtain OGRA, a program logic that is sound for reasoning about programs in the release-acquire fragment of the C11 memory model. We demonstrate the usefulness of this logic by applying it to several challenging examples, ranging from small litmus tests to an implementation of the RCU synchronization primitives.

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. Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL 2011, pp. 55–66. ACM (2011)

    Google Scholar 

  2. Cohen, E.: Coherent causal memory (2014). CoRR abs/1404.2187

    Google Scholar 

  3. Desnoyers, M., McKenney, P.E., Stern, A.S., Dagenais, M.R., Walpole, J.: User-level implementations of read-copy update. IEEE Trans. Parallel Distrib. Syst. 23(2), 375–382 (2012)

    Article  Google Scholar 

  4. Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 267–286. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI 2012, pp. 405–416. ACM (2012)

    Google Scholar 

  6. ISO/IEC 14882:2011: Programming language C++ (2011)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  8. Maranget, L., Sarkar, S., Sewell, P.: A tutorial introduction to the ARM and POWER relaxed memory models (2012). http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf

  9. Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391–407. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6(4), 319–340 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  11. Owicki, S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19(5), 279–285 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  12. Owicki, S.S.: Axiomatic Proof Techniques for Parallel Programs. Ph.D. thesis, Cornell University, Ithaca, NY, USA (1975)

    Google Scholar 

  13. Ridge, T.: A rely-guarantee proof system for x86-TSO. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 55–70. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Sieczkowski, F., Svendsen, K., Birkedal, L., Pichon-Pharabod, J.: A separation logic for fictional sequential consistency. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 736–761. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  15. Tassarotti, J., Dreyer, D., Vafeiadis, V.: Verifying read-copy-update in a logic for weak memory. In: PLDI 2015. ACM (2015)

    Google Scholar 

  16. Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating weak memory with ghosts, protocols, and separation. In: OOPSLA 2014, pp. 691–707. ACM (2014)

    Google Scholar 

  17. 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: POPL 2015, pp. 209–220. ACM (2015)

    Google Scholar 

  18. Vafeiadis, V., Narayan, C.: Relaxed separation logic: A program logic for C11 concurrency. In: OOPSLA 2013, pp. 867–884. ACM (2013)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

    Ori Lahav & Viktor Vafeiadis

Authors
  1. Ori Lahav
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Viktor Vafeiadis
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ori Lahav .

Editor information

Editors and Affiliations

  1. Reykjavik University, Reykjavik, Iceland

    Magnús M. Halldórsson

  2. Kyoto University, Kyoto, Japan

    Kazuo Iwama

  3. The University of Tokyo, Tokyo, Japan

    Naoki Kobayashi

  4. Technische Universiteit Eindhoven, Eindhoven, The Netherlands

    Bettina Speckmann

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lahav, O., Vafeiadis, V. (2015). Owicki-Gries Reasoning for Weak Memory Models. In: Halldórsson, M., Iwama, K., Kobayashi, N., Speckmann, B. (eds) Automata, Languages, and Programming. ICALP 2015. Lecture Notes in Computer Science(), vol 9135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47666-6_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-47666-6_25

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-47665-9

  • Online ISBN: 978-3-662-47666-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation