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

research-article

Open access

Don’t Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion

Authors:

Daniel Kroening,

Daniel PoetzlAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 39, Issue 2

Article No.: 6, Pages 1 - 38

https://doi.org/10.1145/2994593

Published: 29 May 2017 Publication History

Abstract

Modern architectures rely on memory fences to prevent undesired weakenings of memory consistency. As the fences’ semantics may be subtle, the automation of their placement is highly desirable. But precise methods for restoring consistency do not scale to deployed systems’ code. We choose to trade some precision for genuine scalability: our technique is suitable for large code bases. We implement it in our new musketeer tool and report experiments on more than 700 executables from packages found in Debian GNU/Linux 7.1, including memcached with about 10,000 LoC.

References

[1]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. 2013. Memorax, A precise and sound tool for automatic fence insertion under TSO. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13) (LNCS). Springer, 530--536.

Digital Library

[2]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Magnus Lang, and Tuan Phong Ngo. 2015. Precise and sound automatic fence insertion procedure under PSO. In International Conference on Networked Systems (NETYS’15).

[3]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Tuan-Phong Ngo. 2015. The best of both worlds: Trading efficiency and optimality in fence insertion for TSO. In European Symposium on Programming on Programming (ESOP’15). Springer, 308--332.

Digital Library

[4]

Sarita V. Adve and Kourosh Gharachorloo. 1995. Shared memory consistency models: A tutorial. IEEE Comput. 29, 12 (1995), 66--76.

Digital Library

[5]

Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, and Michael Tautschnig. 2011. Soundness of data flow analyses for weak memory models. In Programming Languages and Systems (APLAS’11) (LNCS), Vol. 7078. Springer, 272--288.

Digital Library

[6]

Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. 2013. Software verification for weak memory via program transformation. In European Symposium on Programming (ESOP’13) (LNCS). Springer, 512--532.

Digital Library

[7]

Jade Alglave and Luc Maranget. 2011. Stability in weak memory models. In Computer Aided Verification (CAV’11) (LNCS), Vol. 6806. Springer, 50--66.

Digital Library

[8]

Jade Alglave, Luc Maranget, S. Sarkar, and Peter Sewell. 2010. Fences in weak memory models. In Computer Aided Verification (CAV’10) (LNCS), Vol. 6174. Springer, 258--272.

Digital Library

[9]

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.

Digital Library

[10]

John Bender, Mohsen Lesani, and Jens Palsberg. 2015. Declarative fence insertion. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA’15). ACM, 367--385.

Digital Library

[11]

Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. 2013. Checking and enforcing robustness against TSO. In European Symposium on Programming (ESOP’13) (LNCS), Vol. 7792. Springer, 533--553.

Digital Library

[12]

Ahmed Bouajjani, R. Meyer, and E. Moehlmann. 2011. Deciding robustness against total store ordering. In Automata, Languages and Programming (ICALP’11) (LNCS), Vol. 6756. Springer, 428--440.

Digital Library

[13]

C11. 2011. Information technology -- Programming languages -- C. In BS ISO/IEC 9899:2011.

[14]

David Chase and Yossi Lev. 2005. Dynamic circular work-stealing deque. In Symposium on Parallelism in Algorithms and Architectures (SPAA’05). ACM, 21--28.

Digital Library

[15]

David Detlefs, Christine H. Flood, Alex Garthwaite, Paul A. Martin, Nir Shavit, and Guy L. Steele Jr. 2000. Even better DCAS-based concurrent deques. In Distributed Computing (DISC’00) (LNCS), Vol. 1914. Springer, 59--73.

Digital Library

[16]

David Dice. 2009. A race in LockSuport park() arising from weak memory models. Retrieved from https://blogs.oracle.com/dave/entry/a_race_in_locksupport_park.

[17]

Edsger W. Dijkstra. 1965. Solution of a problem in concurrent programming control. Commun. ACM 8, 9 (1965), 569.

Digital Library

[18]

Xing Fang, Jaejin Lee, and Samuel P. Midkiff. 2003. Automatic fence insertion for shared memory multiprocessing. In International Conference on Supercomputing (ICS’03). ACM, 285--294.

Digital Library

[19]

Matteo Frigo, Charles E. Leiserson, and Keith H. Randall. 1998. The implementation of the Cilk-5 multithreaded language. In Programming Language Design and Implementation (PLDI’98). ACM, 212--223.

Digital Library

[20]

Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan and Kaufmann, Burlington.

Digital Library

[21]

IBM. 2009. Power ISA Version 2.06 Revision B.

[22]

