[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/3293883.3295702acmconferencesArticle/Chapter ViewAbstractPublication PagesppoppConference Proceedingsconference-collections
research-article

Verifying C11 programs operationally

Published: 16 February 2019 Publication History

Abstract

This paper develops an operational semantics for a release-acquire fragment of the C11 memory model with relaxed accesses. We show that the semantics is both sound and complete with respect to the axiomatic model of Batty et al. The semantics relies on a per-thread notion of observability, which allows one to reason about a weak memory C11 program in program order. On top of this, we develop a proof calculus for invariant-based reasoning, which we use to verify the release-acquire version of Peterson's mutual exclusion algorithm.

References

[1]
P. A. Abdulla, M. F. Atig, B. Jonsson, and T. P. Ngo. 2018. Optimal stateless model checking under the release-acquire semantics. PACMPL 2, OOPSLA (2018), 135:1--135:29.
[2]
S. V. Adve and K. Gharachorloo. 1996. Shared Memory Consistency Models: A Tutorial. IEEE Computer 29, 12 (1996), 66--76.
[3]
J. Alglave, L. Maranget, and M. Tautschnig. 2014. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36, 2 (2014), 7:1--7:74.
[4]
M. Batty, M. Dodds, and A. Gotsman. 2013. Library abstraction for C/C++ concurrency. In POPL, R. Giacobazzi and R. Cousot (Eds.). ACM, 235--248.
[5]
M. Batty, A. F. Donaldson, and J. Wickerson. 2016. Overhauling SC atomics in C11 and OpenCL. In POPL. ACM, 634--648.
[6]
M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. 2011. Mathe-matizing C++ concurrency. In POPL, T. Ball and M. Sagiv (Eds.). ACM, 55--66.
[7]
S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. 2016. Verifying C11 Programs Operationally. CoRR abs/1811.09143 (2016). arXiv:1811.09143 (Full version with proofs.).
[8]
M. Doko and V. Vafeiadis. 2016. A Program Logic for C11 Memory Fences. In VMCAI (LNCS), Vol. 9583. Springer, 413--430.
[9]
M. Doko and V. Vafeiadis. 2017. Tackling Real-Life Relaxed Concurrency with FSL++. In ESOP. 448--475.
[10]
D. S. Fava, M. Steffen, and V. Stolz. 2018. Operational Semantics of a Weak Memory Model with Channel Synchronization. In FM (LNCS), Vol. 10951. Springer, 258--276.
[11]
M. He, V. Vafeiadis, S. Qin, and J. F. Ferreira. 2016. Reasoning about Fences and Relaxed Atomics. In PDP. IEEE Computer Society, 520--527.
[12]
R. Jagadeesan, C. Pitcher, and J. Riely. 2010. Generative Operational Semantics for Relaxed Memory Models. In ESOP (LNCS), Vol. 6012. Springer, 307--326.
[13]
J.-O. Kaiser, H.-H. Dang, D. Dreyer, O. Lahav, and V. Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP. 17:1--17:29.
[14]
J. Kang, C.-K. Hur, O. Lahav, V. Vafeiadis, and D. Dreyer. 2017. A promising semantics for relaxed-memory concurrency. In POPL. ACM, 175--189.
[15]
M. Kokologiannakis, O. Lahav, K. Sagonas, and V. Vafeiadis. 2018. Effective stateless model checking for C/C++ concurrency. PACMPL 2, POPL (2018), 17:1--17:32.
[16]
O. Lahav, N. Giannarakis, and V. Vafeiadis. 2016. Taming release-acquire consistency. In POPL, R. Bodík and R. Majumdar (Eds.). ACM, 649--662.
[17]
O. Lahav and V. Vafeiadis. 2015. Owicki-Gries Reasoning for Weak Memory Models. In ICALP (2) (LNCS), Vol. 9135. Springer, 311--323.
[18]
O. Lahav and V. Vafeiadis. 2016. Explaining Relaxed Memory Models with Program Transformations. In FM (LNCS), J. S. Fitzgerald, C. L. Heitmeyer, S. Gnesi, and A. Philippou (Eds.), Vol. 9995. 479--495.
[19]
O. Lahav, V.Vafeiadis, J. Kang, C.-K. Hur, andD. Dreyer. 2017. Repairing sequential consistency in C/C++11. In PLDI, A. Cohen and M. T. Vechev (Eds.). ACM, 618--632.
[20]
L. Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28, 9 (1979), 690--691.
[21]
C. Lidbury and A. F. Donaldson. 2017. Dynamic race detection for C++11. In POPL. ACM, 443--457.
[22]
K. Nienhuis, K. Memarian, and P. Sewell. 2016. An operational semantics for C/C++11 concurrency. In OOPSLA. ACM, 111--128.
[23]
S. S. Owicki. 1975. Axiomatic Proof Techniques for Parallel Programs. Garland Publishing, New York.
[24]
A. Podkopaev, I. Sergey, and A. Nanevski. 2016. Operational Aspects of C/C++ Concurrency. CoRR abs/1606.01400 (2016). arXiv:1606.01400
[25]
C. Pulte, S. Flur, W. Deacon, J. French, S. Sarkar, and P. Sewell. 2017. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Proc. ACM Program. Lang. 2, POPL, Article 19 (Dec. 2017), 29 pages.
[26]
A. Turon, V. Vafeiadis, and D. Dreyer. 2014. GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation. In OOPSLA. ACM, New York, NY, USA, 691--707.
[27]
J. Wickerson, M. Batty, T. Sorensen, and G. A. Constantinides. 2017. Automatically comparing memory consistency models. In POPL. ACM, 190--204.
[28]
A. Williams. 2018. https://www.justsoftwaresolutions.co.uk/threading/petersons_lock_with_C++0x_atomics.html. Accessed: 2018-06-20.

Cited By

View all
  • (2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
  • (2024)View-Based Axiomatic Reasoning for the Weak Memory Models PSO and SRAScience of Computer Programming10.1016/j.scico.2024.103225(103225)Online publication date: Oct-2024
  • (2023)Putting Weak Memory in Order via a Promising Intermediate RepresentationProceedings of the ACM on Programming Languages10.1145/35912977:PLDI(1872-1895)Online publication date: 6-Jun-2023
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
PPoPP '19: Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming
February 2019
472 pages
ISBN:9781450362252
DOI:10.1145/3293883
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 February 2019

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. C11
  2. operational semantics
  3. soundness and completeness
  4. verification

Qualifiers

  • Research-article

Funding Sources

  • EPSRC
  • DFG

Conference

PPoPP '19

Acceptance Rates

PPoPP '19 Paper Acceptance Rate 29 of 152 submissions, 19%;
Overall Acceptance Rate 230 of 1,014 submissions, 23%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)25
  • Downloads (Last 6 weeks)1
Reflects downloads up to 06 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
  • (2024)View-Based Axiomatic Reasoning for the Weak Memory Models PSO and SRAScience of Computer Programming10.1016/j.scico.2024.103225(103225)Online publication date: Oct-2024
  • (2023)Putting Weak Memory in Order via a Promising Intermediate RepresentationProceedings of the ACM on Programming Languages10.1145/35912977:PLDI(1872-1895)Online publication date: 6-Jun-2023
  • (2023)Mechanised Operational Reasoning for C11 Programs with Relaxed DependenciesFormal Aspects of Computing10.1145/358028535:2(1-27)Online publication date: 13-Jan-2023
  • (2023)Meow: Memory Evaluation through Optimized Workloads - Synthesizing Litmus Tests for Memory Consistency Verification2023 IEEE 20th India Council International Conference (INDICON)10.1109/INDICON59947.2023.10440892(73-78)Online publication date: 14-Dec-2023
  • (2023)Lifting the Reasoning Level in Generic Weak Memory VerificationiFM 202310.1007/978-3-031-47705-8_10(175-192)Online publication date: 6-Nov-2023
  • (2023)Rely-Guarantee Reasoning for Causally Consistent Shared MemoryComputer Aided Verification10.1007/978-3-031-37706-8_11(206-229)Online publication date: 17-Jul-2023
  • (2023)Overcoming Memory Weakness with Unified FairnessComputer Aided Verification10.1007/978-3-031-37706-8_10(184-205)Online publication date: 17-Jul-2023
  • (2023)View-Based Axiomatic Reasoning for PSOTheoretical Aspects of Software Engineering10.1007/978-3-031-35257-7_17(286-304)Online publication date: 27-Jun-2023
  • (2023)Reasoning About Promises in Weak Memory Models with Event StructuresFormal Methods10.1007/978-3-031-27481-7_17(282-300)Online publication date: 3-Mar-2023
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media