Which of my Transient Type Checks are not (Almost) Free?
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 OctDisplayed time zone: Beirut change
11:00 - 12:30 | |||
11:00 30mFull-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 30mFull-paper | Efficient Fail-Fast Dynamic Subtype Checking VMIL Pre-print | ||
12:00 15mTalk | 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 15mTalk | Formal Verification of JIT by Symbolic Execution VMIL Boris Shingarov LabWare |