Module `std::sim`

Deterministic simulation for tests: handlers for std::time::Clock, std::rand::Random, std::rand::Draw, std::task::Tasks, std::net::Net, std::memfs::MemTree and the prelude's Stdin whose answers depend only on their arguments, so code that reaches time, randomness, tasks, the network, the disk and its input only through its row runs the same way every time. Start with world (tasks), net_world (network) or disk_world (disk).

Source: std/sim.weir; committed interface: std/sim.iface. Index

handler SimClock: A clock stopped at t that runs no tasks: sleep moves it forward and returns at once. Install it as with SimClock(0) { … }.
handler SimStdin: A scripted standard input: Stdin.read and Stdin.read_line answer the bytes of input from offset at on, as the root's answer the process's, and 0 once they are all read. Install it as with SimStdin(b"one\ntwo\n", 0usize) { … } around code written with Stdin.
handler SimRandom: A linear congruential generator from seed: each number is the next state, in 0..2147483648. Install it as with SimRandom(atomic(42)) { … }; one seed, one sequence (where draws do not race, as on world's one thread).
handler Sampled: std::rand::Draw sampled from Random (install inside a SimRandom): pick(n) is a draw modulo n, delay(max) one modulo max + 1, fault(p) whether one modulo 100 is below p, part(n) 1 plus one modulo n - 1. A draw is spent only where a choice exists, so a seed's history does not depend on choices it never had.
handler Searched: std::rand::Draw searched: each draw is a weir explore choice point.
enum Draws: Where a world's draws come from: Seed(s) samples them from a generator seeded with s (one seed, one history), Search(f) makes each a weir explore choice point with at most f faults a path (Searched; the body's own Random is then seeded with 0). Under weir run, Search takes every draw's first answer and no fault.
fn world: Runs body in a simulated world: the deterministic executor a test uses.
struct Network: How net_world's network misbehaves, each from the world's draws. Of a hundred completions, fail fail with ECONNRESET (104) when their op waits on a descriptor (accept, connect, recv, send), and short of the others move fewer bytes than they could when they are a recv or send that could move more than one; and each completion takes up to latency ticks of virtual time after the one before it. All three 0: every op completes whole in zero time. A failed op does nothing else: a failed send delivers none of its bytes, a failed recv takes none of those waiting, a failed connect makes no connection and a failed accept leaves the connection queued for the next; the connection stays open on both ends. A short send delivers the first bytes of its buffer, a short recv takes the first of those waiting.
effect Nodes: std::net::Net for a simulated network of nodes (systems.md §21.12): the ops of Net, and the processes node runs its code as. net_world handles it. A task belongs to the process of the task that spawned it, so a node's process is its code and every task that code started, and ending it ends them all, as a process's death ends its threads.
fn net_world: world over a simulated network: the deterministic Net executor a test uses.
struct Disk: How a simulated disk misbehaves, each from the world's draws (systems.md §21.14). Of a hundred read_at, write_at and sync, fail fail with EIO (5): a failed read or write leaves the disk as it was, and a failed sync leaves what it was to make durable (a file's unsynced writes, a directory's unsynced names) readable but never durable: a later sync succeeds without making it so, and any crash takes it back, as Linux's has since 4.13 (its rare arm: taken back at once, as if evicted from the cache); of a hundred write_at, full fail with ENOSPC (28); of a hundred read_at and write_at of more than one byte, short move fewer, a strictly short part (Draw.part); and right after an op that changed the disk the machine crashes crash times in a hundred (disk_world). All four 0: the disk never misbehaves.
fn lose_unsynced: What a crash leaves of the Loopback tree (systems.md §21.14): its unsynced name changes (creations, mkdirs, removes and renames no sync of their directory made durable), then each file holding unsynced writes, are settled as Draw.pick(n) answers among the n ways disk_unsynced and disk_settle count: lost (the common arm), kept, or torn, a file's last write cut to its first half, missing its first half, or missing its second half with the file as long as if it were written (a missing byte reads as before the write, zero past the file's old end). What a failed sync left is lost either way. A crash calls it where it happens, before anything closes a file, since a close syncs. It settles all of the tree, not only the crashed program's part.
fn disk_root: The root directory of the Loopback tree, the simulated disk, opened as MemFs.root() opens it: a descriptor every handler of the tree's ops serves, net_world's among them.
fn disk_faults: Runs body with its file ops misbehaving as disk says (DiskFaults), each fault drawn from the world's Draw: a node's disk in net_world, whose Net serves the simulated tree's files, which disk_root() opens. disk.crash is not read: a node crashes where its program says, and lose_unsynced settles the disk there.
fn disk_world: Runs boot, a program from its start, on a simulated disk (systems.md §21.14): a directory of the root's Loopback tree that no other world of the run uses, empty at the first boot and removed when the world ends, which MemTree.root() opens, misbehaving as disk says with each draw from draws. A write is durable once a sync or a close of a descriptor opened with WRITE answers; a name (a creation, mkdir, remove or rename) once a sync of its directory answers. A crash, at the first op after one that changed the disk, leaves the unsynced names and each file holding unsynced writes lost (as at the last sync), torn (every unsynced change but the last, and of a file's last write its first half) or kept, cancels the boot there, and boots again, until a boot runs to its end: its value is the world's. Under Seed(s) one seed is one history of faults and crashes; under Search(f) weir explore enumerates every history with at most f rare arms (a crash, a torn or kept outcome, a failed or short op). What a test checks across boots, what was acknowledged, lives outside the world, captured by boot.
effect Crash: A simulated node's process dying (systems.md §21.12) [from FoundationDB's simulated reboots]: the op a crash point performs when it fires. The node's code stops there: every task it started is cancelled where it waits, and the code unwinds to the node that runs it, running its guards and drop glue on the way, so the descriptors it held close as a dead process's do and its peers see their connections reset, and what it kept in memory is gone. node then runs it again from the start, its recovery path, which knows only what it reads back: its durable state (a file, or portable state the test lends it).
fn crash_point: A point where the node may crash, a fault point (§21.5) whose fault is the crash: under Draws::Search(f) a rare arm that spends the budget, under Seed p times in a hundred, and never under std::rand::Calm, so production code keeps its crash points.
fn node: Runs body, a node's code, as a process of net_world's, until it returns without crashing: each crash ends the process, every task body started with it as a process's threads die, unwinds body and runs it again from the start. A body that returns ends its process too, as a main that returns does: a server whose body spawns a task per connection keeps its tasks while body serves. Returns how many times it crashed. A node's state that should survive a crash lives outside body, as a disk outlives a process; a crash first leaves each write the simulated disk holds unsynced lost, torn or kept (lose_unsynced), so a node's files survive it as their last syncs left them.

