[antiguru]

2 of 14 in the interactive-runtime stack. Stacks on #40512, followed by #38386. Tracked by CPU-215. The design document is doc/developer/design/20261107_interactive_runtime.md in #40559.

The synchronization under the shared trace (#38386), split out so it can be reviewed and tested without differential.

A rendezvous point carries a view one writer publishes, a list of items, the upper they cover and writer-defined metadata, next to one hold accumulation per hold kind. Readers on any thread register a frontier per kind. A reader that moves a meet sets a flag the writer takes with take_holds_moved and wakes it, so a writer whose holds did not move reads none. Subscribers receive the view as a seed and then every item the writer reports as arrived. The set of subscribers an item goes to is chosen under the same lock that seeds a new subscriber, and the one writer pushes items in order, so a subscriber sees no gap and no duplicate.

A point takes one writer in its life, and a second attach panics, even after the first writer dropped. A closed or dropped writer freezes the point (is_frozen): the view stays as last published and readers never advance to the empty frontier. The writer's hold changes still apply after it closes, so its holds release. The design document argues why.

doc/developer/design/20261105_rendezvous_protocol/ holds a Veil model of the protocol and of the compute lifecycle around it, including the reconcile barrier #40558 adds. SMT proves its safety clauses inductive (1625 checks), and an explicit-state check explores 961,101 states without a violation. Deleting each guard reaches a violation, except two rows of the mutation table: the single-attach refusal, a backstop the model's only attach path never reaches, and the physical-meet bound, which needs four times and two epochs. The README names the lifecycle facts the model assumes by symbol, and lists what it abstracts away.

Inert: nothing outside the tests uses the primitive yet.

Tests use a toy item type: holds balance under random reader and writer operations, a monotone upper, writer drop freezing readers, the single attach, the wake rule, lock_all refusing a point named twice, and subscribers registered while a writer publishes from another thread.

A reviewer should check the seeding argument in Rendezvous::subscribe and Attachment::publish, which takes &mut self, and whether the model's abstractions match the code.

Posted by Claude Code.

🤖 Generated with Claude Code