More termination detection algorithms

[lemmy]

• https://en.wikipedia.org/wiki/Huang's_algorithm (related Create Rationals module CommunityModules#4)
• https://dl.acm.org/doi/10.5555/647172.716117

[lemmy]

A first attempt showing refinement of AsyncTerminationDetecting by Huang. It is not a refinement because ATD doesn't allow pending decrement when an inactive Leader in Huang receives the last weight back.

Node ==
    0..Cardinality(Procs) - 1

M == 
    CHOOSE f \in [ Node -> Procs ]: IsInjective(f)

ATD ==
    INSTANCE AsyncTerminationDetection 
    WITH
        terminationDetected <- TerminationDetected,
        active <- [ n \in Node |-> active[M[n]] ],
        pending <- [n \in Node |-> Len(msgs[M[n]]) ],
        N <- Cardinality(Procs)

ATDSpec == 
    ATD!Spec

THEOREM Spec => ATDSpec

Action property line 63, col 20 to line 63, col 32 of module AsyncTerminationDetection is violated.
The behavior up to this point is:
1: <Initial predicate>
/\ active = {L}
/\ weights = (L :> "1")
/\ msgs = << >>
/\ Terminated = FALSE
/\ TerminationDetected = FALSE
2: <SendMsg line 48, col 5 to line 53, col 27 of module Huang>
/\ active = {L}
/\ weights = (L :> "1/2")
/\ msgs = (L :> <<"1/2">>)
/\ Terminated = FALSE
/\ TerminationDetected = FALSE
3: <IdleLdr line 72, col 5 to line 74, col 33 of module Huang>
/\ active = {}
/\ weights = (L :> "1/2")
/\ msgs = (L :> <<"1/2">>)
/\ Terminated = FALSE
/\ TerminationDetected = FALSE
4: <RcvLdr line 78, col 5 to line 81, col 27 of module Huang>
/\ active = {}
/\ weights = (L :> "1")
/\ msgs = << >>
/\ Terminated = TRUE
/\ TerminationDetected = TRUE

[muenchnerkindl]

The definition of Wakeup(i) in AsyncTerminationDetection could be changed to

/\ pending[i] > 0
/\ / UNCHANGED active
/ ~ active[i] /\ active' = [active EXCEPT ![i] = TRUE]
/\ pending' = [pending EXCEPT ![i] = @ - 1]
/\ UNCHANGED terminationDetected

allowing an inactive receiver to either become active or remain passive. (It should then probably be renamed to Receive.)

[muenchnerkindl]

Ah, GitHub formatting ... maybe this works better:

/\ pending[i] > 0
/\ \/ UNCHANGED active
   \/ ~ active[i] /\ active' = [active EXCEPT ![i] = TRUE]
/\ pending' = [pending EXCEPT ![i] = @ - 1]
/\ UNCHANGED terminationDetected