Registry name lost on a third node when the process registered during a split dies before the split heals #96

syn master (5191a98) and 3.4.2 (34749b6), OTP 27.3.4.11.

After a partial net split heals, one node can be left without the entry of a live registered process while every other node has it, and syn does not bring the entry back on its own.

Take three nodes in one Scope: NodeA, NodeB and NodeCommon. A process on NodeA, PidOnNodeA, is registered under some name and all three nodes hold the entry. The connection between NodeA and NodeB drops while both stay connected to NodeCommon. NodeB purges NodeA's entries, no longer sees the name, starts its own PidOnNodeB and registers it under the same name. The sync_register goes to NodeB's nodes_map, which is NodeCommon alone; NodeCommon owns neither process, so handle_registry_sync replaces PidOnNodeA with PidOnNodeB, the newer registration. NodeA hears nothing. Then PidOnNodeB dies before the connection comes back: NodeB's DOWN handler removes it and broadcasts sync_unregister, again to NodeCommon alone, and the sync_unregister handler there finds the same pid and removes the entry. NodeCommon now has nothing for the name.

NodeA and NodeB reconnect and exchange snapshots. NodeB's has nothing for the name, NodeA's gives NodeB PidOnNodeA back as a plain new entry. Neither owner sees a conflict, so resolve_conflict never runs, and the keep-local branch, the one place in the protocol that re-broadcasts a kept registration with a fresh time, sends nothing. NodeCommon never lost its connection to NodeA, so no snapshot from NodeA reaches it either.

End state: all three nodes connected and in the scope's subcluster, syn:lookup returns {PidOnNodeA, Meta} on NodeA and NodeB and undefined on NodeCommon. It lasts until NodeCommon resyncs with NodeA (after a disconnect, or a restart of either scope process) or NodeA broadcasts the entry again (a registration that changes its metadata, or a conflict NodeA wins). No resolver is called on this route, so the default resolution and a custom one end the same. If PidOnNodeB is still alive when the owners reconnect, it heals: both owners see the conflict in the other's snapshot, and the one that keeps its process re-broadcasts it to NodeCommon too.

Reproduction

The TLA+ model in test/tla finds it as soon as it gets a third node. With one change to test/tla/syn.cfg,

Nodes = {n1, n2, n3}

the command from test/tla/README.md (TLC 2.18, the jar in test/tla) reports Invariant AllRegistered is violated at state 12 after about a second. n1 is NodeA, n2 is NodeB and n3 is NodeCommon; the only difference from the story above is that n1 registers after the cut, so n2 never holds n1's entry.

TLC stops there because AllRegistered is checked per node, and n3 sees both other nodes while n1 and n2 are still apart. To check the state after the split heals, we added an invariant that applies only once every link is back and every queue is empty, in a module next to syn.tla:

---- MODULE syn_connected ----
EXTENDS syn

Quiescent == \A n \in Nodes: Len(inbox[n]) = 0

FullyConnected == \A n \in Nodes: visible_nodes[n] = AllOtherNodes(n)

LiveNames == {r \in DOMAIN registered: registered[r] > 0}

AllRegisteredWhenConnected ==
    (Quiescent /\ FullyConnected) =>
        \A n \in Nodes: AllRegisteredForNode(locally_registered[n]) = LiveNames
====

syn_connected.cfg is syn.cfg with Nodes = {n1, n2, n3} and AllRegisteredWhenConnected in place of AllRegistered. Run on these two files, the README command reports Invariant AllRegisteredWhenConnected is violated at state 17 after about ten seconds. In that state every link is back, every queue is empty, n1 and n2 hold a under n1, and n3 holds nothing. The two-node configuration cannot reach either state: with two nodes no node owns neither process.

We also have a deterministic three-node test with peer (the cut made with erlang:disconnect_node/1, PidOnNodeB killed with exit/2, bounded waits only). It fails on master 5191a98 in 10 of 10 runs and on 3.4.2 in every run, with the default resolution and with a custom resolver that keeps the older start time from Meta; the variant that leaves PidOnNodeB alive until the reconnect passes every time. The peers run with prevent_overlapping_partitions set to false, only so that NodeCommon keeps both connections; with the OTP default, global on NodeCommon drops both. We can turn it into a case for syn_registry_SUITE.

Where we hit it

A 15-node cluster with prevent_overlapping_partitions at its default and a resolver that keeps the process with the older start time. global's partition prevention produced waves of disconnects, and one node was cut from NodeA five times in five seconds. Three nodes ended up with no entry for a live process while every node was connected to every other and in the scope's subcluster, and still had none the next day; two more lost it the same way and got it back only when a later wave cut them from NodeA and the reconnect snapshot restored it. The cut node's logs have a gap in the second that matters, so the route on the cluster is our reconstruction: PidOnNodeB seems to have lost a conflict to NodeA's snapshot on NodeB (our resolver keeps the older process; the default one would have kept PidOnNodeB), NodeB then told the third nodes to drop it, and NodeA never saw PidOnNodeB. The end state matches the test.

Not the late unregister from test/tla/README.md

In the case listed under "Calls Made From Another Node", a node writes an entry for a process on another node, and a sync_unregister that node sent earlier removes it. Here every node registers only its own processes and every message arrives in order; the entry is lost because the one message that would restore it on the third node, the winner's re-broadcast after a conflict, is never sent, since the winner's node never sees the challenger.

Once the direction is agreed I can send a PR, or the test case for the suite on its own.