[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

Compositional Reasoning for Non-multicopy Atomic Architectures

Published: 23 June 2023 Publication History

Abstract

Rely/guarantee reasoning provides a compositional approach to reasoning about concurrent programs. However, such reasoning traditionally assumes a sequentially consistent memory model and hence is unsound on modern hardware in the presence of data races. In this article, we present a rely/guarantee-based approach for non-multicopy atomic weak memory models, i.e., where a thread’s stores are not simultaneously propagated to all other threads and hence are not observable by other threads at the same time. Such memory models include those of the earlier versions of the ARM processor as well as the POWER processor.
This article builds on our approach to compositional reasoning for multicopy atomic architectures, i.e., where a thread’s stores are simultaneously propagated to all other threads. In that context, an operational semantics can be based on thread-local instruction reordering. We exploit this to provide an efficient compositional proof technique in which weak memory behaviour can be shown to preserve rely/guarantee reasoning on a sequentially consistent memory model. To achieve this, we introduce a side-condition, reordering interference freedom on each thread, reducing the complexity of weak memory to checks over pairs of reorderable instructions.
In this article, we extend our approach to non-multicopy atomic weak memory models. We utilise the idea of reordering interference freedom between parallel components. This by itself would break compositionality but serves as a vehicle to derive a refined compatibility check between rely and guarantee conditions, which takes into account the effects of propagations of stores that are only partial, i.e., not covering all threads. All aspects of our approach have been encoded and proved sound in Isabelle/HOL.

References

[1]
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. 2017. Context-bounded analysis for POWER. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17)(Lecture Notes in Computer Science, Vol. 10206). 56–74. DOI:
[2]
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, and Konstantinos Sagonas. 2019. Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc. ACM Program. Lang. 3, OOPSLA (2019), 150:1–150:29. DOI:
[3]
Jade Alglave, Luc Maranget, and Michael 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. DOI:
[4]
Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of the 4th International Symposium on Formal Methods for Components and Objects (FMCO’05)(Lecture Notes in Computer Science, Vol. 4111). Springer, 364–387. DOI:
[5]
Mark Batty, Mike Dodds, and Alexey Gotsman. 2013. Library abstraction for C/C++ concurrency. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13). ACM, 235–248. DOI:
[6]
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11). ACM, 55–66. DOI:
[7]
Hans-Juergen Boehm. 2012. Can seqlocks get along with programming language memory models? In Proceedings of the ACM SIGPLAN Workshop on Memory Systems Performance and Correctness: Held in Conjunction with PLDI’12. ACM, 12–20. DOI:
[8]
Stephen Brookes and Peter W. O’Hearn. 2016. Concurrent separation logic. ACM SIGLOG News 3, 3 (2016), 47–65. DOI:
[9]
Robert J. Colvin. 2021. Parallelized sequential composition and hardware weak memory models. In Proceedings of the 19th International Conference on Software Engineering and Formal Methods(Lecture Notes in Computer Science, Vol. 13085). Springer, 201–221.
[10]
Robert J. Colvin and Graeme Smith. 2018. A wide-spectrum language for verification of programs on weak memory models. In Proceedings of the 22nd International Symposium on Formal Methods (FM’18) (series Lecture Notes in Computer Science, Vol. 10951). Springer, 240–257. DOI:
[11]
Nicholas Coughlin, Kirsten Winter, and Graeme Smith. 2021. Rely/guarantee reasoning for multicopy atomic weak memory models. In Proceedings of the 24th International Symposium on Formal Methods(Lecture Notes in Computer Science, Vol. 13047). Springer, 292–310.
[12]
Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. 2020. Owicki-Gries reasoning for C11 RAR. In Proceedings of the 34th European Conference on Object-Oriented Programming (ECOOP’20)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 11:1–11:26.
[13]
Edsger W. Dijkstra and Carel S. Scholten. 1990. Predicate Calculus and Program Semantics. Springer-Verlag, Berlin.
[14]
Vijay D’Silva, Mathias Payer, and Dawn Xiaodong Song. 2015. The correctness-security gap in compiler optimization. In Proceedings of the IEEE Symposium on Security and Privacy Workshops (SPW’15). IEEE Computer Society, 73–87. DOI:
[15]
Xinyu Feng. 2009. Local rely-guarantee reasoning. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 315–327. DOI:
[16]
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 architecture, operationally: Concurrency and ISA. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’16). ACM, 608–621. DOI:
[17]
Natalia Gavrilenko, Hernán Ponce de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. 2019. BMC for weak memory models: Relation analysis for compact SMT encodings. In Proceedings of the 31st International Conference on Computer Aided Verification (CAV’19)(Lecture Notes in Computer Science, Vol. 11561). Springer, 355–365. DOI:
[18]
C. A. R. Hoare. 1969. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576–580. DOI:
[19]
Cliff B. Jones. 1983. Specification and design of (parallel) programs. In Proceedings of the IFIP Congress. 321–332.
[20]
Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In Proceedings of the 31st European Conference on Object-Oriented Programming (ECOOP’17)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 17:1–17:29. DOI:
[21]
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A promising semantics for relaxed-memory concurrency. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17). ACM, 175–189. Retrieved from http://dl.acm.org/citation.cfm?id=3009850.
[22]
G. A. Kildall. 1973. A unified approach to global program optimization. In Proceedings of the Principles of Programming Languages Symposium (POPL’73). ACM, 194–206.
[23]
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis. 2021. PerSeVerE: Persistency semantics for verification under ext4. Proc. ACM Program. Lang. 5, POPL (2021), 1–29. DOI:
[24]
Markus Kusano and Chao Wang. 2017. Thread-modular static analysis for relaxed memory models. In Proceedings of the 11th Joint Meeting on Foundations of Software Engineering (ESEC/FSE’17). ACM, 337–348. DOI:
[25]
Ori Lahav and Udi Boker. 2020. Decidable verification under a causally consistent shared memory. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM, 211–226. DOI:
[26]
Ori Lahav and Viktor Vafeiadis. 2015. Owicki-Gries reasoning for weak memory models. In Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP’15)(Lecture Notes in Computer Science, Vol. 9135). Springer, 311–323. DOI:
[27]
K. Rustan M. Leino. 2010. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning(Lecture Notes in Computer Science, Vol. 6355). Springer, 348–370. DOI:
[28]
Maged M. Michael and Michael L. Scott. 1996. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proceedings of the 15th Annual ACM Symposium on Principles of Distributed Computing. ACM, 267–275. DOI:
[29]
Mark Moir and Nir Shavit. 2004. Concurrent data structures. In Handbook of Data Structures and Applications.Chapman and Hall/CRC. DOI:
[30]
Tobias Nipkow and Gerwin Klein. 2014. Concrete Semantics—With Isabelle/HOL. Springer. DOI:
[31]
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL—A Proof Assistant for Higher-order Logic. (Lecture Notes in Computer Science, Vol. 2283). Springer. DOI:
[32]
Gary L. Peterson. 1981. Myths about the mutual exclusion problem. Inf. Process. Lett. 12, 3 (1981), 115–116. DOI:
[33]
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2018. Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2, POPL (2018), 19:1–19:29. DOI:
[34]
Azalea Raad, Marko Doko, Lovro Rozic, Ori Lahav, and Viktor Vafeiadis. 2019. On library correctness under weak memory consistency: Specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang. 3, POPL (2019), 68:1–68:31. DOI:
[35]
Tom Ridge. 2010. A rely-guarantee proof system for x86-TSO. In Proceedings of the 3rd International Conference on Verified Software: Theories, Tools, Experiments (VSTTE’10)(Lecture Notes in Computer Science, Vol. 6217). Springer, 55–70. DOI:
[36]
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. 2011. Understanding POWER multiprocessors. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’11). ACM, 175–186. DOI:
[37]
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53, 7 (2010), 89–97. DOI:
[38]
Daniel J. Sorin, Mark D. Hill, and David A. Wood. 2011. A Primer on Memory Consistency and Cache Coherence. Morgan & Claypool Publishers. DOI:
[39]
Ketil Stølen. 1991. A method for the development of totally correct shared-state parallel programs. In Proceedings of the 2nd International Conference on Concurrency Theory(Lecture Notes in Computer Science, Vol. 527). Springer, 510–525.
[40]
Thibault Suzanne and Antoine Miné. 2018. Relational thread-modular abstract interpretation under relaxed memory models. In Proceedings of the 16th Asian Symposium on Programming Languages and Systems (APLAS’18)(Lecture Notes in Computer Science, Vol. 11275). Springer, 109–128. DOI:
[41]
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor Vafeiadis. 2018. A separation logic for a promising semantics. In Proceedings of the 27th European Symposium on Programming: Programming Languages and Systems (ESOP’18), Held as Part of the European Joint Conferences on Theory and Practice of Software(Lecture Notes in Computer Science, Vol. 10801). Springer, 357–384. DOI:
[42]
Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. 2014. GPS: Navigating weak memory with ghosts, protocols, and separation. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA’14). ACM, 691–707. DOI:
[43]
Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed separation logic: A program logic for C11 concurrency. In Proceedings of theACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA’13). ACM, 867–884. DOI:
[44]
Viktor Vafeiadis and Matthew J. Parkinson. 2007. A marriage of rely/guarantee and separation logic. In Proceedings of the 18th International Conference on Concurrency Theory(Lecture Notes in Computer Science, Vol. 4703). Springer, 256–271. DOI:
[45]
Andrew Waterman, Yunsup Lee, David A Patterson, and Krste Asanovi. 2016. The RISC-V Instruction Set Manual. Volume 1: User-level ISA, Version 2.2. Technical Report EECS-2016-118. Department of Electrical Engineering and Computer Science, University of California, Berkeley.
[46]
Kirsten Winter, Nicholas Coughlin, and Graeme Smith. 2021. Backwards-directed information flow analysis for concurrent programs. In Proceedings of the 34th IEEE Computer Security Foundations Symposium (CSF’21). IEEE, 1–16. DOI:
[47]
Daniel Wright, Mark Batty, and Brijesh Dongol. 2021. Owicki-Gries reasoning for C11 programs with relaxed dependencies. In Proceedings of the 24th International Symposium on Formal Methods(Lecture Notes in Computer Science, Vol. 13047). Springer, 237–254. DOI:
[48]
Qiwen Xu, Willem P. de Roever, and Jifeng He. 1997. The rely-guarantee method for verifying shared variable concurrent programs. Form. Asp. Comput. 9, 2 (1997), 149–174. DOI:

