Send and Sync: The Predicates the Safety Rests On, and a Hole in One

The concurrency design from the last episode rests its entire safety story on two questions the type system must be able to answer about any value: is it safe to move to another thread (that property is called Send), and is it safe to share a reference to it across threads (Sync). Get those two predicates right and the data races the design exists to prevent cannot happen; get them wrong and the whole guarantee is a fiction. This episode is about how they were built — deliberately small — and about the subtle hole that smallness let hide.

Two more predicates, not a trait system

Consistent with the restraint the whole language runs on, Send and Sync are not a trait system with declared instances and a solver. They are structural predicates — functions that, given a type, decide yes or no by looking at the type’s shape — added as the fourth and fifth alongside the Trivial and cleanup-needing distinctions the language already tracked. The same machinery that answers “can this live in a region?” now also answers “can this cross a thread?”

Most of the derivation is mechanical. The primitives are Send and Sync. A tuple is safe to move if all its elements are. Closures and channels are safe to move and share. A region borrow — a reference tied to a region — is never Send, which is a small, load-bearing rule: because a borrow can’t cross, a child thread simply cannot hold a reference into its parent’s memory, and the “each thread gets its own region” guarantee falls out for free rather than needing separate tracking.

Where structure isn’t enough, an author marks the type. A capability that owns a resource is movable but single-owner, so it is Send but not Sync. A capability with its own internal lock is marked shareable — Send and Sync both. A capability holding something inherently single-threaded, like a raw file descriptor, is marked neither. Markers are authoritative where they appear; anything unmarked derives its answer from its structure. It is exactly the shape of the Trivial rule from the memory model — marked types by decree, unmarked types by their contents — reused for the thread boundary.

The hole: stopping at the name

There was a soundness bug in that derivation, and it is worth dwelling on because it is the precise hazard the structural style creates. The predicate handled tuples correctly — a tuple is transparent, and checking all its elements was natural. But a named record or variant is different: its name is one thing, and its contents — the fields, the payloads — live in a separate declaration. The predicate, meeting an unmarked named type, checked its type arguments but never looked through to its actual contents. It stopped at the name.

The consequence was a real hole. Take a type that is deliberately not Send — a connection holding a raw descriptor, marked thread-local. Now wrap it in a one-line record or variant: a Box whose single field is that connection. The predicate, asked whether Box is Send, saw an unmarked named type with no non-Send type arguments, and answered yes — because it never opened Box to find the non-Send connection inside. Which means you could take a value the design specifically forbids from crossing a thread boundary, wrap it in a trivial record, and hand it across unchallenged. The exact data race the entire concurrency model was built to make impossible was reachable through a wrapper.

The hole is the shadow of the simplicity

This bug is not an accident of implementation; it is the specific risk of the choice made in the previous episode. A trait solver would have required someone to declare that Box is Send, and the compiler would then check that declaration against Box’s contents — a hole there would announce itself as a rejected declaration. A structural predicate declares nothing; it silently derives the answer, which is lighter and required no boilerplate — and that is exactly why the hole was silent. When a predicate decides by reading a type’s structure, it is only sound if it reads all of the structure. Reading part of it doesn’t fail loudly; it returns a confident, wrong yes. The restraint that made Send and Sync cheap is the same restraint that made this particular mistake possible.

The fix keeps the design and closes the gap. Markers stay authoritative — a marked type’s answer is by decree, unchanged. For an unmarked record or variant, the predicate now looks up the type’s real contents, substitutes any type parameters so a container’s element type is resolved to what it actually holds, and recurses into those contents — with a guard that tracks types already being visited, so a recursive type (a list node that refers to itself) can’t send the check into an infinite loop. After the fix, a wrapped non-Send value is correctly non-Send, and the predicate behaves exactly as the Trivial rule always did: markers on top, structure all the way down.

Found by looking, not by failing

One detail matters as much as the fix: how the hole was found. It did not surface from a failing test — no test happened to wrap a thread-local value in a record and try to send it, and a passing suite would have gone on reporting green over an unsound predicate indefinitely. It was found by a deliberate audit, a cross-cutting review of the Send/Sync machinery prompted by an unrelated bug in the same area. Someone went looking for holes in the guarantee rather than waiting for one to bite.

That is the only way soundness bugs of this kind get caught before they matter, because their signature is silence: the wrong answer looks exactly like the right one until the specific adversarial program shows up. A language whose entire pitch is verifiable correctness has to treat its own guarantees as things to be actively attacked, not assumed — and the honest posture the series keeps returning to includes turning that skepticism on your own type checker.

The predicates that decide whether a value may cross a thread boundary are now sound. The other half of moving values between threads is tracking when a value has been handed off, so that using it afterward is caught. That is a flow problem, not a structural one, and it has its own subtle cases. Next: move tracking.