tiny.machine

Overview · API · Code relationships · Verification · Audit

Overview

A virtual machine runs a guest operating system kernel so that the same run can be produced again later, from stored state, with the result checkable against a recorded identity. The guest kernel boots directly from an ELF image, with no firmware stage in between. The execution rules fix one virtual CPU and one fixed-size region of guest memory.

The guest stops only when it signals the host, so every stop is a place the guest chose. When the guest stops idle, the machine produces authenticated evidence that the guest's work settled before anything outside observes it. Every outside influence reaches the guest as a recorded and checked input, bound to the identity of the execution rules and to a digest of the state it arrived against. Each delivered input carries the authority to run the guest work that settles it. The caller supplies all of the machine's memory: the state of each running machine, the guest's memory, and the storage for saved state. The package holds none of its own.

Hardware and host make two runs differ in places that are many and easy to miss: instruction results, interrupts, the clock, entropy, device behavior, and scheduling.

The package took from KVM, the Linux kernel interface for running a virtual machine on host hardware, documented in the Linux KVM API, and from the x86-64 architecture manuals, the Intel Software Developer Manuals. What it took was one virtual CPU per machine, a fixed guest memory region registered with the host kernel, x86-64 instruction semantics, and direct kernel boot.

KVM is one of two backends behind the same execution rules, and the second is a portable x86-64 interpreter that executes the admitted instruction forms in software, the reference backend. The backend is chosen together with one execution contract and the determinism claims that pairing makes (a profile), and a portable_x86_64_interpreter_v1 profile selects the interpreter.

The package answers the many easy-to-miss places by listing all 42 of them in canonical order, one entry per place (the inventory). Each namespace declares the named places it answers for (its divergence sources), and the package concatenates those declarations into one list. A test audits the concatenated list against the inventory for exact count and exact order, and a dropped or duplicated place fails it. The inventory records each place's control once per backend, so the interpreter can enforce what KVM only assumes: instruction results are enforced for the interpreter and assumed for KVM.

A KVM profile and its portable counterpart carry the same identity of the shared execution rules, computed over the encoded profile with the backend field and the claim fields zeroed (the contract fingerprint), so a run under one can be compared against a run under the other. Eight namespaces divide the package: admission, checkpoint, explore, fabric, fault, profile, instance, and world.

• K0: the restricted kernel from lib/os that an instance boots, exchanging request and event messages with the host through fixed rings in guest RAM.
• guest RAM: the machine's fixed 67,108,864 bytes of memory, addressed from zero.
• doorbell: the one-byte guest output port that K0 writes to yield, carrying ready, quiescent, or guest_fault.
• turn: one input delivered to a node together with the guest work that settles it.
• quiescence receipt: the authenticated evidence a quiescent stop produces for one turn.
• activation fence: the world, generation, and token authorized for one run turn.
• instance: one live K0 execution that borrows its caller-owned storage and its guest-memory backing until deinit.
• instance storage: the caller-owned bytes holding one instance lifecycle's whole state, at an address the caller keeps stable.
• checkpoint: captured machine execution state carrying an identity that any holder of the bytes can recompute.

Definitions

Types and contracts

Public types and contracts.