handler `SimClock`

pub handler SimClock(mut t: Int) for Clock

A clock stopped at t that runs no tasks: sleep moves it forward and returns at once. Install it as with SimClock(0) { … }.

Handles Clock, with clauses:

fn now()
tail fn sleep(d: Int)

handler `SimStdin`

pub handler SimStdin(input: &[u8], mut at: usize) for Stdin

A scripted standard input: Stdin.read and Stdin.read_line answer the bytes of input from offset at on, as the root's answer the process's, and 0 once they are all read. Install it as with SimStdin(b"one\ntwo\n", 0usize) { … } around code written with Stdin.

Handles Stdin, with clauses:

tail fn read(b: &mut [u8])
tail fn read_line(b: &mut [u8])

handler `SimRandom`

pub handler SimRandom(seed: Atomic<Int>): shared for Random

A linear congruential generator from seed: each number is the next state, in 0..2147483648. Install it as with SimRandom(atomic(42)) { … }; one seed, one sequence (where draws do not race, as on world's one thread).

Handles Random, with clauses:

fn next()

handler `Sampled`

pub handler Sampled: shared for Draw with Random

std::rand::Draw sampled from Random (install inside a SimRandom): pick(n) is a draw modulo n, delay(max) one modulo max + 1, fault(p) whether one modulo 100 is below p, part(n) 1 plus one modulo n - 1. A draw is spent only where a choice exists, so a seed's history does not depend on choices it never had.

Handles Draw, with clauses:

fn pick(n: Int)
fn delay(max: Int)
fn fault(p: Int)
fn part(n: Int)

handler `Searched`

pub handler Searched(faults: Atomic<Int>): shared for Draw

std::rand::Draw searched: each draw is a weir explore choice point.

Each draw has a common arm and rare ones, and a path takes at most faults rare arms (install as with Searched(atomic(2)) { … }). pick(n)'s common arm is 0 (the oldest enabled op, the first task due), every other answer rare; fault(p) for p > 0 is rare when true (p weighs nothing: a fault is reachable or not), and delay(max) for max > 0 when it answers max. part(n), the size of a short count, answers 1 as its common arm and n - 1 or n / 2 as rare ones, the sizes that take different paths through a reader's loop. Past the budget every draw is its common arm and no choice, so the search spends its paths on combinations of few deviations, and weir explore --stop-on-failure reports a failure with as few rare arms as any has.

Handles Draw, with clauses:

fn pick(n: Int)
fn delay(max: Int)
fn fault(p: Int)
fn part(n: Int)

enum `Draws`

pub enum Draws: copy {
    Seed(Int),
    Search(Int),
}

Where a world's draws come from: Seed(s) samples them from a generator seeded with s (one seed, one history), Search(f) makes each a weir explore choice point with at most f faults a path (Searched; the body's own Random is then seeded with 0). Under weir run, Search takes every draw's first answer and no fault.

