Conrad Watt
Skip Editorial Notes SectionSkip Abstract Section
Skip Supplemental Material SectionEditorial Notes
A corrigendum was issued for this paper on December 29, 2020. You can download the corrigendum from the supplemental material section of this citation page.
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 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.
Supplemental Material
Available for Download
pdf
3360559-corrigendum.pdf (475.2 KB)
Corrigendum to "Weakening WebAssembly" by Watt et al., Proceedings of the ACM on Programming Languages Volume 3, Issue OOPSLA (PACMPL 3:OOPSLA).
- Sarita V. Adve and Mark D. Hill. 1990. Weak Ordering — a New Definition. In Proceedings of the 17th Annual International Symposium on Computer Architecture (ISCA ’90). ACM, New York, NY, USA, 2–14. Google Scholar
Digital Library
- Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. 2015. GP U Concurrency: Weak Behaviours and Programming Assumptions. In Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’15). ACM, New York, NY, USA, 577–591. Google ScholarDigital Library
- Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. 2009. The Semantics of Power and ARM Multiprocessor Machine Code. In Proceedings of the 4th Workshop on Declarative Aspects of Multicore Programming. ACM, New York, NY, USA. Google ScholarDigital Library
- Mark Batty. 2014. The C11 and C++11 Concurrency Model. Ph.D. Dissertation. University of Cambridge.Google Scholar
- Mark Batty, Mike Dodds, and Alexey Gotsman. 2013. Library Abstraction for C/C++ Concurrency. SIGPLAN Not. 48, 1 (Jan. 2013), 235–248. Google ScholarDigital Library
- Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015. The Problem of Programming Language Concurrency Semantics. In Programming Languages and Systems, Jan Vitek (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 283–307.Google Scholar
- Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. 2012. Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Philadelphia). 509–520. Google ScholarDigital Library
- Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). ACM, New York, NY, USA, 55–66. Google ScholarDigital Library
- Mark Batty and Peter Sewell. 2014. The Thin-air Problem. https://www.cl.cam.ac.uk/~pes20/cpp/notes42.html .Google Scholar
- Hans-J. Boehm. 2005. Threads Cannot Be Implemented As a Library. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’05). ACM, New York, NY, USA, 261–268. Google ScholarDigital Library
- Hans-J. Boehm. 2011. How to Miscompile Programs with "Benign" Data Races. In Proceedings of the 3rd USENIX Conference on Hot Topic in Parallelism (HotPar’11). USENIX Association, Berkeley, CA, USA, 3–3. http://dl.acm.org/citation.cfm?id= 2001252.2001255Google ScholarDigital Library
- Hans-J. Boehm and Sarita V. Adve. 2008. Foundations of the C++ Concurrency Memory Model. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’08). ACM, New York, NY, USA, 68–78. Google ScholarDigital Library
- Hans-J. Boehm and Brian Demsky. 2014. Outlawing Ghosts: Avoiding Out-of-thin-air Results. In Proceedings of the Workshop on Memory Systems Performance and Correctness (MSPC ’14). ACM, New York, NY, USA, Article 7, 6 pages. Google ScholarDigital Library
- Pietro Cenciarelli, Alexander Knapp, and Eleonora Sibilio. 2007. The Java Memory Model: Operationally, Denotationally, Axiomatically. In Proceedings of the 16th European Symposium on Programming (ESOP’07). Springer-Verlag, Berlin, Heidelberg, 331–346. http://dl.acm.org/citation.cfm?id=1762174.1762206Google Scholar
- Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy. 2018. Bounding Data Races in Space and Time. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). ACM, New York, NY, USA, 242–255. Google ScholarDigital Library
- ECMA International. 2018a. ECMAScript 2018 Language Specification - Data Race Freedom. https://www.ecmainternational.org/ecma- 262/9.0/index.html#sec- data- race- freedom .Google Scholar
- ECMA International. 2018b. ECMAScript 2018 Language Specification - Memory Model. https://www.ecma- international. org/ecma- 262/9.0/index.html#sec- memory- model .Google Scholar
- Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 architecture, operationally: concurrency and ISA. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, FL, USA. 608–621.Google ScholarDigital Library
- Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. 2017. Mixed-size Concurrency: ARM, POWER, C/C++11, and SC. SIGPLAN Not. 52, 1 (Jan. 2017), 429–442. Google ScholarDigital Library
- Kourosh Gharachorloo, Sarita V. Adve, Anoop Gupta, John L. Hennessy, and Mark D. Hill. 1992. Programming for Different Memory Consistency Models. J. Parallel and Distrib. Comput. 15 (1992), 399–407.Google ScholarCross Ref
- Kathryn E. Gray, Gabriel Kerneis, Dominic Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. 2015. An Integrated Concurrency and core-ISA Architectural Envelope Definition, and Test Oracle, for IBM POWER Multiprocessors. In Proceedings of the 48th International Symposium on Microarchitecture (MICRO-48). ACM, New York, NY, USA, 635–646. Google ScholarDigital Library
- 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).Google Scholar
- Lars T Hansen. 2017. Resizing details / underspecification. https://github.com/WebAssembly/threads/issues/26 .Google Scholar
- David Herman, Luke Wagner, and Alon Zakai. 2014. asm.js. http://asmjs.org/spec/latest .Google Scholar
- Lisa Higham, LillAnne Jackson, and Jalal Kawash. 2006. Programmer-centric Conditions for Itanium Memory Consistency. In Proceedings of the 8th International Conference on Distributed Computing and Networking (ICDCN’06). Springer-Verlag, 58–69. Google ScholarDigital Library
- David Howells, Paul E. McKenney, Will Deacon, and Peter Zijlstra. 2019. Linux Kernel Memory Barriers. https://www. kernel.org/doc/Documentation/memory- barriers.txt .Google Scholar
- Jukka Jylänki. 2015. Emscripten gains experimental pthreads support! https://groups.google.com/forum/#!topic/emscriptendiscuss/gQQRjajQ6iY .Google Scholar
- Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A Promising Semantics for Relaxedmemory Concurrency. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM, New York, NY, USA, 175–189. Google ScholarDigital Library
- Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing Sequential Consistency in C/C++11. SIGPLAN Not. 52, 6 (June 2017), 618–632. Google ScholarDigital Library
- Leslie Lamport. 1978. Time, Clocks, and the Ordering of Events in a Distributed System. Commun. ACM 21, 7 (July 1978), 558–565. Google ScholarDigital Library
- Andreas Lochbihler. 2018. Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler. Journal of Automated Reasoning 61, 1 (01 Jun 2018), 243–332. Google ScholarDigital Library
- Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. 2012. An Axiomatic Memory Model for POWER Multiprocessors. In Proceedings of the 24th International Conference on Computer Aided Verification. 495–512. Google ScholarDigital Library
- Jeremy Manson, William Pugh, and Sarita V. Adve. 2005. The Java Memory Model. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’05). ACM, New York, NY, USA, 378–391. Google ScholarDigital Library
- Cristian Mattarei, Clark Barrett, Shu-yu Guo, Bradley Nelson, and Ben Smith. 2018. EMME: A Formal Tool for ECMAScript Memory Model Evaluation. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 55–71.Google Scholar
- Paul E. McKenney, Alan Jeffrey, and Ali Sezgin. 2005. N4375: Out-of-Thin-Air Execution is Vacuous. C++ Standards Committee Papers (2005).Google Scholar
- Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. 2016. An operational semantics for C/C++11 concurrency. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. ACM, New York, NY, USA, 18. Google ScholarDigital Library
- Scott Owens, Susmit Sarkar, and Peter Sewell. 2009. A better x86 memory model: x86-TSO. In Proceedings of Theorem Proving in Higher Order Logics, LNCS 5674. 391–407. Google ScholarDigital Library
- Jean Pichon-Pharabod and Peter Sewell. 2016. A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, St. Petersburg, FL, USA, January 20 - 22, 2016. 622–633. Google ScholarDigital Library
- Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2018. Bridging the Gap between Programming Languages and Hardware Weak Memory Models. Technical Report. Google Scholar
- Andreas Rossberg. 2018. Reference Types Proposal for WebAssembly. https://github.com/WebAssembly/reference- types .Google Scholar
- Andreas Rossberg. 2019. GC Extension. https://github.com/WebAssembly/gc/blob/master/proposals/gc/Overview.md .Google Scholar
- Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. 2012. Synchronising C/C++ and POWER. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’12). ACM, New York, NY, USA, 311–322. Google ScholarDigital Library
- Peter Sewell and Jaroslav Sevcik. 2016. C/C++11 mappings to processors. https://www.cl.cam.ac.uk/~pes20/cpp/ cpp0xmappings.html .Google Scholar
- Ben Smith. 2019. Threading proposal for WebAssembly. https://github.com/WebAssembly/threads .Google Scholar
- Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. 2015. Common Compiler Optimisations Are Invalid in the C11 Memory Model and What We Can Do About It. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). ACM, New York, NY, USA, 209–220. Google ScholarDigital Library
- Jaroslav Ševčík. 2011. Safe Optimisations for Shared-memory Concurrent Programs. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’11). ACM, New York, NY, USA, 306–316. Google ScholarDigital Library
- Jaroslav Ševčík and David Aspinall. 2008. On Validity of Program Transformations in the Java Memory Model. In Proceedings of the 22nd European Conference on Object-Oriented Programming (ECOOP ’08). Springer-Verlag, Berlin, Heidelberg, 27–51. Google ScholarDigital Library
- Conrad Watt. 2018. Mechanising and Verifying the WebAssembly Specification. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). ACM, New York, NY, USA, 53–65. Google ScholarDigital Library
- WebAssembly Working Group. 2019. WebAssembly Specifications. https://webassembly.github.io/spec/ .Google Scholar
Index Terms
- Weakening WebAssembly
Recommendations
Bringing the web up to speed with WebAssembly
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and ImplementationThe maturation of the Web platform has given rise to sophisticated and demanding Web applications such as interactive 3D visualization, audio and video software, and games. With that, efficiency and security of code on the Web has become more important ...
Bringing the web up to speed with WebAssembly
PLDI '17The maturation of the Web platform has given rise to sophisticated and demanding Web applications such as interactive 3D visualization, audio and video software, and games. With that, efficiency and security of code on the Web has become more important ...
Comments