research-article

Open access

Verifying observational robustness against a c11-style memory model

Authors:

Ori LahavAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 4, Pages 1 - 33

https://doi.org/10.1145/3434285

Published: 04 January 2021 Publication History

Abstract

We study the problem of verifying the robustness of concurrent programs against a C11-style memory model that includes relaxed accesses and release/acquire accesses and fences, and show that this verification problem can be reduced to a standard reachability problem under sequential consistency. We further observe that existing robustness notions do not allow the verification of programs that use speculative reads as in the sequence lock mechanism, and introduce a novel "observational robustness" property that fills this gap. In turn, we show how to soundly check for observational robustness. We have implemented our method and applied it to several challenging concurrent algorithms, demonstrating the applicability of our approach. To the best of our knowledge, this is the first method for verifying robustness against a programming language concurrency model that includes relaxed accesses and release/acquire fences.

References

[1]

Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, and Shankaranarayanan Krishna. 2019. Verification of programs under the release-acquire semantics. In PLDI. ACM, New York, NY, USA, 1117-1132. https://doi.org/10.1145/3314221. 3314649

Digital Library

[2]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Magnus Lång, and Tuan Phong Ngo. 2015b. Precise and sound automatic fence insertion procedure under PSO. In NETYS. Springer International Publishing, Cham, 32-47.

[3]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Tuan-Phong Ngo. 2015a. The best of both worlds: Trading eficiency and optimality in fence insertion for TSO. In ESOP. Springer-Verlag New York, Inc., New York, 308-332. https://doi.org/10. 1007/978-3-662-46669-8_13

Digital Library

[4]

Sarita V. Adve and Mark D. Hill. 1990. Weak ordering-a new definition. In ISCA. ACM, New York, 2-14. https://doi.org/10. 1145/325164.325100

Digital Library

[5]

Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl. 2017. Don't sit on the fence: a static analysis approach to automatic fence insertion. ACM Trans. Program. Lang. Syst. 39, 2, Article 6 (May 2017 ), 38 pages. https://doi.org/10.1145/ 2994593

Digital Library

[6]

Jade Alglave and Luc Maranget. 2011. Stability in weak memory models. In CAV. Springer-Verlag, Berlin, Heidelberg, 50-66. http://dl.acm.org/citation.cfm?id= 2032305. 2032311

Digital Library

[7]

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, Article 7 ( July 2014 ), 74 pages. https://doi.org/10.1145/2627752

Digital Library

[8]

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2010. On the verification problem for weak memory models. In POPL. ACM, New York, 7-18. https://doi.org/10.1145/1706299.1706303

Digital Library

[9]

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. 2012. What's decidable about weak memory models?. In ESOP. Springer-Verlag, Berlin, Heidelberg, 26-46. https://doi.org/10.1007/978-3-642-28869-2_2

Digital Library

[10]

Helge Bahmann and Tim Blechmann. 2012. Atomic usage examples. Retrieved june 08, 2020 from https://www.boost.org/ doc/libs/1_55_0/doc/html/atomic/usage_examples.html

[11]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C+ + concurrency. In POPL. ACM, New York, 55-66. https://doi.org/10.1145/1925844.1926394

Digital Library

[12]

Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. 2019a. Checking robustness against snapshot isolation. In Computer Aided Verification. Springer International Publishing, Cham, 286-304.

[13]

Sidi Mohamed Beillahi, Ahmed Bouajjani, and Constantin Enea. 2019b. Robustness against transactional causal consistency. In CONCUR 2019, Vol. 140. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 30 : 1-30 : 18. https: //doi.org/10.4230/LIPIcs.CONCUR. 2019.30

[14]

Giovanni Bernardi and Alexey Gotsman. 2016. Robustness against consistency models with atomic visibility. In CONCUR. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 7 : 1-7 : 15. https://doi.org/10.4230/LIPIcs. CONCUR. 2016.7

[15]

Hans-J. Boehm. 2012. Can Seqlocks get along with programming language memory models?. In MSPC. ACM, New York, 12-20. https://doi.org/10.1145/2247684.2247688

Digital Library

[16]

Hans-J. Boehm and Brian Demsky. 2014. Outlawing ghosts: avoiding out-of-thin-air results. In MSPC. ACM, New York, NY, USA, Article 7, 6 pages. https://doi.org/10.1145/2618128.2618134