Variants:

Seed(Int)
Search(Int)

fn `world`

pub fn world<T>(
    start: Int,
    draws: Draws,
    body: fn() -> T with
        Tasks any portable inside(Random, Draw, captures),
        Random any portable,
        Draw any portable env {S},
) -> T with Alloc {alloc: tail} portable, Panic

Runs body in a simulated world: the deterministic executor a test uses.

world(0, Draws::Seed(1), || { … }): its clock starts at start, its draws come from draws, and the tasks it spawns run with it on one thread, in virtual time (time passes only while every task sleeps), until every one has finished; one seed is one schedule, and Search makes each pick among tasks due at once a weir explore choice. No task moves to another thread, so body may hold what is not portable; a task may capture the Tasks capability, the generator and what the body's literal captures. Panics if body did not finish (stop() cancelled it), or on a deadlock: nothing is due and a task waits on a key no task can wake (--explain-path names each).

Tasks interleave where one suspends (sleep, yield_now, park) and at a preemption point (Tasks.preempt(), where every std::sync wait begins): under Search a preemption is a rare arm that runs the other tasks ready at the time first. Under Search, weir explore may also pause a task after each atomic operation, critical section left holding no lock, or std call that synchronised, a rare arm too, so another task's work lands between two atomic operations of one task (a lost update by load then store); natively a task runs on between its suspensions (systems.md §21.17 says what the search covers and what it does not).

Committed interface (std/sim.iface):

bound Alloc: Alloc { alloc: tail } any portable
bound Panic: Panic { panic: terminal } any
may diverge
performs with no capability: Alloc
scheduling point: always
holds what may not move at a scheduling point: always
destroys values of T
callback body: envelope {S}; pinned: always

struct `Network`

pub struct Network: copy {
    pub fail: Int,
    pub short: Int,
    pub latency: Int,
}

How net_world's network misbehaves, each from the world's draws. Of a hundred completions, fail fail with ECONNRESET (104) when their op waits on a descriptor (accept, connect, recv, send), and short of the others move fewer bytes than they could when they are a recv or send that could move more than one; and each completion takes up to latency ticks of virtual time after the one before it. All three 0: every op completes whole in zero time. A failed op does nothing else: a failed send delivers none of its bytes, a failed recv takes none of those waiting, a failed connect makes no connection and a failed accept leaves the connection queued for the next; the connection stays open on both ends. A short send delivers the first bytes of its buffer, a short recv takes the first of those waiting.

Fields:

pub fail: Int
pub short: Int
pub latency: Int

effect `Nodes`

pub effect Nodes : Net default portable migrates cross {
    fn enter_node() -> Int;
    fn end_node(parent: Int);
}

std::net::Net for a simulated network of nodes (systems.md §21.12): the ops of Net, and the processes node runs its code as. net_world handles it. A task belongs to the process of the task that spawned it, so a node's process is its code and every task that code started, and ending it ends them all, as a process's death ends its threads.

op `enter_node`

fn enter_node() -> Int;

Control kind tail: the clause's result is the op's, and the performer goes on, never aborted or suspended.

The running task starts a process of its own: it, and every task it spawns from now on, belong to the new process until it ends. Answers the process the task belonged to.

op `end_node`

fn end_node(parent: Int);

Control kind tail: the clause's result is the op's, and the performer goes on, never aborted or suspended.

Ends the running task's process: every other task of it is cancelled where it waits (its op in flight asked to cancel, as stop() asks; one not yet started before it starts), and one that runs on with a completion that came first is cancelled at its next op. The running task goes back to process parent, which enter_node answered.

fn `net_world`

pub fn net_world<T>(
    start: Int,
    draws: Draws,
    net: Network,
    body: fn() -> T with
        Nodes any portable inside(Draw, captures),
        Random any,
        Draw any portable env {S},
) -> T with Alloc {alloc: tail} portable, Loopback portable, Panic

world over a simulated network: the deterministic Net executor a test uses.

