Cited By
View all- Rao XRadziuk SWatt CGardner P(2025)Progressful Interpreters for Efficient WebAssembly MechanisationProceedings of the ACM on Programming Languages10.1145/37048589:POPL(627-655)Online publication date: 9-Jan-2025
Bringing the WebAssembly Standard up to Speed with SpecTec
Authors: 
Dongjun Youn, Wonho Shin, Jaehyun Lee, 
Sukyoung Ryu, 
Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, Andreas RossbergAuthors Info & Claims
Article No.: 210, Pages 1559 - 1584
Abstract
WebAssembly (Wasm) is a portable low-level bytecode language and virtual machine that has seen increasing use in a variety of ecosystems. Its specification is unusually rigorous – including a full formal semantics for the language – and every new feature must be specified in this formal semantics, in prose, and in the official reference interpreter before it can be standardized. With the growing size of the language, this manual process with its redundancies has become laborious and error-prone, and in this work, we offer a solution. We present SpecTec, a domain-specific language (DSL) and toolchain that facilitates both the Wasm specification and the generation of artifacts necessary to standardize new features. SpecTec serves as a single source of truth — from a SpecTec definition of the Wasm semantics, we can generate a typeset specification, including formal definitions and prose pseudocode descriptions, and a meta-level interpreter. Further backends for test generation and interactive theorem proving are planned. We evaluate SpecTec’s ability to represent the latest Wasm 2.0 and show that the generated meta-level interpreter passes 100% of the applicable official test suite. We show that SpecTec is highly effective at discovering and preventing errors by detecting historical errors in the specification that have been corrected and ten errors in five proposals ready for inclusion in the next version of Wasm. Our ultimate aim is that SpecTec should be adopted by the Wasm standards community and used to specify future versions of the standard.
References
[1]
2022. ESMeta: An ECMAScript specification metalanguage used for automatically generating language-based tools. https://github.com/es-meta/esmeta
[2]
Heejin Ahn and WebAssembly Community Group. 2023. Exception Handling Proposal for WebAssembly. https://github.com/WebAssembly/exception-handling/
[3]
Andreas Rossberg. 2021. Fix variable name typos. https://github.com/WebAssembly/spec/commit/4353b29
[4]
Andreas Rossberg. 2022. Add missing case for declarative elem segments. https://github.com/WebAssembly/spec/commit/ff149b4
[5]
Andreas Rossberg. 2023. Fix reduction rule for label. https://github.com/WebAssembly/spec/commit/8f5c489
[6]
Andreas Rossberg. 2023. Remove an obsolete exec step. https://github.com/WebAssembly/spec/commit/f54b5b8
[7]
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. 2017. Intrinsically-Typed Definitional Interpreters for Imperative Languages. Proc. ACM Program. Lang., 2, POPL (2017), Article 16, dec, 34 pages. https://doi.org/10.1145/3158104
[8]
Ben Visness. 2023. Add missing type to elem.drop and store soundness. https://github.com/WebAssembly/spec/commit/5b18d52
[9]
Stefan Berghofer, Lukas Bulwahn, and Florian Haftmann. 2009. Turning Inductive into Equational Specifications. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs ’09). Springer-Verlag, Berlin, Heidelberg. 131–146. isbn:9783642033582 https://doi.org/10.1007/978-3-642-03359-9_11
[10]
Martin Bodin, Arthur Chargueraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith. 2014. A Trusted Mechanised JavaScript Specification. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA. 87–100. isbn:9781450325448 https://doi.org/10.1145/2535838.2535876
[11]
Denis Bogdănaş and Grigore Roşu. 2015. K-Java: A Complete Semantics of Java. In Proceedings of the Symposium on Principles of Programming Languages (POPL).
[12]
David M. Cerna and Temur Kutsia. 2023. Anti-unification and Generalization: A Survey. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI-23, Edith Elkind (Ed.). International Joint Conferences on Artificial Intelligence Organization, 6563–6573. https://doi.org/10.24963/ijcai.2023/736 Survey Track
[13]
Sam Clegg and WebAssembly Community Group. 2023. Extended Constant Expressions Proposal for WebAssembly. https://github.com/WebAssembly/extended-const/
[14]
De Moura, Leonardo and Bjørner, Nikolaj. 2008. Z3: An Efficient SMT Solver. TACAS’08/ETAPS’08. Springer-Verlag, 337–340. isbn:3540787992
[15]
Dongjun Youn. 2023. Add missing access to current frame in prose. https://github.com/WebAssembly/spec/commit/be820b2
[16]
Dongjun Youn. 2023. Fix spec for execution of struct.new, array.new_fixed and br_on_cast(_fail). https://github.com/WebAssembly/gc/pull/456
[17]
ECMA International. 2023. ECMA-262, 14th edition, ECMAScript ® 2023 Language Specification. https://262.ecma-international.org
[18]
Andreas Rossberg (editor). 2022. WebAssembly Specification (Release 2.0). https://webassembly.github.io/spec/core/
[19]
Chucky Ellison and Grigore Roşu. 2012. An Executable Formal Semantics of C with Applications. In Proceedings of the Symposium on Principles of Programming Languages (POPL).
[20]
Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. The MIT Press.
[21]
Adam T. Geller. 2021. WASM-Redex. https://github.com/atgeller/WASM-Redex
[22]
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). Association for Computing Machinery, New York, NY, USA. 635–646. isbn:9781450340342 https://doi.org/10.1145/2830772.2830775
[23]
Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. 2010. The Essence of Javascript. In Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP’10). Springer-Verlag, Berlin, Heidelberg. 126–150. isbn:3642141064
[24]
Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017. Bringing the Web up to Speed with WebAssembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. Association for Computing Machinery, New York, NY, USA. 185–200. isbn:9781450349888 https://doi.org/10.1145/3062341.3062363
[25]
Adam Hall and Umakishore Ramachandran. 2019. An Execution Model for Serverless Functions at the Edge. In Proceedings of the International Conference on Internet of Things Design and Implementation. Association for Computing Machinery, New York, NY, USA. 225–236. isbn:9781450362832 https://doi.org/10.1145/3302505.3310084
[26]
Pat Hickey. 2019. Lucet Takes WebAssembly Beyond the Browser. https://www.fastly.com/blog/announcing-lucet-fastly-native-webassembly-compiler-runtime
[27]
Runtime Verification Inc. 2023. KWasm. https://github.com/runtimeverification/wasm-semantics
[28]
ISO/IEC. 2018. ISO/IEC 9899:2018. https://www.iso.org/standard/74528.html
[29]
Jaehyun Lee. 2023. Dimension mismatch in the premise of array.new_data reduction rule. https://github.com/WebAssembly/gc/issues/476
[30]
Jim Blandy. 2023. Remove stray x indices. https://github.com/WebAssembly/spec/commit/e7f6e1c
[31]
Julien Cretin. 2022. Fix typo in element execution. https://github.com/WebAssembly/spec/commit/793b3ff
[32]
Julien Cretin. 2022. Fix typos in instruction validation rules. https://github.com/WebAssembly/spec/commit/79ef7af
[33]
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the Foundations of the Rust Programming Language. Proc. ACM Program. Lang., 2, POPL (2017), Article 66, dec, 34 pages. https://doi.org/10.1145/3158154
[34]
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 (2018), e20. https://doi.org/10.1017/S0956796818000151
[35]
Richard M. Karp. 1972. Reducibility among Combinatorial Problems. 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
[36]
Keith Winstein. 2022. Fix missing immediate on table.set. https://github.com/WebAssembly/spec/commit/f6ae547
[37]
Gerwin Klein and Tobias Nipkow. 2006. A Machine-Checked Model for a Java-like Language, Virtual Machine, and Compiler. ACM Trans. Program. Lang. Syst., 28, 4 (2006), jul, 619–695. issn:0164-0925 https://doi.org/10.1145/1146809.1146811
[38]
Donald E. Knuth. 2000. Dancing links. arxiv:cs/0011047.
[39]
Robbert Krebbers. 2015. The C standard formalized in Coq. Ph. D. Dissertation. Radboud University Nijmegen.
[40]
Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA. 179–191. isbn:9781450325448 https://doi.org/10.1145/2535838.2535841
[41]
Peter Lammich. 2019. Refinement to Imperative HOL. 62, 4 (2019), apr, 481–503. issn:0168-7433 https://doi.org/10.1007/s10817-017-9437-1
[42]
Daniel K. Lee, Karl Crary, and Robert Harper. 2007. Towards a Mechanized Metatheory of Standard ML. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’07). Association for Computing Machinery, New York, NY, USA. 173–184. isbn:1595935754 https://doi.org/10.1145/1190216.1190245
[43]
Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM, 52, 7 (2009), jul, 9 pages. issn:0001-0782 https://doi.org/10.1145/1538788.1538814
[44]
Andreas Lochbihler and Lukas Bulwahn. 2011. Animating the Formalised Semantics of a Java-Like Language. In Interactive Theorem Proving, Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 216–232. isbn:978-3-642-22863-6
[45]
Maxime Chabert and Christine Solnon. 2020. A Global Constraint for the Exact Cover Problem: Application to Conceptual Clustering. Journal of Artificial Intelligence Research, 67 (2020), 509 – 547.
[46]
Microsoft. 2013. C# Language Specification 5.0. https://www.microsoft.com/en-us/download/details.aspx?id=7029
[47]
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. 1997. The Definition of Standard ML (Revised).
[48]
Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. 2014. Lem: reusable engineering of real-world semantics. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). Association for Computing Machinery, New York, NY, USA. 175–188. isbn:9781450328739 https://doi.org/10.1145/2628136.2628143
[49]
Michael Norrish. 1998. C formalised in HOL.
[50]
Oracle. 2023. Java Language and Virtual Machine Specifications. https://docs.oracle.com/javase/specs/
[51]
Daejun Park, Andrei Ştefănescu, and Grigore Roşu. 2015. KJS: A Complete Formal Semantics of JavaScript. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’15).
[52]
Jihyeok Park, Seungmin An, and Sukyoung Ryu. 2022. Automatically Deriving JavaScript Static Analyzers from Specifications Using Meta-Level Static Analysis. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE). Association for Computing Machinery, New York, NY, USA. 1022––1034.
[53]
Jihyeok Park, Seungmin An, Wonho Shin, Yusung Sim, and Sukyoung Ryu. 2021. JSTAR: JavaScript Specification Type Analyzer using Refinement. In Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering (ASE). Association for Computing Machinery, New York, NY, USA. 606–616.
[54]
Jihyeok Park, Seungmin An, Dongjun Youn, Gyeongwon Kim, and Sukyoung Ryu. 2021. JEST: N+1-version Differential Testing of Both JavaScript Engines and Specification. In Proceedings of IEEE/ACM 43rd International Conference on Software Engineering (ICSE). Association for Computing Machinery, New York, NY, USA. 13–24.
[55]
Jihyeok Park, Jihee Park, Seungmin An, and Sukyoung Ryu. 2020. JISET: JavaScript IR-based Semantics Extraction Toolchain. In Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering (ASE). 647–658. https://doi.org/10.1145/3324884.3416632
[56]
Sphinx Project. 2008. Sphinx. https://www.sphinx-doc.org/
[57]
R1ru. 2023. Pop dummy frame after Invocation. https://github.com/WebAssembly/spec/commit/be1f563
[58]
Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner, and Lars Birkedal. 2023. Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. Proc. ACM Program. Lang., 7, PLDI (2023), Article 151, jun, 25 pages. https://doi.org/10.1145/3591265
[59]
Alastair Reid. 2016. Trustworthy Specifications of ARM® V8-A and v8-M System Level Architecture. In Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design (FMCAD ’16). FMCAD Inc, Austin, Texas. 161–168. isbn:9780983567868
[60]
Robert Bruce Findler and Jacob Matthews. 2023. R6RS Semantics Model and Reference Implementations. https://www.r6rs.org/refimpl/
[61]
Andreas Rossberg. 2023. As low-level as possible, but no lower. https://icfp23.sigplan.org/details/icfp-2023-icfp-keynotes/38/As-low-level-as-possible-but-no-lower
[62]
Andreas Rossberg and WebAssembly Community Group. 2023. Function Reference Types Proposal for WebAssembly. https://github.com/WebAssembly/function-references/
[63]
Andreas Rossberg and WebAssembly Community Group. 2023. GC Proposal for WebAssembly. https://github.com/WebAssembly/gc/
[64]
Andreas Rossberg and WebAssembly Community Group. 2023. Multiple Memories Proposal for WebAssembly. https://github.com/WebAssembly/multi-memory/
[65]
Andreas Rossberg and WebAssembly Community Group. 2023. Tail Call Proposal for WebAssembly. https://github.com/WebAssembly/tail-call/
[66]
Alan Schmitt. 2019. Skeletal Semantics. https://skeletons.inria.fr/
[67]
Peter Sewell and Francesco Zappa Nardelli. 2007. Ott release, version 0.10.9. http://www.cl.cam.ac.uk/~pes20/ott/
[68]
Ben Smith, Conrad Watt, and WebAssembly Community Group. 2023. Threads Proposal for WebAssembly. https://github.com/WebAssembly/threads/
[69]
SpecTec Team. 2023. https://github.com/Wasm-DSL/spectec. https://github.com/Wasm-DSL/spectec
[70]
Guy Steele. 2017. It’s Time for a New Old Language. In Principal and Practices of Parallel Programming (ACM SIGPLAN Notices, Vol. 52). 1.
[71]
Asumu Takikawa. 2019. wasm-redex. https://github.com/takikawa/wasm-redex
[72]
TC39. 2022. CI: Integrate ESMeta. https://github.com/tc39/test262/pull/3730
[73]
TC39. 2022. Meta: integrate esmeta type checker into CI. https://github.com/tc39/ecma262/pull/2926
[74]
Spoofax Team. 2010. Spoofax: The Language Designer’s Workbench. https://spoofax.dev
[75]
SpecTec Team. 2024. Automatically Generated WebAssembly Specification. https://github.com/Wasm-DSL/spectec/blob/fe709a16901fef96bc603b5d710898436613144f/spectec/WebAssembly.pdf
[76]
SpecTec Team. 2024. pldi24-spectec/artifact: v1.0.1. https://doi.org/10.5281/zenodo.10807169
[77]
W3C Team. 2015. WebAssembly Community Group. https://www.w3.org/community/webassembly/
[78]
Ata Tekeli. 2022. WebAssembly (WASM) in Blockchain. https://blog.devgenius.io/webassembly-wasm-in-blockchain-f651a8ac767b
[79]
Tom Stuart. 2023. Add missing value to table.grow reduction rule. https://github.com/WebAssembly/spec/commit/3545ad0
[80]
Kenton Varda. 2017. Introducing Cloudflare Workers: Run JavaScript Service Workers at the Edge. https://blog.cloudflare.com/introducing-cloudflare-workers/
[81]
Runtime Verification. 2013. K Semantic Framework. https://kframework.org/
[82]
Stefan Wallentowitz, Bastian Kersting, and Dan Mihai Dumitriu. 2022. Potential of WebAssembly for Embedded Systems. In 2022 11th Mediterranean Conference on Embedded Computing (MECO). 1–4. https://doi.org/10.1109/MECO55406.2022.9797106
[83]
Conrad Watt. 2018. Mechanising and verifying the WebAssembly specification. Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, https://dl.acm.org/doi/10.1145/3167082
[84]
Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, and Philippa Gardner. 2021. Two Mechanisations of WebAssembly 1.0. In Proceedings of the 24 th international symposium of Formal Methods (FM21), Beijing, China; November 20-25, 2021, Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan (Eds.) (Lecture Notes in Computer Science, Vol. 13047). Springer, 61–79. https://doi.org/10.1007/978-3-030-90870-6_4
[85]
Conrad Watt, Maja Trela, Peter Lammich, and Florian Märkl. 2023. WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly. Proc. ACM Program. Lang., 7, PLDI (2023), Article 110, jun, 24 pages. https://doi.org/10.1145/3591224
[86]
WebAssembly Community Group. 2023. WebAssembly Core Testsuite. https://github.com/WebAssembly/spec/tree/main/test/core
[87]
WebAssembly Community Group. 2023. WebAssembly Parser. https://github.com/WebAssembly/spec/tree/main/interpreter/text
[88]
WebAssembly Community Group. 2023. WebAssembly Reference Interpreter: Scripts. https://github.com/WebAssembly/spec/blob/main/interpreter/README.md##scripts
[89]
WebAssembly Community Group. 2023. WebAssembly specification, reference interpreter, and test suite. https://github.com/WebAssembly
[90]
Whirlicote. 2022. Fix naming typo. https://github.com/WebAssembly/spec/commit/04beeb7
[91]
Wonho Shin. 2023. Add current frame. https://github.com/WebAssembly/gc/pull/484
[92]
Wonho Shin. 2023. Fix getfiled auxiliary function. https://github.com/WebAssembly/gc/pull/463
[93]
Wonho Shin. 2023. Fix ref.null semantics. https://github.com/WebAssembly/gc/pull/478
[94]
Wonho Shin. 2023. Minor changes on array.new_elem. https://github.com/WebAssembly/gc/pull/477
[95]
Wonho Shin. 2023. Pass index argument to getfield function. https://github.com/WebAssembly/gc/pull/464
Index Terms
- Bringing the WebAssembly Standard up to Speed with SpecTec
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 ...
Progressful Interpreters for Efficient WebAssembly Mechanisation
Mechanisations of programming language specifications are now increasingly common, providing machine-checked modelling of the specification and verification of desired properties such as type safety. However it is challenging to maintain these ...
A Domain-Specific Language for Abstract Syntax Model to Concrete Syntax Model Mappings
MODELSWARD 2014: Proceedings of the 2nd International Conference on Model-Driven Engineering and Software DevelopmentModel-based parser generators such as ModelCC effectively decouple language design from language processing. ModelCC allows the specification of the abstract syntax model of a language as a set of language elements and their relationships. ModelCC ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 June 2024
Published in PACMPL Volume 8, Issue PLDI
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- NRF
- IITP MSIT
- Samsung Electronics Co., Ltd
- EHOP
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 700Total Downloads
- Downloads (Last 12 months)700
- Downloads (Last 6 weeks)99
Reflects downloads up to 05 Feb 2025
Other Metrics
Citations
Cited By
View all- Rao XRadziuk SWatt CGardner P(2025)Progressful Interpreters for Efficient WebAssembly MechanisationProceedings of the ACM on Programming Languages10.1145/37048589:POPL(627-655)Online publication date: 9-Jan-2025
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in