Write a Blog >>
SPLASH 2017
Sun 22 - Fri 27 October 2017 Vancouver, Canada
Wed 25 Oct 2017 14:15 - 14:37 at Regency A - Gradual Types and Memory Chair(s): Jennifer B. Sartor

Programmers in dynamic languages wishing to constrain and understand the behavior of their programs may turn to gradually-typed languages, which allow types to be specified optionally and check values at the boundary between dynamic and static code. Unfortunately, the performance cost of these run-time checks can be severe, slowing down execution by at least 10x when checks are present. Modern virtual machines (VMs) for dynamic languages use speculative techniques to improve performance: If a particular value was seen once, it is likely that similar values will be seen in the future. They combine optimization-relevant properties of values into cacheable “shapes”, then use a single shape check to subsume checks for each property. Values with the same memory layout or the same field types have the same shape. This greatly reduces the amount of type checking that needs to be performed at run-time to execute dynamic code. While very valuable to the VM’s optimization, these checks do little to benefit the programmer aside from improving performance. We present in this paper a design for intrinsic object contracts, which makes the obligations of gradually-typed languages’ type checks an intrinsic part of object shapes, and thus can subsume run-time type checks into existing shape checks, eliminating redundant checks entirely. With an implementation on a VM for JavaScript used as a target for SafeTypeScript’s safety guarantees, we demonstrate slowdown averaging 7% in fully-typed code relative to unchecked code, and no more than 45% in pessimal configurations.

Wed 25 Oct

Displayed time zone: Tijuana, Baja California change

13:30 - 15:00
Gradual Types and MemoryOOPSLA at Regency A
Chair(s): Jennifer B. Sartor Vrije Universiteit Brussel
13:30
22m
Talk
Sound Gradual Typing: Only Mostly Dead
OOPSLA
Spenser Andrew Bauman Indiana University, USA, Sam Tobin-Hochstadt Indiana University, Jeremy G. Siek Indiana University, USA, Carl Friedrich Bolz-Tereick
DOI
13:52
22m
Talk
Sound Gradual Typing Is Nominally Alive and Well
OOPSLA
Fabian Muehlboeck Cornell University, Ross Tate Cornell University
DOI
14:15
22m
Talk
The VM Already Knew That: Leveraging Compile-Time Knowledge to Optimize Gradual Typing
OOPSLA
Gregor Richards University of Waterloo, Ellen Arteca University of Waterloo, Canada, Alexi Turcotte University of Waterloo
DOI
14:37
22m
Talk
Model Checking Copy Phases of Concurrent Copying Garbage Collection with Various Memory Models
OOPSLA
Tomoharu Ugawa Kochi University of Technology, Japan, Tatsuya Abe Chiba Institute of Technology, Japan, Toshiyuki Maeda Chiba Institute of Technology, Japan
DOI