Runs body as world does, with Nodes, and so std::net::Net, served by the root's Loopback, the in-memory network of one host (Net says which address reaches which listener), on every backend: net_world(0, Draws::Seed(1), Network { fail: 0, short: 0, latency: 0 }, || { … }). Which enabled op completes next, after how many ticks, and whether it fails or comes up short are drawn from draws as net says: under Seed one seed is one schedule and one network history, under Search(f) weir explore enumerates every schedule and history with at most f faults (a failed op, a short count, a full latency, a preemption). Panics on a deadlock, when every task left waits on the network or on a key no task can wake (--explain-path names each), or when the body did not finish. Call stop() when the body is done so that a server still waiting is cancelled and its cleanup runs. A task that serves owns its listener (move(l on_abort { close(l) })): the body runs first and its tasks start when it suspends or returns, so a listener the body opened is moved into the acceptor task.

A task may borrow portable state declared outside the call (a server's counters the test reads once net_world returns): Nodes is installed inside the call, so it ends before they do. node runs a crashable node's code as a process of its own.

Committed interface (std/sim.iface):

bound Alloc: Alloc { alloc: tail } any portable
bound Loopback: Loopback any portable
bound Panic: Panic { panic: terminal } any
may diverge
performs with no capability: Alloc
scheduling point: always
holds what may not move at a scheduling point: always
destroys values of T
callback body: envelope {S}; pinned: always

struct `Disk`

pub struct Disk: copy {
    pub fail: Int,
    pub short: Int,
    pub full: Int,
    pub crash: Int,
}

How a simulated disk misbehaves, each from the world's draws (systems.md §21.14). Of a hundred read_at, write_at and sync, fail fail with EIO (5): a failed read or write leaves the disk as it was, and a failed sync leaves what it was to make durable (a file's unsynced writes, a directory's unsynced names) readable but never durable: a later sync succeeds without making it so, and any crash takes it back, as Linux's has since 4.13 (its rare arm: taken back at once, as if evicted from the cache); of a hundred write_at, full fail with ENOSPC (28); of a hundred read_at and write_at of more than one byte, short move fewer, a strictly short part (Draw.part); and right after an op that changed the disk the machine crashes crash times in a hundred (disk_world). All four 0: the disk never misbehaves.

Fields:

pub fail: Int
pub short: Int
pub full: Int
pub crash: Int

fn `lose_unsynced`

pub fn lose_unsynced() with Draw any cross, Loopback any

What a crash leaves of the Loopback tree (systems.md §21.14): its unsynced name changes (creations, mkdirs, removes and renames no sync of their directory made durable), then each file holding unsynced writes, are settled as Draw.pick(n) answers among the n ways disk_unsynced and disk_settle count: lost (the common arm), kept, or torn, a file's last write cut to its first half, missing its first half, or missing its second half with the file as long as if it were written (a missing byte reads as before the write, zero past the file's old end). What a failed sync left is lost either way. A crash calls it where it happens, before anything closes a file, since a close syncs. It settles all of the tree, not only the crashed program's part.

Committed interface (std/sim.iface):

bound Draw: Draw any cross
bound Loopback: Loopback any
may diverge
scheduling point: Draw not quiet | Loopback not quiet

fn `disk_root`

pub fn disk_root() -> Result<Fd, Int> with Alloc {alloc: tail} portable, Loopback portable

The root directory of the Loopback tree, the simulated disk, opened as MemFs.root() opens it: a descriptor every handler of the tree's ops serves, net_world's among them.

Committed interface (std/sim.iface):

bound Alloc: Alloc { alloc: tail } any portable
bound Loopback: Loopback any portable
may diverge
scheduling point: always

fn `disk_faults`

pub fn disk_faults<T>(disk: Disk, body: fn() -> T with Fs env {A, S}) -> T with
    Fs any portable cross,
    Draw any portable cross,
    Alloc {alloc: tail} portable,
    Loopback portable,

Runs body with its file ops misbehaving as disk says (DiskFaults), each fault drawn from the world's Draw: a node's disk in net_world, whose Net serves the simulated tree's files, which disk_root() opens. disk.crash is not read: a node crashes where its program says, and lose_unsynced settles the disk there.

Committed interface (std/sim.iface):

bound Fs: Fs any portable cross
bound Draw: Draw any portable cross
bound Alloc: Alloc { alloc: tail } any portable
bound Loopback: Loopback any portable
aborts: Fs.list, Fs.mkdir, Fs.open, Fs.read_at, Fs.remove, Fs.rename, Fs.size, Fs.sync, Fs.write_at
scheduling point: always
callback body: envelope {A, S}

fn `disk_world`

