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

research-article

Partially redundant fence elimination for x86, ARM, and power processors

Authors:

Robin Morisset,

Francesco Zappa NardelliAuthors Info & Claims

CC 2017: Proceedings of the 26th International Conference on Compiler Construction

Pages 1 - 10

https://doi.org/10.1145/3033019.3033021

Published: 05 February 2017 Publication History

Abstract

We show how partial redundancy elimination (PRE) can be instantiated to perform provably correct fence elimination for multi-threaded programs running on top of the x86, ARM and IBM Power relaxed memory models. We have implemented our algorithm in the backends of the <pre>LLVM</pre> compiler infrastructure. The optimisation does not induce an observable overhead at compile-time and can result in up-to 10% speedup on some benchmarks.

References

[1]

C/C++11 mappings to processors. https://www.cl.cam.ac.uk/ ~pes20/cpp/cpp0xmappings.html. Accessed: 2015-10-15.

[2]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. Memorax, a precise and sound tool for automatic fence insertion under TSO. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, pages 530–536, 2013.

Digital Library

[3]

Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl. Don’t sit on the fence - A static analysis approach to automatic fence insertion. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 508–524, 2014.

[4]

Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2):7:1–7:74, July 2014.

Digital Library

[5]

Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. Clarifying and compiling c/c++ concurrency: From c++11 to power. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, pages 509–520, New York, NY, USA, 2012. ACM.

Digital Library

[6]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing c++ concurrency. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’11, pages 55–66, New York, NY, USA, 2011. ACM.

Digital Library

[7]

Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. Checking and enforcing robustness against tso. In Proceedings of the 22Nd European Conference on Programming Languages and Systems, ESOP’13, pages 533–553, Berlin, Heidelberg, 2013. Springer-Verlag.

Digital Library

[8]

Soham Chakraborty and Viktor Vafeiadis. Validating optimizations of concurrent c/c++ programs. In Proceedings of the 2016 International Symposium on Code Generation and Optimization, CGO ’16, pages 216–226, New York, NY, USA, 2016. ACM.

Digital Library

[9]

Reinoud Elhorst. Lowering C11 atomics for ARM in LLVM. Available from http://llvm.org/devmtg/2014-04/PDFs/Talks/ Reinoud-report.pdf, 2014.

[10]

Lester R Ford and Delbert R Fulkerson. Maximal flow through a network. Canadian journal of Mathematics, 8(3):399–404, 1956.

[11]

Andrew V. Goldberg and Robert E. Tarjan. A new approach to the maximum-flow problem. J. ACM, 35(4):921–940, October 1988.

Digital Library

[12]

R Nigel Horspool and HC Ho. Partial redundancy elimination driven by a cost-benefit analysis. In Computer Systems and Software Engineering, 1997., Proceedings of the Eighth Israeli Conference on, pages 111–118, 1997.

Digital Library

[13]

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.

Digital Library

[14]

Chris Lattner and Vikram S. Adve. LLVM: A compilation framework for lifelong program analysis & transformation. In 2nd IEEE / ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA, pages 75–88, 2004.

Digital Library

[15]

Nhat Minh Lˆe. Kahn process networks as concurrent data structures: lock freedom, parallelism, relaxation in shared memory. PhD thesis, École normale supérieure, France, December 2016.

[16]

Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin Vechev, and Eran Yahav. Dynamic synthesis for relaxed memory models. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, pages 429–440, New York, NY, USA, 2012. ACM.

Digital Library

[17]

Robin Morisset, Pankaj Pawan, and Francesco Zappa Nardelli. Compiler testing via a theory of sound optimisations in the C11/C++11 memory model. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, pages 187–196, 2013.

Digital Library

[18]

Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding power multiprocessors. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, pages 175–186, New York, NY, USA, 2011. ACM.

Digital Library

[19]

Bernhard Scholz, R. Nigel Horspool, and Jens Knoop. Optimizing for space and time usage with speculative partial redundancy elimination. In Proceedings of the 2004 ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES’04), Washington, DC, USA, June 11-13, 2004, pages 221–230, 2004.

Digital Library

[20]

Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. X86-tso: A rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7):89–97, July 2010.

Digital Library

[21]