Saurabh Joshi and Daniel Kroening. 2015. Property-driven fence insertion using reorder bounded model checking. In International Symposium on Formal Methods (FM’15). Springer, 291--307.

[23]

Vineet Kahlon, Nishant Sinha, Erik Kruus, and Yun Zhang. 2009. Static data race detection for concurrent programs with asynchronous calls. In International Symposium on the Foundations of Software Engineering (FSE’09). ACM, 13--22.

Digital Library

[24]

Arvind Krishnamurthy and Katherine A. Yelick. 1996. Analyses and optimizations for shared address space programs. J. Par. Dist. Comp. 38, 2 (1996), 130--144.

Digital Library

[25]

Daniel Kroening and Michael Tautschnig. 2014. Automating software analysis at large scale. In Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS’14). Springer, 30--39.

Digital Library

[26]

Michael Kuperstein, Martin T. Vechev, and Eran Yahav. 2010. Automatic inference of memory fences. In Formal Methods in Computer-Aided Design (FMCAD’10). IEEE, 111--119.

Digital Library

[27]

Michael Kuperstein, Martin T. Vechev, and Eran Yahav. 2011. Partial-coherence abstractions for relaxed memory models. In Programming Language Design and Implementation (PLDI’11). 187--198.

Digital Library

[28]

Leslie Lamport. 1979. How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans. Comput. 46, 7 (1979), 690--691.

Digital Library

[29]

Leslie Lamport. 1987. A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5, 1 (1987), 1--11.

Digital Library

[30]

Jaejin Lee and David A. Padua. 2001. Hiding relaxed memory consistency with a compiler. IEEE Trans. Comput. 50 (2001), 824--833.

Digital Library

[31]

Alexander Linden and Pierre Wolper. 2013. A verification-based approach to memory fence insertion in PSO memory systems. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS’13) (LNCS), Vol. 7795. Springer, 339--353.

Digital Library

[32]

Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin T. Vechev, and Eran Yahav. 2012. Dynamic synthesis for relaxed memory models. In Programming Language Design and Implementation (PLDI’12). ACM, 429--440.

Digital Library

[33]

Daniel Lustig, Caroline Trippel, Michael Pellauer, and Margaret Martonosi. 2015. ArMOR: Defending against memory consistency model mismatches in heterogeneous architectures. In International Symposium on Computer Architecture (ISCA’15). ACM, 388--400.

Digital Library

[34]

Daniel Marino, Abhayendra Singh, Todd D. Millstein, Madanlal Musuvathi, and Satish Narayanasamy. 2011. A case for an SC-preserving compiler. In Programming Language Design and Implementation (PLDI’11). ACM, 199--210.

Digital Library

[35]

Yuri Meshman, Andrei Dan, Martin Vechev, and Eran Yahav. 2014. Synthesis of memory fences via refinement propagation. In Static Analysis Symposium (SAS’14). Springer, 237--252.

[36]

Maged M. Michael and Michael L. Scott. 1996. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Symposium on Principles of Distributed Computing (PODC’96). ACM, 267--275.

Digital Library

[37]

Maged M. Michael, Martin T. Vechev, and Vijay A. Saraswat. 2009. Idempotent work stealing. In Principles and Practice of Parallel Programming (PPOPP’09). ACM, 45--54.

Digital Library

[38]

Vincent Nimal. 2015. Static Analyses over Weak Memory. Ph.D. Dissertation. University of Oxford.

[39]

Brian Norris and Brian Demsky. 2013. CDSchecker: Checking concurrent data structures written with C/C++ atomics. In Object Oriented Programming Systems Languages & Applications (OOPSLA’13). 131--150.

Digital Library

[40]

Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A better x86 memory model: x86-TSO. In Theorem Proving in Higher Order Logics (TPHOLs’09) (LNCS), Vol. 5674. Springer, 391--407.

Digital Library

[41]

Gary L. Peterson. 1981. Myths about the mutual exclusion problem. Inf. Process. Lett. 12, 3 (1981), 115--116.

[42]

Dennis Shasha and Marc Snir. 1988. Efficient and correct execution of parallel programs that share memory. TOPLAS 10, 2 (1988), 282--312.

Digital Library

[43]

SPARC. 1994. SPARC Architecture Manual Version 9.

Digital Library

[44]

Michael F. Spear, Maged M. Michael, Michael L. Scott, and Peng Wu. 2009. Reducing memory ordering overheads in software transactional memory. In International Symposium on Code Generation and Optimization (CGO’09). IEEE, 13--24.

Digital Library

[45]

