BatchParallelApply: no errors found
Workers own disjoint output columns. TLC finds no interleaving in which an output cell is written twice or the final state differs from the sequential result.
Concurrency
Multi-threading HST: parallelize by batch, not by column.
The delta-apply is the hot path: given a fixed operator and a sparse change, HST recomputes only the rows affected by that change. When you have many state vectors to update at once, that work multiplies across the batch, and the batch is the axis that parallelizes cleanly.
Two axes
Batch updates can run independently. Column splits need a reduction.
Parallelize by batch. Each of the B state vectors is an independent problem against the same operator. Give each thread a separate block of the batch and it writes a separate block of the output: no locks, no shared accumulation, no reduction. Speedup tracks core count until memory bandwidth saturates.
Parallelize by column. Split the changed columns across threads and several threads contribute to the same output rows. Each needs a private partial buffer, and the partials must be summed at the end. That reduction is real work the batch path never pays, so column scaling is sub-linear, and at large batch the reduction can cost more than it saves.
For small deltas and small batches, threading buys little because the apply is already cheap. The win shows up in the workload shape that matters most for production evaluation: small deltas, large batches.
Measured
Speedup vs. single-threaded, 8 threads on a 10-core Apple M1 Max.
| Batch B | CSC · batch | CSC · column | HST · batch |
|---|---|---|---|
| 16 | 5.8× | 1.9× | 6.5× |
| 64 | 6.6× | 2.0× | 7.0× |
| 256 | 5.8× | 0.9× | 6.5× |
Measured wall-clock at T=8 on an Apple M1 Max (10-core, arm64). Operator N=M=16,000, tile 32, 256 changed columns reaching 7,776 output rows (1.33M nonzeros). Every parallel result is verified against the single-threaded result: bit-identical for batch-parallel, <1e-10 relative for column-parallel. Column-parallel at B=256 falls below 1× because the O(T·B·R) reduction outgrows the apply. These are arm64 numbers and should not be read across to x86. Measured at the embedded library level, which is the only level HST ships at: the batch-parallel path above is what its lanes run on. The B=64 and B=256 rows are kernel measurements; the shipping hst_open_batched entry point currently caps B at 32, so treat those two rows as headroom rather than as a configuration you can request today.
Live
Batch-parallel, running in your browser.
This runs a small HST-shaped delta-apply across Web Workers: single-threaded baseline vs. one batch-slice per worker. It is illustrative; browser JavaScript is not the production runtime. But the shape is the same: more workers, more speedup, until you run out of cores.
—speedup
—workers
—batch
Ready.
Runs entirely client-side with Web Workers. Hardware concurrency reported by your browser:
— logical cores. Timings vary with your machine and current load.
Verified
The concurrency is model-checked, not just benchmarked.
A fast result that is silently wrong is worse than a slow one. The threading model is specified in TLA+ and exhaustively model-checked with TLC over every possible interleaving of the workers. TLC is exhaustive over the state space it is given, not over all worker and matrix sizes, so this is a strong check on the algorithm's shape rather than a proof about the shipped binary. It complements the equality assertions in the benchmark; it does not replace them.
ColumnParallelApply (safe): no errors found
Private partials plus a reduction barrier. TLC finds no interleaving in which the reduced output differs from the sequential result.
ColumnParallelApply (naive): race caught
Drop the reduction barrier and write straight into shared state, and TLC returns a lost-update counterexample: two workers read the same value and one clobbers the other. This is why column-parallel needs the reduction.
Formal model-checking artifacts are available during technical evaluation.