Write a Blog >>
SPLASH 2019
Sun 20 - Fri 25 October 2019 Athens, Greece
Thu 24 Oct 2019 11:22 - 11:45 at Attica - Language Design Chair(s): Tiark Rompf

WebAssembly (Wasm) is a safe, portable virtual instruction set that can be hosted in a wide range of environments, such as a Web browser. It is a low-level language whose instructions are intended to compile directly to bare hardware. While the initial version of Wasm focussed on single-threaded computation, a recent proposal extends it with low-level support for multiple threads and atomic instructions for synchronised access to shared memory. To support the correct compilation of concurrent programs, it is necessary to give a suitable specification of its memory model.

Wasm's language definition is based on a fully formalised specification that carefully avoids undefined behaviour. We present a substantial extension to this semantics, incorporating a relaxed memory model, along with a few proposed extensions. Wasm's memory model is unique in that its linear address space can be dynamically grown during execution, while all accesses are bounds-checked. This leads to the novel problem of specifying how observations about the size of the memory can propagate between threads. We argue that, considering desirable compilation schemes, we cannot give a sequentially consistent semantics to memory growth.

We show that our model provides sequential consistency for data-race-free executions (SC-DRF). However, because Wasm is to run on the Web, we must also consider interoperability of its model with that of JavaScript. We show, by counter-example, that JavaScript's memory model is not SC-DRF, in contrast to what is claimed in its specification. We propose two axiomatic conditions that should be added to the JavaScript model to correct this difference.

We also describe a prototype SMT-based litmus tool which acts as an oracle for our axiomatic model, visualising its behaviours, including memory resizing.

Thu 24 Oct

Displayed time zone: Beirut change

11:00 - 12:30
Language DesignOOPSLA at Attica
Chair(s): Tiark Rompf Purdue University
11:00
22m
Talk
DeepSEA: A Language for Certified System Software
OOPSLA
Vilhelm Sjöberg Yale University, Yuyang Sang Yale University, Shu-chun Weng Yale University, Zhong Shao Yale University
DOI Pre-print
11:22
22m
Talk
Weakening WebAssembly
OOPSLA
Conrad Watt University of Cambridge, Andreas Rossberg Dfinity Stiftung, Jean Pichon-Pharabod University of Cambridge
DOI
11:45
22m
Talk
Safer Smart Contract Programming with Scilla
OOPSLA
Ilya Sergey Yale-NUS College and National University of Singapore, Vaivaswatha Nagaraj Zilliqa Research, Jacob Johannsen Zilliqa Research, Amrit Kumar Zilliqa Research, Anton Trunov Zilliqa Research, Ken Chan Zilliqa Research
DOI Pre-print File Attached
12:07
22m
Talk
Scala Implicits Are Everywhere: A Large-Scale Study of the Use of Scala Implicits in the Wild
OOPSLA
Filip Křikava Czech Technical University, Heather Miller Carnegie Mellon University, Jan Vitek Northeastern University
DOI Pre-print