Andreas Haas Andreas Rossberg Derek L. Schuff∗ Ben L. Titzer Google GmbH, Germany /∗Google Inc, USA {ahaas,rossberg,dschuff,titzer}@google.com
Michael Holman Microsoft Inc, USA [email protected]
Dan Gohman Luke Wagner Alon Zakai Mozilla Inc, USA {sunfishcode,luke,azakai}@mozilla.com
JF Bastien Apple Inc, USA [email protected]
https://share.summari.com/webassemblymd-github?utm_source=Chrome
- The 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 than ever. WebAssembly is an abstraction over modern hardware, making it language-, hardware-, and platform-independent
- Previous attempts at solving this problem fell short of properties that a low level compilation target should have
- Safe: code originates from untrusted sources
- Fast: optimized ahead of time
- Compact: code transmitted over the network should be as compact as possible to reduce load times
- Portable: code targeting the Web must be hardware and platform-independent to allow applications to run across all browser and hardware types with the same behavior
- Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage
- Even though WebAssembly is a Binary Code Format, We Present it as a Language with Syntax and Structure
- WebAssembly abstract syntax
- Modules
- A binary takes the form of amodule
- It contains definitions for functions, globals, tables, and memories
- While a module corresponds to the static representation of a program, aninstance corresponds to a dynamic representation, complete with mutable memory and an execution stack
- Instantiating a module requires providing definitions for all imports, which may be exports from previously created WebAssembly instances
- WebAssembly as a Language Provides Us with Convenient and Effective Formal Tools for Specifying and Reasoning About Its Semantics Very Precisely
- Stores and Instances
- Execution Operates Relative to a Globalstores.
- A Store is a Record of the Lists of Module Instances, Tables and Memories That Have Been Allocated in It
- Indices into these lists can be thought of as Addresses, and "allocation" simply Appends to these Lists
- As Described in Section 2.1, a Module Must BeinstantiAtedbefore it Can Be Used
- The Result is an InitializedinStance
- Instantiation
- Instantiating a modulem= (modulef∗glob∗tab?mem?) in a storesrequires providing external function closures
- Values are simply Represented by at.constinStruction, Which is Convenient for the Reduction Rules
- Notation Likesfuncto Refer to Thefunccomponent of a Store Records; Similarly for Other Records
- Closure is the Runtime Representation of a Function, ConSisting of the Actual Function Definition and a Reference to the Instance From Which it Originated
- Functions Can Be Imported From a Different InStance
- Code is fetched from untrusted sources
- Before it can be executed safely, it must bevalidated
- Typing rules
- Contexts
- When Spelling out a context record, we omit CompoNents That Are Empty
- Instructions
- Most of the Typing Rules for IndiVidual Instructions are straightforward
- We Focus on Specific Points of Interest
- The Rules for Control Constructs Require That Their Type Matches the Explicit Annotationtf, and They Extend the ConText with a Local Label
- Label Types are Used in the Typed of Branch Instructions, Which Require Suitable Operands on the Stack to Match the Stack at the Join Point
- Composing Instructions May Require Extending These Types to Deeper Stacks so That They Match Up
- WebAssembly is Transmitted Over the Wire as a Binary EnCoding of the Abstract Syntax Presented in Figure 1.
- A Binary Represents a Single Module and is Divided into Sections According to the Different Kinds of Entities Declared in It, Plus a Few Auxiliary Sections. Function Types Are ColLected in Their Own Section to Allow Sharing. e.g. Code for FuncTion Bodies is Deferred to a Separate Section Placed After All Declarations.
- WebAssembly is similar to a Virtual ISA in that it does not Define how programs are loaded into the Execution Engine or how they perform I/O
- The Embedder Defines How modules are loaded, how imports and exports between modules are resolved, and how WebAssembly Traps are handled
- JavaScript API: WebAssembly Modules can be loaded, compiled, and invoked through a JavaScript API
- Linking: Instances can instantiate multiple modules and use expos from one as an import to the other
- It is possible to link multiple modules that have been created by different producers
- As a low level language, WebAssembly provides no built-in object model
- The major design goal of WebAssembly has been high perforance without sacrificing safety or portability.
- It was important to validate that WebAssembly could be decoded to SSA form in a single linear pass to be fed to these JITs.
- The validated validation speed was approximately fast enough to perform validation at full network speed of 1 Gib/s.
- The most direct precursors of WebAssembly are (P)NaCl [42, 11, 18] and asm.js [4], which we Discussed in Section 1.1.
- Previous Systems such as CCured [34] and Cyclone [23] have Imposed Safety at the C Language Level, which generally Requires Program Changes.
- ComPilers That Target Typed Assembly Languages Must Produce Well-typed (or Proof-carrying) Code by Preserving Types Throughout Compilation
- WebAssembly Radically Reduces the Scope of Responsibility for the VM: it is not required to Enforce the type system of the Original ProGram at the Granularity of Individual Objects; Instead, it must Only Enforce Memory Safety at a Much Coarser GranularIty of a module's Memory.
- The Initial Version of WebAssembly Focuses on Supportinglow-levelcode, Specifically Compiled From C/C++
- A Few Important Features Are Still Missing for Fully Comprehensive Support of This Domain and Will be Added in Future Versions
- zero-cost exceptions,threads, and SIMDinstructions.
- Beyond that, we intend to evolve WebAssembly further into an Attractive Target Forhigh-levellanguages by Including Relevant Primitives Liketail calls,stack Switching, OrcorouTines, and/orgarbage collector