A store-buffer memory-model interpreter

Implement a deterministic interpreter for a small store-buffer machine:

pub fn interpret(program: Vec<Instr>, schedule: Vec<usize>) -> Vec<i64>

This is a teaching model with explicit rules. It runs no real threads and uses no atomics. Its seq_cst flag selects the behavior below; these rules are not a specification or implementation recipe for Rust's memory model.

Machine state

There are two threads, two shared variables and two registers per thread, all indexed by 0 or 1. Memory and registers start at zero. Each thread also has an initially empty FIFO buffer of pending (variable, value) writes.

Keep the supplied enum and its fields unchanged because the harness constructs it:

#[derive(Clone, Copy)]
pub enum Instr {
    Store { thread: usize, var: usize, value: i64, seq_cst: bool },
    Load  { thread: usize, var: usize, reg: usize, seq_cst: bool },
    Flush { thread: usize },
}

Inputs use valid variable and register indices. Instructions for thread IDs other than 0 or 1 are ignored.

Instruction rules

Every reference to a buffer in this table means the executing thread's own buffer. Draining writes every pending entry to shared memory in FIFO order.

Instruction	Effect
`Store`, `seq_cst: false`	Append the write to the buffer; leave shared memory unchanged.
`Store`, `seq_cst: true`	Drain the buffer, then write the new value directly to shared memory.
`Load`, `seq_cst: false`	Read the newest buffered write to that variable, if any; otherwise read shared memory. Save the value in the selected register.
`Load`, `seq_cst: true`	Drain the buffer, then read shared memory into the selected register.
`Flush`	Remove the oldest buffered write and apply it to shared memory. An empty buffer makes this a no-op.

A relaxed load can read its own pending writes through store-to-load forwarding, but cannot inspect the other thread's buffer. For example, buffered writes x = 3, then x = 7, make a relaxed load of x return 7. A single Flush instead publishes the oldest write, x = 3.

Schedule and return value

Preserve the relative order of each thread's instructions in program. Each entry in schedule executes that thread's next instruction. Skip an entry if its thread ID is outside 0..2 or that thread has no instructions left. Instructions the schedule never reaches do not execute.

After the schedule, drain thread 0's buffer completely, then thread 1's. This fixed cleanup order is an exercise convention. It affects final memory when both buffers contain writes to the same variable. It does not run any remaining instructions or change values already saved in registers.

Return exactly:

[t0.r0, t0.r1, t1.r0, t1.r1, mem[0], mem[1]]

An empty program or empty schedule returns six zeros.

Worked example: store buffering

Let x be variable 0 and y be variable 1:

T0: store x = 1; load y into t0.r0
T1: store y = 1; load x into t1.r0
schedule: [0, 0, 1, 1]

With all four instructions using seq_cst: false, T0 buffers its write and reads y = 0. T1 then buffers its write and reads x = 0: T0's write is still pending. Final draining publishes both writes, so the result is [0, 0, 0, 0, 1, 1]. The registers keep the earlier load results.

Set all four flags to true and the result becomes [0, 0, 1, 0, 1, 1]. T0 writes x directly before reading the initial y; T1 writes y directly before reading x = 1.

What to change

The starter writes every store directly to memory and reads every load from memory, ignoring the flag. Implement buffering, forwarding, single-entry flushing and final draining using the rules above. The supplied per-thread instruction lists and program counters already handle scheduling.

Limits of the model

Testing can expose a memory-ordering bug; a passing run does not establish that every possible execution is correct. This interpreter makes one chosen execution reproducible, but does not explore schedules for you.

It also omits acquire/release operations, fences and read-modify-write operations. Use Rust's actual atomic-ordering guarantees when reasoning about concurrent Rust code. A result from this exercise alone cannot establish that a real concurrent algorithm is correct.