Cited By
View all- Tran DOgata K(2024)Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJRewriting Logic and Its Applications10.1007/978-3-031-65941-6_3(45-61)Online publication date: 6-Apr-2024
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
Authors: 
Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon KangAuthors Info & Claims
Article No.: 251, Pages 828 - 856
Abstract
Formal verification is an effective method to address the challenge of designing correct and efficient concurrent data structures. But verification efforts often ignore memory reclamation, which involves nontrivial synchronization between concurrent accesses and reclamation. When incorrectly implemented, it may lead to critical safety errors such as use-after-free and the ABA problem. Semi-automatic safe memory reclamation schemes such as hazard pointers and RCU encapsulate the complexity of manual memory management in modular interfaces. However, this modularity has not been carried over to formal verification.
We propose modular specifications of hazard pointers and RCU, and formally verify realistic implementations of them in concurrent separation logic. Specifically, we design abstract predicates for hazard pointers that capture the meaning of validating the protection of nodes, and those for RCU that support optimistic traversal to possibly retired nodes. We demonstrate that the specifications indeed facilitate modular verification in three criteria: compositional verification, general applicability, and easy integration. In doing so, we present the first formal verification of Harris’s list, the Harris-Michael list, the Chase-Lev deque, and RDCSS with reclamation. We report the Coq mechanization of all our results in the Iris separation logic framework.
References
[1]
Yehuda Afek, Guy Korland, and Eitan Yanovsky. 2010. Quasi-Linearizability: Relaxed Consistency for Improved Concurrency. In Principles of Distributed Systems - 14th International Conference, OPODIS 2010, Tozeur, Tunisia, December 14-17, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6490). Springer, 395–410. https://doi.org/10.1007/978-3-642-17653-1_29
[2]
Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan Stern. 2018. Frightening Small Children and Disconcerting Grown-Ups: Concurrency in the Linux Kernel. SIGPLAN Not., 53, 2 (2018), March, 405–418. issn:0362-1340 https://doi.org/10.1145/3296957.3177156
[3]
Dan Alistarh, William Leiserson, Alexander Matveev, and Nir Shavit. 2017. Forkscan: Conservative Memory Reclamation for Modern Operating Systems. In Proceedings of the Twelfth European Conference on Computer Systems (EuroSys ’17). Association for Computing Machinery, New York, NY, USA. 483–498. isbn:9781450349383 https://doi.org/10.1145/3064176.3064214
[4]
Dan Alistarh, William Leiserson, Alexander Matveev, and Nir Shavit. 2018. ThreadScan: Automatic and Scalable Memory Reclamation. ACM Trans. Parallel Comput., 4, 4 (2018), Article 18, may, 18 pages. issn:2329-4949 https://doi.org/10.1145/3201897
[5]
Daniel Anderson, Guy E. Blelloch, and Yuanhao Wei. 2021. Concurrent Deferred Reference Counting with Constant-Time Overhead. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Association for Computing Machinery, New York, NY, USA. 526–541. isbn:9781450383912 https://doi.org/10.1145/3453483.3454060
[6]
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). Association for Computing Machinery, New York, NY, USA. 55–66. isbn:9781450304900 https://doi.org/10.1145/1926385.1926394
[7]
Richard Bornat, Cristiano Calcagno, Peter O’Hearn, and Matthew Parkinson. 2005. Permission Accounting in Separation Logic. SIGPLAN Not., 40, 1 (2005), jan, 259–270. issn:0362-1340 https://doi.org/10.1145/1047659.1040327
[8]
John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 55–72. isbn:978-3-540-44898-3
[9]
Trevor Alexander Brown. 2015. Reclaiming Memory for Lock-Free Data Structures: There Has to Be a Better Way. In Proceedings of the 2015 ACM Symposium on Principles of Distributed Computing (PODC ’15). Association for Computing Machinery, New York, NY, USA. 261–270. isbn:9781450336178 https://doi.org/10.1145/2767386.2767436
[10]
David Chase and Yossi Lev. 2005. Dynamic Circular Work-Stealing Deque. In Proceedings of the Seventeenth Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA ’05). Association for Computing Machinery, New York, NY, USA. 21–28. isbn:1581139861 https://doi.org/10.1145/1073970.1073974
[11]
Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 – Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 207–231. isbn:978-3-662-44202-9
[12]
Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2019. RustBelt Meets Relaxed Memory. Proc. ACM Program. Lang., 4, POPL (2019), Article 34, Dec., 29 pages. https://doi.org/10.1145/3371102
[13]
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 Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). Association for Computing Machinery, New York, NY, USA. 792–808. isbn:9781450392655 https://doi.org/10.1145/3519939.3523451
[14]
John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, and Heike Wehrheim. 2014. Quiescent Consistency: Defining and Verifying Relaxed Linearizability. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8442). Springer, 200–214. https://doi.org/10.1007/978-3-319-06410-9_15
[15]
M. Desnoyers, P. E. McKenney, A. S. Stern, M. R. Dagenais, and J. Walpole. 2012. User-Level Implementations of Read-Copy Update. IEEE Transactions on Parallel and Distributed Systems, 23, 2 (2012), 375–382. https://doi.org/10.1109/TPDS.2011.159
[16]
Simon Doherty, Lindsay Groves, Victor Luchangco, and Mark Moir. 2004. Formal Verification of a Practical Lock-Free Queue Algorithm. In Formal Techniques for Networked and Distributed Systems – FORTE 2004, David de Frutos-Escrig and Manuel Núñez (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 97–114. isbn:978-3-540-30232-2 https://doi.org/10.1007/978-3-540-30232-2_7
[17]
Marko Doko and Viktor Vafeiadis. 2017. Tackling Real-Life Relaxed Concurrency with FSL++. In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 448–475. isbn:978-3-662-54434-1
[18]
Keir Fraser. 2004. Practical lock-freedom. Ph. D. Dissertation.
[19]
Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, and Yu Zhang. 2010. Reasoning about Optimistic Concurrency Using a Program Logic for History. In CONCUR 2010 - Concurrency Theory, Paul Gastin and François Laroussinie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 388–402. isbn:978-3-642-15375-4 https://doi.org/10.1007/978-3-642-15375-4_27
[20]
Alexey Gotsman, Noam Rinetzky, and Hongseok Yang. 2013. Verifying Concurrent Memory Reclamation Algorithms with Grace. In Proceedings of the 22nd European Conference on Programming Languages and Systems (ESOP’13). Springer-Verlag, Berlin, Heidelberg. 249–269. isbn:9783642370359 https://doi.org/10.1007/978-3-642-37036-6_15
[21]
Alexey Gotsman and Hongseok Yang. 2012. Linearizability with Ownership Transfer. In CONCUR 2012 – Concurrency Theory, Maciej Koutny and Irek Ulidowski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 256–271. isbn:978-3-642-32940-1 https://doi.org/10.1007/978-3-642-32940-1_19
[22]
Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. 2016. Local Linearizability for Concurrent Container-Type Data Structures. In 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada (LIPIcs, Vol. 59). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 6:1–6:15. https://doi.org/10.4230/LIPIcs.CONCUR.2016.6
[23]
Timothy L. Harris. 2001. A Pragmatic Implementation of Non-Blocking Linked-Lists. In Proceedings of the 15th International Conference on Distributed Computing (DISC ’01). Springer-Verlag, Berlin, Heidelberg. 300–314. isbn:3540426051
[24]
Timothy L. Harris, Keir Fraser, and Ian A. Pratt. 2002. A Practical Multi-Word Compare-and-Swap Operation. In Proceedings of the 16th International Conference on Distributed Computing (DISC ’02). Springer-Verlag, Berlin, Heidelberg. 265–279. isbn:3540000739
[25]
Thomas E. Hart, Paul E. McKenney, Angela Demke Brown, and Jonathan Walpole. 2007. Performance of Memory Reclamation for Lockless Synchronization. J. Parallel Distrib. Comput., 67, 12 (2007), dec, 1270–1285. issn:0743-7315 https://doi.org/10.1016/j.jpdc.2007.04.010
[26]
Danny Hendler, Nir Shavit, and Lena Yerushalmi. 2004. A Scalable Lock-Free Stack Algorithm. In Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures (SPAA ’04). Association for Computing Machinery, New York, NY, USA. 206–215. isbn:1581138407 https://doi.org/10.1145/1007912.1007944
[27]
Thomas A. Henzinger, Christoph M. Kirsch, Hannes Payer, Ali Sezgin, and Ana Sokolova. 2013. Quantitative relaxation of concurrent data structures. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013. ACM, 317–328. https://doi.org/10.1145/2429069.2429109
[28]
Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst., 12, 3 (1990), July, 463–492. issn:0164-0925 https://doi.org/10.1145/78969.78972
[29]
Iris Team. 2023. Iris examples. https://gitlab.mpi-sws.org/iris/examples
[30]
Iris Team. 2023. The Iris project website. https://iris-project.org/
[31]
Bart Jacobs and Frank Piessens. 2011. Expressive Modular Fine-Grained Concurrency Specification. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). Association for Computing Machinery, New York, NY, USA. 271–282. isbn:9781450304900 https://doi.org/10.1145/1926385.1926417
[32]
Radha Jagadeesan and James Riely. 2014. Between Linearizability and Quiescent Consistency - Quantitative Quiescent Consistency. In Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 8573). Springer, 220–231. https://doi.org/10.1007/978-3-662-43951-7_19
[33]
Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, and Jeehoon Kang. 2023. Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic (Coq development and appendix). https://doi.org/10.1145/3580418 Project webpage:
[34]
Ralf Jung. 2019. Logical Atomicity in Iris: the Good, the Bad, and the Ugly. Iris Workshop. https://people.mpi-sws.org/~jung/iris/talk-iris2019.pdf
[35]
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. J. Funct. Program., 28 (2018), e20. https://doi.org/10.1017/S0956796818000151
[36]
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2019. The Future is Ours: Prophecy Variables in Separation Logic. Proc. ACM Program. Lang., 4, POPL (2019), Article 45, dec, 32 pages. https://doi.org/10.1145/3371113
[37]
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 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. ACM, 637–650. https://doi.org/10.1145/2676726.2676980
[38]
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 31st European Conference on Object-Oriented Programming (ECOOP 2017), Peter Müller (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 74). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 17:1–17:29. isbn:978-3-95977-035-4 issn:1868-8969 https://doi.org/10.4230/LIPIcs.ECOOP.2017.17
[39]
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxed-Memory Concurrency. SIGPLAN Not., 52, 1 (2017), jan, 175–189. issn:0362-1340 https://doi.org/10.1145/3093333.3009850
[40]
Jeehoon Kang and Jaehwang Jung. 2020. A Marriage of Pointer- and Epoch-Based Reclamation. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). Association for Computing Machinery, New York, NY, USA. 314–328. isbn:9781450376136 https://doi.org/10.1145/3385412.3385978
[41]
Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ’17). Association for Computing Machinery, New York, NY, USA. 205–217. isbn:9781450346603 https://doi.org/10.1145/3009837.3009855
[42]
Siddharth Krishna, Dennis Shasha, and Thomas Wies. 2017. Go with the Flow: Compositional Abstractions for Concurrent Data Structures. Proc. ACM Program. Lang., 2, POPL (2017), Article 37, Dec., 31 pages. https://doi.org/10.1145/3158125
[43]
Ismail Kuru and Colin S. Gordon. 2019. Safe Deferred Memory Reclamation with Types. In Programming Languages and Systems, Luís Caires (Ed.). Springer International Publishing, Cham. 88–116. isbn:978-3-030-17184-1 https://doi.org/10.1007/978-3-030-17184-1_4
[44]
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing Sequential Consistency in C/C++11. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). Association for Computing Machinery, New York, NY, USA. 618–632. isbn:9781450349888 https://doi.org/10.1145/3062341.3062352
[45]
Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers, 28, 9 (1979), 690–691. https://doi.org/10.1109/TC.1979.1675439
[46]
Jean-Marie Madiot and François Pottier. 2022. A Separation Logic for Heap Space under Garbage Collection. Proc. ACM Program. Lang., 6, POPL (2022), Article 11, jan, 28 pages. https://doi.org/10.1145/3498672
[47]
Paul E. McKenney, Maged Michael, Jens Maurer, Peter Sewell, Martin Uecker, Hans Boehm, Hubert Tong, Niall Douglas, Thomas Rodgers, Will Deacon, Michael Wong, David Goldblatt, Kostya Serebryany, and Anthony Williams. 2021. P2414R1: Pointer lifetime-end zap proposed solutions. https://wg21.link/p2414r1
[48]
P. E. McKenney and J. D. Slingwine. 1998. Read-copy update: Using execution history to solve concurrency problems. In PDCS ’98.
[49]
Paul E. McKenney, Michael Wong, Maged M. Michael, Geoffrey Romer, Andrew Hunter, Arthur O’Dwyer, Daisy Hollman, JF Bastien, Hans Boehm, David Goldblatt, Frank Birbacher, Erik Rigtorp, Tomasz Kamiński, and Jens Maurer. 2023. P2545R4: Read-Copy Update (RCU). https://wg21.link/p2545r4
[50]
Meta. 2023. Folly: Facebook Open-source Library. https://github.com/facebook/folly
[51]
Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2020. Cosmo: A Concurrent Separation Logic for Multicore OCaml. Proc. ACM Program. Lang., 4, ICFP (2020), Article 96, aug, 29 pages. https://doi.org/10.1145/3408978
[52]
Roland Meyer, Thomas Wies, and Sebastian Wolff. 2022. A Concurrent Program Logic with a Future and History. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), Article 174, oct, 30 pages. https://doi.org/10.1145/3563337
[53]
Roland Meyer and Sebastian Wolff. 2019. Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis. Proc. ACM Program. Lang., 3, POPL (2019), Article 58, Jan., 31 pages. https://doi.org/10.1145/3290371
[54]
Roland Meyer and Sebastian Wolff. 2019. Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation. Proc. ACM Program. Lang., 4, POPL (2019), Article 68, dec, 36 pages. https://doi.org/10.1145/3371136
[55]
Maged Michael, Maged M. Michael, Michael Wong, Paul McKenney, Andrew Hunter, Daisy S. Hollman, JF Bastien, Hans Boehm, David Goldblatt, Frank Birbacher, and Mathias Stearn. 2023. P2530R3: Hazard Pointers for C++26. https://wg21.link/p2530r3
[56]
Maged M. Michael. 2002. High Performance Dynamic Lock-Free Hash Tables and List-Based Sets. In Proceedings of the Fourteenth Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA ’02). Association for Computing Machinery, New York, NY, USA. 73–82. isbn:1581135297 https://doi.org/10.1145/564870.564881
[57]
Maged M. Michael. 2004. Hazard Pointers: Safe Memory Reclamation for Lock-Free Objects. IEEE Trans. Parallel Distrib. Syst., 15, 6 (2004), June, 491–504. issn:1045-9219 https://doi.org/10.1109/TPDS.2004.8
[58]
Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms. In PODC 1996.
[59]
Ike Mulder and Robbert Krebbers. 2023. Proof Automation for Linearizability in Separation Logic. Proc. ACM Program. Lang., 7, OOPSLA1 (2023), Article 91, apr, 30 pages. https://doi.org/10.1145/3586043
[60]
Ike Mulder, Robbert Krebbers, and Herman Geuvers. 2022. Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). Association for Computing Machinery, New York, NY, USA. 809–824. isbn:9781450392655 https://doi.org/10.1145/3519939.3523432
[61]
Ruslan Nikolaev and Binoy Ravindran. 2020. Universal Wait-Free Memory Reclamation. Association for Computing Machinery, New York, NY, USA. 130–143. isbn:9781450368186 https://doi.org/10.1145/3332466.3374540
[62]
Ruslan Nikolaev and Binoy Ravindran. 2021. Brief Announcement: Crystalline: Fast and Memory Efficient Wait-Free Reclamation. In 35th International Symposium on Distributed Computing (DISC 2021), Seth Gilbert (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 209). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 60:1–60:4. isbn:978-3-95977-210-5 issn:1868-8969 https://doi.org/10.4230/LIPIcs.DISC.2021.60
[63]
Matthew Parkinson, Richard Bornat, and Peter O’Hearn. 2007. Modular Verification of a Non-Blocking Stack. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’07). Association for Computing Machinery, New York, NY, USA. 297–302. isbn:1595935754 https://doi.org/10.1145/1190216.1190261
[64]
Matthew Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Manuel Costa, Pantazis Deligiannis, Aaron Blankstein, Dylan McDermott, and Jonathan Balkind. 2017. Project Snowflake: Non-blocking safe manual memory management in .NET. Microsoft. https://www.microsoft.com/en-us/research/publication/project-snowflake-non-blocking-safe-manual-memory-management-net/
[65]
Gali Sheffi, Maurice Herlihy, and Erez Petrank. 2021. VBR: Version Based Reclamation. In Proceedings of the 33rd ACM Symposium on Parallelism in Algorithms and Architectures (SPAA ’21). Association for Computing Machinery, New York, NY, USA. 443–445. isbn:9781450380706 https://doi.org/10.1145/3409964.3461817
[66]
Ajay Singh, Trevor Brown, and Ali Mashtizadeh. 2021. NBR: Neutralization Based Reclamation. In Proceedings of the 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP ’21). Association for Computing Machinery, New York, NY, USA. 175–190. isbn:9781450382946 https://doi.org/10.1145/3437801.3441625
[67]
Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (Lecture Notes in Computer Science, Vol. 8410). Springer, 149–168. https://doi.org/10.1007/978-3-642-54833-8_9
[68]
Joseph Tassarotti, Derek Dreyer, and Viktor Vafeiadis. 2015. Verifying Read-Copy-Update in a Logic for Weak Memory. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 110–120. isbn:9781450334686 https://doi.org/10.1145/2737924.2737992
[69]
Bogdan Tofan, Gerhard Schellhorn, and Wolfgang Reif. 2011. Formal Verification of a Lock-Free Stack with Hazard Pointers. In Theoretical Aspects of Computing – ICTAC 2011, Antonio Cerone and Pekka Pihlajasaari (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 239–255. isbn:978-3-642-23283-1 https://doi.org/10.1007/978-3-642-23283-1_16
[70]
R. K. Treiber. 1986. Systems programming: coping with parallelism.
[71]
Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. 2014. GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA ’14). Association for Computing Machinery, New York, NY, USA. 691–707. isbn:9781450325851 https://doi.org/10.1145/2660193.2660243
[72]
Viktor Vafeiadis. 2010. Automatically Proving Linearizability. In Computer Aided Verification, Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 450–464. isbn:978-3-642-14295-6 https://doi.org/10.1007/978-3-642-14295-6_40
[73]
Viktor Vafeiadis. 2010. RGSep Action Inference. In Verification, Model Checking, and Abstract Interpretation, Gilles Barthe and Manuel Hermenegildo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 345–361. isbn:978-3-642-11319-2 https://doi.org/10.1007/978-3-642-11319-2_25
[74]
Viktor Vafeiadis. 2011. Concurrent Separation Logic and Operational Semantics. Electronic Notes in Theoretical Computer Science, 276 (2011), 335–351. issn:1571-0661 https://doi.org/10.1016/j.entcs.2011.09.029 Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII)
[75]
Viktor Vafeiadis. 2017. Program Verification Under Weak Memory Consistency Using Separation Logic. In Computer Aided Verification, Rupak Majumdar and Viktor Kunčak (Eds.). Springer International Publishing, Cham. 30–46. isbn:978-3-319-63387-9
[76]
Haosen Wen, Joseph Izraelevitz, Wentao Cai, H. Alan Beadle, and Michael L. Scott. 2018. Interval-Based Memory Reclamation. SIGPLAN Not., 53, 1 (2018), feb, 1–13. issn:0362-1340 https://doi.org/10.1145/3200691.3178488
[77]
Sebastian Wolff. 2021. Verifying Non-blocking Data Structures with Manual Memory Management. Ph. D. Dissertation. https://doi.org/10.24355/dbbs.084-202108191157-0
Index Terms
- Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
Recommendations
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory. A wealth of algorithms and libraries has been developed to explore this exciting technology. As noted by others, ...
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 ...
Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJ
Rewriting Logic and Its ApplicationsAbstractVerification of concurrent programs is very tough because the proof needs to account for a huge number of interleavings of execution steps of all threads. As concurrent programs are often implemented in C/C++, which do not support garbage ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2023
2250 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 16 October 2023
Published in PACMPL Volume 7, Issue OOPSLA2
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
- 436Total Downloads
- Downloads (Last 12 months)353
- Downloads (Last 6 weeks)37
Reflects downloads up to 21 Nov 2024
Other Metrics
Citations
Cited By
View all- Tran DOgata K(2024)Verifying Safe Memory Reclamation in Concurrent Programs with CafeOBJRewriting Logic and Its Applications10.1007/978-3-031-65941-6_3(45-61)Online publication date: 6-Apr-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in