Resonate Quint Specification

A formal specification of Resonate's Distributed Async Await using Quint, a modern specification language for distributed systems.

Overview

This project models an asynchronous computation system with promises, callbacks, and durable state management. It consists of two main components:

• Worker: Executes multi-step computations with spawn and await operations
• Server: Manages promises and their lifecycle (creation, completion, callbacks, state updates)

Modules

Server (server.qnt)

Models a promise-based execution server with the following capabilities:

Types:

• Promise: Represents an asynchronous computation with id, status (Pending/Resolved), callbacks, state, and value
• Request: Operations on promises (Create, Complete, Callback, UpdateState)
• Command: Actions to be executed (Invoke, Resume)

Core Function:

• exec: Processes requests and updates the promise store, returning the updated store, promise, and commands to execute

Worker (worker.qnt)

Models a worker that executes multi-step computations:

Types:

• WorkerAction: Actions a worker can perform (Spawn, Await, Return)
• WorkerState: Current execution state with step counter and data

Core Function:

• foo: Example computation that demonstrates spawning sub-computations, awaiting results, and returning values