More Web Proxy on the site http://driver.im/

research-article

Open access

Implementing and verifying release-acquire transactional memory in C11

Authors:

Sadegh Dalvandi,

Brijesh DongolAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 6, Issue OOPSLA2

Article No.: 189, Pages 1817 - 1844

https://doi.org/10.1145/3563352

Published: 31 October 2022 Publication History

Abstract

Transactional memory (TM) is an intensively studied synchronisation paradigm with many proposed implementations in software and hardware, and combinations thereof. However, TM under relaxed memory, e.g., C11 (the 2011 C/C++ standard) is still poorly understood, lacking rigorous foundations that support verifiable implementations. This paper addresses this gap by developing TMS2-ra, a relaxed operational TM specification. We integrate TMS2-ra with RC11 (the repaired C11 memory model that disallows load-buffering) to provide a formal semantics for TM libraries and their clients. We develop a logic, TARO, for verifying client programs that use TMS2-ra for synchronisation. We also show how TMS2-ra can be implemented by a C11 library, TML-ra, that uses relaxed and release-acquire atomics, yet guarantees the synchronisation properties required by TMS2-ra. We benchmark TML-ra and show that it outperforms its sequentially consistent counterpart in the STAMP benchmarks. Finally, we use a simulation-based verification technique to prove correctness of TML-ra. Our entire development is supported by the Isabelle/HOL proof assistant.

References

[1]

P. A. Abdulla, J. Arora, M. F. Atig, and S. N. Krishna. 2019. Verification of programs under the release-acquire semantics. In PLDI, K. S. McKinley and K. Fisher (Eds.). ACM, 1117–1132. https://doi.org/10.1145/3314221.3314649

Digital Library

[2]

J. Alglave and P. Cousot. 2017. Ogre and Pythia: an invariance proof method for weak consistency models. In POPL, G. Castagna and A. D. Gordon (Eds.). ACM, 3–18. isbn:978-1-4503-4660-3