Zehra Sura, Xing Fang, Chi-Leung Wong, Samuel P. Midkiff, Jaejin Lee, and David A. Padua. 2005. Compiler techniques for high performance sequentially consistent Java programs. In Symposium on Principles and Practice of Parallel Programming (PPOPP’05). ACM, 2--13.

Digital Library

[46]

Boleslaw K. Szymanski. 1988. A simple solution to Lamport’s concurrent programming problem with linear wait. In International Conference on Supercomputing (ICS’88). 621--626.

Digital Library

[47]

Robert Tarjan. 1973. Enumeration of the elementary circuits of a directed graph. SIAM J. Comput. 2, 3 (1973), 211--216.

Digital Library

[48]

Viktor Vafeiadis and Francesco Zappa Nardelli. 2011. Verifying fence elimination optimisations. In Static Analysis (SAS’11) (LNCS), Vol. 6887. Springer, 146--162.

Digital Library

[49]

Glynn Winskel. 1986. Event structures. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course. 325--392.

Digital Library

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
Margalit RChristakis MPradel M(2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685549
Huang ZWang CRoychoudhury APaiva AAbreu RStorey M(2024)Constraint Based Program Repair for Persistent Memory BugsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639204(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639204
Show More Cited By

Index Terms

Don’t Sit on the Fence: A Static Analysis Approach to Automatic Fence Insertion
1. Theory of computation
  1. Models of computation
    1. Concurrency
      1. Parallel computing models
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

Declarative fence insertion
OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

Previous work has shown how to insert fences that enforce sequential consistency. However, for many concurrent algorithms, sequential consistency is unnecessarily strong and can lead to high execution overhead. The reason is that, often, correctness ...
Probabilistic Concurrency Testing for Weak Memory Programs
ASPLOS 2023: Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2

The Probabilistic Concurrency Testing (PCT) algorithm that provides theoretical guarantees on the probability of detecting concurrency bugs does not apply to weak memory programs. The PCT algorithm builds on the interleaving semantics of sequential ...
Don't Sit on the Fence
Proceedings of the 16th International Conference on Computer Aided Verification - Volume 8559

Modern architectures rely on memory fences to prevent undesired weakenings of memory consistency. As the fences' semantics may be subtle, the automation of their placement is highly desirable. But precise methods for restoring consistency do not scale ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 39, Issue 2

June 2017

194 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/3062396

Editor:
Andrew Myers
Cornell University, USA

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 May 2017

Accepted: 01 September 2016

Revised: 01 August 2016

Received: 01 June 2015

Published in TOPLAS Volume 39, Issue 2

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

ERC
SRC
EPSRC

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
721
Total Downloads

Downloads (Last 12 months)181
Downloads (Last 6 weeks)17

Reflects downloads up to 09 Jan 2025

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
Margalit RChristakis MPradel M(2024)Robustness against the C/C++11 Memory ModelProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3685549(1881-1885)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3685549
Huang ZWang CRoychoudhury APaiva AAbreu RStorey M(2024)Constraint Based Program Repair for Persistent Memory BugsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639204(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639204
Geeson LSmith L(2024)Compiler Testing with Relaxed Memory Models2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO57630.2024.10444836(334-348)Online publication date: 2-Mar-2024
https://doi.org/10.1109/CGO57630.2024.10444836
He XZhang RTian PZhou LLian MYang C(2024) WOPE: A write-optimized and parallel-efficient B -tree for persistent memory Journal of Systems Architecture10.1016/j.sysarc.2024.103187153(103187)Online publication date: Aug-2024
https://doi.org/10.1016/j.sysarc.2024.103187
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
Gouicem RSprokholt DRuehl JRocha RSpink TChakraborty SBhatotia PAamodt TJerger NSwift M(2023)Risotto: A Dynamic Binary Translator for Weak Memory Model ArchitecturesProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3567955.3567962(107-122)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3567955.3567962
Wijs A(2023)Embedding Formal Verification in Model-Driven Software Engineering with Slco: An OverviewFormal Aspects of Component Software10.1007/978-3-031-52183-6_11(206-227)Online publication date: 26-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-52183-6_11
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
Lustig DCooksey SGiroux OSalapura VZahran MChong FTang L(2022)Mixed-proxy extensions for the NVIDIA PTX memory consistency modelProceedings of the 49th Annual International Symposium on Computer Architecture10.1145/3470496.3533045(1058-1070)Online publication date: 18-Jun-2022
https://dl.acm.org/doi/10.1145/3470496.3533045
Show More Cited By

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