Write a Blog >>
ECOOP 2021
Sun 11 - Sat 17 July 2021 Online
co-located with ECOOP and ISSTA 2021
Wed 14 Jul 2021 18:50 - 19:10 at ECOOP 1 - Types (time band 1) Chair(s): Sam Tobin-Hochstadt
Fri 16 Jul 2021 10:40 - 11:00 at ECOOP 1 - Types / Program Analysis (time band 3) Chair(s): George Fourtounis

Compilers that can type check compilation units in parallel can make more efficient use of multi-core architectures, which are nowadays widespread. Developing parallel type checker implementations is complicated by the need to handle concurrency and synchronization between checking of compilation units. Dependencies between compilation units are induced by name resolution, and a parallel type checker needs to ensure that units have defined all relevant names before other units do a lookup. Mutually recursive references and implicitly discovered dependencies between compilation units preclude determining a static compilation order for many programming languages.

In this paper, we present a new framework for implementing hierarchical type checkers that provides implicit parallel execution in the presence of dynamic, mutually recursive, dependencies between compilation units. The resulting type checkers can be written without explicit handling of communication or synchronization with different compilation units. We achieve this by providing type checkers with an API for name resolution based on scope graphs, a language-independent formalism that supports a wide range of binding patterns. We introduce the notion of \emph{scope state} to ensure safe name resolution. Scope state tracks the completeness of a scope, and is used to decide whether a scope graph query between compilation units must be delayed. Our framework is implemented in Java using the actor paradigm. We evaluated our approach by parallelizing the solver for Statix, a meta-language for type checkers based on scope graphs, using our framework. This parallelizes every Statix-based type checker, provided its specification follows a split declaration-type style. Benchmarks show that the approach results in speedups up to approximately $3x$ on $6$ cores for the parallel Statix solver for larger projects.

Scope State: Presentation (scope-states.pdf)844KiB

Wed 14 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

18:30 - 19:30
Types (time band 1)ECOOP Technical Papers at ECOOP 1
Chair(s): Sam Tobin-Hochstadt Indiana University
18:30
20m
Talk
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types
ECOOP Technical Papers
Anish Tondwalkar University of California, San Diego, Matthew Kolosick University of California, San Diego, Ranjit Jhala University of California at San Diego
DOI
18:50
20m
Talk
Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers
ECOOP Technical Papers
Hendrik van Antwerpen Delft University of Technology, Eelco Visser Delft University of Technology
DOI File Attached
19:10
20m
Talk
Idris 2: Quantitative Type Theory in Practice
ECOOP Technical Papers
Edwin Brady University of St Andrews, UK
DOI Media Attached

Fri 16 Jul

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:00 - 11:20
Types / Program Analysis (time band 3)ECOOP Technical Papers at ECOOP 1
Chair(s): George Fourtounis University of Athens
10:00
20m
Talk
Accelerating Object-Sensitive Pointer Analysis by Exploiting Object Containment and Reachability
ECOOP Technical Papers
Dongjie He University of New South Wales, Jingbo Lu UNSW Sydney, Yaoqing Gao Huawei Canada, Jingling Xue UNSW
DOI Pre-print
10:20
20m
Talk
Lossless, Persisted Summarization of Static Callgraph, Points-To and Data-Flow AnalysisDistinguished Paper
ECOOP Technical Papers
Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann Technical University Dortmund, Eric Bodden University of Paderborn; Fraunhofer IEM
Link to publication DOI Pre-print
10:40
20m
Talk
Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers
ECOOP Technical Papers
Hendrik van Antwerpen Delft University of Technology, Eelco Visser Delft University of Technology
DOI File Attached
11:00
20m
Talk
Idris 2: Quantitative Type Theory in Practice
ECOOP Technical Papers
Edwin Brady University of St Andrews, UK
DOI Media Attached