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 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 Times are displayed in time zone: Beirut change
|11:00 - 11:22|
|DeepSEA: A Language for Certified System Software|
Vilhelm SjöbergYale University, Yuyang SangYale University, Shu-chun WengYale University, Zhong ShaoYale UniversityDOI Pre-print
|11:22 - 11:45|
Conrad WattUniversity of Cambridge, Andreas RossbergDfinity Stiftung, Jean Pichon-PharabodUniversity of CambridgeDOI
|11:45 - 12:07|
|Safer Smart Contract Programming with Scilla|
Ilya SergeyYale-NUS College and National University of Singapore, Vaivaswatha NagarajZilliqa Research, Jacob JohannsenZilliqa Research, Amrit KumarZilliqa Research, Anton TrunovZilliqa Research, Ken ChanZilliqa ResearchDOI Pre-print File Attached
|12:07 - 12:30|
|Scala Implicits Are Everywhere: A Large-Scale Study of the Use of Scala Implicits in the Wild|
Filip KřikavaCzech Technical University, Heather MillerCarnegie Mellon University, Jan VitekNortheastern UniversityDOI Pre-print