• InstanceRamAlignment
• InstanceRamBytes
• Capacity: The ten bounded resources one profile pins, so a caller names one to ask for its bound: instances, checkpoint candidates, admissions, request records, event records, and the byte bounds for terminal, entropy, semantic, effect-request, and effect-result payloads.
• Checkpoint: A borrowed handle to published checkpoint metadata and a normalized memory image.
• CheckpointCpuState: Holds the register state a restarted machine begins from as the CPU state a checkpoint keeps in its material, taken from the kernel manifest's initial-state type.
• CheckpointMemoryDigest: The SHA-256 identity of one normalized memory image.
• CheckpointRamAlignment
• CheckpointRamBytes
• CheckpointStateDigest: The SHA-256 identity of one restart state.
• CheckpointStorage: Caller-owned metadata for one durable checkpoint.
• Contract: Holds the rules for executing a guest that every backend of one canonical kind obeys, so a caller can compare contracts to know whether two runs obeyed the same rules.
• ContractFingerprint: The identity of the shared execution rules.
• ExecutionFingerprint
• Fabric
• FabricRoot
• FaultChoice: The outcome recorded at one fault point, its choice.
• FaultDecision: A point together with the choice made at it, a fault decision.
• FaultKind: The eleven fault families a point can name, its fault kind: a machine crash, a process crash, an I/O error, packet loss, packet delay, packet reorder, a partition, a clock jump, an entropy choice, capacity exhaustion, and a host service failure.
• FaultPoint: The named place where a fault can be injected, a fault point.
• Geometry: The memory geometry a contract fixes gives how many vCPUs run, the page size, the base address, and the number of bytes, so a caller can check its own memory layout before constructing an instance.
• Instance: Operates one K0 guest that is running now, borrowing its storage and whatever backs its guest memory, so every lifecycle call goes through this handle.
• InstanceExit: Reports one execution boundary in the form a caller sees, so every run answers with this value and the answer decides whether the lifecycle goes on.
• InstanceInput: Gathers everything one cold start of a K0 guest needs into one value, so a caller supplies all of this at once and knows how long to keep the image and the manifest around.
• InstanceRestoreError
• InstanceRestoreInput: Gathers everything needed to bring a checkpoint back into RAM the caller owns, so a caller supplies all of this at once for a restore.
• InstanceRestoreResult: Reports how a restore turned out, so the caller learns the state of the restored buffers across the three outcomes.
• InstanceSharedRestoreInput: Gathers everything needed for a portable restore whose pages come from an immutable root provider, so the caller supplies a provider and branch storage.
• InstanceStartResult: Reports how a cold start turned out, so the caller learns the state of its buffers across the three outcomes.
• InstanceStorage: Holds the bytes a caller sets aside for one running instance, so the caller supplies the storage and holds it still.
• MachineRoot: One checkpoint root under an execution profile.
• Profile: One execution contract, the backend chosen to run it, and the determinism claims that pairing makes define a profile.
• ProfileFingerprint: The identity of one full profile.
• QuiescenceReceipt: The checkable evidence for one quiescent turn a caller has acknowledged, so a caller holds the evidence one settled turn leaves behind.
• SemanticReceipt: The part of a quiescence receipt a checkpoint works from, so a checkpoint identifies guest state with this value.
• Usage: A requested value per bounded resource, held as one fixed array with a getter and a setter so a caller fills one in to have a whole set of requests checked at once.

Namespaces

Public namespaces.

• profile: Comparing two runs requires writing down the rules both ran under and what exactly is being claimed about them, and this namespace holds both as one execution contract, the backend chosen to run it, and the determinism claims that pairing makes (a profile), with the evidence for each claim named.
• admission: Replaying a run requires feeding the guest exactly the inputs the first run saw, in the same order, and this namespace records each one so a later reader can check the whole history from the receipts alone.
• explore: Some bugs show up only under one particular order of inputs, scheduling, and faults, so finding one means running a deterministic machine many times with different choices, checking each run against rules written beforehand, and keeping every bound fixed in advance.
• fault: Testing how a system survives failure means choosing, at a named place, whether the failure happens, and a replay has to make the same choices the recorded run made.
• instance: Two runs of one guest operating system from one starting state with one set of inputs do the same work and land in the same place.
• checkpoint: A program running under a virtual machine has to be halted and turned into a value that carries a name, and a run has to be started again from that value later.
• fabric
• world: Machines that talk to each other advance separately, so stopping them all at one instant, storing that instant, and bringing it back later takes a definition of what one instant is, and this namespace supplies it.

Values and defaults

Public values and defaults.

• determinism_sources

Code relationships

Direct static dependencies extracted from parsed source by semantic graph analysis.

Uses: tiny.accy, tiny.bench, tiny.coz, tiny.hypothesis, tiny.isa, tiny.pluck, tiny.sdfii, tiny.smg, tiny.sql, tiny.sys, tiny.wayland
Used by: alloc_phase, tiny.accy, tiny.choir, tiny.gui, tiny.pluck, tiny.profiling, tiny.smg, tiny.syn, tiny.sys

Verification

No verification records are cataloged for this module in this build.

Audit