Proc. ACM Program. Lang., vol. 4, issue ICFP: "A Unified View of Modalities ..."
A Unified View of Modalities in Type Systems
Andreas Abel and Jean-Philippe Bernardy
(University of Gothenburg, Sweden)
We propose to unify the treatment of a broad range of modalities in typed lambda calculi. We do so by defining a generic structure of modalities, and show that this structure arises naturally from the structure of intuitionistic logic, and as such finds instances in a wide range of type systems previously described in literature. Despite this generality, this structure has a rich metatheory, which we expose.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Parsing with Zippers (Functional ..."
Parsing with Zippers (Functional Pearl)
Pierce Darragh and Michael D. Adams
(University of Utah, USA; University of Michigan, USA)
Parsing with Derivatives (PwD) is an elegant approach to parsing context-free grammars (CFGs). It takes the equational theory behind Brzozowski's derivative for regular expressions and augments that theory with laziness, memoization, and fixed points. The result is a simple parser for arbitrary CFGs. Although recent work improved the performance of PwD, it remains inefficient due to the algorithm repeatedly traversing some parts of the grammar.
In this functional pearl, we show how to avoid this inefficiency by suspending the state of the traversal in a zipper. When subsequent derivatives are taken, we can resume the traversal from where we left off without retraversing already traversed parts of the grammar.
However, the original zipper is designed for use with trees, and we want to parse CFGs. CFGs can include shared regions, cycles, and choices between alternates, which makes them incompatible with the traditional tree model for zippers. This paper develops a generalization of zippers to properly handle these additional features. Just as PwD generalized Brzozowski's derivatives from regular expressions to CFGs, we generalize Huet's zippers from trees to CFGs.
Abstract The resulting parsing algorithm is concise and efficient: it takes only 31 lines of OCaml code to implement the derivative function but performs 6,500 times faster than the original PwD and 3.24 times faster than the optimized implementation of PwD.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "SteelCore: An Extensible Concurrent ..."
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez
(Microsoft Research, USA; Microsoft Research, India; Carnegie Mellon University, USA; Inria, France; University of Ljubljana, Slovenia; CIFASIS-CONICET, Argentina)
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself.
Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F⋆ proof assistant in a manner that enables dependently typed, effectful F⋆ programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions.
Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Kinds Are Calling Conventions ..."
Kinds Are Calling Conventions
Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg
(University of Oregon, USA; Microsoft Research, UK; Bryn Mawr College, USA; Tweag I/O, USA)
A language supporting polymorphism is a boon to programmers: they can express complex ideas once and reuse functions in a variety of situations. However, polymorphism is pain for compilers tasked with producing efficient code that manipulates concrete values.
This paper presents a new intermediate language that allows for efficient static compilation, while still supporting flexible polymorphism. Specifically, it permits polymorphism over not only the types of values, but also the representation of values, the arity of primitive machine functions, and the evaluation order of arguments---all three of which are useful in practice. The key insight is to encode information about a value's calling convention in the kind of its type, rather than in the type itself.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "A Unified View of Modalities ..."
A Unified View of Modalities in Type Systems
Andreas Abel and Jean-Philippe Bernardy
(University of Gothenburg, Sweden)
We propose to unify the treatment of a broad range of modalities in typed lambda calculi. We do so by defining a generic structure of modalities, and show that this structure arises naturally from the structure of intuitionistic logic, and as such finds instances in a wide range of type systems previously described in literature. Despite this generality, this structure has a rich metatheory, which we expose.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Scala Step-by-Step: Soundness ..."
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers
(Delft University of Technology, Netherlands; IRIF, France; University of Paris, France; CNRS, France; Aarhus University, Denmark)
The metatheory of Scala’s core type system—the Dependent Object Types (DOT) calculus—is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and in practice. To address some of these problems, we use a semantics-first approach to develop a logical relations model for a new version of DOT, called guarded DOT (gDOT). Our logical relations model makes use of an abstract form of step-indexing, as supported by the Iris framework, to model various forms of recursion in gDOT. To demonstrate the expressiveness of gDOT, we show that it handles Scala examples that could not be handled by previous versions of DOT, and prove using our logical relations model that gDOT provides the desired data abstraction. The gDOT type system, its semantic model, its soundness proofs, and all examples in the paper have been mechanized in Coq.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Compiling Effect Handlers ..."
Compiling Effect Handlers in Capability-Passing Style
Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann
(University of Tübingen, Germany)
Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper, we aim to achieve abstraction without regret for effect handlers.
We present a language for effect handlers in _capability-passing style_ (λCap) and an implementation of this language as a translation to simply-typed lambda calculus in _iterated continuation-passing style_. A suite of benchmarks indicates that the novel combination of capability-passing style and iterated CPS enables significant speedups over existing languages with effect handlers or control operators. Our implementation technique is general and allows us to generate code in any language that supports first-class functions.
We then identify a subset of programs for which we can further improve the performance and guarantee full elimination of the effect handler abstraction. To formally capture this subset, we refine λCap to λ λCap with a more restrictive type system. We present a type-directed translation for λ λCap that inserts staging annotations and prove that no abstractions or applications related to effect handlers occur in the translated program. Using this second translation we observe additional speedups in some of the benchmarks.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Effect Handlers, Evidently ..."
Effect Handlers, Evidently
Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen
(Microsoft Research, USA; University of Tübingen, Germany; University of Edinburgh, UK)
Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even _too_ powerful. In this article we define a restriction of general effect handlers with _scoped resumptions_. We argue one can still express all important effects, while improving reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers, which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations _in place_ (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Separation Logic for Sequential ..."
Separation Logic for Sequential Programs (Functional Pearl)
Arthur Charguéraud
(Inria, France; University of Strasbourg, France; CNRS, France; ICube, France)
This paper presents a simple mechanized formalization of Separation Logic for sequential programs. This formalization is aimed for teaching the ideas of Separation Logic, including its soundness proof and its recent enhancements. The formalization serves as support for a course that follows the style of the successful Software Foundations series, with all the statement and proofs formalized in Coq. This course only assumes basic knowledge of lambda-calculus, semantics and logics, and therefore should be accessible to a broad audience.
Publisher's Version
Info
Proc. ACM Program. Lang., vol. 4, issue ICFP: "A General Approach to Define ..."
A General Approach to Define Binders using Matching Logic
Xiaohong Chen and Grigore Roşu
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)
We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system if and only if it is provable in matching logic, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete, a desired property that is not enjoyed by many existing lambda-calculus semantics. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Recovering Purity with Comonads ..."
Recovering Purity with Comonads and Capabilities
Vikraman Choudhury and Neel Krishnaswami
(Indiana University, USA; University of Cambridge, UK)
In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus can be extended to support effects with a monadic type discipline, an impure typed lambda calculus can be extended to support purity with a comonadic type discipline.
We establish the correctness of our type system via a simple denotational model, which we call the capability space model. Our model formalises the intuition common to systems programmers that the ability to perform effects should be controlled via access to a permission or capability, and that a program is capability-safe if it performs no effects that it does not have a runtime capability for. We then identify the axiomatic categorical structure that the capability space model validates, and use these axioms to give a categorical semantics for our comonadic type system. We then give an equational theory (substitution and the call-by-value β and η laws) for the imperative lambda calculus, and show its soundness relative to this semantics.
Finally, we give a translation of the pure simply-typed lambda calculus into our comonadic imperative calculus, and show that any two terms which are βη-equal in the STLC are equal in the equational theory of the comonadic calculus, establishing that pure programs can be mapped in an equation-preserving way into our imperative calculus.
Publisher's Version
Info
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Program Sketching with Live ..."
Program Sketching with Live Bidirectional Evaluation
Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh
(University of Chicago, USA; University of Michigan, USA)
We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes. The key innovation, called live bidirectional evaluation, propagates examples "backward" through partially evaluated sketches. Live bidirectional evaluation enables Smyth to (a) synthesize recursive functions without trace-complete sets of examples and (b) specify and solve interdependent synthesis goals. Eliminating the trace-completeness requirement resolves a significant limitation faced by prior synthesis techniques when given partial specifications in the form of input-output examples.
To assess the practical implications of our techniques, we ran several experiments on benchmarks used to evaluate Myth, a state-of-the-art example-based synthesis tool. First, given expert examples (and no partial implementations), we find that Smyth requires on average 66% of the number of expert examples required by Myth. Second, we find that Smyth is robust to randomly-generated examples, synthesizing many tasks with relatively few more random examples than those provided by an expert. Third, we create a suite of small sketching tasks by systematically employing a simple sketching strategy to the Myth benchmarks; we find that user-provided sketches in Smyth often further reduce the total specification burden (i.e. the combination of partial implementations and examples). Lastly, we find that Leon and Synquid, two state-of-the-art logic-based synthesis tools, fail to complete several tasks on which Smyth succeeds.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Program Sketching with Live ..."
Program Sketching with Live Bidirectional Evaluation
Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh
(University of Chicago, USA; University of Michigan, USA)
We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes. The key innovation, called live bidirectional evaluation, propagates examples "backward" through partially evaluated sketches. Live bidirectional evaluation enables Smyth to (a) synthesize recursive functions without trace-complete sets of examples and (b) specify and solve interdependent synthesis goals. Eliminating the trace-completeness requirement resolves a significant limitation faced by prior synthesis techniques when given partial specifications in the form of input-output examples.
To assess the practical implications of our techniques, we ran several experiments on benchmarks used to evaluate Myth, a state-of-the-art example-based synthesis tool. First, given expert examples (and no partial implementations), we find that Smyth requires on average 66% of the number of expert examples required by Myth. Second, we find that Smyth is robust to randomly-generated examples, synthesizing many tasks with relatively few more random examples than those provided by an expert. Third, we create a suite of small sketching tasks by systematically employing a simple sketching strategy to the Myth benchmarks; we find that user-provided sketches in Smyth often further reduce the total specification burden (i.e. the combination of partial implementations and examples). Lastly, we find that Leon and Synquid, two state-of-the-art logic-based synthesis tools, fail to complete several tasks on which Smyth succeeds.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Denotational Recurrence Extraction ..."
Denotational Recurrence Extraction for Amortized Analysis
Joseph W. Cutler, Daniel R. Licata, and Norman Danner
(Wesleyan University, USA)
A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed techniques for using logical relations to state a formal correctness theorem for a general recurrence extraction translation: a program is bounded by a recurrence when the operational cost is bounded by the extracted cost, and the output value is bounded, according to a value bounding relation defined by induction on types, by the extracted size. This previous work supports higher-order functions by viewing recurrences as programs in a lambda-calculus, or as mathematical entities in a denotational semantics thereof. In this paper, we extend these techniques to support amortized analysis, where costs are rearranged from one portion of a program to another to achieve more precise bounds. We give an intermediate language in which programs can be annotated according to the banker's method of amortized analysis; this language has an affine type system to ensure credits are not spent more than once. We give a recurrence extraction translation of this language into a recurrence language, a simply-typed lambda-calculus with a cost type, and state and prove a bounding logical relation expressing the correctness of this translation. The recurrence language has a denotational semantics in preorders, and we use this semantics to solve recurrences, e.g analyzing binary counters and splay trees.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Denotational Recurrence Extraction ..."
Denotational Recurrence Extraction for Amortized Analysis
Joseph W. Cutler, Daniel R. Licata, and Norman Danner
(Wesleyan University, USA)
A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed techniques for using logical relations to state a formal correctness theorem for a general recurrence extraction translation: a program is bounded by a recurrence when the operational cost is bounded by the extracted cost, and the output value is bounded, according to a value bounding relation defined by induction on types, by the extracted size. This previous work supports higher-order functions by viewing recurrences as programs in a lambda-calculus, or as mathematical entities in a denotational semantics thereof. In this paper, we extend these techniques to support amortized analysis, where costs are rearranged from one portion of a program to another to achieve more precise bounds. We give an intermediate language in which programs can be annotated according to the banker's method of amortized analysis; this language has an affine type system to ensure credits are not spent more than once. We give a recurrence extraction translation of this language into a recurrence language, a simply-typed lambda-calculus with a cost type, and state and prove a bounding logical relation expressing the correctness of this translation. The recurrence language has a denotational semantics in preorders, and we use this semantics to solve recurrences, e.g analyzing binary counters and splay trees.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Parsing with Zippers (Functional ..."
Parsing with Zippers (Functional Pearl)
Pierce Darragh and Michael D. Adams
(University of Utah, USA; University of Michigan, USA)
Parsing with Derivatives (PwD) is an elegant approach to parsing context-free grammars (CFGs). It takes the equational theory behind Brzozowski's derivative for regular expressions and augments that theory with laziness, memoization, and fixed points. The result is a simple parser for arbitrary CFGs. Although recent work improved the performance of PwD, it remains inefficient due to the algorithm repeatedly traversing some parts of the grammar.
In this functional pearl, we show how to avoid this inefficiency by suspending the state of the traversal in a zipper. When subsequent derivatives are taken, we can resume the traversal from where we left off without retraversing already traversed parts of the grammar.
However, the original zipper is designed for use with trees, and we want to parse CFGs. CFGs can include shared regions, cycles, and choices between alternates, which makes them incompatible with the traditional tree model for zippers. This paper develops a generalization of zippers to properly handle these additional features. Just as PwD generalized Brzozowski's derivatives from regular expressions to CFGs, we generalize Huet's zippers from trees to CFGs.
Abstract The resulting parsing algorithm is concise and efficient: it takes only 31 lines of OCaml code to implement the derivative function but performs 6,500 times faster than the original PwD and 3.24 times faster than the optimized implementation of PwD.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Sealing Pointer-Based Optimizations ..."
Sealing Pointer-Based Optimizations behind Pure Functions
Daniel Selsam, Simon Hudon, and Leonardo de Moura
(Microsoft Research, USA; Carnegie Mellon University, USA)
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking search is dramatically simplified by persistent datastructures. However, existing pure functional programming languages all suffer a major limitation in these domains: traversing a term requires time proportional to the tree size of the term as opposed to its graph size. This limitation would be particularly devastating when building automation for interactive theorem provers such as Lean and Coq, for which the exponential blowup of term-tree sizes has proved to be both common and difficult to prevent. All that is needed to recover the optimal scaling is the ability to perform simple operations on the memory addresses of terms, and yet allowing these operations to be used freely would clearly violate the basic premise of referential transparency. We show how to use dependent types to seal the necessary pointer-address manipulations behind pure functional interfaces while requiring only a negligible amount of additional trust. We have implemented our approach for the upcoming version (v4) of Lean, and our approach could be adopted by other languages based on dependent type theory as well.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Kinds Are Calling Conventions ..."
Kinds Are Calling Conventions
Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg
(University of Oregon, USA; Microsoft Research, UK; Bryn Mawr College, USA; Tweag I/O, USA)
A language supporting polymorphism is a boon to programmers: they can express complex ideas once and reuse functions in a variety of situations. However, polymorphism is pain for compilers tasked with producing efficient code that manipulates concrete values.
This paper presents a new intermediate language that allows for efficient static compilation, while still supporting flexible polymorphism. Specifically, it permits polymorphism over not only the types of values, but also the representation of values, the arity of primitive machine functions, and the evaluation order of arguments---all three of which are useful in practice. The key insight is to encode information about a value's calling convention in the kind of its type, rather than in the type itself.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Kinds Are Calling Conventions ..."
Kinds Are Calling Conventions
Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg
(University of Oregon, USA; Microsoft Research, UK; Bryn Mawr College, USA; Tweag I/O, USA)
A language supporting polymorphism is a boon to programmers: they can express complex ideas once and reuse functions in a variety of situations. However, polymorphism is pain for compilers tasked with producing efficient code that manipulates concrete values.
This paper presents a new intermediate language that allows for efficient static compilation, while still supporting flexible polymorphism. Specifically, it permits polymorphism over not only the types of values, but also the representation of values, the arity of primitive machine functions, and the evaluation order of arguments---all three of which are useful in practice. The key insight is to encode information about a value's calling convention in the kind of its type, rather than in the type itself.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "SteelCore: An Extensible Concurrent ..."
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez
(Microsoft Research, USA; Microsoft Research, India; Carnegie Mellon University, USA; Inria, France; University of Ljubljana, Slovenia; CIFASIS-CONICET, Argentina)
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself.
Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F⋆ proof assistant in a manner that enables dependently typed, effectful F⋆ programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions.
Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Regular Language Type Inference ..."
Regular Language Type Inference with Term Rewriting
Timothée Haudebourg, Thomas Genet, and Thomas Jensen
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
This paper defines a new type system applied to the fully automatic verification of safety properties of tree-processing higher-order functional programs. We use term rewriting systems to model the program and its semantics and tree automata to model algebraic data types. We define the regular abstract interpretation of the input term rewriting system where the abstract domain is a set of regular languages. From the regular abstract interpretation we derive a type system where each type is a regular language. We define an inference procedure for this type system which allows us check the validity of safety properties. The inference mechanism is built on an invariant learning procedure based on the tree automata completion algorithm. This invariant learning procedure is regularly-complete and complete in refutation, meaning that if it is possible to give a regular type to a term then we will eventually find it, and if there is no possible type (regular or not) then we will eventually find a counter-example.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Scala Step-by-Step: Soundness ..."
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers
(Delft University of Technology, Netherlands; IRIF, France; University of Paris, France; CNRS, France; Aarhus University, Denmark)
The metatheory of Scala’s core type system—the Dependent Object Types (DOT) calculus—is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and in practice. To address some of these problems, we use a semantics-first approach to develop a logical relations model for a new version of DOT, called guarded DOT (gDOT). Our logical relations model makes use of an abstract form of step-indexing, as supported by the Iris framework, to model various forms of recursion in gDOT. To demonstrate the expressiveness of gDOT, we show that it handles Scala examples that could not be handled by previous versions of DOT, and prove using our logical relations model that gDOT provides the desired data abstraction. The gDOT type system, its semantic model, its soundness proofs, and all examples in the paper have been mechanized in Coq.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Achieving High-Performance ..."
Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Kœhler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; University of Glasgow, UK)
Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a portability nightmare that is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.
Many emerging DSLs used in performance demanding domains such as deep learning or high-performance image processing attempt to simplify or even fully automate the optimization process. Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.
In this functional pearl, we show how to employ functional programming techniques to solve this challenge with elegance. We present two functional languages that work together - each addressing a separate concern. RISE is a functional language for expressing computations using well known functional data-parallel patterns. ELEVATE is a functional language for describing optimization strategies. A high-level RISE program is transformed into a low-level form using optimization strategies written in ELEVATE . From the rewritten low-level program high-performance parallel code is automatically generated. In contrast to existing high-performance domain-specific systems with scheduling APIs, in our approach programmers are not restricted to a set of built-in operations and optimizations but freely define their own computational patterns in RISE and optimization strategies in ELEVATE in a composable and reusable way. We show how our holistic functional approach achieves competitive performance with the state-of-the-art imperative systems Halide and TVM.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Lower Your Guards: A Compositional ..."
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
Sebastian Graf, Simon Peyton Jones, and Ryan G. Scott
(KIT, Germany; Microsoft Research, UK; Indiana University, USA)
A compiler should warn if a function defined by pattern matching does not cover its inputs—that is, if there are missing or redundant patterns. Generating such warnings accurately is difficult for modern languages due to the myriad of language features that interact with pattern matching. This is especially true in Haskell, a language with a complicated pattern language that is made even more complex by extensions offered by the Glasgow Haskell Compiler (GHC). Although GHC has spent a significant amount of effort towards improving its pattern-match coverage warnings, there are still several cases where it reports inaccurate warnings.
We introduce a coverage checking algorithm called Lower Your Guards, which boils down the complexities of pattern matching into guard trees. While the source language may have many exotic forms of patterns, guard trees only have three different constructs, which vastly simplifies the coverage checking process. Our algorithm is modular, allowing for new forms of source-language patterns to be handled with little changes to the overall structure of the algorithm. We have implemented the algorithm in GHC and demonstrate places where it performs better than GHC’s current coverage checker, both in accuracy and performance.
Publisher's Version
Published Artifact
Video
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "TLC: Temporal Logic of Distributed ..."
TLC: Temporal Logic of Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, and Xizhe Yin
(University of California at Riverside, USA)
Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To manage this complexity, network middleware has been traditionally built in layered stacks of components.We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to a novel operational semantics for stacks of composed components in partially synchronous networks. We successfully apply TLC to compose and verify a stack of fundamental distributed components.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "A Quick Look at Impredicativity ..."
A Quick Look at Impredicativity
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis
(47 Degrees, Spain; Utrecht University, Netherlands; Microsoft Research, UK; DeepMind, UK)
Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.
Publisher's Version
Video
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Achieving High-Performance ..."
Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Kœhler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; University of Glasgow, UK)
Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a portability nightmare that is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.
Many emerging DSLs used in performance demanding domains such as deep learning or high-performance image processing attempt to simplify or even fully automate the optimization process. Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.
In this functional pearl, we show how to employ functional programming techniques to solve this challenge with elegance. We present two functional languages that work together - each addressing a separate concern. RISE is a functional language for expressing computations using well known functional data-parallel patterns. ELEVATE is a functional language for describing optimization strategies. A high-level RISE program is transformed into a low-level form using optimization strategies written in ELEVATE . From the rewritten low-level program high-performance parallel code is automatically generated. In contrast to existing high-performance domain-specific systems with scheduling APIs, in our approach programmers are not restricted to a set of built-in operations and optimizations but freely define their own computational patterns in RISE and optimization strategies in ELEVATE in a composable and reusable way. We show how our holistic functional approach achieves competitive performance with the state-of-the-art imperative systems Halide and TVM.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Information Flow Control ..."
Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama
(University of California at San Diego, USA; Carnegie Mellon University, USA; Technion, Israel; Massachusetts Institute of Technology, USA)
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application.
The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Regular Language Type Inference ..."
Regular Language Type Inference with Term Rewriting
Timothée Haudebourg, Thomas Genet, and Thomas Jensen
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
This paper defines a new type system applied to the fully automatic verification of safety properties of tree-processing higher-order functional programs. We use term rewriting systems to model the program and its semantics and tree automata to model algebraic data types. We define the regular abstract interpretation of the input term rewriting system where the abstract domain is a set of regular languages. From the regular abstract interpretation we derive a type system where each type is a regular language. We define an inference procedure for this type system which allows us check the validity of safety properties. The inference mechanism is built on an invariant learning procedure based on the tree automata completion algorithm. This invariant learning procedure is regularly-complete and complete in refutation, meaning that if it is possible to give a regular type to a term then we will eventually find it, and if there is no possible type (regular or not) then we will eventually find a counter-example.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Effects for Efficiency: Asymptotic ..."
Effects for Efficiency: Asymptotic Speedup with First-Class Control
Daniel Hillerström, Sam Lindley, and John Longley
(University of Edinburgh, UK; Imperial College London, UK; Heriot-Watt University, UK)
We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure PCF-like base language λb and its extension with effect handlers λh.
We show that λh admits an asymptotically more efficient implementation of generic count than any λb implementation.
We also show that this efficiency gap remains when λb is extended with mutable state.
To our knowledge this result is the first of its kind for control operators.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Effect Handlers, Evidently ..."
Effect Handlers, Evidently
Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen
(Microsoft Research, USA; University of Tübingen, Germany; University of Edinburgh, UK)
Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even _too_ powerful. In this article we define a restriction of general effect handlers with _scoped resumptions_. We argue one can still express all important effects, while improving reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers, which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations _in place_ (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Resource Types ..."
Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, and Nadia Polikarpova
(University of California at San Diego, USA; Carnegie Mellon University, USA)
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Raising Expectations: Automating ..."
Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang, David M. Kahn, and Jan Hoffmann
(Carnegie Mellon University, USA)
This article presents a type-based analysis for deriving upper bounds on the expected execution cost of probabilistic programs. The analysis is naturally compositional, parametric in the cost model, and supports higher-order functions and inductive data types. The derived bounds are multivariate polynomials that are functions of data structures. Bound inference is enabled by local type rules that reduce type inference to linear constraint solving. The type system is based on the potential method of amortized analysis and extends automatic amortized resource analysis (AARA) for deterministic programs. A main innovation is that bounds can contain symbolic probabilities, which may appear in data structures and function arguments. Another contribution is a novel soundness proof that establishes the correctness of the derived bounds with respect to a distribution-based operational cost semantics that also includes nontrivial diverging behavior. For cost models like time, derived bounds imply termination with probability one. To highlight the novel ideas, the presentation focuses on linear potential and a core language. However, the analysis is implemented as an extension of Resource Aware ML and supports polynomial bounds and user defined data structures. The effectiveness of the technique is evaluated by analyzing the sample complexity of discrete distributions and with a novel average-case estimation for deterministic programs that combines expected cost analysis with statistical methods.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Sealing Pointer-Based Optimizations ..."
Sealing Pointer-Based Optimizations behind Pure Functions
Daniel Selsam, Simon Hudon, and Leonardo de Moura
(Microsoft Research, USA; Carnegie Mellon University, USA)
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking search is dramatically simplified by persistent datastructures. However, existing pure functional programming languages all suffer a major limitation in these domains: traversing a term requires time proportional to the tree size of the term as opposed to its graph size. This limitation would be particularly devastating when building automation for interactive theorem provers such as Lean and Coq, for which the exponential blowup of term-tree sizes has proved to be both common and difficult to prevent. All that is needed to recover the optimal scaling is the ability to perform simple operations on the memory addresses of terms, and yet allowing these operations to be used freely would clearly violate the basic premise of referential transparency. We show how to use dependent types to seal the necessary pointer-address manipulations behind pure functional interfaces while requiring only a negligible amount of additional trust. We have implemented our approach for the upcoming version (v4) of Lean, and our approach could be adopted by other languages based on dependent type theory as well.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Signature Restriction for ..."
Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi
(National Institute of Informatics, Japan; SOKENDAI, Japan; University of Tokyo, Japan; Kyoto University, Japan)
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Information Flow Control ..."
Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama
(University of California at San Diego, USA; Carnegie Mellon University, USA; Technion, Israel; Massachusetts Institute of Technology, USA)
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application.
The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Strong Functional Pearl: Harper’s ..."
Strong Functional Pearl: Harper’s Regular-Expression Matcher in Cedille
Aaron Stump, Christopher Jenkins, Stephan Spahn, and Colin McDonald
(University of Iowa, USA; University of Notre Dame, USA)
This paper describes an implementation of Harper's continuation-based regular-expression matcher as a strong functional program in Cedille; i.e., Cedille statically confirms termination of the program on all inputs. The approach uses neither dependent types nor termination proofs. Instead, a particular interface dubbed a recursion universe is provided by Cedille, and the language ensures that all programs written against this interface terminate. Standard polymorphic typing is all that is needed to check the code against the interface. This answers a challenge posed by Bove, Krauss, and Sozeau.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Regular Language Type Inference ..."
Regular Language Type Inference with Term Rewriting
Timothée Haudebourg, Thomas Genet, and Thomas Jensen
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)
This paper defines a new type system applied to the fully automatic verification of safety properties of tree-processing higher-order functional programs. We use term rewriting systems to model the program and its semantics and tree automata to model algebraic data types. We define the regular abstract interpretation of the input term rewriting system where the abstract domain is a set of regular languages. From the regular abstract interpretation we derive a type system where each type is a regular language. We define an inference procedure for this type system which allows us check the validity of safety properties. The inference mechanism is built on an invariant learning procedure based on the tree automata completion algorithm. This invariant learning procedure is regularly-complete and complete in refutation, meaning that if it is possible to give a regular type to a term then we will eventually find it, and if there is no possible type (regular or not) then we will eventually find a counter-example.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Stable Relations and Abstract ..."
Stable Relations and Abstract Interpretation of Higher-Order Programs
Benoît Montagu and Thomas Jensen
(Inria, France)
We present a novel denotational semantics for the untyped call-by-value λ-calculus, where terms are interpreted as stable relations, i.e. as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. The definition also admits a presentation as a program logic. Following the principles of abstract interpretation, we use our denotational semantics as a collecting semantics to derive a modular relational analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its result—a form of frame condition for functional programs.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Duplo: A Framework for OCaml ..."
Duplo: A Framework for OCaml Post-Link Optimisation
Nandor Licker and Timothy M. Jones
(University of Cambridge, UK)
We present a novel framework, Duplo, for the low-level post-link optimisation of OCaml programs, achieving a speedup of 7% and a reduction of at least 15% of the code size of widely-used OCaml applications. Unlike existing post-link optimisers, which typically operate on target-specific machine code, our framework operates on a Low-Level Intermediate Representation (LLIR) capable of representing both the OCaml programs and any C dependencies they invoke through the foreign-function interface (FFI). LLIR is analysed, transformed and lowered to machine code by our post-link optimiser, LLIR-OPT. Most importantly, LLIR allows the optimiser to cross the OCaml-C language boundary, mitigating the overhead incurred by the FFI and enabling analyses and transformations in a previously unavailable context. The optimised IR is then lowered to amd64 machine code through the existing target-specific code generator of LLVM, modified to handle garbage collection just as effectively as the native OCaml backend. We equip our optimiser with a suite of SSA-based transformations and points-to analyses capable of capturing the semantics and representing the memory models of both languages, along with a cross-language inliner to embed C methods into OCaml callers. We evaluate the gains of our framework, which can be attributed to both our optimiser and the more sophisticated amd64 backend of LLVM, on a wide-range of widely-used OCaml applications, as well as an existing suite of micro- and macro-benchmarks used to track the performance of the OCaml compiler.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Cosmo: A Concurrent Separation ..."
Cosmo: A Concurrent Separation Logic for Multicore OCaml
Glen Mével, Jacques-Henri Jourdan, and François Pottier
(Inria, France; University of Paris-Saclay, France; CNRS, France; LRI, France)
Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code? To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing nonatomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model. We illustrate this claim via a number of case studies: we verify several implementations of locks with respect to a classic, memory-model-independent specification. Thus, a coarse-grained application that uses locks as the sole means of synchronization can be verified in the Concurrent-Separation-Logic fragment of Cosmo, without any knowledge of the weak memory model.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Raising Expectations: Automating ..."
Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang, David M. Kahn, and Jan Hoffmann
(Carnegie Mellon University, USA)
This article presents a type-based analysis for deriving upper bounds on the expected execution cost of probabilistic programs. The analysis is naturally compositional, parametric in the cost model, and supports higher-order functions and inductive data types. The derived bounds are multivariate polynomials that are functions of data structures. Bound inference is enabled by local type rules that reduce type inference to linear constraint solving. The type system is based on the potential method of amortized analysis and extends automatic amortized resource analysis (AARA) for deterministic programs. A main innovation is that bounds can contain symbolic probabilities, which may appear in data structures and function arguments. Another contribution is a novel soundness proof that establishes the correctness of the derived bounds with respect to a distribution-based operational cost semantics that also includes nontrivial diverging behavior. For cost models like time, derived bounds imply termination with probability one. To highlight the novel ideas, the presentation focuses on linear potential and a core language. However, the analysis is implemented as an extension of Resource Aware ML and supports polynomial bounds and user defined data structures. The effectiveness of the technique is evaluated by analyzing the sample complexity of discrete distributions and with a novel average-case estimation for deterministic programs that combines expected cost analysis with statistical methods.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Resource Types ..."
Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, and Nadia Polikarpova
(University of California at San Diego, USA; Carnegie Mellon University, USA)
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Achieving High-Performance ..."
Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Kœhler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; University of Glasgow, UK)
Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a portability nightmare that is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.
Many emerging DSLs used in performance demanding domains such as deep learning or high-performance image processing attempt to simplify or even fully automate the optimization process. Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.
In this functional pearl, we show how to employ functional programming techniques to solve this challenge with elegance. We present two functional languages that work together - each addressing a separate concern. RISE is a functional language for expressing computations using well known functional data-parallel patterns. ELEVATE is a functional language for describing optimization strategies. A high-level RISE program is transformed into a low-level form using optimization strategies written in ELEVATE . From the rewritten low-level program high-performance parallel code is automatically generated. In contrast to existing high-performance domain-specific systems with scheduling APIs, in our approach programmers are not restricted to a set of built-in operations and optimizations but freely define their own computational patterns in RISE and optimization strategies in ELEVATE in a composable and reusable way. We show how our holistic functional approach achieves competitive performance with the state-of-the-art imperative systems Halide and TVM.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Elaboration with First-Class ..."
Elaboration with First-Class Implicit Function Types
András Kovács
(Eötvös Loránd University, Hungary)
Implicit functions are dependently typed functions, such that arguments are provided (by default) by inference machinery instead of programmers of the surface language. Implicit functions in Agda are an archetypal example. In the Haskell language as implemented by the Glasgow Haskell Compiler (GHC), polymorphic types are another example. Implicit function types are first-class if they are treated as any other type in the surface language. This holds in Agda and partially holds in GHC. Inference and elaboration in the presence of first-class implicit functions poses a challenge; in the context of Haskell and ML-like languages, this has been dubbed “impredicative instantiation” or “impredicative inference”. We propose a new solution for elaborating first-class implicit functions, which is applicable to full dependent type theories and compares favorably to prior solutions in terms of power, generality and simplicity. We build atop Norell’s bidirectional elaboration algorithm for Agda, and we note that the key issue is incomplete information about insertions of implicit abstractions and applications. We make it possible to track and refine information related to such insertions, by adding a function type to a core Martin-L'of type theory, which supports strict (definitional) currying. This allows us to represent undetermined domain arities of implicit function types, and we can decide at any point during elaboration whether implicit abstractions should be inserted.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Scala Step-by-Step: Soundness ..."
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers
(Delft University of Technology, Netherlands; IRIF, France; University of Paris, France; CNRS, France; Aarhus University, Denmark)
The metatheory of Scala’s core type system—the Dependent Object Types (DOT) calculus—is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and in practice. To address some of these problems, we use a semantics-first approach to develop a logical relations model for a new version of DOT, called guarded DOT (gDOT). Our logical relations model makes use of an abstract form of step-indexing, as supported by the Iris framework, to model various forms of recursion in gDOT. To demonstrate the expressiveness of gDOT, we show that it handles Scala examples that could not be handled by previous versions of DOT, and prove using our logical relations model that gDOT provides the desired data abstraction. The gDOT type system, its semantic model, its soundness proofs, and all examples in the paper have been mechanized in Coq.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Recovering Purity with Comonads ..."
Recovering Purity with Comonads and Capabilities
Vikraman Choudhury and Neel Krishnaswami
(Indiana University, USA; University of Cambridge, UK)
In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus can be extended to support effects with a monadic type discipline, an impure typed lambda calculus can be extended to support purity with a comonadic type discipline.
We establish the correctness of our type system via a simple denotational model, which we call the capability space model. Our model formalises the intuition common to systems programmers that the ability to perform effects should be controlled via access to a permission or capability, and that a program is capability-safe if it performs no effects that it does not have a runtime capability for. We then identify the axiomatic categorical structure that the capability space model validates, and use these axioms to give a categorical semantics for our comonadic type system. We then give an equational theory (substitution and the call-by-value β and η laws) for the imperative lambda calculus, and show its soundness relative to this semantics.
Finally, we give a translation of the pure simply-typed lambda calculus into our comonadic imperative calculus, and show that any two terms which are βη-equal in the STLC are equal in the equational theory of the comonadic calculus, establishing that pure programs can be mapped in an equation-preserving way into our imperative calculus.
Publisher's Version
Info
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Effect Handlers, Evidently ..."
Effect Handlers, Evidently
Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen
(Microsoft Research, USA; University of Tübingen, Germany; University of Edinburgh, UK)
Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even _too_ powerful. In this article we define a restriction of general effect handlers with _scoped resumptions_. We argue one can still express all important effects, while improving reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers, which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations _in place_ (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Achieving High-Performance ..."
Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Kœhler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; University of Glasgow, UK)
Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a portability nightmare that is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.
Many emerging DSLs used in performance demanding domains such as deep learning or high-performance image processing attempt to simplify or even fully automate the optimization process. Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.
In this functional pearl, we show how to employ functional programming techniques to solve this challenge with elegance. We present two functional languages that work together - each addressing a separate concern. RISE is a functional language for expressing computations using well known functional data-parallel patterns. ELEVATE is a functional language for describing optimization strategies. A high-level RISE program is transformed into a low-level form using optimization strategies written in ELEVATE . From the rewritten low-level program high-performance parallel code is automatically generated. In contrast to existing high-performance domain-specific systems with scheduling APIs, in our approach programmers are not restricted to a set of built-in operations and optimizations but freely define their own computational patterns in RISE and optimization strategies in ELEVATE in a composable and reusable way. We show how our holistic functional approach achieves competitive performance with the state-of-the-art imperative systems Halide and TVM.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "TLC: Temporal Logic of Distributed ..."
TLC: Temporal Logic of Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, and Xizhe Yin
(University of California at Riverside, USA)
Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To manage this complexity, network middleware has been traditionally built in layered stacks of components.We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to a novel operational semantics for stacks of composed components in partially synchronous networks. We successfully apply TLC to compose and verify a stack of fundamental distributed components.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Denotational Recurrence Extraction ..."
Denotational Recurrence Extraction for Amortized Analysis
Joseph W. Cutler, Daniel R. Licata, and Norman Danner
(Wesleyan University, USA)
A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed techniques for using logical relations to state a formal correctness theorem for a general recurrence extraction translation: a program is bounded by a recurrence when the operational cost is bounded by the extracted cost, and the output value is bounded, according to a value bounding relation defined by induction on types, by the extracted size. This previous work supports higher-order functions by viewing recurrences as programs in a lambda-calculus, or as mathematical entities in a denotational semantics thereof. In this paper, we extend these techniques to support amortized analysis, where costs are rearranged from one portion of a program to another to achieve more precise bounds. We give an intermediate language in which programs can be annotated according to the banker's method of amortized analysis; this language has an affine type system to ensure credits are not spent more than once. We give a recurrence extraction translation of this language into a recurrence language, a simply-typed lambda-calculus with a cost type, and state and prove a bounding logical relation expressing the correctness of this translation. The recurrence language has a denotational semantics in preorders, and we use this semantics to solve recurrences, e.g analyzing binary counters and splay trees.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Duplo: A Framework for OCaml ..."
Duplo: A Framework for OCaml Post-Link Optimisation
Nandor Licker and Timothy M. Jones
(University of Cambridge, UK)
We present a novel framework, Duplo, for the low-level post-link optimisation of OCaml programs, achieving a speedup of 7% and a reduction of at least 15% of the code size of widely-used OCaml applications. Unlike existing post-link optimisers, which typically operate on target-specific machine code, our framework operates on a Low-Level Intermediate Representation (LLIR) capable of representing both the OCaml programs and any C dependencies they invoke through the foreign-function interface (FFI). LLIR is analysed, transformed and lowered to machine code by our post-link optimiser, LLIR-OPT. Most importantly, LLIR allows the optimiser to cross the OCaml-C language boundary, mitigating the overhead incurred by the FFI and enabling analyses and transformations in a previously unavailable context. The optimised IR is then lowered to amd64 machine code through the existing target-specific code generator of LLVM, modified to handle garbage collection just as effectively as the native OCaml backend. We equip our optimiser with a suite of SSA-based transformations and points-to analyses capable of capturing the semantics and representing the memory models of both languages, along with a cross-language inliner to embed C methods into OCaml callers. We evaluate the gains of our framework, which can be attributed to both our optimiser and the more sophisticated amd64 backend of LLVM, on a wide-range of widely-used OCaml applications, as well as an existing suite of micro- and macro-benchmarks used to track the performance of the OCaml compiler.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Effects for Efficiency: Asymptotic ..."
Effects for Efficiency: Asymptotic Speedup with First-Class Control
Daniel Hillerström, Sam Lindley, and John Longley
(University of Edinburgh, UK; Imperial College London, UK; Heriot-Watt University, UK)
We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure PCF-like base language λb and its extension with effect handlers λh.
We show that λh admits an asymptotically more efficient implementation of generic count than any λb implementation.
We also show that this efficiency gap remains when λb is extended with mutable state.
To our knowledge this result is the first of its kind for control operators.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Effects for Efficiency: Asymptotic ..."
Effects for Efficiency: Asymptotic Speedup with First-Class Control
Daniel Hillerström, Sam Lindley, and John Longley
(University of Edinburgh, UK; Imperial College London, UK; Heriot-Watt University, UK)
We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of functions. We consider the generic count problem using a pure PCF-like base language λb and its extension with effect handlers λh.
We show that λh admits an asymptotically more efficient implementation of generic count than any λb implementation.
We also show that this efficiency gap remains when λb is extended with mutable state.
To our knowledge this result is the first of its kind for control operators.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Program Sketching with Live ..."
Program Sketching with Live Bidirectional Evaluation
Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh
(University of Chicago, USA; University of Michigan, USA)
We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes. The key innovation, called live bidirectional evaluation, propagates examples "backward" through partially evaluated sketches. Live bidirectional evaluation enables Smyth to (a) synthesize recursive functions without trace-complete sets of examples and (b) specify and solve interdependent synthesis goals. Eliminating the trace-completeness requirement resolves a significant limitation faced by prior synthesis techniques when given partial specifications in the form of input-output examples.
To assess the practical implications of our techniques, we ran several experiments on benchmarks used to evaluate Myth, a state-of-the-art example-based synthesis tool. First, given expert examples (and no partial implementations), we find that Smyth requires on average 66% of the number of expert examples required by Myth. Second, we find that Smyth is robust to randomly-generated examples, synthesizing many tasks with relatively few more random examples than those provided by an expert. Third, we create a suite of small sketching tasks by systematically employing a simple sketching strategy to the Myth benchmarks; we find that user-provided sketches in Smyth often further reduce the total specification burden (i.e. the combination of partial implementations and examples). Lastly, we find that Leon and Synquid, two state-of-the-art logic-based synthesis tools, fail to complete several tasks on which Smyth succeeds.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "SteelCore: An Extensible Concurrent ..."
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez
(Microsoft Research, USA; Microsoft Research, India; Carnegie Mellon University, USA; Inria, France; University of Ljubljana, Slovenia; CIFASIS-CONICET, Argentina)
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself.
Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F⋆ proof assistant in a manner that enables dependently typed, effectful F⋆ programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions.
Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Sparcl: A Language for Partially-Invertible ..."
Sparcl: A Language for Partially-Invertible Computation
Kazutaka Matsuda and Meng Wang
(Tohoku University, Japan; University of Bristol, UK)
Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing on partially-invertible functions—functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible.
We develop a language Sparcl for programming such functions in a natural way, where partial-invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the “partially” part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language Sparcl is linear-typed, and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language, and prove that Sparcl correctly guarantees invertibility for its programs. We demonstrate the expressiveness of Sparcl with examples including tree rebuilding from preorder and inorder traversals and Huffman coding.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Strong Functional Pearl: Harper’s ..."
Strong Functional Pearl: Harper’s Regular-Expression Matcher in Cedille
Aaron Stump, Christopher Jenkins, Stephan Spahn, and Colin McDonald
(University of Iowa, USA; University of Notre Dame, USA)
This paper describes an implementation of Harper's continuation-based regular-expression matcher as a strong functional program in Cedille; i.e., Cedille statically confirms termination of the program on all inputs. The approach uses neither dependent types nor termination proofs. Instead, a particular interface dubbed a recursion universe is provided by Cedille, and the language ensures that all programs written against this interface terminate. Standard polymorphic typing is all that is needed to check the code against the interface. This answers a challenge posed by Bove, Krauss, and Sozeau.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Composing and Decomposing ..."
Composing and Decomposing Op-Based CRDTs with Semidirect Products
Matthew Weidner, Heather Miller, and Christopher Meiklejohn
(Carnegie Mellon University, USA)
Operation-based Conflict-free Replicated Data Types (CRDTs) are eventually consistent replicated data types that automatically resolve conflicts between concurrent operations. Op-based CRDTs must be designed differently for each data type, and current designs use ad-hoc techniques to handle concurrent operations that do not naturally commute. We present a new construction, the semidirect product of op-based CRDTs, which combines the operations of two CRDTs into one while handling conflicts between their concurrent operations in a uniform way. We demonstrate the construction's utility by using it to construct novel CRDTs, as well as decomposing several existing CRDTs as semidirect products of simpler CRDTs. Although it reproduces common CRDT semantics, the semidirect product can be viewed as a restricted kind of operational transformation, thus forming a bridge between these two opposing techniques for constructing replicated data types.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "SteelCore: An Extensible Concurrent ..."
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez
(Microsoft Research, USA; Microsoft Research, India; Carnegie Mellon University, USA; Inria, France; University of Ljubljana, Slovenia; CIFASIS-CONICET, Argentina)
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself.
Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F⋆ proof assistant in a manner that enables dependently typed, effectful F⋆ programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions.
Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Cosmo: A Concurrent Separation ..."
Cosmo: A Concurrent Separation Logic for Multicore OCaml
Glen Mével, Jacques-Henri Jourdan, and François Pottier
(Inria, France; University of Paris-Saclay, France; CNRS, France; LRI, France)
Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code? To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing nonatomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model. We illustrate this claim via a number of case studies: we verify several implementations of locks with respect to a classic, memory-model-independent specification. Thus, a coarse-grained application that uses locks as the sole means of synchronization can be verified in the Concurrent-Separation-Logic fragment of Cosmo, without any knowledge of the weak memory model.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Composing and Decomposing ..."
Composing and Decomposing Op-Based CRDTs with Semidirect Products
Matthew Weidner, Heather Miller, and Christopher Meiklejohn
(Carnegie Mellon University, USA)
Operation-based Conflict-free Replicated Data Types (CRDTs) are eventually consistent replicated data types that automatically resolve conflicts between concurrent operations. Op-based CRDTs must be designed differently for each data type, and current designs use ad-hoc techniques to handle concurrent operations that do not naturally commute. We present a new construction, the semidirect product of op-based CRDTs, which combines the operations of two CRDTs into one while handling conflicts between their concurrent operations in a uniform way. We demonstrate the construction's utility by using it to construct novel CRDTs, as well as decomposing several existing CRDTs as semidirect products of simpler CRDTs. Although it reproduces common CRDT semantics, the semidirect product can be viewed as a restricted kind of operational transformation, thus forming a bridge between these two opposing techniques for constructing replicated data types.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Stable Relations and Abstract ..."
Stable Relations and Abstract Interpretation of Higher-Order Programs
Benoît Montagu and Thomas Jensen
(Inria, France)
We present a novel denotational semantics for the untyped call-by-value λ-calculus, where terms are interpreted as stable relations, i.e. as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. The definition also admits a presentation as a program logic. Following the principles of abstract interpretation, we use our denotational semantics as a collecting semantics to derive a modular relational analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its result—a form of frame condition for functional programs.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Program Sketching with Live ..."
Program Sketching with Live Bidirectional Evaluation
Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh
(University of Chicago, USA; University of Michigan, USA)
We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes. The key innovation, called live bidirectional evaluation, propagates examples "backward" through partially evaluated sketches. Live bidirectional evaluation enables Smyth to (a) synthesize recursive functions without trace-complete sets of examples and (b) specify and solve interdependent synthesis goals. Eliminating the trace-completeness requirement resolves a significant limitation faced by prior synthesis techniques when given partial specifications in the form of input-output examples.
To assess the practical implications of our techniques, we ran several experiments on benchmarks used to evaluate Myth, a state-of-the-art example-based synthesis tool. First, given expert examples (and no partial implementations), we find that Smyth requires on average 66% of the number of expert examples required by Myth. Second, we find that Smyth is robust to randomly-generated examples, synthesizing many tasks with relatively few more random examples than those provided by an expert. Third, we create a suite of small sketching tasks by systematically employing a simple sketching strategy to the Myth benchmarks; we find that user-provided sketches in Smyth often further reduce the total specification burden (i.e. the combination of partial implementations and examples). Lastly, we find that Leon and Synquid, two state-of-the-art logic-based synthesis tools, fail to complete several tasks on which Smyth succeeds.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Compiling Effect Handlers ..."
Compiling Effect Handlers in Capability-Passing Style
Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann
(University of Tübingen, Germany)
Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper, we aim to achieve abstraction without regret for effect handlers.
We present a language for effect handlers in _capability-passing style_ (λCap) and an implementation of this language as a translation to simply-typed lambda calculus in _iterated continuation-passing style_. A suite of benchmarks indicates that the novel combination of capability-passing style and iterated CPS enables significant speedups over existing languages with effect handlers or control operators. Our implementation technique is general and allows us to generate code in any language that supports first-class functions.
We then identify a subset of programs for which we can further improve the performance and guarantee full elimination of the effect handler abstraction. To formally capture this subset, we refine λCap to λ λCap with a more restrictive type system. We present a type-directed translation for λ λCap that inserts staging annotations and prove that no abstractions or applications related to effect handlers occur in the translated program. Using this second translation we observe additional speedups in some of the benchmarks.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Higher-Order Demand-Driven ..."
Higher-Order Demand-Driven Symbolic Evaluation
Zachary Palmer, Theodore Park, Scott Smith, and Shiwei Weng
(Swarthmore College, USA; Johns Hopkins University, USA)
Symbolic backwards execution (SBE) is a useful variation on standard forward symbolic evaluation; it allows a symbolic evaluation to start anywhere in the program and proceed by executing in reverse to the program start. SBE brings goal-directed reasoning to symbolic evaluation and has proven effective in e.g. automated test generation for imperative languages.
In this paper we define DDSE, a novel SBE which operates on a functional as opposed to imperative language; furthermore, it is defined as a natural extension of a backwards-executing interpreter. We establish the soundness of DDSE and define a test generation algorithm for this toy language. We report on an initial reference implementation to confirm the correctness of the principles.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Higher-Order Demand-Driven ..."
Higher-Order Demand-Driven Symbolic Evaluation
Zachary Palmer, Theodore Park, Scott Smith, and Shiwei Weng
(Swarthmore College, USA; Johns Hopkins University, USA)
Symbolic backwards execution (SBE) is a useful variation on standard forward symbolic evaluation; it allows a symbolic evaluation to start anywhere in the program and proceed by executing in reverse to the program start. SBE brings goal-directed reasoning to symbolic evaluation and has proven effective in e.g. automated test generation for imperative languages.
In this paper we define DDSE, a novel SBE which operates on a functional as opposed to imperative language; furthermore, it is defined as a natural extension of a backwards-executing interpreter. We establish the soundness of DDSE and define a test generation algorithm for this toy language. We report on an initial reference implementation to confirm the correctness of the principles.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "The Simple Essence of Algebraic ..."
The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
Lionel Parreaux
(EPFL, Switzerland)
MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand.
We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system.
This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Kinds Are Calling Conventions ..."
Kinds Are Calling Conventions
Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg
(University of Oregon, USA; Microsoft Research, UK; Bryn Mawr College, USA; Tweag I/O, USA)
A language supporting polymorphism is a boon to programmers: they can express complex ideas once and reuse functions in a variety of situations. However, polymorphism is pain for compilers tasked with producing efficient code that manipulates concrete values.
This paper presents a new intermediate language that allows for efficient static compilation, while still supporting flexible polymorphism. Specifically, it permits polymorphism over not only the types of values, but also the representation of values, the arity of primitive machine functions, and the evaluation order of arguments---all three of which are useful in practice. The key insight is to encode information about a value's calling convention in the kind of its type, rather than in the type itself.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Lower Your Guards: A Compositional ..."
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
Sebastian Graf, Simon Peyton Jones, and Ryan G. Scott
(KIT, Germany; Microsoft Research, UK; Indiana University, USA)
A compiler should warn if a function defined by pattern matching does not cover its inputs—that is, if there are missing or redundant patterns. Generating such warnings accurately is difficult for modern languages due to the myriad of language features that interact with pattern matching. This is especially true in Haskell, a language with a complicated pattern language that is made even more complex by extensions offered by the Glasgow Haskell Compiler (GHC). Although GHC has spent a significant amount of effort towards improving its pattern-match coverage warnings, there are still several cases where it reports inaccurate warnings.
We introduce a coverage checking algorithm called Lower Your Guards, which boils down the complexities of pattern matching into guard trees. While the source language may have many exotic forms of patterns, guard trees only have three different constructs, which vastly simplifies the coverage checking process. Our algorithm is modular, allowing for new forms of source-language patterns to be handled with little changes to the overall structure of the algorithm. We have implemented the algorithm in GHC and demonstrate places where it performs better than GHC’s current coverage checker, both in accuracy and performance.
Publisher's Version
Published Artifact
Video
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "A Quick Look at Impredicativity ..."
A Quick Look at Impredicativity
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis
(47 Degrees, Spain; Utrecht University, Netherlands; Microsoft Research, UK; DeepMind, UK)
Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.
Publisher's Version
Video
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Staged Selective Parser Combinators ..."
Staged Selective Parser Combinators
Jamie Willis, Nicolas Wu, and Matthew Pickering
(Imperial College London, UK; University of Bristol, UK)
Parser combinators are a middle ground between the fine control of hand-rolled parsers and the high-level almost grammar-like appearance of parsers created via parser generators. They also promote a cleaner, compositional design for parsers. Historically, however, they cannot match the performance of their counterparts.
This paper describes how to compile parser combinators into parsers of hand-written quality. This is done by leveraging the static information present in the grammar by representing it as a tree. However, in order to exploit this information, it will be necessary to drop support for monadic computation since this generates dynamic structure. Selective functors can help recover lost functionality in the absence of monads, and the parser tree can be partially evaluated with staging. This is implemented in a library called Parsley.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Information Flow Control ..."
Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama
(University of California at San Diego, USA; Carnegie Mellon University, USA; Technion, Israel; Massachusetts Institute of Technology, USA)
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application.
The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Resource Types ..."
Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, and Nadia Polikarpova
(University of California at San Diego, USA; Carnegie Mellon University, USA)
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Cosmo: A Concurrent Separation ..."
Cosmo: A Concurrent Separation Logic for Multicore OCaml
Glen Mével, Jacques-Henri Jourdan, and François Pottier
(Inria, France; University of Paris-Saclay, France; CNRS, France; LRI, France)
Multicore OCaml extends OCaml with support for shared-memory concurrency. It is equipped with a weak memory model, for which an operational semantics has been published. This begs the question: what reasoning rules can one rely upon while writing or verifying Multicore OCaml code? To answer it, we instantiate Iris, a modern descendant of Concurrent Separation Logic, for Multicore OCaml. This yields a low-level program logic whose reasoning rules expose the details of the memory model. On top of it, we build a higher-level logic, Cosmo, which trades off some expressive power in return for a simple set of reasoning rules that allow accessing nonatomic locations in a data-race-free manner, exploiting the sequentially-consistent behavior of atomic locations, and exploiting the release/acquire behavior of atomic locations. Cosmo allows both low-level reasoning, where the details of the Multicore OCaml memory model are apparent, and high-level reasoning, which is independent of this memory model. We illustrate this claim via a number of case studies: we verify several implementations of locks with respect to a classic, memory-model-independent specification. Thus, a coarse-grained application that uses locks as the sole means of synchronization can be verified in the Concurrent-Separation-Logic fragment of Cosmo, without any knowledge of the weak memory model.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Achieving High-Performance ..."
Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Kœhler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; University of Glasgow, UK)
Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a portability nightmare that is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.
Many emerging DSLs used in performance demanding domains such as deep learning or high-performance image processing attempt to simplify or even fully automate the optimization process. Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.
In this functional pearl, we show how to employ functional programming techniques to solve this challenge with elegance. We present two functional languages that work together - each addressing a separate concern. RISE is a functional language for expressing computations using well known functional data-parallel patterns. ELEVATE is a functional language for describing optimization strategies. A high-level RISE program is transformed into a low-level form using optimization strategies written in ELEVATE . From the rewritten low-level program high-performance parallel code is automatically generated. In contrast to existing high-performance domain-specific systems with scheduling APIs, in our approach programmers are not restricted to a set of built-in operations and optimizations but freely define their own computational patterns in RISE and optimization strategies in ELEVATE in a composable and reusable way. We show how our holistic functional approach achieves competitive performance with the state-of-the-art imperative systems Halide and TVM.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Kindly Bent to Free Us ..."
Kindly Bent to Free Us
Gabriel Radanne, Hannes Saffrich, and Peter Thiemann
(Inria, France; University of Freiburg, Germany)
Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities.
While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper handling of resources. An important step towards handling resources is the adoption of linear and affine types that enforce single-threaded resource usage. However, the few languages supporting such types require heavy type annotations.
We present Affe, an extension of ML that manages linearity and affinity properties using kinds and constrained types. In addition Affe supports the exclusive and shared borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: it is an impure, strict, functional expression language with complete principal type inference and type abstraction. does not require any linearity annotations in expressions and supports common functional programming idioms.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "SteelCore: An Extensible Concurrent ..."
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez
(Microsoft Research, USA; Microsoft Research, India; Carnegie Mellon University, USA; Inria, France; University of Ljubljana, Slovenia; CIFASIS-CONICET, Argentina)
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself.
Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F⋆ proof assistant in a manner that enables dependently typed, effectful F⋆ programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions.
Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Resource Types ..."
Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, and Nadia Polikarpova
(University of California at San Diego, USA; Carnegie Mellon University, USA)
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Computation Focusing ..."
Computation Focusing
Nick Rioux and Steve Zdancewic
(University of Pennsylvania, USA)
Focusing is a technique from proof theory that exploits type information to prune inessential nondeterminism from proof search procedures. Viewed through the lens of the Curry-Howard correspondence, a focused typing derivation yields terms in normal form. This paper explores how to exploit focusing for reasoning about contextual equivalences and full abstraction. We present a focused polymorphic call-by-push-value calculus and prove a computational completeness result: for every well-typed term, there exists a focused term that is βη-equivalent to it. This completeness result yields a powerful way to refine the context lemmas for establishing contextual equivalences, cutting down the set that must be considered to just focused contexts. The paper demonstrates the application of focusing to establish program equivalences, including free theorems. It also uses focusing to prove full abstraction of a translation of the pure, total call-by-push-value language into a language with divergence and simple effect types, yielding a novel solution to a simple-to-state, but hitherto difficult to solve problem.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "A General Approach to Define ..."
A General Approach to Define Binders using Matching Logic
Xiaohong Chen and Grigore Roşu
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)
We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system if and only if it is provable in matching logic, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete, a desired property that is not enjoyed by many existing lambda-calculus semantics. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Kindly Bent to Free Us ..."
Kindly Bent to Free Us
Gabriel Radanne, Hannes Saffrich, and Peter Thiemann
(Inria, France; University of Freiburg, Germany)
Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities.
While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper handling of resources. An important step towards handling resources is the adoption of linear and affine types that enforce single-threaded resource usage. However, the few languages supporting such types require heavy type annotations.
We present Affe, an extension of ML that manages linearity and affinity properties using kinds and constrained types. In addition Affe supports the exclusive and shared borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: it is an impure, strict, functional expression language with complete principal type inference and type abstraction. does not require any linearity annotations in expressions and supports common functional programming idioms.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Compiling Effect Handlers ..."
Compiling Effect Handlers in Capability-Passing Style
Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann
(University of Tübingen, Germany)
Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper, we aim to achieve abstraction without regret for effect handlers.
We present a language for effect handlers in _capability-passing style_ (λCap) and an implementation of this language as a translation to simply-typed lambda calculus in _iterated continuation-passing style_. A suite of benchmarks indicates that the novel combination of capability-passing style and iterated CPS enables significant speedups over existing languages with effect handlers or control operators. Our implementation technique is general and allows us to generate code in any language that supports first-class functions.
We then identify a subset of programs for which we can further improve the performance and guarantee full elimination of the effect handler abstraction. To formally capture this subset, we refine λCap to λ λCap with a more restrictive type system. We present a type-directed translation for λ λCap that inserts staging annotations and prove that no abstractions or applications related to effect handlers occur in the translated program. Using this second translation we observe additional speedups in some of the benchmarks.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Effect Handlers, Evidently ..."
Effect Handlers, Evidently
Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen
(Microsoft Research, USA; University of Tübingen, Germany; University of Edinburgh, UK)
Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even _too_ powerful. In this article we define a restriction of general effect handlers with _scoped resumptions_. We argue one can still express all important effects, while improving reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers, which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations _in place_ (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Lower Your Guards: A Compositional ..."
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
Sebastian Graf, Simon Peyton Jones, and Ryan G. Scott
(KIT, Germany; Microsoft Research, UK; Indiana University, USA)
A compiler should warn if a function defined by pattern matching does not cover its inputs—that is, if there are missing or redundant patterns. Generating such warnings accurately is difficult for modern languages due to the myriad of language features that interact with pattern matching. This is especially true in Haskell, a language with a complicated pattern language that is made even more complex by extensions offered by the Glasgow Haskell Compiler (GHC). Although GHC has spent a significant amount of effort towards improving its pattern-match coverage warnings, there are still several cases where it reports inaccurate warnings.
We introduce a coverage checking algorithm called Lower Your Guards, which boils down the complexities of pattern matching into guard trees. While the source language may have many exotic forms of patterns, guard trees only have three different constructs, which vastly simplifies the coverage checking process. Our algorithm is modular, allowing for new forms of source-language patterns to be handled with little changes to the overall structure of the algorithm. We have implemented the algorithm in GHC and demonstrate places where it performs better than GHC’s current coverage checker, both in accuracy and performance.
Publisher's Version
Published Artifact
Video
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Signature Restriction for ..."
Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi
(National Institute of Informatics, Japan; SOKENDAI, Japan; University of Tokyo, Japan; Kyoto University, Japan)
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Sealing Pointer-Based Optimizations ..."
Sealing Pointer-Based Optimizations behind Pure Functions
Daniel Selsam, Simon Hudon, and Leonardo de Moura
(Microsoft Research, USA; Carnegie Mellon University, USA)
Functional programming languages are particularly well-suited for building automated reasoning systems, since (among other reasons) a logical term is well modeled by an inductive type, traversing a term can be implemented generically as a higher-order combinator, and backtracking search is dramatically simplified by persistent datastructures. However, existing pure functional programming languages all suffer a major limitation in these domains: traversing a term requires time proportional to the tree size of the term as opposed to its graph size. This limitation would be particularly devastating when building automation for interactive theorem provers such as Lean and Coq, for which the exponential blowup of term-tree sizes has proved to be both common and difficult to prevent. All that is needed to recover the optimal scaling is the ability to perform simple operations on the memory addresses of terms, and yet allowing these operations to be used freely would clearly violate the basic premise of referential transparency. We show how to use dependent types to seal the necessary pointer-address manipulations behind pure functional interfaces while requiring only a negligible amount of additional trust. We have implemented our approach for the upcoming version (v4) of Lean, and our approach could be adopted by other languages based on dependent type theory as well.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "A Quick Look at Impredicativity ..."
A Quick Look at Impredicativity
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis
(47 Degrees, Spain; Utrecht University, Netherlands; Microsoft Research, UK; DeepMind, UK)
Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.
Publisher's Version
Video
Proc. ACM Program. Lang., vol. 4, issue ICFP: "TLC: Temporal Logic of Distributed ..."
TLC: Temporal Logic of Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, and Xizhe Yin
(University of California at Riverside, USA)
Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To manage this complexity, network middleware has been traditionally built in layered stacks of components.We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to a novel operational semantics for stacks of composed components in partially synchronous networks. We successfully apply TLC to compose and verify a stack of fundamental distributed components.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Higher-Order Demand-Driven ..."
Higher-Order Demand-Driven Symbolic Evaluation
Zachary Palmer, Theodore Park, Scott Smith, and Shiwei Weng
(Swarthmore College, USA; Johns Hopkins University, USA)
Symbolic backwards execution (SBE) is a useful variation on standard forward symbolic evaluation; it allows a symbolic evaluation to start anywhere in the program and proceed by executing in reverse to the program start. SBE brings goal-directed reasoning to symbolic evaluation and has proven effective in e.g. automated test generation for imperative languages.
In this paper we define DDSE, a novel SBE which operates on a functional as opposed to imperative language; furthermore, it is defined as a natural extension of a backwards-executing interpreter. We establish the soundness of DDSE and define a test generation algorithm for this toy language. We report on an initial reference implementation to confirm the correctness of the principles.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Information Flow Control ..."
Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama
(University of California at San Diego, USA; Carnegie Mellon University, USA; Technion, Israel; Massachusetts Institute of Technology, USA)
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application.
The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Strong Functional Pearl: Harper’s ..."
Strong Functional Pearl: Harper’s Regular-Expression Matcher in Cedille
Aaron Stump, Christopher Jenkins, Stephan Spahn, and Colin McDonald
(University of Iowa, USA; University of Notre Dame, USA)
This paper describes an implementation of Harper's continuation-based regular-expression matcher as a strong functional program in Cedille; i.e., Cedille statically confirms termination of the program on all inputs. The approach uses neither dependent types nor termination proofs. Instead, a particular interface dubbed a recursion universe is provided by Cedille, and the language ensures that all programs written against this interface terminate. Standard polymorphic typing is all that is needed to check the code against the interface. This answers a challenge posed by Bove, Krauss, and Sozeau.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Information Flow Control ..."
Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama
(University of California at San Diego, USA; Carnegie Mellon University, USA; Technion, Israel; Massachusetts Institute of Technology, USA)
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application.
The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Scala Step-by-Step: Soundness ..."
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers
(Delft University of Technology, Netherlands; IRIF, France; University of Paris, France; CNRS, France; Aarhus University, Denmark)
The metatheory of Scala’s core type system—the Dependent Object Types (DOT) calculus—is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and in practice. To address some of these problems, we use a semantics-first approach to develop a logical relations model for a new version of DOT, called guarded DOT (gDOT). Our logical relations model makes use of an abstract form of step-indexing, as supported by the Iris framework, to model various forms of recursion in gDOT. To demonstrate the expressiveness of gDOT, we show that it handles Scala examples that could not be handled by previous versions of DOT, and prove using our logical relations model that gDOT provides the desired data abstraction. The gDOT type system, its semantic model, its soundness proofs, and all examples in the paper have been mechanized in Coq.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Achieving High-Performance ..."
Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Kœhler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; University of Glasgow, UK)
Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages - like C or OpenCL - force the programmer to intertwine the code describing functionality and optimizations. This results in a portability nightmare that is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.
Many emerging DSLs used in performance demanding domains such as deep learning or high-performance image processing attempt to simplify or even fully automate the optimization process. Using a high-level - often functional - language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.
In this functional pearl, we show how to employ functional programming techniques to solve this challenge with elegance. We present two functional languages that work together - each addressing a separate concern. RISE is a functional language for expressing computations using well known functional data-parallel patterns. ELEVATE is a functional language for describing optimization strategies. A high-level RISE program is transformed into a low-level form using optimization strategies written in ELEVATE . From the rewritten low-level program high-performance parallel code is automatically generated. In contrast to existing high-performance domain-specific systems with scheduling APIs, in our approach programmers are not restricted to a set of built-in operations and optimizations but freely define their own computational patterns in RISE and optimization strategies in ELEVATE in a composable and reusable way. We show how our holistic functional approach achieves competitive performance with the state-of-the-art imperative systems Halide and TVM.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Strong Functional Pearl: Harper’s ..."
Strong Functional Pearl: Harper’s Regular-Expression Matcher in Cedille
Aaron Stump, Christopher Jenkins, Stephan Spahn, and Colin McDonald
(University of Iowa, USA; University of Notre Dame, USA)
This paper describes an implementation of Harper's continuation-based regular-expression matcher as a strong functional program in Cedille; i.e., Cedille statically confirms termination of the program on all inputs. The approach uses neither dependent types nor termination proofs. Instead, a particular interface dubbed a recursion universe is provided by Cedille, and the language ensures that all programs written against this interface terminate. Standard polymorphic typing is all that is needed to check the code against the interface. This answers a challenge posed by Bove, Krauss, and Sozeau.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "SteelCore: An Extensible Concurrent ..."
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez
(Microsoft Research, USA; Microsoft Research, India; Carnegie Mellon University, USA; Inria, France; University of Ljubljana, Slovenia; CIFASIS-CONICET, Argentina)
Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself.
Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F⋆ proof assistant in a manner that enables dependently typed, effectful F⋆ programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions.
Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "A Dependently Typed Calculus ..."
A Dependently Typed Calculus with Pattern Matching and Erasure Inference
Matúš Tejiščák
(University of St. Andrews, UK)
Some parts of dependently typed programs constitute evidence of their type-correctness and, once checked, are unnecessary for execution. These parts can easily become asymptotically larger than the remaining runtime-useful computation, which can cause normally linear-time programs run in exponential time, or worse. We should not make programs run slower by just describing them more precisely.
Current dependently typed systems do not erase such computation satisfactorily. By modelling erasure indirectly through type universes or irrelevance, they impose the limitations of these means to erasure. Some useless computation then cannot be erased and idiomatic programs remain asymptotically sub-optimal.
In this paper, we explain why we need erasure, that it is different from other concepts like irrelevance, and propose a dependently typed calculus with pattern matching with erasure annotations to model it. We show that erasure in well-typed programs is sound in that it commutes with reduction. Assuming the Church-Rosser property, erasure furthermore preserves convertibility in general.
We also give an erasure inference algorithm for erasure-unannotated or partially annotated programs and prove it sound, complete, and optimal with respect to the typing rules of the calculus.
Finally, we show that this erasure method is effective in that it can not only recover the expected asymptotic complexity in compiled programs at run time, but it can also shorten compilation times.
Publisher's Version
Info
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Kindly Bent to Free Us ..."
Kindly Bent to Free Us
Gabriel Radanne, Hannes Saffrich, and Peter Thiemann
(Inria, France; University of Freiburg, Germany)
Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities.
While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper handling of resources. An important step towards handling resources is the adoption of linear and affine types that enforce single-threaded resource usage. However, the few languages supporting such types require heavy type annotations.
We present Affe, an extension of ML that manages linearity and affinity properties using kinds and constrained types. In addition Affe supports the exclusive and shared borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: it is an impure, strict, functional expression language with complete principal type inference and type abstraction. does not require any linearity annotations in expressions and supports common functional programming idioms.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Scala Step-by-Step: Soundness ..."
Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers
(Delft University of Technology, Netherlands; IRIF, France; University of Paris, France; CNRS, France; Aarhus University, Denmark)
The metatheory of Scala’s core type system—the Dependent Object Types (DOT) calculus—is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and in practice. To address some of these problems, we use a semantics-first approach to develop a logical relations model for a new version of DOT, called guarded DOT (gDOT). Our logical relations model makes use of an abstract form of step-indexing, as supported by the Iris framework, to model various forms of recursion in gDOT. To demonstrate the expressiveness of gDOT, we show that it handles Scala examples that could not be handled by previous versions of DOT, and prove using our logical relations model that gDOT provides the desired data abstraction. The gDOT type system, its semantic model, its soundness proofs, and all examples in the paper have been mechanized in Coq.
Publisher's Version
Published Artifact
Info
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Signature Restriction for ..."
Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi
(National Institute of Informatics, Japan; SOKENDAI, Japan; University of Tokyo, Japan; Kyoto University, Japan)
The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "A Quick Look at Impredicativity ..."
A Quick Look at Impredicativity
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis
(47 Degrees, Spain; Utrecht University, Netherlands; Microsoft Research, UK; DeepMind, UK)
Type inference for parametric polymorphism is wildly successful, but has always suffered from an embarrassing flaw: polymorphic types are themselves not first class. We present Quick Look, a practical, implemented, and deployable design for impredicative type inference. To demonstrate our claims, we have modified GHC, a production-quality Haskell compiler, to support impredicativity. The changes required are modest, localised, and are fully compatible with GHC's myriad other type system extensions.
Publisher's Version
Video
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Resource Types ..."
Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, and Nadia Polikarpova
(University of California at San Diego, USA; Carnegie Mellon University, USA)
This article presents liquid resource types, a technique for automatically verifying the resource consumption of functional programs. Existing resource analysis techniques trade automation for flexibility – automated techniques are restricted to relatively constrained families of resource bounds, while more expressive proof techniques admitting value-dependent bounds rely on handwritten proofs. Liquid resource types combine the best of these approaches, using logical refinements to automatically prove precise bounds on a program’s resource consumption. The type system augments refinement types with potential annotations to conduct an amortized resource analysis. Importantly, users can annotate data structure declarations to indicate how potential is allocated within the type, allowing the system to express bounds with polynomials and exponentials, as well as more precise expressions depending on program values. We prove the soundness of the type system, provide a library of flexible and reusable data structures for conducting resource analysis, and use our prototype implementation to automatically verify resource bounds that previously required a manual proof.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Raising Expectations: Automating ..."
Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang, David M. Kahn, and Jan Hoffmann
(Carnegie Mellon University, USA)
This article presents a type-based analysis for deriving upper bounds on the expected execution cost of probabilistic programs. The analysis is naturally compositional, parametric in the cost model, and supports higher-order functions and inductive data types. The derived bounds are multivariate polynomials that are functions of data structures. Bound inference is enabled by local type rules that reduce type inference to linear constraint solving. The type system is based on the potential method of amortized analysis and extends automatic amortized resource analysis (AARA) for deterministic programs. A main innovation is that bounds can contain symbolic probabilities, which may appear in data structures and function arguments. Another contribution is a novel soundness proof that establishes the correctness of the derived bounds with respect to a distribution-based operational cost semantics that also includes nontrivial diverging behavior. For cost models like time, derived bounds imply termination with probability one. To highlight the novel ideas, the presentation focuses on linear potential and a core language. However, the analysis is implemented as an extension of Resource Aware ML and supports polynomial bounds and user defined data structures. The effectiveness of the technique is evaluated by analyzing the sample complexity of discrete distributions and with a novel average-case estimation for deterministic programs that combines expected cost analysis with statistical methods.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Sparcl: A Language for Partially-Invertible ..."
Sparcl: A Language for Partially-Invertible Computation
Kazutaka Matsuda and Meng Wang
(Tohoku University, Japan; University of Bristol, UK)
Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing on partially-invertible functions—functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible.
We develop a language Sparcl for programming such functions in a natural way, where partial-invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the “partially” part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language Sparcl is linear-typed, and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language, and prove that Sparcl correctly guarantees invertibility for its programs. We demonstrate the expressiveness of Sparcl with examples including tree rebuilding from preorder and inorder traversals and Huffman coding.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Composing and Decomposing ..."
Composing and Decomposing Op-Based CRDTs with Semidirect Products
Matthew Weidner, Heather Miller, and Christopher Meiklejohn
(Carnegie Mellon University, USA)
Operation-based Conflict-free Replicated Data Types (CRDTs) are eventually consistent replicated data types that automatically resolve conflicts between concurrent operations. Op-based CRDTs must be designed differently for each data type, and current designs use ad-hoc techniques to handle concurrent operations that do not naturally commute. We present a new construction, the semidirect product of op-based CRDTs, which combines the operations of two CRDTs into one while handling conflicts between their concurrent operations in a uniform way. We demonstrate the construction's utility by using it to construct novel CRDTs, as well as decomposing several existing CRDTs as semidirect products of simpler CRDTs. Although it reproduces common CRDT semantics, the semidirect product can be viewed as a restricted kind of operational transformation, thus forming a bridge between these two opposing techniques for constructing replicated data types.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Higher-Order Demand-Driven ..."
Higher-Order Demand-Driven Symbolic Evaluation
Zachary Palmer, Theodore Park, Scott Smith, and Shiwei Weng
(Swarthmore College, USA; Johns Hopkins University, USA)
Symbolic backwards execution (SBE) is a useful variation on standard forward symbolic evaluation; it allows a symbolic evaluation to start anywhere in the program and proceed by executing in reverse to the program start. SBE brings goal-directed reasoning to symbolic evaluation and has proven effective in e.g. automated test generation for imperative languages.
In this paper we define DDSE, a novel SBE which operates on a functional as opposed to imperative language; furthermore, it is defined as a natural extension of a backwards-executing interpreter. We establish the soundness of DDSE and define a test generation algorithm for this toy language. We report on an initial reference implementation to confirm the correctness of the principles.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Retrofitting Parallelism onto ..."
Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
Publisher's Version
Info
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Staged Selective Parser Combinators ..."
Staged Selective Parser Combinators
Jamie Willis, Nicolas Wu, and Matthew Pickering
(Imperial College London, UK; University of Bristol, UK)
Parser combinators are a middle ground between the fine control of hand-rolled parsers and the high-level almost grammar-like appearance of parsers created via parser generators. They also promote a cleaner, compositional design for parsers. Historically, however, they cannot match the performance of their counterparts.
This paper describes how to compile parser combinators into parsers of hand-written quality. This is done by leveraging the static information present in the grammar by representing it as a tree. However, in order to exploit this information, it will be necessary to drop support for monadic computation since this generates dynamic structure. Selective functors can help recover lost functionality in the absence of monads, and the parser tree can be partially evaluated with staging. This is implemented in a library called Parsley.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Staged Selective Parser Combinators ..."
Staged Selective Parser Combinators
Jamie Willis, Nicolas Wu, and Matthew Pickering
(Imperial College London, UK; University of Bristol, UK)
Parser combinators are a middle ground between the fine control of hand-rolled parsers and the high-level almost grammar-like appearance of parsers created via parser generators. They also promote a cleaner, compositional design for parsers. Historically, however, they cannot match the performance of their counterparts.
This paper describes how to compile parser combinators into parsers of hand-written quality. This is done by leveraging the static information present in the grammar by representing it as a tree. However, in order to exploit this information, it will be necessary to drop support for monadic computation since this generates dynamic structure. Selective functors can help recover lost functionality in the absence of monads, and the parser tree can be partially evaluated with staging. This is implemented in a library called Parsley.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Effect Handlers, Evidently ..."
Effect Handlers, Evidently
Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen
(Microsoft Research, USA; University of Tübingen, Germany; University of Edinburgh, UK)
Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even _too_ powerful. In this article we define a restriction of general effect handlers with _scoped resumptions_. We argue one can still express all important effects, while improving reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers, which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations _in place_ (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Liquid Information Flow Control ..."
Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama
(University of California at San Diego, USA; Carnegie Mellon University, USA; Technion, Israel; Massachusetts Institute of Technology, USA)
We present Lifty, a domain-specific language for data-centric applications that manipulate sensitive data. A Lifty programmer annotates the sources of sensitive data with declarative security policies, and the language statically and automatically verifies that the application handles the data according to the policies. Moreover, if verification fails, Lifty suggests a provably correct repair, thereby easing the programmer burden of implementing policy enforcing code throughout the application.
The main insight behind Lifty is to encode information flow control using liquid types, an expressive yet decidable type system. Liquid types enable fully automatic checking of complex, data dependent policies, and power our repair mechanism via type-driven error localization and patch synthesis. Our experience using Lifty to implement three case studies from the literature shows that (1) the Lifty policy language is sufficiently expressive to specify many real-world policies, (2) the Lifty type checker is able to verify secure programs and find leaks in insecure programs quickly, and (3) even if the programmer leaves out all policy enforcing code, the Lifty repair engine is able to patch all leaks automatically within a reasonable time.
Publisher's Version
Published Artifact
Artifacts Available
Artifacts Functional
Proc. ACM Program. Lang., vol. 4, issue ICFP: "TLC: Temporal Logic of Distributed ..."
TLC: Temporal Logic of Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, and Xizhe Yin
(University of California at Riverside, USA)
Distributed systems are critical to reliable and scalable computing; however, they are complicated in nature and prone to bugs. To manage this complexity, network middleware has been traditionally built in layered stacks of components.We present a novel approach to compositional verification of distributed stacks to verify each component based on only the specification of lower components. We present TLC (Temporal Logic of Components), a novel temporal program logic that offers intuitive inference rules for verification of both safety and liveness properties of functional implementations of distributed components. To support compositional reasoning, we define a novel transformation on the assertion language that lowers the specification of a component to be used as a subcomponent. We prove the soundness of TLC and the lowering transformation with respect to a novel operational semantics for stacks of composed components in partially synchronous networks. We successfully apply TLC to compose and verify a stack of fundamental distributed components.
Publisher's Version
Proc. ACM Program. Lang., vol. 4, issue ICFP: "Computation Focusing ..."
Computation Focusing
Nick Rioux and Steve Zdancewic
(University of Pennsylvania, USA)
Focusing is a technique from proof theory that exploits type information to prune inessential nondeterminism from proof search procedures. Viewed through the lens of the Curry-Howard correspondence, a focused typing derivation yields terms in normal form. This paper explores how to exploit focusing for reasoning about contextual equivalences and full abstraction. We present a focused polymorphic call-by-push-value calculus and prove a computational completeness result: for every well-typed term, there exists a focused term that is βη-equivalent to it. This completeness result yields a powerful way to refine the context lemmas for establishing contextual equivalences, cutting down the set that must be considered to just focused contexts. The paper demonstrates the application of focusing to establish program equivalences, including free theorems. It also uses focusing to prove full abstraction of a translation of the pure, total call-by-push-value language into a language with divergence and simple effect types, yielding a novel solution to a simple-to-state, but hitherto difficult to solve problem.
Publisher's Version