Bringing the WebAssembly Standard up to Speed with SpecTec

Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, Andreas Rossberg

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

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.
Original languageEnglish
Number of pages26
JournalProceedings of the ACM on Programming Languages
Volume8 (PLDI)
Publication statusAccepted/In press - 1 Apr 2024
Event45th ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI) - Copenhagen, Denmark
Duration: 24 Jun 202428 Jun 2024
Conference number: 45

Fingerprint

Dive into the research topics of 'Bringing the WebAssembly Standard up to Speed with SpecTec'. Together they form a unique fingerprint.

Cite this