Digital Library

[17]

Hans-J Boehm, Olivier Giroux, and Viktor Vafeiades. 2018. P0982R1: Weaken release sequences. http://www.openstd.org/jtc1/sc22/wg21/docs/papers/2018/p0982r1.html. Accessed: 2020-05-27.

[18]

Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. 2013. Checking and enforcing robustness against TSO. In ESOP. Springer-Verlag, Berlin, Heidelberg, 533-553. https://doi.org/10.1007/978-3-642-37036-6_29

Digital Library

[19]

Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, and Serdar Tasiran. 2018. Reasoning about TSO programs using reduction and abstraction. In CAV. Springer, Cham, 336-353.

[20]

Ahmed Bouajjani, Roland Meyer, and Eike Möhlmann. 2011. Deciding robustness against total store ordering. In ICALP. Springer, Berlin, Heidelberg, 428-440.

Digital Library

[21]

Lucas Brutschy, Dimitar Dimitrov, Peter Müller, and Martin Vechev. 2018. Static serializability analysis for causal consistency. In PLDI. ACM, New York, 90-104. https://doi.org/10.1145/3192366.3192415

Digital Library

[22]

Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. 2007. CheckFence: checking consistency of concurrent data types on relaxed memory models. In PLDI. ACM, New York, 12-21. https://doi.org/10.1145/1250734.1250737

Digital Library

[23]

Sebastian Burckhardt and Madanlal Musuvathi. 2008. Efective program verification for relaxed memory models. In CAV. Springer-Verlag, Berlin, Heidelberg, 107-120. https://doi.org/10.1007/978-3-540-70545-1_12

Digital Library

[24]

Jabob Burnim, Koushik Sen, and Christos Stergiou. 2011. Sound and complete monitoring of sequential consistency for relaxed memory models. In TACAS. Springer, Berlin, Heidelberg, 11-25.

[25]

David Chase and Yossi Lev. 2005. Dynamic circular work-stealing deque. In SPAA. ACM, New York, NY, USA, 21-28. https://doi.org/10.1145/1073970.1073974

Digital Library

[26]

Sadegh Dalvandi, Simon Doherty, Brijesh Dongol, and Heike Wehrheim. 2020. Owicki-Gries Reasoning for C11 RAR. In ECOOP, Vol. 166. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 11 : 1-11 : 26. https://doi.org/10. 4230/LIPIcs.ECOOP. 2020.11

[27]

Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2019. RustBelt meets relaxed memory. Proc. ACM Program. Lang. 4, POPL, Article 34 ( Dec. 2019 ), 29 pages. https://doi.org/10.1145/3371102

Digital Library

[28]

Egor Derevenetc. 2015. Robustness against relaxed memory models. Ph.D. Dissertation. University of Kaiserslautern. http://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4074

[29]

Egor Derevenetc and Roland Meyer. 2014. Robustness against Power is PSpace-complete. In ICALP. Springer, Berlin, Heidelberg, 158-170.

[30]

Simon Doherty, Brijesh Dongol, Heike Wehrheim, and John Derrick. 2019. Verifying C11 programs operationally. In PPoPP. ACM, New York, 355-365. https://doi.org/10.1145/3293883.3295702

Digital Library

[31]

Marko Doko and Viktor Vafeiadis. 2017. Tackling real-life relaxed concurrency with FSL++. In ESOP. Springer Berlin Heidelberg, Berlin, Heidelberg, 448-475.

[32]

Alan Fekete, Dimitrios Liarokapis, Elizabeth O'Neil, Patrick O'Neil, and Dennis Shasha. 2005. Making snapshot isolation serializable. ACM Trans. Database Syst. 30, 2 ( June 2005 ), 492-528. https://doi.org/10.1145/1071610.1071615

Digital Library

[33]

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 POPL. ACM, New York, 608-621. https://doi.org/10.1145/2837614.2837615

Digital Library

[34]

Kourosh Gharachorloo, Sarita V. Adve, Anoop Gupta, John L. Hennessy, and Mark D. Hill. 1992. Programming for diferent memory consistency models. J. Parallel and Distrib. Comput. 15, 4 ( 1992 ), 399-407. https://doi.org/10.1016/ 0743-7315 ( 92 ) 90052-O

