Towards Understanding the Costs of Avoiding Out-of-Thin-Air Results

Eliminating out-of-thin-air (OOTA) behaviors 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 very challenging. We explore two solutions to this problem that forbid OOTA results that enforce slightly stronger memory models. 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. We implement and evaluated both solutions in the LLVM compiler framework.

Getting Started

Our prototype compiler implementation that restricts OOTA behavior can be found here:

http://plrg.eecs.uci.edu/git/?p=oota-llvm.git

Our benchmarks can be accessed through the following links:

http://plrg.eecs.uci.edu/git/?p=folly.git/

http://plrg.eecs.uci.edu/git/?p=junction.git

http://plrg.eecs.uci.edu/git/?p=libcds.git

In case you want to grab a copy of how to build the version of Linux kernel and Ubuntu Filesystem images that we used, here’s a link to the documentation and the copies of images that we used:

http://plrg.eecs.uci.edu/git/?p=FireflyDocs.git

http://plrg.eecs.uci.edu/git/?p=FireflyImages.git

Disclaimer

We make no warranties that the output of our compiler framework is free of errors. You are responsible for assuring the correctness of your software. See the GPL2 license for further disclaimers.

Contact

Please feel free to contact us for more information. Bug reports are welcome, and we are happy to hear from our users.

Contact Peizhao Ou at peizhaoo@uci.edu or Brian Demsky at bdemsky@uci.edu for questions about our compiler framework.

Copyright

CDSChecker is distributed under the GPL v2. See the LICENSE file for details.

Acknowledgments

This material is based upon work supported by the National Science Foundation under Grant CCF-1319786, OAC-1740210 and CNS-1703598.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.