[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.

Digital Library

[4]

A. Armstrong and B. Dongol. 2017. Modularising Opacity Verification for Hybrid Transactional Memory. In FORTE, A. Bouajjani and A. Silva (Eds.) (LNCS, Vol. 10321). Springer, 33–49.

[5]

A. Armstrong, B. Dongol, and S. Doherty. 2017. Proving Opacity via Linearizability: A Sound and Complete Method. In FORTE, A. Bouajjani and A. Silva (Eds.) (LNCS, Vol. 10321). Springer, 50–66.

[6]

G. Assa, H. Meir, G. Golan-Gueta, I. Keidar, and A. Spiegelman. 2020. Nesting and composition in transactional data structure libraries. In PPoPP ’20, R. Gupta and X. Shen (Eds.). ACM, 405–406. https://doi.org/10.1145/3332466.3374514

Digital Library

[7]

G. Assa, H. Meir, G. Golan-Gueta, I. Keidar, and A. Spiegelman. 2021. Using Nesting to Push the Limits of Transactional Data Structure Libraries. In OPODIS, Q. Bramas, V. Gramoli, and A. Milani (Eds.) (LIPIcs, Vol. 217). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 30:1–30:17. https://doi.org/10.4230/LIPIcs.OPODIS.2021.30

[8]

H. Attiya, A. Gotsman, S. Hans, and N. Rinetzky. 2018. Characterizing Transactional Memory Consistency Conditions Using Observational Refinement. J. ACM, 65, 1 (2018), 2:1–2:44.

[9]

M. Batty, A. F. Donaldson, and J. Wickerson. 2016. Overhauling SC atomics in C11 and OpenCL. In POPL. ACM, 634–648.

[10]

M. Batty, S. Owens, S. Sarkar, P. Sewell, and T. Weber. 2011. Mathematizing C++ concurrency. In POPL, T. Ball and M. Sagiv (Eds.). ACM, 55–66. isbn:978-1-4503-0490-0

[11]

S. M. Beillahi, A. Bouajjani, and C. Enea. 2021. Checking Robustness Between Weak Transactional Consistency Models. In ESOP, N. Yoshida (Ed.) (LNCS, Vol. 12648). Springer, 87–117. https://doi.org/10.1007/978-3-030-72019-3_4

Digital Library

[12]

S. M. Beillahi, A. Bouajjani, and C. Enea. 2021. Robustness Against Transactional Causal Consistency. Log. Methods Comput. Sci., 17, 1 (2021), https://lmcs.episciences.org/7149

[13]

E. Vafeiadi Bila, B. Dongol, O. Lahav, A. Raad, and J. Wickerson. 2022. View-Based Owicki-Gries Reasoning for Persistent x86-TSO. In ESOP, I. Sergey (Ed.) (Lecture Notes in Computer Science, Vol. 13240). Springer, 234–261. https://doi.org/10.1007/978-3-030-99336-8_9

Digital Library

[14]

S. Böhme and T. Nipkow. 2010. Sledgehammer: Judgement Day. In IJCAR (LNCS, Vol. 6173). Springer, 107–121.

[15]

N. G. Bronson, J. Casper, H. Chafi, and K. Olukotun. 2010. Transactional predication: high-performance concurrent sets and maps for STM. In PODC, A. W. Richa and R. Guerraoui (Eds.). ACM, 6–15. https://doi.org/10.1145/1835698.1835703

Digital Library

[16]

N. Chong, T. Sorensen, and J. Wickerson. 2018. The semantics of transactions and weak memory in x86, Power, ARM, and C++. In PLDI, J. S. Foster and D. Grossman (Eds.). ACM, 211–225. https://doi.org/10.1145/3192366.3192373

Digital Library

[17]

cppreference.com. 2022. std::atomic_compare_exchange. https://en.cppreference.com/w/cpp/atomic/atomic_compare_exchange Accessed 18 July, 2022

[18]

L. Dalessandro, D. Dice, M. L. Scott, N. Shavit, and M. F. Spear. 2010. Transactional Mutex Locks. In Euro-Par (2) (LNCS, Vol. 6272). Springer, 2–13.

[19]

S. Dalvandi, S. Doherty, B. Dongol, and H. Wehrheim. 2020. Owicki-Gries Reasoning for C11 RAR. In ECOOP, R. Hirschfeld and T. Pape (Eds.) (LIPIcs, Vol. 166). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 11:1–11:26. https://doi.org/10.4230/LIPIcs.ECOOP.2020.11

[20]

S. Dalvandi, S. Doherty, B. Dongol, and H. Wehrheim. 2020. Owicki-Gries Reasoning for C11 RAR (Artifact). Dagstuhl Artifacts Ser., 6, 2 (2020), 15:1–15:2. https://doi.org/10.4230/DARTS.6.2.15

[21]

S. Dalvandi and B. Dongol. 2021. Verifying C11-style weak memory libraries. In PPoPP, J. Lee and E. Petrank (Eds.). ACM, 451–453. https://doi.org/10.1145/3437801.3441619

Digital Library

[22]

S. Dalvandi and B. Dongol. 2022. Implementing and Verifying Release-Acquire Transactional Memory (Artifact). https://doi.org/10.5281/zenodo.6899919

Digital Library

[23]

S. Dalvandi and B. Dongol. 2022. Implementing and Verifying Release-Acquire Transactional Memory (Extended Version). https://doi.org/10.48550/ARXIV.2208.00315

[24]

S. Dalvandi, B. Dongol, S. Doherty, and H. Wehrheim. 2022. Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. J. Autom. Reason., 66, 1 (2022), 141–171. https://doi.org/10.1007/s10817-021-09610-2

Digital Library

[25]

H.-H. Dang, J. Jung, J. Choi, D.-T. Nguyen, W. Mansky, J. Kang, and D. Dreyer. 2022. Compass: strong and compositional library specifications in relaxed memory separation logic. In PLDI, R. Jhala and I. Dillig (Eds.). ACM, 792–808. https://doi.org/10.1145/3519939.3523451

Digital Library

[26]

W. P. de Roever and K. Engelhardt. 1998. Data Refinement: Model-oriented Proof Theories and their Comparison (Cambridge Tracts in Theoretical Computer Science, Vol. 46). Cambridge University Press. isbn:0-521-64170-5

[27]

J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim. 2018. Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput., 30, 5 (2018), 597–625. https://doi.org/10.1007/s00165-017-0433-3

Digital Library

[28]

D. Dice, O. Shalev, and N. Shavit. 2006. Transactional Locking II. In DISC, S. Dolev (Ed.) (Lecture Notes in Computer Science, Vol. 4167). Springer, 194–208. https://doi.org/10.1007/11864219_14

Digital Library

[29]

S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim. 2016. Proving Opacity of a Pessimistic STM. In OPODIS, P. Fatourou, E. Jiménez, and F. Pedone (Eds.) (LIPIcs, Vol. 70). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 35:1–35:17.

[30]

S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. 2018. Making Linearizability Compositional for Partially Ordered Executions. In iFM, C. A. Furia and K. Winter (Eds.) (LNCS, Vol. 11023). Springer, 110–129. https://doi.org/10.1007/978-3-319-98938-9_7

[31]

S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. 2019. Verifying C11 programs operationally. In PPoPP, Jeffrey K. Hollingsworth and Idit Keidar (Eds.). ACM, 355–365. isbn:978-1-4503-6225-2

[32]

S. Doherty, L. Groves, V. Luchangco, and M. Moir. 2013. Towards formally specifying and verifying transactional memory. Formal Asp. Comput., 25, 5 (2013), 769–799.

Digital Library

[33]

M. Doko and V. Vafeiadis. 2017. Tackling Real-Life Relaxed Concurrency with FSL++. In ESOP. 448–475.

[34]

S. Dolan, KC Sivaramakrishnan, and A. Madhavapeddy. 2018. Bounding Data Races in Space and Time. In PLDI (PLDI 2018). ACM, New York, NY, USA. 242–255. isbn:978-1-4503-5698-5

[35]

B. Dongol and L. Groves. 2016. Contextual Trace Refinement for Concurrent Objects: Safety and Progress. In ICFEM, K. Ogata, M. Lawford, and S. Liu (Eds.) (Lecture Notes in Computer Science, Vol. 10009). 261–278. https://doi.org/10.1007/978-3-319-47846-3_17

[36]

B. Dongol, R. Jagadeesan, and J. Riely. 2018. Transactions in relaxed memory architectures. PACMPL, 2, POPL (2018), 18:1–18:29.

[37]

B. Dongol, R. Jagadeesan, and J. Riely. 2019. Modular transactions: bounding mixed races in space and time. In PPoPP, J. K. Hollingsworth and I. Keidar (Eds.). ACM, 82–93. https://doi.org/10.1145/3293883.3295708

Digital Library

[38]

B. Dongol, R. Jagadeesan, J. Riely, and A. Armstrong. 2018. On abstraction and compositionality for weak-memory linearisability. In VMCAI (LNCS, Vol. 10747). Springer, 183–204.

[39]

M. Emmi and C. Enea. 2019. Weak-consistency specification via visibility relaxation. Proc. ACM Program. Lang., 3, POPL (2019), 60:1–60:28. https://doi.org/10.1145/3290373

Digital Library

[40]

A. Gotsman and H. Yang. 2011. Liveness-Preserving Atomicity Abstraction. In ICALP, L. Aceto, M. Henzinger, and J. Sgall (Eds.) (Lecture Notes in Computer Science, Vol. 6756). Springer, 453–465. https://doi.org/10.1007/978-3-642-22012-8_36

[41]

R. Guerraoui and M. Kapalka. 2010. Principles of Transactional Memory. Morgan & Claypool Publishers.

[42]

M. He, V. Vafeiadis, S. Qin, and J. F. Ferreira. 2016. Reasoning about Fences and Relaxed Atomics. In PDP. IEEE Computer Society, 520–527. isbn:978-1-4673-8776-7

[43]

M. Herlihy and J. E. B. Moss. 1993. Transactional Memory: Architectural Support for Lock-Free Data Structures. In ISCA, A. J. Smith (Ed.). ACM, 289–300.

[44]

M. Herlihy and J. M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM TOPLAS, 12, 3 (1990), 463–492.

[45]

R. Jagadeesan, A. Jeffrey, and J. Riely. 2020. Pomsets with preconditions: a simple model of relaxed memory. Proc. ACM Program. Lang., 4, OOPSLA (2020), 194:1–194:30. https://doi.org/10.1145/3428262

Digital Library

[46]

J.-O. Kaiser, H.-H. Dang, D. D., O. Lahav, and V. Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP, P. Müller (Ed.) (LIPIcs, Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 17:1–17:29. isbn:978-3-95977-035-4

[47]

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.

[48]

A. Khyzha and O. Lahav. 2022. Abstraction for Crash-Resilient Objects. In ESOP, Ilya Sergey (Ed.) (Lecture Notes in Computer Science, Vol. 13240). Springer, 262–289. https://doi.org/10.1007/978-3-030-99336-8_10

Digital Library

[49]

M. Kokologiannakis, A. Raad, and V. Vafeiadis. 2019. Model checking for weakly consistent libraries. In PLDI, K. S. McKinley and K. Fisher (Eds.). ACM, 96–110. https://doi.org/10.1145/3314221.3314609

Digital Library

[50]

S. Krishna, M. Emmi, C. Enea, and D. Jovanovic. 2020. Verifying Visibility-Based Weak Consistency. In ESOP, P. Müller (Ed.) (LNCS, Vol. 12075). Springer, 280–307. https://doi.org/10.1007/978-3-030-44914-8_11

Digital Library

[51]

O. Lahav, E. Namakonov, J. Oberhauser, A. Podkopaev, and V. Vafeiadis. 2021. Making weak memory models fair. Proc. ACM Program. Lang., 5, OOPSLA (2021), 1–27. https://doi.org/10.1145/3485475

Digital Library

[52]

O. Lahav and V. Vafeiadis. 2015. Owicki-Gries Reasoning for Weak Memory Models. In ICALP, M. M. Halldórsson, K. Iwama, N. Kobayashi, and B. Speckmann (Eds.) (LNCS, Vol. 9135). Springer, 311–323. isbn:978-3-662-47665-9

[53]

O. Lahav, V. Vafeiadis, J. Kang, C.-K. Hur, and D. Dreyer. 2017. Repairing sequential consistency in C/C++11. In PLDI. ACM, 618–632.

[54]

L. Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers, 28, 9 (1979), 690–691.

Digital Library

[55]

S.-H. Lee, M. Cho, A. Podkopaev, S. Chakraborty, C.-K. Hur, O. Lahav, and V. Vafeiadis. 2020. Promising 2.0: global optimizations in relaxed memory concurrency. In PLDI, A. F. Donaldson and E. Torlak (Eds.). ACM, 362–376. https://doi.org/10.1145/3385412.3386010

Digital Library

[56]

M. Lesani, V. Luchangco, and M. Moir. 2012. Putting Opacity in Its Place. In WTTM.

[57]

M. Lesani, L. Xia, A. Kaseorg, C. J. Bell, A. Chlipala, B. C. Pierce, and S. Zdancewic. 2022. C4: verified transactional objects. Proc. ACM Program. Lang., 6, OOPSLA (2022), 1–31. https://doi.org/10.1145/3527324

Digital Library

[58]

N. A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann. isbn:1-55860-348-4

[59]

R. Margalit and O. Lahav. 2021. Verifying Observational Robustness against a C11-Style Memory Model. Proc. ACM Program. Lang., 5, POPL (2021), Article 4, Jan., 33 pages. https://doi.org/10.1145/3434285

Digital Library

[60]

A. Matveev and N. Shavit. 2015. Reduced Hardware NOrec: A Safe and Scalable Hybrid Transactional Memory. In ASPLOS, Ö. Ö., K. Ebcioglu, and S. Dwarkadas (Eds.). ACM, 59–71. https://doi.org/10.1145/2694344.2694393

Digital Library

[61]

C. C. Minh, J. Chung, C. Kozyrakis, and K. Olukotun. 2008. STAMP: Stanford Transactional Applications for Multi-Processing. In IISWC, D. Christie, A. Lee, O. Mutlu, and B. G. Zorn (Eds.). IEEE Computer Society, 35–46. https://doi.org/10.1109/IISWC.2008.4636089

[62]

S. S. Owicki and D. Gries. 1976. An Axiomatic Proof Technique for Parallel Programs I. Acta Inf., 6 (1976), 319–340.

[63]

M. Paviotti, S. Cooksey, A. Paradis, D. Wright, S. Owens, and M. Batty. 2020. Modular Relaxed Dependencies in Weak Memory Concurrency. In ESOP, P. Müller (Ed.) (LNCS, Vol. 12075). Springer, 599–625. https://doi.org/10.1007/978-3-030-44914-8_22

Digital Library

[64]

A. Podkopaev, I. Sergey, and A. Nanevski. 2016. Operational Aspects of C/C++ Concurrency. CoRR, abs/1606.01400 (2016), arxiv:1606.01400.

[65]

A. Raad, M. Doko, L. Rozic, O. Lahav, and V. 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. https://doi.org/10.1145/3290381

Digital Library

[66]

A. Raad, O. Lahav, and V. Vafeiadis. 2018. On Parallel Snapshot Isolation and Release/Acquire Consistency. In ESOP, A. Ahmed (Ed.) (LNCS, Vol. 10801). Springer, 940–967. https://doi.org/10.1007/978-3-319-89884-1_33

[67]

A. Raad, O. Lahav, and V. Vafeiadis. 2019. On the Semantics of Snapshot Isolation. In VMCAI, C. Enea and R. Piskac (Eds.) (LNCS, Vol. 11388). Springer, 1–23. https://doi.org/10.1007/978-3-030-11245-5_1

[68]

M. Rodriguez and M. F. Spear. 2020. Brief Announcement: On Implementing Software Transactional Memory in the C++ Memory Model. In PODC, Y. Emek and C. Cachin (Eds.). ACM, 224–226. https://doi.org/10.1145/3382734.3405746

Digital Library

[69]

S. Scargall. 2020. Programming Persistent Memory: A Comprehensive Guide for Developers. APress. https://doi.org/10.1007/978-1-4842-4932-1_8

[70]

G. Sela, M. Herlihy, and E. Petrank. 2021. Brief Announcement: Linearizability: A Typo. In PODC, A. Miller, K. Censor-Hillel, and J. H. Korhonen (Eds.). ACM, 561–564. https://doi.org/10.1145/3465084.3467944

Digital Library

[71]

N. Shavit and D. Touitou. 1997. Software Transactional Memory. Distributed Computing, 10, 2 (1997), 99–116.

[72]

M. Spear, H. Boehm, V. Luchangco, M. L. Scott, and M. Wong. 2020. Transactional Memory Lite Support in C++. isocpp.

[73]

A. J. Summers and P. Müller. 2018. Automating Deductive Verification for Weak-Memory Programs. In TACAS, D. Beyer and M. Huisman (Eds.) (LNCS, Vol. 10805). Springer, 190–209. isbn:978-3-319-89959-6

[74]

K. Svendsen, J. Pichon-Pharabod, M. Doko, O. Lahav, and V. Vafeiadis. 2018. A Separation Logic for a Promising Semantics. In ESOP, A. Ahmed (Ed.) (LNCS, Vol. 10801). Springer, 357–384. isbn:978-3-319-89883-4

[75]

J. Tassarotti, D. Dreyer, and V. Vafeiadis. 2015. Verifying read-copy-update in a logic for weak memory. In PLDI, D. Grove and S. Blackburn (Eds.). ACM, 110–120. https://doi.org/10.1145/2737924.2737992

Digital Library

[76]

A. Turon, V. Vafeiadis, and D. Dreyer. 2014. GPS: navigating weak memory with ghosts, protocols, and separation. In OOPSLA, A. P. Black and T. D. Millstein (Eds.). ACM, 691–707. isbn:978-1-4503-2585-1

[77]

V. Vafeiadis and C. Narayan. 2013. Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA. 867–884.

[78]

D. Wright, M. Batty, and B. Dongol. 2021. Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. 13047 (2021), 237–254. https://doi.org/10.1007/978-3-030-90870-6_13

Digital Library

[79]

S. Xiong, A. Cerone, A. Raad, and P. Gardner. 2020. Data Consistency in Transactional Storage Systems: A Centralised Semantics. In ECOOP, R. Hirschfeld and T. Pape (Eds.) (LIPIcs, Vol. 166). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 21:1–21:31. https://doi.org/10.4230/LIPIcs.ECOOP.2020.21

[80]

P. Zardoshti, T. Zhou, P. Balaji, M. L. Scott, and M. F. Spear. 2019. Simplifying Transactional Memory Support in C++. ACM Trans. Archit. Code Optim., 16, 3 (2019), 25:1–25:24. https://doi.org/10.1145/3328796

Digital Library

Cited By

Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Semenyuk MBatty MDongol B(2023)Verifying Read-Copy Update Under RC11Software Engineering and Formal Methods10.1007/978-3-031-47115-5_17(301-319)Online publication date: 6-Nov-2023
https://dl.acm.org/doi/10.1007/978-3-031-47115-5_17

Index Terms

Implementing and verifying release-acquire transactional memory in C11
1. Computing methodologies
  1. Concurrent computing methodologies
2. Theory of computation
  1. Models of computation
    1. Concurrency
  2. Semantics and reasoning

Recommendations

Verifying Read-Copy Update Under RC11
Software Engineering and Formal Methods
Abstract
Read-Copy Update (RCU) is a key lock-free synchronisation mechanism that is used extensively in the Linux kernel. One use of RCU is safe memory reclamation in languages such as C/C++ that do not support garbage collection. Correctness of RCU is, ...
Verifying C11-style weak memory libraries
PPoPP '21: Proceedings of the 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalabiility, we also require modular techniques with verifiable library abstractions. We address this ...
Towards formally specifying and verifying transactional memory
Abstract
Over the last decade, great progress has been made in developing practical transactional memory (TM) implementations, but relatively little attention has been paid to precisely specifying what it means for them to be correct, or formally proving ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 6, Issue OOPSLA2

October 2022

1932 pages

EISSN:2475-1421

DOI:10.1145/3554307

Editor:
Philip Wadler
University of Edinburgh, UK

Issue’s Table of Contents

Copyright © 2022 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: 31 October 2022

Published in PACMPL Volume 6, Issue OOPSLA2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Available / v1.1

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
283
Total Downloads

Downloads (Last 12 months)120
Downloads (Last 6 weeks)18

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Semenyuk MBatty MDongol B(2023)Verifying Read-Copy Update Under RC11Software Engineering and Formal Methods10.1007/978-3-031-47115-5_17(301-319)Online publication date: 6-Nov-2023
https://dl.acm.org/doi/10.1007/978-3-031-47115-5_17

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents