A type- and control-flow analysis is a program analysis that yields both type-flow information, approximating the types that may instantiate type variables, and control-flow information, approximating the values (especially lambda- and Lambda-expressions) that may be bound to variables. Moreover, each of the flows informs the other; control-flow establishes the types that may instantiate Lambda-bound type variables by determining the Lambda-expressions that flow to a type-application expression, while type-flow filters control-flow by rejecting the flow of values having static types that are incompatible (according to the type-flow information) with the static type of the receiving variable. In previous work [1,13,14], we introduced a (monovariant) type- and control-flow analysis for System F (with recursion). While System F has an expressive type system and has served as a useful core calculus in which to express interesting language features, it only allows abstraction over types and does not allow abstraction over type constructors. Increasingly, researchers are looking at System F-omega, with both term- and type-level abstraction over types of arbitrary kind, as a core calculus in which to explore advanced language features. Hence, we are motivated to define a type- and control-flow analysis for System F-omega that is able to analyze the rich structure of System F-omega types. In this work, we present a preliminary type- and control-flow analysis for System F-omega (with recursion). As in previous work, we give both a specification-based formulation of the analysis, used to prove soundness of the analysis, and a flow-graph-based formulation, used to guide the implementation of an algorithm. While the macro structure of the development for System F-omega follows that for System F, moving to System F-omega introduces subtle challenges that have left some unanswered questions about the meta-theory. In particular, the decidability of type compatibility defined in terms of System F-omega's definitional type equivalence remains an open question. In order to be computable, our flow-graph-based formulation uses a restricted form of definitional type equivalence and performs a 0CFA at the type-level, yielding an analysis result that is less precise than the "best" (but as of yet, uncomputable) analysis result accepted by the specification-based formulation. Our soundness results have been formalized in the Coq proof assistant. This work is based in part on the first author's MS thesis [53].

Since its inception in 1972, the C programming language has employed a design philosophy that gives developers free reign and fine-grained control. Unfortunately, despite multiple generations of new engineers, C projects still suffer from chronic human errors that lead to vulnerabilities. Newer languages like Rust have taken a different approach with the stated goal of mitigating these errors via enforcing types and borrow checking at compile-time. These guarantees are promising, and indeed much work is being committed to "translating" C to Rust. But how much of an impact would Rust have had? The goal of this work is to inform the discussion around secure programming language designs by historically analyzing vulnerabilities in C with respect to Rust. We made a comprehensive mapping of the entire Common Weakness Enumeration vulnerability taxonomy to those that Rust would (and would not) be able to mitigate. We identified 68 prominent open source projects with C code, collected their vulnerability history data, and used their CWE designations to explore a best-case speculation on how many vulnerabilities might have been prevented with Rust. We estimate that 58.2% of historical vulnerabilities in our selection of open source C projects would have been virtually impossible in Rust. Depending on one’s expectations, this number might be surprisingly high or surprisingly low, so we hope this study will help ground the discussion about the decision for C projects to "oxidize."

A type- and control-flow analysis is a program analysis that yields both type-flow information, approximating the types that may instantiate type variables, and control-flow information, approximating the values (especially λ - and -expressions) that may be bound to variables. Moreover, each of the flows informs the other; control-flow establishes the types that may instantiate -bound type variables by determining the -expressions that flow to a type-application expression, while type-flow filters control-flow by rejecting the flow of values having static types that are incompatible (according to the type-flow information) with the static type of the receiving variable. In previous work [1, 13, 14], we introduced a (monovariant) type- and control-flow analysis for System F (with recursion). While System F has an expressive type system and has served as a useful core calculus in which to express interesting language features, it only allows abstraction over types and does not allow abstraction over type constructors. Increasingly, researchers are looking at System F _ω , with both term- and type-level abstraction over types of arbitrary kind, as a core calculus in which to explore advanced language features. Hence, we are motivated to define a type- and control-flow analysis for System F _ω that is able to analyze the rich structure of System F _ω types. In this work, we present a preliminary type- and control-flow analysis for System F _ω (with recursion). As in previous work, we give both a specification-based formulation of the analysis, used to prove soundness of the analysis, and a flow-graph-based formulation, used to guide the implementation of an algorithm. While the macro structure of the development for System F _ω follows that for System F, moving to System F _ω introduces subtle challenges that have left some unanswered questions about the meta-theory. In particular, the decidability of type compatibility defined in terms of System F _ω ’s definitional type equivalence remains an open question. In order to be computable, our flow-graph-based formulation uses a restricted form of definitional type equivalence and performs a 0CFA at the type-level, yielding an analysis result that is less precise than the “best” (but as of yet, uncomputable) analysis result accepted by the specification-based formulation. Our soundness results have been formalized in the Coq proof assistant. This work is based in part on the first author’s MS thesis [53].

On any modern computer architecture today, parallelism comes with a modest cost, born from the creation and management of threads or tasks. Today, programmers battle this cost by manually optimizing/tuning their codes to minimize the cost of parallelism without harming its benefit, performance. This is a difficult battle: programmers must reason about architectural constant factors hidden behind layers of software abstractions, including thread schedulers and memory managers, and their impact on performance, also at scale. In languages that support higher-order functions, the battle hardens: higher order functions can make it difficult, if not impossible, to reason about the cost and benefits of parallelism. Motivated by these challenges and the numerous advantages of high-level languages, we believe that it has become essential to manage parallelism automatically so as to minimize its cost and maximize its benefit. This is a challenging problem, even when considered on a case-by-case, application-specific basis. But if a solution were possible, then it could combine the many correctness benefits of high-level languages with performance by managing parallelism without the programmer effort needed to ensure performance. This paper proposes techniques for such automatic management of parallelism by combining static (compilation) and run-time techniques. Specifically, we consider the Parallel ML language with task parallelism, and describe a compiler pipeline that embeds "potential parallelism" directly into the call-stack and avoids the cost of task creation by default. We then pair this compilation pipeline with a run-time system that dynamically converts potential parallelism into actual parallel tasks. Together, the compiler and run-time system guarantee that the cost of parallelism remains low without losing its benefit. We prove that our techniques have no asymptotic impact on the work and span of parallel programs and thus preserve their asymptotic properties. We implement the proposed techniques by extending the MPL compiler for Parallel ML and show that it can eliminate the burden of manual optimization while delivering good practical performance.

Defunctionalization is a program transformation that removes all first-class functions from a source program, yielding an equivalent target program that contains only first-order functions. As originally described by Reynolds, defunctionalization transforms an untyped higher-order source program into an untyped first-order target program that uses a single, global dispatch function. In addition to being limited to untyped languages, a drawback of this approach is that obscures control flow, making it appear as though the code associated with every source function could be invoked at every call site of the target program. Subsequent work has extended defunctionalization to both simply-typed and polymorphically-typed languages, but the latter continues to use a single, global dispatch function. Other work has extended defunctionalization to be guided by a control-flow analysis of a simply-typed source program, where the types of the target program exactly capture the results of the flow analysis and make it apparent which (limited) set of functions can be invoked at each call site. Our work draws inspiration from these previous approaches and proposes a novel flow-directed defunctionalization for a polymorphically-typed source language. Guided by a type- and control-flow analysis, which exploits well-typedness of the source program to filter flows that are incompatible with static types, the transformation must construct evidence that filtered flows are impossible in order to ensure the well-typedness of the target program.

Nested parallelism has proved to be a popular approach for programming the rapidly expanding range of multicore computers. It allows programmers to express parallelism at a high level and relies on a run-time system and a scheduler to deliver efficiency and scalability. As a result, many programming languages and extensions that support nested parallelism have been developed, including in C/C++, Java, Haskell, and ML. Yet, writing efficient and scalable nested parallel programs remains challenging, primarily due to difficult concurrency bugs arising from destructive updates or effects. For decades, researchers have argued that functional programming can simplify writing parallel programs by allowing more control over effects but functional programs continue to underperform in comparison to parallel programs written in lower-level languages. The fundamental difficulty with functional languages is that they have high demand for memory, and this demand only grows with parallelism. In this paper, we identify a memory property, called disentanglement, of nested-parallel programs, and propose memory management techniques for improved efficiency and scalability. Disentanglement allows for (destructive) effects as long as concurrently executing threads do not gain knowledge of the memory objects allocated by each other. We formally define disentanglement by considering an ML-like higher-order language with mutable references and presenting a dynamic semantics for it that enables reasoning about computation graphs of nested parallel programs. Based on this graph semantics, we formalize a classic correctness property---determinacy race freedom---and prove that it implies disentanglement. This establishes that disentanglement applies to a relatively broad class of parallel programs. We then propose memory management techniques for nested-parallel programs that take advantage of disentanglement for improved efficiency and scalability. We show that these techniques are practical by extending the MLton compiler for Standard ML to support this form of nested parallelism. Our empirical evaluation shows that our techniques are efficient and scale well.

It is well known that modern functional programming languages are naturally amenable to parallel programming. Achieving efficient parallelism using functional languages, however, remains difficult. Perhaps the most important reason for this is their lack of support for efficient in-place updates, i.e., mutation, which is important for the implementation of both parallel algorithms and the run-time system services (e.g., schedulers and synchronization primitives) used to execute them. In this paper, we propose techniques for efficient mutation in parallel functional languages. To this end, we couple the memory manager with the thread scheduler to make reading and updating data allocated by nested threads efficient. We describe the key algorithms behind our technique, implement them in the MLton Standard ML compiler, and present an empirical evaluation. Our experiments show that the approach performs well, significantly improving efficiency over existing functional language implementations.

Software Transactional Memory (STM) has become very popular in Haskell. Currently, there are nearly 500 packages on Haskell’s package archive that directly use STM. Despite the widespread use in real world applications, Haskell’s STM implementation has seen very few updates since its introduction in 2005. In this work, we describe our efforts to redesign the STM implementation in the Glasgow Haskell Compiler (GHC), based on a TL2-like implementation that is able to support both orElse and retry without the use of traditional nested transactions. We argue that our implementation is simpler than the current GHC implementation while supporting opacity. We also demonstrate that our implementation performs better than the current GHC implementation on a number of benchmarks by multiple orders of magnitude for long-running transactions. In an effort to measure the performance of orElse and retry, we present an STM-based work stealing scheduler. With orElse and retry, we are able to elegantly implement the scheduler in just a few lines of code. We have modified the Par Monad, a realworld Haskell package that provides deterministic parallelism, to use our STM-based work stealing scheduler and show that it is not only simpler but is able to perform as well as the current scheduler.

Transactional events are a recent concurrency abstraction that combines first-class synchronous message-passing events with allor-nothing transactions. Transactional events provide both a sequencing combinator, which permits the description of behaviors in which multiple potential synchronization actions (including communications between threads) either all occur in sequence or none of them occur, and a nondeterministic choice combinator, which permits the description of behaviors in which exactly one of a set of potential synchronization actions occurs. While prior work gave a semantics and an implementation for transactional events, it provided no guarantees about which of the many non-deterministic executions might be exhibited by a program. For concurrent systems, like transactional events, it is natural to expect certain fairness conditions to hold on executions. Intuitively, fairness guarantees that any system component that could (sufficiently often) make progress does, in fact, make progress. In this work, we investigate fairness for transactional events. We give a rigorous definition of fair program executions in transactional events, describe a refined operational semantics that guarantees fair executions, and discuss restrictions and assumptions necessary for the correctness of an implementation based on the refined semantics. This is a companion technical report, providing additional commentary and proof details, to a paper [1] appearing in Implementation and Application of Functional Languages: 23rd International Symposium (IFL’11).

We articulate the need for managing (data) locality automatically rather than leaving it to the programmer, especially in parallel programming systems. To this end, we propose techniques for coupling tightly the computation (including the thread scheduler) and the memory manager so that data and computation can be positioned closely in hardware. Such tight coupling of computation and memory management is in sharp contrast with the prevailing practice of considering each in isolation. For example, memory-management techniques usually abstract the computation as an unknown "mutator", which is treated as a "black box". As an example of the approach, in this paper we consider a specific class of parallel computations, nested-parallel computations. Such computations dynamically create a nesting of parallel tasks. We propose a method for organizing memory as a tree of heaps reflecting the structure of the nesting. More specifically, our approach creates a heap for a task if it is separately scheduled on a processor. This allows us to couple garbage collection with the structure of the computation and the way in which it is dynamically scheduled on the processors. This coupling enables taking advantage of locality in the program by mapping it to the locality of the hardware. For example for improved locality a heap can be garbage collected immediately after its task finishes when the heap contents is likely in cache.

Software transactional memory (STM) has proven to be a useful abstraction for developing concurrent applications, where programmers denote transactions with an atomic construct that delimits a collection of reads and writes to shared mutable references. The runtime system then guarantees that all transactions are observed to execute atomically with respect to each other. Traditionally, when the runtime system detects that one transaction conflicts with another, it aborts one of the transactions and restarts its execution from the beginning. This can lead to problems with both execution time and throughput. In this paper, we present a novel approach that uses first-class continuations to restart a conflicting transaction at the point of a conflict, avoiding the re-execution of any work from the beginning of the transaction that has not been compromised. In practice, this allows transactions to complete more quickly, decreasing execution time and increasing throughput. We have implemented this idea in the context of the Manticore project, an ML-family language with support for parallelism and concurrency. Crucially, we rely on constant-time continuation capturing via a continuation-passing-style (CPS) transformation and heap-allocated continuations. When comparing our STM that performs partial aborts against one that performs full aborts, we achieve a decrease in execution time of up to 31% and an increase in throughput of up to 351%.

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 higher-order 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.

At IFL'12, we presented a novel monovariant flow analysis for System F (with recursion) that yields both type-flow and control-flow information. [5] The type-flow information approximates the type expressions that may instantiate type variables and the control-flow information approximates the λ- and Λ-expressions that may be bound to variables. Furthermore, the two flows are mutually beneficial: control flow determines which Λ-expressions may be applied to which type expressions (and, hence, which type expressions may instantiate which type variables), while type flow filters the λ- and Λ-expressions that may be bound to variables (by rejecting expressions with static types that are incompatible with the static type of the variable under the type flow). Using a specification-based formulation of the type- and control-flow analysis, we proved the analysis to be sound, decidable, and computable. Unfortunately, naïvely implementing the analysis using a standard least fixed-point iteration yields an O(n13) algorithm. In this work, we give an alternative flow-graph-based formulation of the type- and control-flow analysis. We prove that the flow-graph-based formulation induces solutions satisfying the specification-based formulation and, hence, that the flow-graph-based formulation of the analysis is sound. We give a direct algorithm implementing the flow-graph-based formulation and demonstrate that it is O(n4). By distinguishing the size l of expressions in the program from the size m of types in the program and performing an amortized complexity analysis, we further demonstrate that the algorithm is O(l3 + m4).

Purely functional programming languages have proven to be an attractive option for implementing parallel applications. The absence of mutable state eliminates the possibility for race conditions, which relieves programmers from reasoning about the exponential interleavings of threads and nondeterministic behavior. Unfortunately, there are applications that, by making use of shared state, can achieve significant constant factor speedups compared to their purely functional counterparts. IVars have been proposed as a possible solution, allowing threads to share information via write-once references, while preserving a deterministic semantics. However, in the presence of speculative parallelism (cancelation), this determinism guarantee is lost. In this work we show how to go about combining these two features by proposing a dynamic rollback mechanism for enforcing determinism. We have formalized the semantics of a parallel functional language extended with IVars, speculative parallelism, and our proposed rollback mechanism using the Coq proof assistant and have proven that it preserves determinism. Additionally, we describe a preliminary implementation in the context of the Manticore project and give some initial performance results.

A long-standing practical challenge in the optimization of higher-order languages is inlining functions with free variables. Inlining code statically at a function call site is safe if the compiler can guarantee that the free variables have the same bindings at the inlining point as they do at the point where the function is bound as a closure (code and free variables). There have been many attempts to create a heuristic to check this correctness condition, from Shivers' kCFA-based reflow analysis to Might's Delta-CFA and anodization, but all of those have performance unsuitable for practical compiler implementations. In practice, modern language implementations rely on a series of tricks to capture some common cases (e.g., closures whose free variables are only top-level identifiers such as +) and rely on hand-inlining by the programmer for anything more complicated. This work provides the first practical, general approach for inlining functions with free variables. We also provide a proof of correctness, an evaluation of both the execution time and performance impact of this optimization, and some tips and tricks for implementing an efficient and precise control-flow analysis.

Data parallelism has proven to be an effective technique for high-level programming of a certain class of parallel applications, but it is not well suited to irregular parallel computations. Blelloch and others proposed nested data parallelism (NDP) as a language mechanism for programming irregular parallel applications in a declarative data-parallel style. The key to this approach is a compiler transformation that flattens the NDP computation and data structures into a form that can be executed efficiently on a wide-vector SIMD architecture. Unfortunately, this technique is ill suited to execution on today's multicore machines. We present a new technique, called data-only flattening , for the compilation of NDP, which is suitable for multicore architectures. Data-only flattening transforms nested data structures in order to expose programs to various optimizations while leaving control structures intact. We present a formal semantics of data-only flattening in a core language with a rewriting system. We demonstrate the effectiveness of this technique in the Parallel ML implementation and we report encouraging experimental results across various benchmark applications.

We present a monovariant flow analysis for System F (with recursion). The flow analysis yields both control-flow information, approximating the λ - and -expressions that may be bound to variables, and type-flow information, approximating the type expressions that may instantiate type variables. Moreover, the two flows are mutually beneficial: the control flow determines which -expressions may be applied to which type expressions (and, hence, which type expressions may instantiate which type variables), while the type flow filters the λ - and -expressions that may be bound to variables (by rejecting expressions with static types that are incompatible with the static type of the variable under the type flow). As is typical for a monovariant control-flow analysis, control-flow information is expressed as an abstract environment mapping variables to sets of (syntactic) λ - and -expressions that occur in the program under analysis. Similarly, type-flow information is expressed as an abstract environment mapping type variables to sets of (syntactic) types that occur in the program under analysis. Compatibility of static types (with free type variables) under a type flow is decided by interpreting the abstract environment as productions for a regular-tree grammar and querying if the languages generated by taking the types in question as starting terms have a non-empty intersection.

We present a monovariant flow analysis for System F (with recursion). The flow analysis yields both control-flow information, approximating the λand Λ-expressions that may be bound to variables, and type-flow information, approximating the type expressions that may instantiate type variables. Moreover, the two flows are mutually beneficial: the control flow determines which Λ-expressions may be applied to which type expressions (and, hence, which type expressions may instantiate which type variables), while the type flow filters the λand Λ-expressions that may be bound to variables (by rejecting expressions with static types that are incompatible with the static type of the variable under the type flow). As is typical for a monovariant control-flow analysis, control-flow information is expressed as an abstract environment mapping variables to sets of (syntactic) λand Λ-expressions that occur in the program under analysis. Similarly, type-flow information is expressed as an abstract environment mapping type variables to sets of (syntactic) types that occur in the program under analysis. Compatibility of static types (with free type variables) under a type flow is decided by interpreting the abstract environment as productions for a regular-tree grammar and querying if the languages generated by taking the types in question as starting terms have a non-empty intersection. This is a companion technical report, providing additional commentary and proof details, to a paper [11] appearing in Implementation and Application of Functional Languages: 24th International Symposium (IFL’12).