You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A multi-tape Turing machine's step is simultaneous across tapes by definition, and TM-1's ISA says so: arch/mod.rs calls wrmv "the fused write+move of one formal step". The bus then throws that away. BusRequest addresses exactly one device — DeviceWrite { dev, index }, DeviceMoveLeft { dev } — so Arch::lower flattens the vectors into a sequence of up to 2N transactions, and the core waits for each.
For an in-memory tape that costs nothing real. For a physical tape stand, where a move is milliseconds of mechanism, it is the whole cost of the machine: sixteen tapes that could have stepped together step one after another.
Most of the machinery already exists
AsyncTapeDevice is per-device. Its contract is "one command in flight per device" (vm/devices/async_device.rs), so the device layer already permits a command outstanding on tape 0 while tape 1 has one too.
Devices already price themselves.DevicePoll::Ready { reply, cost: Option<u32> } lets a device report what its operation actually cost, rather than taking the model price from TactProfile.
The batch boundary already exists.Arch::lower returns a Vec<MicroOp> for exactly one instruction, and the driver walks it. That vector is the formal step.
What blocks it is upstream of all three: Core holds a single pending: Pending slot, so it never issues a second bus request before the first is answered.
Proposal
Let a device declare that it buffers rather than blocks. A buffering tapeblock accumulates at most one write and one move per tape — the bound the ISA already guarantees, since a wrmv vector has one slot per tape per kind — and executes the per-tape pairs in parallel when the batch closes.
The buffer's shape becomes the contract: 0, 1 or 2 commands per tape, and when there are 2 the write precedes the move. That bound is what makes the thing implementable in fixed hardware rather than needing an unbounded queue.
The barrier
Two, and neither needs a new bus request:
The end of an instruction's micro-op vector. The driver already knows where that is. One formal step in, one flush out.
A device's own buffer limit. A second write to a tape that already has one buffered forces a flush of that device before the new command is accepted — the same shape as today's "issue while pending is a caller bug", relaxed from a bound of 1 to a bound of 2 with a known order.
Why it is semantically safe
wrmv's rule is that ALL writes precede ALL moves, behaviorally the wr; mov pair. That rule has no cross-tape content: tapes are independent devices, and no move on one tape can observe another tape's write. So executing per-tape (write, move) pairs in parallel is observationally identical to executing them in the flattened order — the ordering that matters is within a tape, and the buffer preserves it.
Tact accounting. A parallel batch costs max of its members, not sum. DevicePoll's per-reply cost is the hook; the driver currently adds them up.
Fault timing. A StrictTape faults on the content of the cell it writes. Buffered, that fault surfaces at the flush rather than at the write, so the core has to accept a fault arriving at a barrier and attribute it to a device.
The equivalence contract needs restating, not reusing
async_equivalence.rs currently pins that a latency device "must change nothing but the number of pump calls" — same outcome, same stats, bit for bit. A parallel device deliberately breaks the tact half of that, which is the entire point of it.
So it needs its own statement, and the distinction is worth getting right: a parallel run must produce the same final tape, the same outcome, and the same step count as the serial one, and is expected to differ in tacts. Anything else moving means the parallelism changed the computation rather than its schedule.
A multi-tape Turing machine's step is simultaneous across tapes by definition, and TM-1's ISA says so:
arch/mod.rscallswrmv"the fused write+move of one formal step". The bus then throws that away.BusRequestaddresses exactly one device —DeviceWrite { dev, index },DeviceMoveLeft { dev }— soArch::lowerflattens the vectors into a sequence of up to 2N transactions, and the core waits for each.For an in-memory tape that costs nothing real. For a physical tape stand, where a move is milliseconds of mechanism, it is the whole cost of the machine: sixteen tapes that could have stepped together step one after another.
Most of the machinery already exists
AsyncTapeDeviceis per-device. Its contract is "one command in flight per device" (vm/devices/async_device.rs), so the device layer already permits a command outstanding on tape 0 while tape 1 has one too.DevicePoll::Ready { reply, cost: Option<u32> }lets a device report what its operation actually cost, rather than taking the model price fromTactProfile.Arch::lowerreturns aVec<MicroOp>for exactly one instruction, and the driver walks it. That vector is the formal step.What blocks it is upstream of all three:
Coreholds a singlepending: Pendingslot, so it never issues a second bus request before the first is answered.Proposal
Let a device declare that it buffers rather than blocks. A buffering tapeblock accumulates at most one write and one move per tape — the bound the ISA already guarantees, since a
wrmvvector has one slot per tape per kind — and executes the per-tape pairs in parallel when the batch closes.The buffer's shape becomes the contract: 0, 1 or 2 commands per tape, and when there are 2 the write precedes the move. That bound is what makes the thing implementable in fixed hardware rather than needing an unbounded queue.
The barrier
Two, and neither needs a new bus request:
Why it is semantically safe
wrmv's rule is that ALL writes precede ALL moves, behaviorally thewr; movpair. That rule has no cross-tape content: tapes are independent devices, and no move on one tape can observe another tape's write. So executing per-tape (write, move) pairs in parallel is observationally identical to executing them in the flattened order — the ordering that matters is within a tape, and the buffer preserves it.What has to change
Pendingslot becomes the limit. This is the real work, and it is why this should be settled before A hardware PM-1: RTL core against the bus contract (simulation-first arc) #87: an RTL core is built against this contract.maxof its members, notsum.DevicePoll's per-replycostis the hook; the driver currently adds them up.StrictTapefaults on the content of the cell it writes. Buffered, that fault surfaces at the flush rather than at the write, so the core has to accept a fault arriving at a barrier and attribute it to a device.The equivalence contract needs restating, not reusing
async_equivalence.rscurrently pins that a latency device "must change nothing but the number of pump calls" — same outcome, same stats, bit for bit. A parallel device deliberately breaks the tact half of that, which is the entire point of it.So it needs its own statement, and the distinction is worth getting right: a parallel run must produce the same final tape, the same outcome, and the same step count as the serial one, and is expected to differ in tacts. Anything else moving means the parallelism changed the computation rather than its schedule.