It’s a Syn (Part 8)

Graham Hay

If we make the register request async:

Register(n) ==
    ...
            IN inbox' = [inbox EXCEPT![n] = Append(inbox[n], [action |-> "register_or_update_on_node", name |-> next_val])]

RegisterOrUpdateOnNode(n) ==
    /\ Len(inbox[n]) > 0
    /\ Head(inbox[n]).action = "register_or_update_on_node"
    /\ LET message == Head(inbox[n])
        l == [locally_registered[n] EXCEPT![n] = locally_registered[n][n] @@ [r \in {message.name} |-> time]]
        already_registered == message.name \in AllRegisteredForNode(locally_registered[n])
        IN
        (IF already_registered THEN
            \* {error, taken}
            registered' = registered
            /\ locally_registered' = locally_registered
            /\ inbox' = [inbox EXCEPT![n] = Tail(inbox[n])]
            /\ names' = names
        ELSE
            registered' = registered \union {message.name}
            /\ locally_registered' = [locally_registered EXCEPT![n] = l]
            /\ inbox' = [o \in Nodes |-> CASE
                (o = n) -> Tail(inbox[n])
                [] (o \in visible_nodes[n]) -> Append(inbox[o], [action |-> "sync_register", name |-> message.name, from |-> n, time |-> time])
                [] OTHER -> inbox[o]
            ]
            /\ names' = [names EXCEPT![n] = names[n] \ {message.name}]
        )
        /\ states' = Append(states, <<"RegisterOrUpdateOnNode", n, message.name>>)
    /\ time' = time + 1
    /\ UNCHANGED <<visible_nodes, disconnections>>

we now need to handle the case that the name was registered in the new race we have added.

Other than that the process is the same, and the same vars are updated. If we do the same for unregister:

Unregister(n) ==
        ...
        IN inbox' = [inbox EXCEPT![n] = Append(inbox[n], [action |-> "unregister_on_node", name |-> item_to_remove])]
 
UnregisterOnNode(n) ==
    /\ Len(inbox[n]) > 0
    /\ Head(inbox[n]).action = "unregister_on_node"
    /\ LET message == Head(inbox[n])
        l == [r \in (DOMAIN locally_registered[n][n] \ {message.name}) |-> locally_registered[n][n][r]]
        already_removed == message.name \notin AllRegisteredForNode(locally_registered[n])
        IN
        (IF already_removed THEN
            \* {error, undefined}
            registered' = registered
            /\ locally_registered' = locally_registered
            /\ inbox' = [inbox EXCEPT![n] = Tail(inbox[n])]
            /\ names' = names
        ELSE
            registered' = (IF message.name \in RegisteredElsewhere(n) THEN registered ELSE registered \ {message.name})
            /\ locally_registered' = [locally_registered EXCEPT![n] = ([locally_registered[n] EXCEPT![n] = l])]
            /\ inbox' = [o \in Nodes |-> CASE
                (o = n) -> Tail(inbox[n])
                [] (o \in visible_nodes[n]) -> Append(inbox[o], [action |-> "sync_unregister", name |-> message.name, from |-> n])
                [] OTHER -> inbox[o]
            ]
            /\ names' = [names EXCEPT![n] = names[n] \ {message.name}]
        )
        /\ states' = Append(states, <<"UnregisterOnNode", n, message.name>>)
    /\ time' = time + 1
    /\ UNCHANGED <<visible_nodes, disconnections>>

we still have a failure of the same invariant:

Error: Invariant AllRegistered is violated.
Error: The behavior up to this point is:
...

State 10: <Next line 234, col 5 to line 246, col 22 of module syn>
/\ disconnections = 0
/\ locally_registered = (n1 :> (n1 :> << >> @@ n2 :> << >>) @@ n2 :> (n1 :> <<>> @@ n2 :> << >>))
/\ time = 9
/\ states = << <<"Register", n1, "a">>,
   <<"Register", n2, "a">>,
   <<"RegisterOrUpdateOnNode", n1, "a">>,
   <<"RegisterOrUpdateOnNode", n2, "a">>,
   <<"SyncRegister", n2, "a">>,
   <<"Unregister", n2, "a">>,
   <<"UnregisterOnNode", n2, "a">>,
   <<"SyncRegister", n1, "a">>,
   <<"SyncUnregister", n1, "a">> >>
/\ visible_nodes = (n1 :> {n2} @@ n2 :> {n1})
/\ registered = {"a"}
/\ inbox = (n1 :> <<>> @@ n2 :> <<>>)
/\ names = (n1 :> {} @@ n2 :> {})

but now the problem is that our canonical list of registrations still thinks the name should be there, even though it was removed.

I think this fix was too simplistic, and I will need to go back to my first idea: of refcounting registrations.

Leave a comment