[35]

Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. 2012. Show no weakness: sequentially consistent specifications of TSO libraries. In DISC. Springer-Verlag, Berlin, Heidelberg, 31-45. https://doi.org/10.1007/978-3-642-33651-5_3

Digital Library

[36]

Gerard J. Holzmann. 1997. The model checker SPIN. IEEE Transactions on software engineering 23, 5 ( 1997 ), 279-295.

Digital Library

[37]

Jeehoon Kang. 2018. Deque proof. Retrieved June 11, 2020 from https://github.com/jeehoonkang/crossbeam-rfcs/blob/dequeproof/text/2018-01-07-deque-proof.md

[38]

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2017. Efective stateless model checking for C/C++ concurrency. Proc. ACM Program. Lang. 2, POPL, Article 17 ( Dec. 2017 ), 32 pages. https://doi.org/10.1145/3158105

Digital Library

[39]

Dexter Kozen. 1977. Lower bounds for natural proof systems. In SFCS. IEEE Computer Society, Washington, 254-266. https://doi.org/10.1109/SFCS. 1977.16

Digital Library

[40]

Ori Lahav and Roy Margalit. 2019. Robustness against release/acquire semantics. In PLDI. ACM, New York, NY, USA, 126-141. https://doi.org/10.1145/3314221.3314604

Digital Library

[41]

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing sequential consistency in C/C++11. In PLDI. ACM, New York, 618-632. https://doi.org/10.1145/3062341.3062352

Digital Library

[42]

Alexander Linden and Pierre Wolper. 2011. A verification-based approach to memory fence insertion in relaxed memory systems. In SPIN. Springer-Verlag, Berlin, Heidelberg, 144-160. http://dl.acm.org/citation.cfm?id= 2032692. 2032707

Digital Library

[43]

Alexander Linden and Pierre Wolper. 2013. A verification-based approach to memory fence insertion in PSO memory systems. In TACAS. Springer-Verlag, Berlin, Heidelberg, 339-353. https://doi.org/10.1007/978-3-642-36742-7_24

Digital Library

[44]

Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin Vechev, and Eran Yahav. 2012. Dynamic synthesis for relaxed memory models. In PLDI. ACM, New York, 429-440. https://doi.org/10.1145/2254064.2254115

Digital Library

[45]

Roy Margalit and Ori Lahav. 2020. Verifying observational robustness against a C11-style memory model. https: //www.cs.tau.ac.il/~orilahav/papers/popl21_robustness_full.pdf (full version of this paper).

[46]

Kartik Nagar and Suresh Jagannathan. 2018. Automated detection of serializability violations under weak consistency. In CONCUR, Vol. 118. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 41 : 1-41 : 18. https: //doi.org/10.4230/LIPIcs.CONCUR. 2018.41

[47]

Scott Owens. 2010. Reasoning about the implementation of concurrency abstractions on x86-TSO. In ECOOP. Springer-Verlag, Berlin, Heidelberg, 478-503.

Digital Library

[48]

Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2019. Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. PACMPL 3, POPL, Article 69 ( Jan. 2019 ), 31 pages. https://doi.org/10.1145/3290382

Digital Library

[49]

Rust. 2020. std::sync::Arc. Retrieved June 11, 2020 from https://doc.rust-lang.org/src/alloc/sync.rs.html# 213-216

[50]

Matthew D. Sinclair, Johnathan Alsop, and Sarita V. Adve. 2017. Chasing away RAts: semantics and evaluation for relaxed atomics on heterogeneous systems. In ISCA. ACM, New York, NY, USA, 161-174. https://doi.org/10.1145/3079856.3080206

Digital Library

[51]

Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed separation logic: A program logic for C11 concurrency. In OOPSLA. ACM, New York, 867-884. https://doi.org/10.1145/2509136.2509532

Digital Library

[52]

Dmitriy V' jukov. 2008. C+ + atomics and memory ordering. Retrieved June 23, 2020 from https://bartoszmilewski.com/ 2008 /12/01/c-atomics-and-memory-ordering/#comment-111

[53]

