Cited By
View all- Somers TKrebbers R(2024)Verified Lock-Free Session Channels with LinkingProceedings of the ACM on Programming Languages10.1145/36897328:OOPSLA2(588-617)Online publication date: 8-Oct-2024
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
Authors: 
Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon KangAuthors Info & Claims
Article No.: 154, Pages 175 - 198
Abstract
Linearizability is the de facto standard for correctness of concurrent objects—it essentially says that all the object’s operations behave as if they were atomic. There have been a number of recent advances in developing increasingly strong linearizability specifications for relaxed memory consistency (RMC), but scalable proof methods for these specifications do not exist due to the challenges arising from out-of-order executions (requiring event reordering) and selected synchronization (requiring tracking of view transfers).
We propose a proof recipe for the linearizable history specifications by Dang et al. in the Iris-based iRC11 concurrent separation logic in Coq. Key to our proof recipe is the notion of object modification order (OMO), which generalizes the modification order of the C11 memory model to an object-local setting. Using OMO we minimize the conditions that need to be proved for event reordering. To enable proof reuse for concurrent libraries that are built on top of others, OMO provides the novel notion of a commit-with relation that connects the linearization points of the lower and upper libraries. Using our recipe, we verify the linearizability of the Michael–Scott queue, the elimination stack, and Folly’s MPMC queue in RMC for the first time; and verify stronger specifications of a spinlock and atomic reference counting in RMC than prior work.
References
[1]
Mark Batty, Mike Dodds, and Alexey Gotsman. 2013. Library Abstraction for C/C++ Concurrency. In POPL. 235–248. issn:0362-1340 https://doi.org/10.1145/2480359.2429099
[2]
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In POPL. 55–66. isbn:9781450304900 https://doi.org/10.1145/1926385.1926394
[3]
John Bender and Jens Palsberg. 2019. A formalization of Java’s concurrent access modes. PACMPL, 3, OOPSLA (2019), Article 142, https://doi.org/10.1145/3360568
[4]
Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. 2021. Theorems for free from separation logic specifications. PACMPL, 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473586
[5]
Stephen D. Brookes. 2004. A Semantics for Concurrent Separation Logic. In CONCUR (LNCS, Vol. 3170). 16–34. https://doi.org/10.1007/978-3-540-28644-8_2
[6]
Stephen D. Brookes and William C. Rounds. 1983. Behavioural equivalence relations induced by programming logics. In ICALP (LNCS, Vol. 154). 97–108. isbn:978-3-540-40038-7 https://doi.org/10.1007/BFB0036900
[7]
Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP (LNCS, Vol. 8586). 207–231. isbn:978-3-662-44202-9 https://doi.org/10.1007/978-3-662-44202-9_9
[8]
Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2020. RustBelt Meets Relaxed Memory. PACMPL, 4, POPL (2020), Article 34, https://doi.org/10.1145/3371102
[9]
Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, and Derek Dreyer. 2022. Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic. In PLDI. 792–808. isbn:9781450392655 https://doi.org/10.1145/3519939.3523451
[10]
Marko Doko and Viktor Vafeiadis. 2016. A Program Logic for C11 Memory Fences. In VMCAI (LNCS, Vol. 9583). 413–430. isbn:978-3-662-49122-5 https://doi.org/10.1007/978-3-662-49122-5_20
[11]
Marko Doko and Viktor Vafeiadis. 2017. Tackling Real-Life Relaxed Concurrency with FSL++. In ESOP (LNCS). 448–475. isbn:978-3-662-54433-4 https://doi.org/10.1007/978-3-662-54434-1_17
[12]
Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy. 2018. Bounding data races in space and time. In PLDI. 242–255. isbn:9781450356985 https://doi.org/10.1145/3192366.3192421
[13]
Brijesh Dongol, Radha Jagadeesan, James Riely, and Alasdair Armstrong. 2018. On abstraction and compositionality for weak-memory linearisability. In VMCAI (LNCS, Vol. 10747). 183–204. isbn:978-3-319-73721-8 https://doi.org/10.1007/978-3-319-73721-8_9
[14]
Ivana Filipović, Peter O’Hearn, Noam Rinetzky, and Hongseok Yang. 2010. Abstraction for concurrent objects. TCS, 411, 51 (2010), 4379–4398. issn:0304-3975 https://doi.org/10.1016/j.tcs.2010.09.021
[15]
Danny Hendler, Nir Shavit, and Lena Yerushalmi. 2004. A scalable lock-free stack algorithm. In SPAA. 206–215. isbn:1581138407 https://doi.org/10.1145/1007912.1007944
[16]
Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. TOPLAS, 12, 3 (1990), 463–492. issn:0164-0925 https://doi.org/10.1145/78969.78972
[17]
Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256–269. https://doi.org/10.1145/2951913.2951943
[18]
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP, 28 (2018), e20. https://doi.org/10.1017/S0956796818000151
[19]
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020. The future is ours: prophecy variables in separation logic. PACMPL, 4, POPL (2020), Article 45, https://doi.org/10.1145/3371113
[20]
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. 637–650. issn:0362-1340 https://doi.org/10.1145/2775051.2676980
[21]
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxed-Memory Concurrency. In POPL. 175–189. issn:0362-1340 https://doi.org/10.1145/3093333.3009850
[22]
Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019. Model Checking for Weakly Consistent Libraries. In PLDI. 96–110. isbn:9781450367127 https://doi.org/10.1145/3314221.3314609
[23]
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. MoSeL: a general, extensible modal framework for interactive proofs in separation logic. PACMPL, 2, ICFP (2018), 77:1–77:30. https://doi.org/10.1145/3236772
[24]
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP (LNCS, Vol. 10201). 696–723. https://doi.org/10.1007/978-3-662-54434-1_26
[25]
Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205–217. https://doi.org/10.1145/3009837.3009855
[26]
Siddharth Krishna, Dennis Shasha, and Thomas Wies. 2018. Go with the Flow: Compositional Abstractions for Concurrent Data Structures. PACMPL, 2, POPL (2018), Article 37, https://doi.org/10.1145/3158125
[27]
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing Sequential Consistency in C/C++11. In PLDI. 618–632. isbn:9781450349888 https://doi.org/10.1145/3062341.3062352
[28]
Meta. 2023. Folly: Facebook Open-source Library. https://github.com/facebook/folly
[29]
Glen Mével and Jacques-Henri Jourdan. 2021. Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model. PACMPL, 5, ICFP (2021), Article 66, https://doi.org/10.1145/3473571
[30]
Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2020. Cosmo: A Concurrent Separation Logic for Multicore OCaml. PACMPL, 4, ICFP (2020), Article 96, https://doi.org/10.1145/3408978
[31]
Roland Meyer, Thomas Wies, and Sebastian Wolff. 2022. A Concurrent Program Logic with a Future and History. PACMPL, 6, OOPSLA2 (2022), Article 174, https://doi.org/10.1145/3563337
[32]
Roland Meyer, Thomas Wies, and Sebastian Wolff. 2023. Embedding Hindsight Reasoning in Separation Logic. PACMPL, 7, PLDI (2023), Article 182, https://doi.org/10.1145/3591296
[33]
Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms. In PODC. 267–275. isbn:0897918002 https://doi.org/10.1145/248052.248106
[34]
Ike Mulder and Robbert Krebbers. 2023. Proof Automation for Linearizability in Separation Logic. PACMPL, 7, OOPSLA1 (2023), 91:462–91:491. https://doi.org/10.1145/3586043
[35]
Ike Mulder, Robbert Krebbers, and Herman Geuvers. 2022. Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris. PLDI. 809–824. isbn:978-1-4503-9265-5 https://doi.org/10.1145/3519939.3523432
[36]
Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2017. Viper: A verification infrastructure for permission-based reasoning. 104–125. https://doi.org/10.3233/978-1-61499-810-5-104
[37]
Peter W. O’Hearn. 2004. Resources, Concurrency and Local Reasoning. In CONCUR (LNCS, Vol. 3170). 49–67. https://doi.org/10.1007/978-3-540-28644-8_4
[38]
Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, and Jeehoon Kang. 2024. Artifact for "A Proof Recipe for Linearizability in Relaxed Memory Separation Logic", PLDI 2024. https://doi.org/10.5281/zenodo.10933398
[39]
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. 2019. On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models. PACMPL, 3, POPL (2019), Article 68, https://doi.org/10.1145/3290381
[40]
Abhishek Kr Singh and Ori Lahav. 2023. An Operational Approach to Library Abstraction under Relaxed Memory Concurrency. PACMPL, 7, POPL (2023), Article 53, https://doi.org/10.1145/3571246
[41]
Graeme Smith, Kirsten Winter, and Robert J. Colvin. 2020. Linearizability on Hardware Weak Memory Models. Form. Asp. Comput., 32, 1 (2020), 1–32. issn:0934-5043 https://doi.org/10.1007/s00165-019-00499-8
[42]
Alexander J. Summers and Peter Müller. 2018. Automating Deductive Verification for Weak-Memory Programs. In TACAS (LNCS, Vol. 10805). 190–209. isbn:978-3-319-89960-2 https://doi.org/10.1007/978-3-319-89960-2_11
[43]
R.K. Treiber. 1986. Systems Programming: Coping with Parallelism. International Business Machines Incorporated, Thomas J. Watson Research Center. https://books.google.co.kr/books?id=YQg3HAAACAAJ
[44]
Viktor Vafeiadis. 2010. Automatically Proving Linearizability. In CAV (LNCS, Vol. 6174). 450–464. isbn:978-3-642-14295-6 https://doi.org/10.1007/978-3-642-14295-6_40
[45]
Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed Separation Logic: A Program Logic for C11 Concurrency. In OOPSLA. 867–884. https://doi.org/10.1145/2509136.2509532
[46]
Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael–Scott queue (proof pearl). In CPP. 76–90. https://doi.org/10.1145/3437992.3439930
[47]
Felix A. Wolf, Malte Schwerhoff, and Peter Müller. 2021. Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA. In FM (LNCS, Vol. 13047). 407–426. isbn:978-3-030-90870-6 https://doi.org/10.1007/978-3-030-90870-6_22
[48]
He Zhu, Gustavo Petri, and Suresh Jagannathan. 2015. Poling: SMT Aided Linearizability Proofs. In CAV (LNCS, Vol. 9207). 3–19. isbn:978-3-319-21668-3 https://doi.org/10.1007/978-3-319-21668-3_1
Index Terms
- A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
Recommendations
Proof Automation for Linearizability in Separation Logic
Recent advances in concurrent separation logic enabled the formal verification of increasingly sophisticated fine-grained (i.e., lock-free) concurrent programs. For such programs, the golden standard of correctness is linearizability, which expresses ...
Relaxed separation logic: a program logic for C11 concurrency
OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applicationsWe introduce relaxed separation logic (RSL), the first program logic for reasoning about concurrent programs running under the C11 relaxed memory model. From a user's perspective, RSL is an extension of concurrent separation logic (CSL) with proof rules ...
Relaxed separation logic: a program logic for C11 concurrency
OOPSLA '13We introduce relaxed separation logic (RSL), the first program logic for reasoning about concurrent programs running under the C11 relaxed memory model. From a user's perspective, RSL is an extension of concurrent separation logic (CSL) with proof rules ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 June 2024
Published in PACMPL Volume 8, Issue PLDI
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- Samsung Research Funding & Incubation Center of Samsung Electronics
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 262Total Downloads
- Downloads (Last 12 months)262
- Downloads (Last 6 weeks)77
Reflects downloads up to 12 Nov 2024
Other Metrics
Citations
Cited By
View all- Somers TKrebbers R(2024)Verified Lock-Free Session Channels with LinkingProceedings of the ACM on Programming Languages10.1145/36897328:OOPSLA2(588-617)Online publication date: 8-Oct-2024
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in