Repository logo
 

Weakening WebAssembly

Published version
Peer-reviewed

Type

Conference Object

Change log

Authors

Pichon-Pharabod, Jean 
Rossberg, Andreas 

Abstract

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 operational 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 guarantees Sequential Consistency of Data-Race-Free programs (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.

Description

Keywords

4613 Theory Of Computation, 46 Information and Computing Sciences, 4612 Software Engineering

Journal Title

Proceedings of the ACM on Programming Languages

Conference Name

OOPSLA 2019: Object-Oriented Programming Systems, Languages and Applications

Journal ISSN

2475-1421
2475-1421

Volume Title

3

Publisher

Association for Computing Machinery
Sponsorship
Engineering and Physical Sciences Research Council (EP/K008528/1)
Engineering and Physical Sciences Research Council (1790117)