pub fn disk_world<T>(
    draws: Draws,
    disk: Disk,
    boot: fn() -> T with MemTree any portable, Draw any portable env {S},
) -> T with Alloc {alloc: tail} portable, Loopback portable, Panic

Runs boot, a program from its start, on a simulated disk (systems.md §21.14): a directory of the root's Loopback tree that no other world of the run uses, empty at the first boot and removed when the world ends, which MemTree.root() opens, misbehaving as disk says with each draw from draws. A write is durable once a sync or a close of a descriptor opened with WRITE answers; a name (a creation, mkdir, remove or rename) once a sync of its directory answers. A crash, at the first op after one that changed the disk, leaves the unsynced names and each file holding unsynced writes lost (as at the last sync), torn (every unsynced change but the last, and of a file's last write its first half) or kept, cancels the boot there, and boots again, until a boot runs to its end: its value is the world's. Under Seed(s) one seed is one history of faults and crashes; under Search(f) weir explore enumerates every history with at most f rare arms (a crash, a torn or kept outcome, a failed or short op). What a test checks across boots, what was acknowledged, lives outside the world, captured by boot.

Committed interface (std/sim.iface):

bound Alloc: Alloc { alloc: tail } any portable
bound Loopback: Loopback any portable
bound Panic: Panic { panic: terminal } any
may diverge
scheduling point: always
holds what may not move at a scheduling point: always
destroys values of T
callback boot: envelope {S}; pinned: always; holds boot
cleanup on an abort suspends on Loopback

effect `Crash`

pub effect Crash {
    fallible fn crash();
}

A simulated node's process dying (systems.md §21.12) [from FoundationDB's simulated reboots]: the op a crash point performs when it fires. The node's code stops there: every task it started is cancelled where it waits, and the code unwinds to the node that runs it, running its guards and drop glue on the way, so the descriptors it held close as a dead process's do and its peers see their connections reset, and what it kept in memory is gone. node then runs it again from the start, its recovery path, which knows only what it reads back: its durable state (a file, or portable state the test lends it).

op `crash`

fallible fn crash();

Control kind fallible: the clause resumes at once or aborts the with (abort(v)), so the perform is an abort edge.

The node crashes here: its tasks end, and its code unwinds to node, which runs it again.

fn `crash_point`

pub fn crash_point(p: Int) with Draw cross, Crash migrates cross

A point where the node may crash, a fault point (§21.5) whose fault is the crash: under Draws::Search(f) a rare arm that spends the budget, under Seed p times in a hundred, and never under std::rand::Calm, so production code keeps its crash points.

Committed interface (std/sim.iface):

bound Draw: Draw any cross
bound Crash: std::sim::Crash cross
migrates: Crash.crash migrates inline
aborts: Crash.crash
scheduling point: Crash not quiet | Draw not quiet

fn `node`

pub fn node(body: fn() with Crash any portable) -> Int with
    Nodes any portable cross,
    Draw any portable cross,
    Loopback any portable,

Runs body, a node's code, as a process of net_world's, until it returns without crashing: each crash ends the process, every task body started with it as a process's threads die, unwinds body and runs it again from the start. A body that returns ends its process too, as a main that returns does: a server whose body spawns a task per connection keeps its tasks while body serves. Returns how many times it crashed. A node's state that should survive a crash lives outside body, as a disk outlives a process; a crash first leaves each write the simulated disk holds unsynced lost, torn or kept (lose_unsynced), so a node's files survive it as their last syncs left them.

Committed interface (std/sim.iface):

bound Nodes: std::sim::Nodes any portable cross
bound Draw: Draw any portable cross
bound Loopback: Loopback any portable
may diverge
scheduling point: Draw not quiet | Loopback not quiet | Nodes not quiet
callback body: envelope {A, S}; holds body

Module std::sim

handler SimClock

handler SimStdin

handler SimRandom

handler Sampled

handler Searched

enum Draws

fn world

struct Network

effect Nodes

op enter_node

op end_node

fn net_world

struct Disk

fn lose_unsynced

fn disk_root

fn disk_faults

fn disk_world

effect Crash

op crash

fn crash_point

fn node

Module `std::sim`

handler `SimClock`

handler `SimStdin`

handler `SimRandom`

handler `Sampled`

handler `Searched`

enum `Draws`

fn `world`

struct `Network`

effect `Nodes`

op `enter_node`

op `end_node`

fn `net_world`

struct `Disk`

fn `lose_unsynced`

fn `disk_root`

fn `disk_faults`

fn `disk_world`

effect `Crash`

op `crash`

fn `crash_point`

fn `node`