{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:31:28Z","timestamp":1761611488523,"version":"3.41.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K008528\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>\n          <jats:p>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.<\/jats:p>\n          <jats:p>We also describe a prototype SMT-based litmus tool which acts as an oracle for our axiomatic model, visualising its behaviours, including memory resizing.<\/jats:p>","DOI":"10.1145\/3360559","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Weakening WebAssembly"],"prefix":"10.1145","volume":"3","author":[{"given":"Conrad","family":"Watt","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Andreas","family":"Rossberg","sequence":"additional","affiliation":[{"name":"Dfinity Stiftung, Germany"}]},{"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429099"},{"volume-title":"The Problem of Programming Language Concurrency Semantics","author":"Batty Mark","key":"e_1_2_2_6_1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_9_1","unstructured":"Mark Batty and Peter Sewell. 2014. The Thin-air Problem. https:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/notes42.html .  Mark Batty and Peter Sewell. 2014. The Thin-air Problem. https:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/notes42.html ."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065042"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2001252.2001255"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"volume-title":"Axiomatically. In Proceedings of the 16th European Symposium on Programming (ESOP\u201907)","year":"2007","author":"Cenciarelli Pietro","key":"e_1_2_2_14_1"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_2_2_16_1","unstructured":"ECMA International. 2018a. ECMAScript 2018 Language Specification - Data Race Freedom. https:\/\/www.ecmainternational.org\/ecma- 262\/9.0\/index.html#sec- data- race- freedom .  ECMA International. 2018a. ECMAScript 2018 Language Specification - Data Race Freedom. https:\/\/www.ecmainternational.org\/ecma- 262\/9.0\/index.html#sec- data- race- freedom ."},{"key":"e_1_2_2_17_1","unstructured":"ECMA International. 2018b. ECMAScript 2018 Language Specification - Memory Model. https:\/\/www.ecma- international. org\/ecma- 262\/9.0\/index.html#sec- memory- model .  ECMA International. 2018b. ECMAScript 2018 Language Specification - Memory Model. https:\/\/www.ecma- international. org\/ecma- 262\/9.0\/index.html#sec- memory- model ."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009839"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-7315(92)90052-O"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Andreas Haas Andreas Rossberg Derek Schuff Ben Titzer Dan Gohman Luke Wagner Alon Zakai JF Bastien and Michael Holman. 2017. Bringing the Web up to Speed with WebAssembly. In Principles of Programming Languages (POPL).  Andreas Haas Andreas Rossberg Derek Schuff Ben Titzer Dan Gohman Luke Wagner Alon Zakai JF Bastien and Michael Holman. 2017. Bringing the Web up to Speed with WebAssembly. In Principles of Programming Languages (POPL).","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_2_2_23_1","unstructured":"Lars T Hansen. 2017. Resizing details \/ underspecification. https:\/\/github.com\/WebAssembly\/threads\/issues\/26 .  Lars T Hansen. 2017. Resizing details \/ underspecification. https:\/\/github.com\/WebAssembly\/threads\/issues\/26 ."},{"key":"e_1_2_2_24_1","unstructured":"David Herman Luke Wagner and Alon Zakai. 2014. asm.js. http:\/\/asmjs.org\/spec\/latest .  David Herman Luke Wagner and Alon Zakai. 2014. asm.js. http:\/\/asmjs.org\/spec\/latest ."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11947950_7"},{"key":"e_1_2_2_26_1","unstructured":"David Howells Paul E. McKenney Will Deacon and Peter Zijlstra. 2019. Linux Kernel Memory Barriers. https:\/\/www. kernel.org\/doc\/Documentation\/memory- barriers.txt .  David Howells Paul E. McKenney Will Deacon and Peter Zijlstra. 2019. Linux Kernel Memory Barriers. https:\/\/www. kernel.org\/doc\/Documentation\/memory- barriers.txt ."},{"key":"e_1_2_2_27_1","unstructured":"Jukka Jyl\u00e4nki. 2015. Emscripten gains experimental pthreads support! https:\/\/groups.google.com\/forum\/#!topic\/emscriptendiscuss\/gQQRjajQ6iY .  Jukka Jyl\u00e4nki. 2015. Emscripten gains experimental pthreads support! https:\/\/groups.google.com\/forum\/#!topic\/emscriptendiscuss\/gQQRjajQ6iY ."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062352"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9452-x"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"volume-title":"EMME: A Formal Tool for ECMAScript Memory Model Evaluation. In Tools and Algorithms for the Construction and Analysis of Systems","year":"2018","author":"Mattarei Cristian","key":"e_1_2_2_34_1"},{"volume-title":"N4375: Out-of-Thin-Air Execution is Vacuous. C++ Standards Committee Papers","year":"2005","author":"McKenney Paul E.","key":"e_1_2_2_35_1"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983997"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_2_2_40_1","unstructured":"Andreas Rossberg. 2018. Reference Types Proposal for WebAssembly. https:\/\/github.com\/WebAssembly\/reference- types .  Andreas Rossberg. 2018. Reference Types Proposal for WebAssembly. https:\/\/github.com\/WebAssembly\/reference- types ."},{"key":"e_1_2_2_41_1","unstructured":"Andreas Rossberg. 2019. GC Extension. https:\/\/github.com\/WebAssembly\/gc\/blob\/master\/proposals\/gc\/Overview.md .  Andreas Rossberg. 2019. GC Extension. https:\/\/github.com\/WebAssembly\/gc\/blob\/master\/proposals\/gc\/Overview.md ."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_2_2_43_1","unstructured":"Peter Sewell and Jaroslav Sevcik. 2016. C\/C++11 mappings to processors. https:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/ cpp0xmappings.html .  Peter Sewell and Jaroslav Sevcik. 2016. C\/C++11 mappings to processors. https:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/ cpp0xmappings.html ."},{"key":"e_1_2_2_44_1","unstructured":"Ben Smith. 2019. Threading proposal for WebAssembly. https:\/\/github.com\/WebAssembly\/threads .  Ben Smith. 2019. Threading proposal for WebAssembly. https:\/\/github.com\/WebAssembly\/threads ."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993534"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167082"},{"key":"e_1_2_2_49_1","unstructured":"WebAssembly Working Group. 2019. WebAssembly Specifications. https:\/\/webassembly.github.io\/spec\/ .  WebAssembly Working Group. 2019. WebAssembly Specifications. https:\/\/webassembly.github.io\/spec\/ ."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360559","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360559","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360559"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":47,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360559"],"URL":"https:\/\/doi.org\/10.1145\/3360559","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}