weave

Systematic, deterministic exploration of concurrent Go — the schedule space, not one lucky run.

Go has no loom. weave is that tool: a scheduler that makes every scheduling decision itself and walks the decision tree, so a concurrency bug is found on purpose rather than by luck.

func TestTransfer(t *testing.T) {
    weave.Check(t, func(w *weave.W) {
        balance := weave.NewVar(w, "balance", 100)
        w.Go("withdraw", func() { balance.Set(balance.Get() - 10) })
        w.Go("deposit",  func() { balance.Set(balance.Get() + 50) })
    })
}

Fails on the first run. Every run.

---

Why this exists

go test -race is very good at what it does, and what it does is observe the interleaving that actually happened. If your machine's scheduler never produces the one ordering that breaks the code, the detector has nothing to report. -count=1000 is a lottery with better odds, not a proof — and the interleavings a quiet laptop produces are exactly the ones production doesn't.

testing/synctest (GA in Go 1.25) makes concurrent tests deterministic, which is a real advance. But it is deterministic in one schedule; the docs are explicit that it is not a full deterministic scheduler for every possible race.

Rust has had loom for this since 2019. Go's only comparable work is an academic prototype (GoPie, ASE'23). This is the gap.

What it does

Exactly one modelled goroutine runs at a time. Every synchronisation operation — Lock, Unlock, Send, Recv, Wait, and every access to a shared weave.Var — hands control back to the scheduler. The set of scheduling points is therefore finite and the state space is walkable.

The scheduler explores it depth-first with replay: each run re-executes the body from scratch under a prefix of forced choices, then backtracks into the next unexplored branch. Stateless model checking, à la Verisoft and CHESS — it costs re-execution but needs no snapshotting of your program's heap.

It detects:

• data races, via vector clocks — reported as a missing happens-before edge between two named accesses
• deadlocks, with every goroutine's blocking reason
• broken invariants you state with w.Assert — bugs that are not races at all
• panics, attributed to the schedule that caused them

and then minimises the failing schedule by delta debugging before printing it as a ladder diagram.

Output

A lock-order inversion. It needs a preemption between the two acquisitions — the interleaving a stress test almost never produces:

weave: deadlock found after exploring 11 schedule(s)

  all goroutines are blocked
      G1 a          blocked on lock m2
      G2 b          blocked on lock m1

minimal failing interleaving (1 preemption(s)):

  G0 main                   G1 a                      G2 b
  -----------------------   -----------------------   -----------------------
  go a                                                                          weave_test.go:146
  go b                                                                          weave_test.go:152
>                           lock m1                                             weave_test.go:147
                            lock m2                                             weave_test.go:148
>                                                     lock m2                   weave_test.go:153
                                                      lock m1                   weave_test.go:154
                                                      BLOCKED lock m1
>                           BLOCKED lock m2

> marks a context switch. BLOCKED marks a park — without it, a lock attempt that blocked would be indistinguishable in the trace from one that succeeded, which is the most misleading thing a deadlock trace could do.

The bug -race can never find

This transfer releases the lock between the debit and the credit:

mu.Lock(); a.Set(a.Get() - 10); mu.Unlock()   // the invariant is broken across this gap
mu.Lock(); b.Set(b.Get() + 10); mu.Unlock()

Every access is under the mutex. There is no data race — not "unlikely to be detected", but none to detect. go test -race will be silent on this code forever, however many times you run it. Yet an auditor taking the same lock in between sees money that has left one account and not arrived at the other:

weave: panic found after exploring 13 schedule(s)

  assertion failed: money conservation violated: a+b = 90, want 100

minimal failing interleaving (1 preemption(s)):

  G0 main                   G1 transfer               G2 audit
  -----------------------   -----------------------   -----------------------
  go transfer                                                                   weave_test.go:92
  go audit                                                                      weave_test.go:101