Zehra Sura, Xing Fang, Chi-Leung Wong, Samuel P. Midkiff, Jaejin Lee, and David Padua. Compiler techniques for high performance sequentially consistent java programs. In Proceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’05, pages 2–13, New York, NY, USA, 2005. ACM.

Digital Library

[22]

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 209–220, 2015.

Digital Library

[23]

Viktor Vafeiadis and Francesco Zappa Nardelli. Verifying fence elimination optimisations. In Static Analysis - 18th International Symposium, SAS 2011, Venice, Italy, September 14-16, 2011. Proceedings, pages 146–162, 2011.

Digital Library

[24]

Jaroslav ˇSevˇc´ık. Safe optimisations for shared-memory concurrent programs. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, pages 306–316, New York, NY, USA, 2011. ACM.

Digital Library

[25]

Jingling Xue and Jens Knoop. A fresh look at PRE as a maximum flow problem. In Compiler Construction, 15th International Conference, CC 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 30-31, 2006, Proceedings, pages 139–154, 2006.

Digital Library

Cited By

Gao CMeng XLi WLai JZhang YRen FBagchi SZhang Y(2024)CrossMappingProceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference10.5555/3691992.3692054(1013-1028)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.5555/3691992.3692054
Ramanathan NConstantinides GWickerson J(2021)Global Analysis of C Concurrency in High-Level SynthesisIEEE Transactions on Very Large Scale Integration (VLSI) Systems10.1109/TVLSI.2020.302611229:1(24-37)Online publication date: Jan-2021
https://doi.org/10.1109/TVLSI.2020.3026112
Liu NZang BChen HGupta RShen X(2020)No barrier in the roadProceedings of the 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/3332466.3374535(348-361)Online publication date: 19-Feb-2020
https://dl.acm.org/doi/10.1145/3332466.3374535
Show More Cited By

Index Terms

Partially redundant fence elimination for x86, ARM, and power processors

Recommendations

Exploiting SIMD Asymmetry in ARM-to-x86 Dynamic Binary Translation

Single instruction multiple data (SIMD) has been adopted for decades because of its superior performance and power efficiency. The SIMD capability (i.e., width, number of registers, and advanced instructions) has diverged rapidly on different SIMD ...
Doubling the number of registers on ARM processors
INTERACT '12: Proceedings of the 2012 16th Workshop on Interaction between Compilers and Computer Architectures (INTERACT)

It is critical that more architectural registers are available to the compiler and programmer, as a small number of architectural registers might hinder the compiler and programmer from producing efficient code. Although modern chip manufacturing ...
Retargetable pipeline hazard detection for partially bypassed processors

Register bypassing is a widely used feature in modern processors to eliminate certain data hazards. Although complete bypassing is ideal for performance, it has significant impact on the cycle time, area, and power consumption of the processor. Owing to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

CC 2017: Proceedings of the 26th International Conference on Compiler Construction

February 2017

141 pages

ISBN:9781450352338

DOI:10.1145/3033019

General Chair:
Peng Wu
Huawei, USA
,
Program Chair:
Sebastian Hack
Saarland University, Germany

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part 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 components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 February 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Google

Conference

CC '17

CC '17: Compiler Construction

February 5 - 6, 2017

TX, Austin, USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
196
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gao CMeng XLi WLai JZhang YRen FBagchi SZhang Y(2024)CrossMappingProceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference10.5555/3691992.3692054(1013-1028)Online publication date: 10-Jul-2024
https://dl.acm.org/doi/10.5555/3691992.3692054
Ramanathan NConstantinides GWickerson J(2021)Global Analysis of C Concurrency in High-Level SynthesisIEEE Transactions on Very Large Scale Integration (VLSI) Systems10.1109/TVLSI.2020.302611229:1(24-37)Online publication date: Jan-2021
https://doi.org/10.1109/TVLSI.2020.3026112
Liu NZang BChen HGupta RShen X(2020)No barrier in the roadProceedings of the 25th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/3332466.3374535(348-361)Online publication date: 19-Feb-2020
https://dl.acm.org/doi/10.1145/3332466.3374535
Ramanathan NConstantinides GWickerson J(2018)Concurrency-Aware Thread Scheduling for High-Level Synthesis2018 IEEE 26th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM)10.1109/FCCM.2018.00025(101-108)Online publication date: Apr-2018
https://doi.org/10.1109/FCCM.2018.00025

View Options

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents