research-article

Open access

Towards understanding the costs of avoiding out-of-thin-air results

Authors:

Brian DemskyAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue OOPSLA

Article No.: 136, Pages 1 - 29

https://doi.org/10.1145/3276506

Published: 24 October 2018 Publication History

Abstract

Eliminating so-called “out-of-thin-air” (OOTA) results is an open problem with many existing programming language memory models including Java, C, and C++. OOTA behaviors are problematic in that they break both formal and informal modular reasoning about program behavior. Defining memory model semantics that are easily understood, allow existing optimizations, and forbid OOTA results remains an open problem. This paper explores two simple solutions to this problem that forbid OOTA results. One solution is targeted towards C/C++-like memory models in which racing operations are explicitly labeled as atomic operations and a second solution is targeted towards Java-like languages in which all memory operations may create OOTA executions. Our solutions provide a per-candidate execution criterion that makes it possible to examine a single execution and determine whether the memory model permits the execution. We implemented and evaluated both solutions in the LLVM compiler framework. Our results show that on an ARMv8 processor the first solution has no overhead on average and a maximum overhead of 6.3% on 43 concurrent data structures, and that the second solution has an average overhead of 3.1% and a maximum overhead of 17.6% on the SPEC CPU2006 C/C++ benchmarks.

Supplementary Material

WEBM File (a136-ou.webm)

Download
96.71 MB

References

[1]

Sarita V. Adve and Mark D. Hill. 1990. Weak Ordering - A New Definition. In Proceedings of the 17th Annual International Symposium on Computer Architecture.

Digital Library

[2]

Jade Alglave, Luc Maranget, Paul E McKenney, Andrea Parri, and Alan Stern. 2018. Frightening Small Children and Disconcerting Grown-ups: Concurrency in the Linux Kernel. In 23rd International Conference on Architectural Support for Programming Languages and Operating Systems.

Digital Library

[3]

Azul. 2017. https://www.azul.com/press_release/falcon- jit- compiler/ .

[4]

Mark Batty, Mike Dodds, and Alexey Gotsman. 2013. Library Abstraction for C/C++ Concurrency. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[5]

Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015a. The Problem of Programming Language Concurrency Semantics. In Proceedings of the 2015 European Symposium on Programming.

[6]

Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015b. The Problem of Programming Language Concurrency Semantics. In Proceedings of the 24th European Symposium on Programming.

[7]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[8]

Pete Becker. 2011. ISO/IEC 14882:2011, Information Technology – Programming Languages – C++.

[9]

Hans Boehm and Brian Demsky. 2014. Outlawing Ghosts: Avoiding Out-of-Thin-Air Results. In Proceedings of the 2014 ACM SIGPLAN Workshop on Memory Systems Performance and Correctness.

Digital Library

[10]

Hans J. Boehm and Sarita V. Adve. 2008. Foundations of the C++ concurrency memory model. In Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[11]

Matko Botinčan, Paola Glavan, and Davor Runje. 2010. Verification of Causality Requirements in Java Memory Model is Undecidable. In Proceedings of the 8th International Conference on Parallel Processing and Applied Mathematics.

Digital Library

[12]

John Cavazos, Grigori Fursin, Felix Agakov, Edwin Bonilla, Michael FP O’Boyle, and Olivier Temam. 2007. Rapidly Selecting Good Compiler Optimizations Using Performance Counters. In Proceedings of the 5th Annual IEEE/ACM International Symposium on Code Generation and Optimization.

Digital Library

[13]

Pietro Cenciarelli, Alexander Knapp, and Eleonora Sibilio. 2007. The Java Memory Model: Operationally, Denotationally, Axiomatically. In Proceedings of the 2007 European Symposium on Programming.

Digital Library

[14]

Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, and Jan Vitek. 2013. Plan B: A Buffered Memory Model for Java. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[15]

Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy. 2018. Bounding data races in space and time. In Proceedings of the 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 242–255.

Digital Library

[16]

Facebook. 2018. https://github.com/facebook/folly .

[17]

John L Henning. 2006. SPEC CP U2006 Benchmark Descriptions. ACM SIGARCH Computer Architecture News 34, 4 (2006), 1–17.

Digital Library

[18]

Radha Jagadeesan, Corin Pitcher, and James Riely. 2010. Generative Operational Semantics for Relaxed Memory Models. In Proceedings of the 2010 European Symposium on Programming.

Digital Library

[19]

Alan Jeffrey and James Riely. 2016. On Thin Air Reads towards an Event Structures Model of Relaxed Memory. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science.

Digital Library

[20]

ISO JTC. 2011. ISO/IEC 9899:2011, Information Technology – Programming Languages – C.

[21]

ISO JTC. 2014. ISO/IEC 14882:2014, Information Technology – Programming Languages – C++.

[22]

Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for RelaxedMemory Concurrency. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[23]

Max Khiszinsky. 2017. https://github.com/khizmax/libcds .

[24]

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2017. Effective Stateless Model Checking for C/C++ Concurrency. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[25]

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing Sequential Consistency in C/C++ 11. In Proceedings of the 2017 ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 618–632.

Digital Library

[26]

Chris Lattner and Vikram Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the International Symposium on Code Generation and Optimization: Feedback-directed and Runtime Optimization.

Digital Library

[27]

Lun Liu, Todd Millstein, and Madanlal Musuvathi. 2017. A Volatile-by-Default JVM for Server Applications. Proceedings of the ACM on Programming Languages 1, OOPSLA (2017), 49.

Digital Library

[28]

Jeremy Manson, William Pugh, and Sarita V. Adve. 2005. The Java Memory Model. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[29]

Luc Maranget, Susmit Sarkar, and Peter Sewell. 2012. A Tutorial Introduction to The ARM and POWER Relaxed Memory Models. http://www.cl.cam.ac.uk/~pes20/ppc- supplemental/test7.pdf .

[30]

Daniel Marino, Abhayendra Singh, Todd Millstein, Madanlal Musuvathi, and Satish Narayanasamy. 2011. A Case for an SC-Preserving Compiler. In Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[31]

Paul E. McKenney, Alan Jeffrey, Ali Sezgin, and Tony Tye. 2016. Out-of-Thin-Air Execution is Vacuous. http://www.open- std. org/jtc1/sc22/wg21/docs/papers/2016/p0422r0.html .

[32]

Yuri Meshman, Noam Rinetzky, and Eran Yahav. 2015. Pattern-based Synthesis of Synchronization for the C++ Memory Model. In Formal Methods in Computer-Aided Design.

Digital Library

[33]

Brian Norris and Brian Demsky. 2013. CDSChecker: Checking Concurrent Data Structures Written with C/C++ Atomics. In Proceeding of the 28th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications.

Digital Library

[34]

Peizhao Ou and Brian Demsky. 2015. AutoMO: Automatic Inference of Memory Order Parameters for C/C++11. In Proceeding of the 30th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications.

Digital Library

[35]

Peizhao Ou and Brian Demsky. 2017. Checking Concurrent Data Structures Under the C/C++11 Memory Model. In Proceedings of the 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming.

Digital Library

[36]

Peizhao Ou and Brian Demsky. 2018. Towards Understanding the Costs of Avoiding Out-of-Thin-Air Results (extended version). http://plrg.eecs.uci.edu/publications/OOTA- Extended- Version.pdf .

[37]

Zhelong Pan and Rudolf Eigenmann. 2006. Fast and Effective Orchestration of Compiler Optimizations for Automatic Performance Tuning. In Proceedings of the 4th Annual IEEE/ACM International Symposium on Code Generation and Optimization.

Digital Library

[38]

Jean Pichon-Pharabod and Peter Sewell. 2016. A Concurrency Semantics for Relaxed Atomics That Permits Optimisation and Avoids Thin-air Executions. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[39]

Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2017. Promising Compilation to ARMv8 POP. In Proceedings of the 31st European Conference on Object-Oriented Programming.

[40]

Jeff Preshing. 2018. https://github.com/preshing/junction .

[41]

Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2018. Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[42]

Erik Rigtorp. 2017a. https://github.com/rigtorp/SPSCQueue .

[43]

Erik Rigtorp. 2017b. https://github.com/rigtorp/MPMCQueue .

[44]

Carl G Ritson and Scott Owens. 2016. Benchmarking Weak Memory Models. In Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming.

Digital Library

[45]

Barry K Rosen, Mark N Wegman, and F Kenneth Zadeck. 1988. Global Value Numbers and Redundant Computations. In Proceedings of the Symposium on Principles of Programming Languages.

Digital Library

[46]

Jaroslav Ševčík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. 2013. CompCertTSO: A Verified Compiler for Relaxed-memory Concurrency. Journal of the ACM (JACM) 60, 3 (2013), 22.

Digital Library

[47]

Aleksey Shipilëv. 2016a. Java Memory Model Pragmatics. https://shipilev.net/blog/2014/jmm- pragmatics/ .

[48]

Aleksey Shipilëv. 2016b. Java Memory Model Pragmatics. https://shipilev.net/ .

[49]

Matthew D Sinclair, Johnathan Alsop, and Sarita V Adve. 2017. Chasing Away RAts: Semantics and Evaluation for Relaxed Atomics on Heterogeneous Systems. In Proceedings of the 44th Annual International Symposium on Computer Architecture.

Digital Library

[50]

Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, and Madanlal Musuvathi. 2012. End-to-end Sequential Consistency. In Proceedings of the 39th Annual International Symposium on Computer Architecture.

Digital Library

[51]

Michael J Sullivan. 2017. Low-level Concurrent Programming Using the Relaxed Memory Calculus. Ph.D. Dissertation. Carnegie Mellon University.

[52]

Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed separation logic: A Program Logic for C11 Concurrency. In Proceeding of the 28th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications.

Digital Library

[53]

Jaroslav Ševčík and David Aspinall. 2008. On Validity of Program Transformations in the Java Memory Model. In Proceedings of the 22th European Conference on Object-Oriented Programming (ECOOP ’08).

Digital Library

[54]

Yang Zhang and Xinyu Feng. 2016. An Operational Happens-before Memory Model. Frontiers of Computer Science 10, 1 (2016), 54–81.

Digital Library

Cited By

Khoury AKaddaha MSaade MYounes ROutbib RLafon P(2023)Challenges and Solutions for Engineering Applications on SmartphonesSoftware10.3390/software20300172:3(350-376)Online publication date: 18-Aug-2023
https://doi.org/10.3390/software2030017
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
Singh ALahav O(2023)An Operational Approach to Library Abstraction under Relaxed Memory ConcurrencyProceedings of the ACM on Programming Languages10.1145/35712467:POPL(1542-1572)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571246
Show More Cited By

Index Terms

Towards understanding the costs of avoiding out-of-thin-air results
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
    2. General programming languages
      1. Language types
        Concurrent programming languages

Recommendations

Dynamic race detection for C++11
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

The intricate rules for memory ordering and synchronisation associated with the C/C++11 memory model mean that data races can be difficult to eliminate from concurrent programs. Dynamic data race analysis can pinpoint races in large and complex ...
Dynamic race detection for C++11
POPL '17

The intricate rules for memory ordering and synchronisation associated with the C/C++11 memory model mean that data races can be difficult to eliminate from concurrent programs. Dynamic data race analysis can pinpoint races in large and complex ...
The Superthreaded Processor Architecture

The common single-threaded execution model limits processors to exploiting only the relatively small amount of instruction-level parallelism available in application programs. The superthreaded processor, on the other hand, is a concurrent multithreaded ...

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 2, Issue OOPSLA

November 2018

1656 pages

EISSN:2475-1421

DOI:10.1145/3288538

Issue’s Table of Contents

Copyright © 2018 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: 24 October 2018

Published in PACMPL Volume 2, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
1,377
Total Downloads

Downloads (Last 12 months)355
Downloads (Last 6 weeks)40

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Khoury AKaddaha MSaade MYounes ROutbib RLafon P(2023)Challenges and Solutions for Engineering Applications on SmartphonesSoftware10.3390/software20300172:3(350-376)Online publication date: 18-Aug-2023
https://doi.org/10.3390/software2030017
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
Singh ALahav O(2023)An Operational Approach to Library Abstraction under Relaxed Memory ConcurrencyProceedings of the ACM on Programming Languages10.1145/35712467:POPL(1542-1572)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571246
Moiseenko EKokologiannakis MVafeiadis V(2022)Model checking for a multi-execution memory modelProceedings of the ACM on Programming Languages10.1145/35633156:OOPSLA2(758-785)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563315
Colvin R(2022)Separation of Concerning Things: A Simpler Basis for Defining and Programming with the C/C++ Memory ModelFormal Methods and Software Engineering10.1007/978-3-031-17244-1_5(71-89)Online publication date: 24-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-17244-1_5
Liu LMillstein TMusuvathi M(2021)Safe-by-default Concurrency for Modern Programming LanguagesACM Transactions on Programming Languages and Systems10.1145/346220643:3(1-50)Online publication date: 3-Sep-2021
https://dl.acm.org/doi/10.1145/3462206
Cho MLee SHur CLahav OFreund SYahav E(2021)Modular data-race-freedom guarantees in the promising semanticsProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454082(867-882)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454082
Luo WDemsky BSherwood TBerger EKozyrakis C(2021)C11Tester: a race detector for C/C++ atomicsProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446711(630-646)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446711
Moiseenko EPodkopaev AKoznov D(2021)A Survey of Programming Language Memory ModelsProgramming and Computer Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
https://doi.org/10.1134/S0361768821060050
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

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