Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Tue 22 Oct 2019 11:00 - 11:30 at Abbey - Session #2 Chair(s): Anthony Canino

One form of type checking used in gradually typed language is transient type checking: whenever an object `flows’ through code with a type annotation, the object is dynamically checked to ensure it has the methods required by the annotation.

Although naive implementations of transient type checks have a high runtime overhead, just-in-time compilation and optimisation in virtual machines can eliminate much of this overhead. Unfortunately the improvement is not uniform: while most type checks can be optimised away, some will significantly decrease a program’s performance, and some may even increase it.

In this paper, we refine the so called ``Takikawa'' protocol, and use it to identify which type annotations have the greatest effects on performance. In particular, we show how graphing the performance of such benchmarks when varying which type annotations are present in the source code can be used to discern potential patterns in performance. We demonstrate our approach by testing the Moth virtual machine: for many of the benchmarks where Moth’s transient type checking impacts performance, we have been able to identify one or two specific type annotations that are the likely cause. Without these type annotations, the performance impact of transient type checking becomes negligible.

Using our technique programmers can optimise programs by removing expensive type checks, and VM engineers can identify new opportunities for compiler optimisation.

Tue 22 Oct

Displayed time zone: Beirut change

11:00 - 12:30
Session #2VMIL at Abbey
Chair(s): Anthony Canino SUNY Binghamton
11:00
30m
Full-paper
Which of my Transient Type Checks are not (Almost) Free?
VMIL
Isaac Oscar Gariano Victoria University of Wellington, Richard Roberts Victoria University of Wellington, Stefan Marr University of Kent, Michael Homer Victoria University of Wellington, James Noble Victoria University of Wellington
11:30
30m
Full-paper
Efficient Fail-Fast Dynamic Subtype Checking
VMIL
Rohan Padhye University of California, Berkeley, Koushik Sen University of California, Berkeley
Pre-print
12:00
15m
Talk
Towards Gradual Checking of Reference Capabilities
VMIL
Kiko Fernandez-Reyes Uppsala University, Isaac Oscar Gariano Victoria University of Wellington, James Noble Victoria University of Wellington, Tobias Wrigstad Uppsala University
Pre-print
12:15
15m
Talk
Formal Verification of JIT by Symbolic Execution
VMIL