Dmitriy V' jukov. 2013. Relacy race detector. Retrieved July 06, 2020 from http://www.1024cores.net/home/relacy-racedetector

[54]

Anthony Williams. 2008. Peterson's lock with C++0x atomics. Retrieved October 26, 2018 from https://www. justsoftwaresolutions.co.uk/threading/petersons_lock_with_C+ +0x_atomics.html

[55]

Anthony Williams. 2010. Implementing Dekker's algorithm with fences. Retrieved June 08, 2020 from https://www. justsoftwaresolutions.co.uk/threading/implementing_dekkers_algorithm_with_fences.html

Cited By

Nagar KSahoo AChowdhury RJagannathan S(2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689802
de Vilhena PLahav OVafeiadis VRaad A(2024)Extending the C/C++ Memory Model with Inline AssemblyProceedings of the ACM on Programming Languages10.1145/36897498:OOPSLA2(1081-1107)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689749
Abdulla PAtig MBouajjani AKumar KSaivasan P(2024)Verification under Intel-x86 with PersistencyProceedings of the ACM on Programming Languages10.1145/36564258:PLDI(1189-1212)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656425
Show More Cited By

Index Terms

Verifying observational robustness against a c11-style memory model
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Software verification
2. Theory of computation

Recommendations

Robustness against release/acquire semantics
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

We present an algorithm for automatically checking robustness of concurrent programs against C/C++11 release/acquire semantics, namely verifying that all program behaviors under release/acquire are allowed by sequential consistency. Our approach reduces ...
Robustness against the C/C++11 Memory Model
ISSTA 2024: Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis

Concurrency is extremely useful, however reasoning about the correctness of concurrent programs is more difficult than ever. Sequential consistency (SC) semantics provide the ability to reason about correctness, however these come at a high ...
Verifying read-copy-update in a logic for weak memory
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Read-Copy-Update (RCU) is a technique for letting multiple readers safely access a data structure while a writer concurrently modifies it. It is used heavily in the Linux kernel in situations where fast reads are important and writes are infrequent. ...

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 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 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: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Israel Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
793
Total Downloads

Downloads (Last 12 months)196
Downloads (Last 6 weeks)20

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nagar KSahoo AChowdhury RJagannathan S(2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689802
de Vilhena PLahav OVafeiadis VRaad A(2024)Extending the C/C++ Memory Model with Inline AssemblyProceedings of the ACM on Programming Languages10.1145/36897498:OOPSLA2(1081-1107)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689749
Abdulla PAtig MBouajjani AKumar KSaivasan P(2024)Verification under Intel-x86 with PersistencyProceedings of the ACM on Programming Languages10.1145/36564258:PLDI(1189-1212)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656425
Chakraborty SKrishna SMathur UPavlogiannis A(2024)How Hard Is Weak-Memory Testing?Proceedings of the ACM on Programming Languages10.1145/36329088:POPL(1978-2009)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632908
Lee SCho MMargalit RHur CLahav O(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
https://dl.acm.org/doi/10.1145/3591297
Tunç HAbdulla PChakraborty SKrishna SMathur UPavlogiannis A(2023)Optimal Reads-From Consistency Checking for C11-Style Memory ModelsProceedings of the ACM on Programming Languages10.1145/35912517:PLDI(761-785)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591251
Gao MChakraborty SOzkan BAamodt TJerger NSwift M(2023)Probabilistic Concurrency Testing for Weak Memory ProgramsProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3575693.3575729(603-616)Online publication date: 27-Jan-2023
https://dl.acm.org/doi/10.1145/3575693.3575729
Dalvandi SDongol B(2022)Implementing and verifying release-acquire transactional memory in C11Proceedings of the ACM on Programming Languages10.1145/35633526:OOPSLA2(1817-1844)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563352
Rocha RSprokholt DFink MGouicem RSpink TChakraborty SBhatotia PJhala RDillig I(2022)Lasagne: a static binary translator for weak memory model architecturesProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523719(888-902)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523719
Xiao LZhu HXu QVinh P(2022)Modeling and Verifying PSO Memory Model Using CSPMobile Networks and Applications10.1007/s11036-022-01989-527:5(2068-2083)Online publication date: 1-Oct-2022
https://dl.acm.org/doi/10.1007/s11036-022-01989-5
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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