Interleave: Concurrency Replay

Concurrent code can pass ordinary tests and still fail under a rare thread schedule. When that happens, developers need a repeatable way to expose and inspect the failure. Interleave is a proof-of-concept .NET concurrency-testing workflow built around a Last Seat reservation example. A developer runs sequential tests, uses Microsoft Coyote to systematically explore thread interleavings, reviews the violated capacity invariant, and replays a frozen trace to reproduce the same failure. IBM Bob IDE was used to build the sample, Coyote instrumentation, tests, and replay artifact. The intended users are .NET developers investigating race conditions in code that performs check-then-act operations. In the current example, ordinary sequential tests pass; Coyote explored eight paths and found that two callers could reserve a seat with capacity one; the saved trace reproduces that failure. The trace gives a concrete, repeatable artifact for debugging and review instead of relying on timing-sensitive reproduction. The distinctive idea is to treat a concurrency failure as an inspectable witness that can be replayed. This prototype currently demonstrates discovery and reproduction for one scenario. It does not yet repair the race, prove a repaired system race-free, cover arbitrary repositories, or provide a polished interactive interface. The next milestone is Bob-assisted root-cause analysis and repair, followed by replay and additional bounded exploration against the repaired code.