Show simple item record

dc.contributor.authorPichon-Pharabod, Jeanen
dc.contributor.authorWatt, Conraden
dc.contributor.authorRossberg, Andreasen
dc.date.accessioned2020-02-13T00:31:22Z
dc.date.available2020-02-13T00:31:22Z
dc.date.issued2019-10-10en
dc.identifier.issn2475-1421
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/302089
dc.description.abstractWebAssembly (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.
dc.publisherAssociation for Computing Machinery
dc.rightsAttribution 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.titleWeakening WebAssemblyen
dc.typeConference Object
prism.issueIdentifierOOPSLAen
prism.numberarticle 133en
prism.publicationDate2019en
prism.publicationNameProceedings of the ACM on Programming Languagesen
prism.volume3en
dc.identifier.doi10.17863/CAM.49164
dcterms.dateAccepted2019-09-17en
rioxxterms.versionofrecord10.1145/3360559en
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/en
rioxxterms.licenseref.startdate2019-10-10en
dc.contributor.orcidWatt, Conrad [0000-0002-0596-877X]
dc.identifier.eissn2475-1421
rioxxterms.typeConference Paper/Proceeding/Abstracten
pubs.funder-project-idEPSRC (EP/K008528/1)
pubs.funder-project-idEPSRC (1790117)
pubs.conference-nameOOPSLA 2019: Object-Oriented Programming Systems, Languages and Applicationsen
pubs.conference-start-date2019-10-23en


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International
Except where otherwise noted, this item's licence is described as Attribution 4.0 International