Cited By

View all

Index Terms

  1. Compositional Reasoning for Non-multicopy Atomic Architectures

        Recommendations

        Comments

        Please enable JavaScript to view thecomments powered by Disqus.

        Information & Contributors

        Information

        Published In

        cover image Formal Aspects of Computing
        Formal Aspects of Computing  Volume 35, Issue 2
        June 2023
        187 pages
        ISSN:0934-5043
        EISSN:1433-299X
        DOI:10.1145/3605783
        Issue’s Table of Contents

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        Published: 23 June 2023
        Online AM: 14 December 2022
        Accepted: 13 November 2022
        Revised: 20 September 2022
        Received: 31 March 2022
        Published in FAC Volume 35, Issue 2

        Permissions

        Request permissions for this article.

        Check for updates

        Author Tags

        1. Verification
        2. rely/guarantee reasoning
        3. weak memory models
        4. non-multicopy atomicity

        Qualifiers

        • Research-article

        Contributors

        Other Metrics

        Bibliometrics & Citations

        Bibliometrics

        Article Metrics

        • Downloads (Last 12 months)456
        • Downloads (Last 6 weeks)50
        Reflects downloads up to 20 Jan 2025

        Other Metrics

        Citations

        Cited By

        View all
        • (2024)Unifying Weak Memory Verification Using PotentialsFormal Methods10.1007/978-3-031-71162-6_27(519-537)Online publication date: 9-Sep-2024
        • (2024)Detecting Speculative Execution Vulnerabilities on Weak Memory ModelsFormal Methods10.1007/978-3-031-71162-6_25(482-500)Online publication date: 9-Sep-2024
        • (2024)A Rely-Guarantee Framework for Proving Deadlock Freedom Under Causal ConsistencyThe Practice of Formal Methods10.1007/978-3-031-66676-6_5(88-108)Online publication date: 4-Sep-2024
        • (2024)Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore ArchitecturesThe Practice of Formal Methods10.1007/978-3-031-66676-6_4(65-87)Online publication date: 4-Sep-2024
        • (2023)Mechanised Operational Reasoning for C11 Programs with Relaxed DependenciesFormal Aspects of Computing10.1145/358028535:2(1-27)Online publication date: 23-Jun-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

        View Options

        View options

        PDF

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader

        Full Text

        View this article in Full Text.

        Full Text

        Login options

        Full Access

        Media

        Figures

        Other

        Tables

        Share

        Share

        Share this Publication link

        Share on social media