Polynomial-Time Fence Insertion for Structured Programs

Authors Mohammad Taheri , Arash Pourdamghani , Mohsen Lesani

Thumbnail PDF


  • Filesize: 0.95 MB
  • 17 pages

Document Identifiers

Author Details

Mohammad Taheri
  • Sharif University of Technology, Iran
Arash Pourdamghani
  • Sharif University of Technology, Iran
Mohsen Lesani
  • University of California at Riverside, USA


We appreciate the reviewers of our DISC 2019 submission for constructive comments.

Cite AsGet BibTex

Mohammad Taheri, Arash Pourdamghani, and Mohsen Lesani. Polynomial-Time Fence Insertion for Structured Programs. In 33rd International Symposium on Distributed Computing (DISC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 146, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


To enhance performance, common processors feature relaxed memory models that reorder instructions. However, the correctness of concurrent programs is often dependent on the preservation of the program order of certain instructions. Thus, the instruction set architectures offer memory fences. Using fences is a subtle task with performance and correctness implications: using too few can compromise correctness and using too many can hinder performance. Thus, fence insertion algorithms that given the required program orders can automatically find the optimum fencing can enhance the ease of programming, reliability, and performance of concurrent programs. In this paper, we consider the class of programs with structured branch and loop statements and present a greedy and polynomial-time optimum fence insertion algorithm. The algorithm incrementally reduces fence insertion for a control-flow graph to fence insertion for a set of paths. In addition, we show that the minimum fence insertion problem with multiple types of fence instructions is NP-hard even for straight-line programs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Memory management
  • Software and its engineering → Synchronization
  • Software and its engineering → Concurrent programming structures
  • Fence Insertion
  • Synchronization
  • Concurrent Programming


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Magnus Lång, and Tuan Phong Ngo. Precise and sound automatic fence insertion procedure under PSO. In International Conference on Networked Systems, pages 32-47. Springer, 2015. Google Scholar
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Tuan-Phong Ngo. The best of both worlds: Trading efficiency and optimality in fence insertion for TSO. In European Symposium on Programming Languages and Systems, pages 308-332. Springer, 2015. Google Scholar
  3. Sarita V Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. computer, 29(12):66-76, 1996. Google Scholar
  4. Jade Alglave and Patrick Cousot. Ogre and Pythia: an invariance proof method for weak consistency models. In ACM SIGPLAN NOTICES, volume 52 (1), pages 3-18. ACM, 2017. Google Scholar
  5. Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl. Don't sit on the fence: A static analysis approach to automatic fence insertion. ACM Transactions on Programming Languages and Systems (TOPLAS), 39(2):6, 2017. Google Scholar
  6. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Fences in weak memory models. In International Conference on Computer Aided Verification, pages 258-272. Springer, 2010. Google Scholar
  7. Hagit Attiya, Danny Hendler, and Smadar Levy. An O (1)-barriers optimal RMRs mutual exclusion algorithm. In Proceedings of the 2013 ACM symposium on Principles of distributed computing, pages 220-229. ACM, 2013. Google Scholar
  8. Hagit Attiya, Danny Hendler, and Philipp Woelfel. Trading fences with rmrs and separating memory models. In Proceedings of the 2015 ACM Symposium on Principles of Distributed Computing, pages 173-182. ACM, 2015. Google Scholar
  9. John Bender, Mohsen Lesani, and Jens Palsberg. Declarative Fence Insertion. In OOPSLA, 2015. Google Scholar
  10. Korte Bernhard and J Vygen. Combinatorial optimization: Theory and algorithms. Springer, Third Edition, 2005., 2008. Google Scholar
  11. Karl Crary and Michael J Sullivan. A calculus for relaxed memory. In ACM SIGPLAN Notices, volume 50 (1), pages 623-636. ACM, 2015. Google Scholar
  12. Luke Dalessandro, Michael F Spear, and Michael L Scott. NOrec: streamlining STM by abolishing ownership records. In ACM Sigplan Notices, volume 45 (5), pages 67-78. ACM, 2010. Google Scholar
  13. Andrei Marian Dan, Yuri Meshman, Martin Vechev, and Eran Yahav. Predicate abstraction for relaxed memory models. In International Static Analysis Symposium, pages 84-104. Springer, 2013. Google Scholar
  14. Dave Dice, Ori Shalev, and Nir Shavit. Transactional locking II. In International Symposium on Distributed Computing, pages 194-208. Springer, 2006. Google Scholar
  15. Xing Fang, Jaejin Lee, and Samuel P Midkiff. Automatic fence insertion for shared memory multiprocessing. In Proceedings of the 17th annual international conference on Supercomputing, pages 285-294. ACM, 2003. Google Scholar
  16. Uriel Feige. A threshold of ln n for approximating set cover. Journal of the ACM (JACM), 45(4):634-652, 1998. Google Scholar
  17. Richard M Karp. Reducibility among combinatorial problems. In Complexity of computer computations, pages 85-103. Springer, 1972. Google Scholar
  18. Michael Kuperstein, Martin Vechev, and Eran Yahav. Automatic Inference of Memory Fences. In Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD '10, pages 111-120, Austin, TX, 2010. FMCAD Inc. Google Scholar
  19. Michael Kuperstein, Martin Vechev, and Eran Yahav. Partial-coherence Abstractions for Relaxed Memory Models. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 187-198, New York, NY, USA, 2011. ACM. URL: https://doi.org/10.1145/1993498.1993521.
  20. Michael Kuperstein, Martin Vechev, and Eran Yahav. Automatic inference of memory fences. ACM SIGACT News, 43(2):108-123, 2012. Google Scholar
  21. Jaejin Lee and David A Padua. Hiding relaxed memory consistency with compilers. In Parallel Architectures and Compilation Techniques, 2000. Proceedings. International Conference on, pages 111-122. IEEE, 2000. Google Scholar
  22. Mohsen Lesani. Brief Announcement: Fence Insertion for Straight-line Programs is in P. In Proceedings of the ACM Symposium on Principles of Distributed Computing, pages 97-99. ACM, 2017. Google Scholar
  23. Alexander Linden and Pierre Wolper. A verification-based approach to memory fence insertion in relaxed memory systems. In International SPIN Workshop on Model Checking of Software, pages 144-160. Springer, 2011. Google Scholar
  24. Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin Vechev, and Eran Yahav. Dynamic synthesis for relaxed memory models. ACM SIGPLAN Notices, 47(6):429-440, 2012. Google Scholar
  25. Yuri Meshman, Andrei Dan, Martin Vechev, and Eran Yahav. Synthesis of memory fences via refinement propagation. In International Static Analysis Symposium, pages 237-252. Springer, 2014. Google Scholar
  26. Robin Morisset and Francesco Zappa-Nardelli. Partially redundant fence elimination for x86, ARM, and Power processors. In Proceedings of the 26th International Conference on Compiler Construction, pages 1-10. ACM, 2017. Google Scholar
  27. Susmit Sarkar, Peter Sewell, Francesco Zappa-Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O Myreen, and Jade Alglave. The semantics of x86-CC multiprocessor machine code. ACM SIGPLAN Notices, 44(1):379-391, 2009. Google Scholar
  28. Viktor Vafeiadis and Francesco Zappa-Nardelli. Verifying fence elimination optimisations. In International Static Analysis Symposium, pages 146-162. Springer, 2011. Google Scholar