Jung R.,MPI SWS |
Jung R.,Saarland University |
Swasey D.,MPI SWS |
Sieczkowski F.,University of Aarhus |
And 4 more authors.
Conference Record of the Annual ACM Symposium on Principles of Programming Languages | Year: 2015
We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express-and invariants enable us to enforce- user-defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency. Furthermore, through a novel extension of the concept of a view shift, Iris supports the encoding of logically atomic specifications, i.e., Hoare-style specs that permit the client of an operation to treat the operation essentially as if it were atomic, even if it is not. Copyright © 2015 by the Association for Computing Machinery, Inc. (ACM).
Bergstrom L.,Mozilla Research |
Fluet M.,Rochester Institute of Technology |
Le M.,Rochester Institute of Technology |
Reppy J.,University of Chicago |
Sandler N.,University of Chicago
ACM SIGPLAN Notices | Year: 2014
Inlining is an optimization that replaces a call to a function with that function's body. This optimization not only reduces the overhead of a function call, but can expose additional optimization opportunities to the compiler, such as removing redundant operations or unused conditional branches. Another optimization, copy propagation, replaces a redundant copy of a still-live variable with the original. Copy propagation can reduce the total number of live variables, reducing register pressure and memory usage, and possibly eliminating redundant memory-to-memory copies. In practice, both of these optimizations are implemented in nearly every modern compiler. These two optimizations are practical to implement and effective in first-order languages, but in languages with lexically-scoped first-class functions (aka, closures), these optimizations are not available to code programmed in a higher-order style. With higherorder functions, the analysis challenge has been that the environment at the call site must be the same as at the closure capture location, up to the free variables, or the meaning of the program may change. Olin Shivers' 1991 dissertation called this family of optimizations Super-β and he proposed one analysis technique, called reflow, to support these optimizations. Unfortunately, reflow has proven too expensive to implement in practice. Because these higher-order optimizations are not available in functional-language compilers, programmers studiously avoid uses of higher-order values that cannot be optimized (particularly in compiler benchmarks). This paper provides the first practical and effective technique for Super-β (higher-order) inlining and copy propagation, which we call unchanged variable analysis. We show that this technique is practical by implementing it in the context of a real compiler for an ML-family language and showing that the required analyses have costs below 3% of the total compilation time. This technique's effectiveness is shown through a set of benchmarks and example programs, where this analysis exposes additional potential optimization sites. © Copyright 2014 ACM.
St-Amour V.,Northeastern University |
Guo S.-Y.,Mozilla Research
Leibniz International Proceedings in Informatics, LIPIcs | Year: 2015
McCutchan J.,Google |
Feng H.,Intel Corporation |
Matsakis N.D.,Mozilla Research |
Anderson Z.,Google |
Jensen P.,Intel Corporation
WPMVP 2014 - Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Models for SIMD/Vector Processing, Co-located with PPoPP 2014 | Year: 2014
Bocchino R.,Jet Propulsion Laboratory |
Matsakis N.,Mozilla Research |
Taft T.,AdaCore |
Larson B.,Kansas State University |
Seidewitz E.,Model Driven Solutions
HILT 2014 - Proceedings of the ACM Conference on High Integrity Language Technology | Year: 2014
This panel brings together designers of both traditional programming languages, and designers of behavioral specification languages for modeling systems, in each case with a concern for the challenges of multicore programming. Furthermore, several of these efforts have attempted to provide data-race-free programming models, so that multicore programmers need not be faced with the added burden of trying to debug race conditions on top of the existing challenges of building reliable systems. Copyright is held by the owner/author(s).