feat: refactor `ThreadTimestamps`

[DavePearce]

Summary

Overall, whilst this function appears to work correctly, its implementation leaves a lot to be desired. We should be able to improve this code relatively easily, such that it can be maintained more easily in the future and we can audited as well.

Algorithm Summary

The timestamp threading algorithm is responsible for introducing timestamps (as per #1807). For example, the following function:

memory data(u16 addr) -> (u8 byte)

fn read(u16 addr) -> (u8 r) {
[0]     r = data[addr] ; ret
}

would be turned into this:

memory data(addr:u16) -> (byte:u8)

fn read(data$stamp:u16, addr:u16) -> (data$stamp':u16, r:u8) {
[0]     r = data[data$stamp; addr] ; data$stamp' = data$stamp + 1; ret
}

The purpose of the threading algorithm is to make this change efficiently without breaking the original program.

Algorithm (One Line Functions)

In this section, we consider only the case for one-line functions. In fact, extending to multi-line functions is relatively trivial. A one-line function consists only of a single bytecode vector. For the purposes of this discussion, we care only and bytecodes which read/write ram, which impact control-flow (e.g. skip_if) and which terminate a vector (e.g. ret). Without loss of generality, we will also only consider the case of adding the timestamp for a single ram --- again, extending to multiple rams is trivial once it works for one.

Source / Target Stamp

Every vector has a source register holding the current stamp, and a target register which must hold the final stamp. For a one-line function, the source is always the stamp parameter and the target is always the corresponding return. For example:

memory data(addr:u16) -> (byte:u8)

fn read(stamp:u16, addr:u16) -> (stamp':u16, r:u8) {
[0]     r = data[stamp; addr] ; stamp' = stamp + 1; ret
}

Here, stamp is the vector source and stamp' is the vector target.

Stamp Versioning

Following the ideas of static-single assignment form, we use a labelling scheme for introduced temporary stamp registers called "versioning". If stamp is our source, and stamp' our target, then we might also have intermediate registers such as stamp'1, stamp'2, etc. In general, we stay that the stamp parameter has version 0 and, hence, we never write stamp'0.

A minimal example to illustrate would be the following vector:

... = ram[stamp; ...] ; stamp'1 = stamp + 1; ... = ram[stamp'1; ...] ; stamp' = stamp'1 + 1; ret

Here, we can see that stamp'1 is introduced as a temporary intermediate register to hold the stamp value in between reads.

Stamp Conflicts

Stamp conflicts arise at control-flow meet points where the incoming stamps have different versions. A minimal example is the following:

skipif x==0 2 ; ... = ram[stamp; ...] ; stamp' = stamp + 1; ret

When the skipif is taken it branches over the two assignments to the ret. The issue with this example is that, when this happens, the target stamp' has not been assigned. This is evident because, at the ret, we have differing versions for stamp. To identify this, we can use an algorithm in the style of a data-flow analysis to determine the stamp's version before each instruction in the vector. For our example above, this would produce the following:

{0} skipif x==0 2 ; {0} ... = ram[stamp; ...] ; {0} stamp' = stamp + 1; {1} ret

Specifically, the version recorded before each instruction is the largest version which can reach that instruction. Also, since a vector can essentially be viewed as a Directed Acyclic Graph (DAG), the dataflow analysis does not need to be iterated to a fixed point.

Using this information we can spot the conflict when we look at the initial skipif, since it is branching from a position with version 0 to a position with version 1 --- i.e. a conflict.

Resolving Conflicts

Conflict resolution is a process of ensuring matching versions are used at control-flow meet points. There are different resolution strategies to use depending on the context and instructions involved. The essential strategy to resolving conflicts is to referred to here as "stamp forwarding". Specifically, if we are going from a position with version X to a position with version Y then we simply assign stamp'X to `stamp'. The difficulty lies in finding a suitable place to insert the necessary instruction.

For our example above, we can resolve the conflict with a simple transformation like so:

{0} skipif x!=0 2 ; {0} stamp' = stamp ; {1} skip 2 ; {0} ... = ram[stamp; ...] ; {0} stamp' = stamp + 1; {1} ret

To resolve this conflict a "trampoline" has been introduced by inverting the skipif. Specifically, a trampoline is a sequence of instructions which updates the stamp and then "bounces" onto the original intended destination.

NOTE: other instructions which impact control-flow include switch and dispatch instructions.

Threading Single Vectors

To thread a bytecode vector given the source and target registers, the process is therefore:

1. (Versioning Analysis) We utilise the DFA framework to construct the stamp version information which holds before each instruction.
2. (Conflict Resolution) We traverse the vector looking for conflicts and resolve them by inserting trampolines as necessary.

Algorithm (Multi-Line Function)

Since the stamp registers are added specifically for the purpose of threading, we can actually simplify the multi-line case to be a minor extension of the one-line case. Specifically, we have:

• (Inital Vector). For the vector at pc==0 we have the source stamp as the incoming parameter (i.e. stamp), and the target stamp as the corresponding return variable (i.e. stamp').
• (Other Vectors). For a vector at pc>0 we have both the source and target stamps as the corresponding return variable stamp').

Reusing the return variable stamp' works because nothing else is using this register and, since its a multi-line function, we can assign to it across vectors. Thus, the problem primarily becomes one of versioning the stamp within a vector. Furthermore, introduced temporary registers (e.g. stamp'1) can be reused across vectors.

NOTE: In the very special case that the inital vector at pc==0 is itself a jump destination, then we cannot use the incoming parameter as the source stamp. This is because, when control comes from some internal jmp, the stamp will be located in the return stamp'. Therefore, we are forced to introduce a new initial vector which simple moves stamp into stamp' to eliminate the conflict.

[OlivierBBB]

Implemented in #2122, with one addition to the sketch above and one deliberate deviation, both worth recording here.

Addition — naming the final version. The examples above write the last advance directly into stamp' (e.g. stamp' = stamp'1 + 1), which is what keeps a one-line function at one added instruction — but the rule selecting which version gets to be stamp' is left implicit. The PR makes it explicit: per row, the largest version live at any exit binds to the canonical register; every other version gets a fresh temporary. Monotonicity of versions along a path makes this safe (no path can define that version and later write the canonical again).

Deviation — no trampolines. Conflict resolution keeps the existing placement machinery (edge blocks + skip retargeting in rebuildVector) rather than inverting branches: inversion doesn't generalise to switch/dispatch, and the placement code handles all three uniformly. The panic on conditional edges carrying distinct stamps into one merge point remains an unsupported shape — though it now fires strictly less often, since same-count paths compare equal as versions where the old position-tagged states conflicted.

Measured trade. On the linea riscv corpus the refactor is a net win (8087 → 7913 instructions, rows identical), but pure versioning cannot fully match the old base+offset scheme: when sibling branches each perform an access, both define the same version register, and an early-exiting path keeps a definition only its sibling consumes (+12 instructions across 4 functions, write_16 the worst at +2). The old scheme's position-tagged bases existed precisely to give sibling-path definitions distinct registers. Two recovery mechanisms (value-chain folding with per-instance retraction via row-DAG reachability) were implemented and measured at +230 lines of machinery for those 12 instructions, and dropped.