PLDI 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
Thu 27 Jun 2024 11:20 - 11:40 at Iceland / Denmark - Managed Languages

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.

Thu 27 Jun

Displayed time zone: Windhoek change

10:40 - 12:20
10:40
20m
Talk
Linear Matching of JavaScript Regular Expressions
PLDI Research Papers
DOI Pre-print
11:00
20m
Talk
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
PLDI Research Papers
Michael Fitzgibbons Northeastern University, Zoe Paraskevopoulou Ethereum Foundation, Noble Mushtak Northeastern University, Michelle Thalakottur Northeastern University, Jose Sulaiman Manzur Northeastern University, Amal Ahmed Northeastern University, USA
DOI
11:20
20m
Talk
Bringing the WebAssembly Standard up to Speed with SpecTec
PLDI Research Papers
Dongjun Youn KAIST, Shin Wonho KAIST, Jaehyun Lee KAIST, Sukyoung Ryu KAIST, Joachim Breitner unaffiliated, Philippa Gardner Imperial College London, Sam Lindley University of Edinburgh, Matija Pretnar University of Ljubljana, Xiaojia Rao Imperial College, Conrad Watt Nanyang Technological University, Andreas Rossberg Independent
DOI
11:40
20m
Talk
Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes
PLDI Research Papers
Aditya Anand Indian Institute of Technology Bombay, Solai Adithya IIT Mandi, Swapnil Rustagi IIT Mandi, Priyam Seth IIT Mandi, Vijay Sundaresan IBM Canada, Daryl Maier IBM Canada, V Krishna Nandivada IIT Madras, Manas Thakur Indian Institute of Technology Bombay
DOI Pre-print
12:00
20m
Talk
Concurrent Immediate Reference Counting
PLDI Research Papers
Jaehwang Jung KAIST, Jeonghyeon Kim KAIST, Matthew J. Parkinson Microsoft Azure Research, Jeehoon Kang KAIST
DOI