-
Graph IRs for Impure Higher-Order Languages (Technical Report)
Authors:
Oliver Bračevac,
Guannan Wei,
Songlin Jia,
Supun Abeysinghe,
Yuxuan Jiang,
Yuyan Bao,
Tiark Rompf
Abstract:
This is a companion report for the OOPSLA 2023 paper of the same title, presenting a detailed end-to-end account of the $λ^*_{\mathsf{G}}$ graph IR, at a level of detail beyond a regular conference paper. Our first concern is adequacy and soundness of $λ^*_{\mathsf{G}}$, which we derive from a direct-style imperative functional language (a variant of Bao et al.'s $λ^*$-calculus with reachability t…
▽ More
This is a companion report for the OOPSLA 2023 paper of the same title, presenting a detailed end-to-end account of the $λ^*_{\mathsf{G}}$ graph IR, at a level of detail beyond a regular conference paper. Our first concern is adequacy and soundness of $λ^*_{\mathsf{G}}$, which we derive from a direct-style imperative functional language (a variant of Bao et al.'s $λ^*$-calculus with reachability types and a simple effect system) by a series of type-preserving translations into a calculus in monadic normalform (MNF). Static reachability types and effects entirely inform $λ^*_{\mathsf{G}}$'s dependency synthesis. We argue for its adequacy by proving its functional properties along with dependency safety via progress and preservation lemmas with respect to a notion of call-by-value (CBV) reduction that checks the observed order of effects.
Our second concern is establishing the correctness of $λ^*_{\mathsf{G}}$'s equational rules that drive compiler optimizations (e.g., DCE, $λ$-hoisting, etc.), by proving contextual equivalence using logical relations. A key insight is that the functional properties of dependency synthesis permit a logical relation on $λ^*_{\mathsf{G}}$ in MNF in terms of previously developed logical relations for the direct-style $λ^*$-calculus.
Finally, we also include a longer version of the conference paper's section on code generation and code motion for $λ^*_{\mathsf{G}}$ as implemented in Scala~LMS.
△ Less
Submitted 14 September, 2023;
originally announced September 2023.
-
Modeling Reachability Types with Logical Relations
Authors:
Yuyan Bao,
Guannan Wei,
Oliver Bračevac,
Tiark Rompf
Abstract:
Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages. While key type soundness results for reachability types have been established using syntactic techniques in prior work, stronger metatheoretic properties have so far been unexplored. This paper presents an alternative semantic model of reachability types using logical relations…
▽ More
Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages. While key type soundness results for reachability types have been established using syntactic techniques in prior work, stronger metatheoretic properties have so far been unexplored. This paper presents an alternative semantic model of reachability types using logical relations, providing a framework in which to study key properties of interest such as (1) semantic type soundness, including of not syntactically well-typed code fragments, (2) termination, especially in the presence of higher-order state, and (3) program equivalence, especially reordering of non-interfering expressions for parallelization or compiler optimization.
△ Less
Submitted 11 September, 2023;
originally announced September 2023.
-
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Authors:
Guannan Wei,
Oliver Bračevac,
Songlin Jia,
Yuyan Bao,
Tiark Rompf
Abstract:
Reachability types are a recent proposal that has shown promise in scaling to higher-order but monomorphic settings, tracking aliasing and separation on top of a substrate inspired by separation logic. The prior $λ^*$ reachability type system qualifies types with sets of reachable variables and guarantees separation if two terms have disjoint qualifiers. However, naive extensions with type polymor…
▽ More
Reachability types are a recent proposal that has shown promise in scaling to higher-order but monomorphic settings, tracking aliasing and separation on top of a substrate inspired by separation logic. The prior $λ^*$ reachability type system qualifies types with sets of reachable variables and guarantees separation if two terms have disjoint qualifiers. However, naive extensions with type polymorphism and/or precise reachability polymorphism are unsound, making $λ^*$ unsuitable for adoption in real languages. Combining reachability and type polymorphism that is precise, sound, and parametric remains an open challenge.
This paper presents a rethinking of the design of reachability tracking and proposes a solution to the key challenge of reachability polymorphism. Instead of always tracking the transitive closure of reachable variables as in the original design, we only track variables reachable in a single step and compute transitive closures only when necessary, thus preserving chains of reachability over known variables that can be refined using substitution. To enable this property, we introduce a new freshness qualifier, which indicates variables whose reachability sets may grow during evaluation steps. These ideas yield the simply-typed $λ^\diamond$-calculus with precise lightweight, i.e., quantifier-free, reachability polymorphism, and the $\mathsf{F}_{<:}^\diamond$-calculus with bounded parametric polymorphism over types and reachability qualifiers. We prove type soundness and a preservation of separation property in Coq.
△ Less
Submitted 25 July, 2023;
originally announced July 2023.
-
Type-safe, Polyvariadic Event Correlation
Authors:
Oliver Bračevac,
Guido Salvaneschi,
Sebastian Erdweg,
Mira Mezini
Abstract:
The pivotal role that event correlation technology plays in todays applications has lead to the emergence of different families of event correlation approaches with a multitude of specialized correlation semantics, including computation models that support the composition and extension of different semantics. However, type-safe embeddings of extensible and composable event patterns into statically…
▽ More
The pivotal role that event correlation technology plays in todays applications has lead to the emergence of different families of event correlation approaches with a multitude of specialized correlation semantics, including computation models that support the composition and extension of different semantics. However, type-safe embeddings of extensible and composable event patterns into statically-typed general-purpose programming languages have not been systematically explored so far. Event correlation technology has often adopted well-known and intuitive notations from database queries, for which approaches to type-safe embedding do exist. However, we argue in the paper that these approaches, which are essentially descendants of the work on monadic comprehensions, are not well-suited for event correlations and, thus, cannot without further ado be reused/re-purposed for embedding event patterns. To close this gap we propose PolyJoin, a novel approach to type-safe embedding for fully polyvariadic event patterns with polymorphic correlation semantics. Our approach is based on a tagless final encoding with uncurried higher-order abstract syntax (HOAS) representation of event patterns with n variables, for arbitrary $n \in \mathbb{N}$. Thus, our embedding is defined in terms of the host language without code generation and exploits the host language type system to model and type check the type system of the pattern language. Hence, by construction it impossible to define ill-typed patterns. We show that it is possible to have a purely library-level embedding of event patterns, in the familiar join query notation, which is not restricted to monads. PolyJoin is practical, type-safe and extensible. An implementation of it in pure multicore OCaml is readily usable.
△ Less
Submitted 5 July, 2019;
originally announced July 2019.
-
A Co-contextual Type Checker for Featherweight Java (incl. Proofs)
Authors:
Edlira Kuci,
Sebastian Erdweg,
Oliver Bračevac,
Andi Bejleri,
Mira Mezini
Abstract:
This paper addresses compositional and incremental type checking for object-oriented programming languages. Recent work achieved incremental type checking for structurally typed functional languages through co-contextual typing rules, a constraint-based formulation that removes any context dependency for expression typings. However, that work does not cover key features of object-oriented language…
▽ More
This paper addresses compositional and incremental type checking for object-oriented programming languages. Recent work achieved incremental type checking for structurally typed functional languages through co-contextual typing rules, a constraint-based formulation that removes any context dependency for expression typings. However, that work does not cover key features of object-oriented languages: Subtype polymorphism, nominal typing, and implementation inheritance. Type checkers encode these features in the form of class tables, an additional form of typing context inhibiting incrementalization. In the present work, we demonstrate that an appropriate co-contextual notion to class tables exists, paving the way to efficient incremental type checkers for object-oriented languages. This yields a novel formulation of Igarashi et al.'s Featherweight Java (FJ) type system, where we replace class tables by the dual concept of class table requirements and class table operations by dual operations on class table requirements. We prove the equivalence of FJ's type system and our co-contextual formulation. Based on our formulation, we implemented an incremental FJ type checker and compared its performance against javac on a number of realistic example programs.
△ Less
Submitted 23 May, 2018; v1 submitted 16 May, 2017;
originally announced May 2017.
-
CPL: A Core Language for Cloud Computing -- Technical Report
Authors:
Oliver Bračevac,
Sebastian Erdweg,
Guido Salvaneschi,
Mira Mezini
Abstract:
Running distributed applications in the cloud involves deployment. That is, distribution and configuration of application services and middleware infrastructure. The considerable complexity of these tasks resulted in the emergence of declarative JSON-based domain-specific deployment languages to develop deployment programs. However, existing deployment programs unsafely compose artifacts written i…
▽ More
Running distributed applications in the cloud involves deployment. That is, distribution and configuration of application services and middleware infrastructure. The considerable complexity of these tasks resulted in the emergence of declarative JSON-based domain-specific deployment languages to develop deployment programs. However, existing deployment programs unsafely compose artifacts written in different languages, leading to bugs that are hard to detect before run time. Furthermore, deployment languages do not provide extension points for custom implementations of existing cloud services such as application-specific load balancing policies.
To address these shortcomings, we propose CPL (Cloud Platform Language), a statically-typed core language for programming both distributed applications as well as their deployment on a cloud platform. In CPL, application services and deployment programs interact through statically typed, extensible interfaces, and an application can trigger further deployment at run time. We provide a formal semantics of CPL and demonstrate that it enables type-safe, composable and extensible libraries of service combinators, such as load balancing and fault tolerance.
△ Less
Submitted 5 February, 2016; v1 submitted 2 February, 2016;
originally announced February 2016.