>                           lock mu                                             weave_test.go:93
                            read a                                              weave_test.go:94
                            write a                                             weave_test.go:94
                            unlock mu                                           weave_test.go:95
                            lock mu                                             weave_test.go:97
                            BLOCKED lock mu
>                                                     lock mu                   weave_test.go:102
                                                      read a                    weave_test.go:103
                                                      read b                    weave_test.go:103

Atomicity violations across correctly-locked critical sections are a whole class of production bug that no race detector addresses. weave finds them because it checks your invariant, under every schedule.

A data race with zero preemptions

The lost-update example above is reported with 0 preemptions — the two goroutines run one after the other, never overlapping.

That is not a bug in the report. A data race is defined by the absence of a happens-before edge, not by two instructions landing at the same instant. Goroutine B reading a value A wrote, with no channel, lock, or atomic between them, is a race even if the hardware never runs them concurrently — and it is a race that will bite the moment the compiler reorders or a second core gets involved. Vector clocks see this; wall-clock intuition does not.

Preemption bounding

Search follows Musuvathi and Qadeer's CHESS: switching away from a goroutine that could have kept running costs one preemption; switching because it blocked or finished is free. CHESS's empirical result is that the majority of real concurrency bugs surface within a bound of 1–3, so the default is 2.

This is load-bearing, not a knob. With the bound set to zero, the lock-order deadlock above is genuinely unreachable — there is no legal schedule that produces it. One preemption exposes it. There is a test that pins exactly that.

API

weave.Check(t, func(w *weave.W) { ... })                 // default config
weave.CheckConfig(t, weave.Config{MaxPreemptions: 3}, f) // tuned
weave.Explore(cfg, f)                                    // outside a test

Inside the body:

Unbuffered channels are a genuine rendezvous: the sender parks until a receiver takes the value, rather than being modelled as a one-slot buffer.

Limits, stated plainly

weave checks code written against its primitives, not your production types. That is the same bargain loom makes, for the same reason: you cannot explore a schedule space you do not control.

• Models Mutex, RWMutex, WaitGroup, channels, atomics, shared variables.
• Does not model select, real time, or I/O.
• The body must be deterministic given the schedule — no map iteration order, no rand, no raw go statements — or replay is meaningless.
• The space is explored under a preemption bound, so a clean result means "no bug within the bound", not "no bug".
• Stateless search re-executes the body once per schedule. That is fine for unit-sized concurrency and wrong for whole programs.

For finding leaked goroutines in ordinary production code without rewriting it against a model, see the sibling project tether, which does it statically.

Install

go get github.com/tachyurgy/weave

Design notes

• sched.go — the scheduler. Control passes between it and exactly one goroutine by strict alternation over two unbuffered channels; that is what makes a run reproducible. Blocked goroutines carry a ready() predicate the scheduler evaluates while no user code is running, so it observes a quiescent heap and needs no locking of its own.
• race.go — vector clocks and the FastTrack-style read/write shadow state.
• prims.go — the modelled primitives. Each carries a release/acquire syncObj, which is the only legal way information crosses between goroutines.
• weave.go — the explorer: depth-first backtracking, delta-debugging minimisation, ladder rendering.

Two details worth calling out, because both are bugs a determinism tool cannot afford:

Abandoned schedules must not strand goroutines. When a run ends early — a race found, a deadlock — other modelled goroutines are still parked on their resume channels. A search over 20,000 schedules would leak them by the thousand. Teardown resumes each survivor with a sentinel panic that unwinds it. There is a test that runs 50 full searches and asserts the process goroutine count does not grow.

No range over a map on a decision path. Choosing which racing pair to report by iterating a map would make the output depend on Go's map seed — nondeterminism inside the determinism tool. Read owners are sorted.

Zero dependencies outside the standard library.

Tests

go test -race ./...

The suite is built in matched pairs: a broken version that must fail with a specific FailureKind, and the fixed version that must explore the space to exhaustion and find nothing. A checker that flags correct code is worse than no checker, so half the tests exist to prove silence.

License

MIT