Creation of a GNAT Ada Runtime for WASM

Projects Award Nominations
,
1

Creation of a GNAT Ada Runtime for WASM

The Ada Awards Committee has nominated for an award the task of creating an Ada/GNAT runtime for WebAssembly (WASM).

Pointers and past work

  • WASM RTS, this should serve as the base for the task proposed herein.

Motivation

WebAssembly is rapidly becoming the portable, sandboxed compilation target for the web and desktops: it runs in every browser, and with the WASI 0.2 standard it now runs server-side, at the edge, and inside plugin and serverless runtimes under capability-based security. Additionally, it is much faster than JS or compiled Typescript, which is the reason it is starting to be used in higher performance web applications and in embedded systems (microcontrollers or as a plugin system for larger programs).

Ada and SPARK can now be compiled to WASM thanks to GNAT-LLVM, bringing the robustness and proof-readyness of SPARK to an environment that has never received such level of quality. Pairing Ada/SPARK with WebAssembly’s memory isolation and WASI’s capability sandbox produces genuine defense in depth: code proven not to go wrong, running inside a sandbox that contains it even if its assumptions are violated at the boundary. For the plugin, edge, and supply-chain-sensitive ecosystems WASM is built for, a proven-and-sandboxed component is a stronger assurance story than just memory safety alone.

However, as of today, Ada cannot deliver on all that WASM has to offer: there is no usable Ada runtime for WebAssembly. Currently there is only the ZFP/light RTS available, which rules out containers, strings, and ordinary I/O, so real Ada and SPARK programs cannot run on WASM at all. Beyond that, modern versions of WASM (see WASM 3.0) can execute several threads and have extended performance features, nonen of which are being exploited by Ada.

Goals

This goal of this proposal is to build a WebAssembly runtime library (RTS) for Ada/SPARK for the GNAT-LLVM compiler. Most Ada programs - those that use the standard containers, strings, and I/O - should compile and run on WebAssembly. The runtime should target the latest standardized WASM/WASI interface, linked against wasi-libc, so that Ada code runs unmodified on any conformant WASI host (wasmtime, wasmer, Node, WAMR, and others). The deliverable is a packaged runtime plus build integration that turns “Ada can be compiled to WASM in principle” into “Ada and SPARK programs run on WASM in practice,” demonstrated end to end on a formally verified example.

Non-exhaustive list of resources

Milestones

Part 1, work and approach review, initial implementation (Award: 200€)

  • Minimal runtime bring-up: core System packages, a heap allocator, and a last-chance exception handler; a “hello world” Ada program compiled to WASM and run on a WASI host.
  • Expand the minimal runtime to support more Ada standard packages (Ada.Containers (vectors, lists, hashed and ordered maps and sets), Ada.Strings, and Ada.Characters.Handling…)
  • Add the runtime to either GNAT-LLVM or to Alire so that it can be accessible to other users.
  • Create a guide or a blog post in Ada-Lang that documents how to get the setup ready with some simple examples.
  • Cooperate with the other proposal to create documentation about the Ada/GNAT RTS and add any relevant points to it about the work carried out.

Part 2 (Award: 100€)

  • WASI host services over wasip1/wasi-libc: Ada.Calendar and clock access, delay statements, filesystem and file-based Ada.Text_IO, program arguments, environment variables, and stdin input.
  • Create different RTSes with different level of capabilities: akin to light, Jorvik, full-tasking… but for “simple WASM”, “tasking WASM”, “WASI”…
  • Verify the RTS with the ACATS suite.

Constraints

Compiling Ada to WebAssembly via GNAT-LLVM carries one important limitation as of today: WASM provides no zero-cost stack unwinding, so full exception propagation across subprograms is not currently available. Exception support is therefore constrained to handlers local to the frame in which an exception is raised, plus a runtime last-chance handler that reports the exception and terminates the module. This limited profile (No_Exception_Propagation) is a natural fit for SPARK, so it is acceptable.

Guidelines and further indications

The general Ada Awards Guidelines apply to this proposal for those who want to participate. For open, technical discussions on this topic or project, feel free to open topics under the Active Projects forum category.

Best regards,
The Ada Awards Committee.

4 Likes