The VM Already Knew That: Leveraging Compile-Time Knowledge to Optimize Gradual Typing
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 OctDisplayed time zone: Tijuana, Baja California change
13:30 - 15:00 | |||
13:30 22mTalk | Sound Gradual Typing: Only Mostly Dead OOPSLA Spenser Andrew Bauman Indiana University, USA, Sam Tobin-Hochstadt Indiana University, Jeremy G. Siek Indiana University, USA, CF Bolz-Tereick DOI | ||
13:52 22mTalk | Sound Gradual Typing Is Nominally Alive and Well OOPSLA DOI | ||
14:15 22mTalk | 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 22mTalk | 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 |