Send only sets a mutor when first receiver has high priority

Question

Send only sets a mutor when first receiver has high priority

lukecheeseman opened this issue 4 years ago · 6 comments

Send is defined as such:

Send(cown) ==
  LET senders == CurrentMessage(cown) IN
  /\ running[cown]
  /\ fuel > 0
  /\ \E receivers \in SUBSET Cowns:
    /\ Cardinality(receivers) > 0
    /\ queue' =
      (Min(receivers) :> Append(queue[Min(receivers)], receivers)) @@ queue
    /\ IF priority[Min(receivers)] = 1 THEN
      LET prioritizing == Prioritizing({Min(receivers)}) IN
      LET unmuting == LowPriority(prioritizing) IN
      /\ priority' = [c \in prioritizing |-> 1] @@ priority
      /\ scheduled' = [c \in unmuting |-> TRUE] @@ scheduled
      /\ LET mutors == {c \in receivers \ senders: ValidMutor(c)} IN
        IF
          /\ mutors /= {}
          /\ mutor[cown] = Null
          /\ \A c \in senders: priority[c] = 0
          /\ \A c \in senders: c \notin receivers \* TODO: justify
        THEN
          /\ mutor' = (cown :> Min(mutors)) @@ mutor
        ELSE
          /\ UNCHANGED <<mutor>>
      ELSE
        /\ UNCHANGED <<scheduled, priority, mutor>>
  /\ fuel' = fuel - 1
  /\ UNCHANGED <<running, blocker, mute>>

I'm concerned about the guard:

 /\ IF priority[Min(receivers)] = 1 THEN

Does this not mean that we will only select a mutor if the priority of the first receiver is high?

Answer 1 · 2020-11-20T14:56:39.000Z

I'm assuming that has to do with a cown being protected with high priority? But I would think this is the wrong way for this?

Answer 2 · 2020-11-20T14:58:21.000Z


Send(cown) ==
  LET senders == CurrentMessage(cown) IN
  /\ cown \in running
  /\ fuel > 0
  /\ \E receivers \in SUBSET Cowns:
    /\ Cardinality(receivers) > 0
    /\ queue' = (Min(receivers) :> Append(queue[Min(receivers)], receivers)) @@ queue
    /\ IF priority[Min(receivers)] = 1 THEN
        LET prioritizing == Prioritise(Min(receivers)) IN
        LET unmuting == LowPriority(prioritizing) IN
        /\ priority' = [c \in prioritizing |-> 1] @@ priority
        /\ scheduled' = scheduled \union unmuting
       ELSE 
        /\ UNCHANGED <<scheduled, priority>>
    /\ LET mutors == {c \in receivers \ senders: Mutor(c)} IN
        IF mutors /= {} /\ mutor[cown] = Null
          /\ (\A c \in senders: priority[c] = 0)
          /\ (\A c \in senders: c \notin receivers) \* TODO: justify
        THEN
          /\ mutor' = (cown :> Min(mutors)) @@ mutor
        ELSE
          /\ UNCHANGED <<mutor>>
  /\ fuel' = fuel - 1
  /\ UNCHANGED <<running, blocker, mute>>

Answer 3 · 2020-11-20T15:47:41.000Z

I don't see the path where if this cown sends to a muted cown, then the senders also get muted

Answer 4 · 2020-11-20T15:49:42.000Z

Ignore this, i had conflated the receiver being high to unmute and make progress and the receiver being overloaded or muted to mute the sender

Answer 5 · 2020-11-20T16:20:35.000Z

I'm going to reopen this to discusss it, I still don't understand why muting is guarded by checking the min receiver has a high priroity. @Theodus do you have any description?

Answer 6 · 2020-11-25T14:00:59.000Z

This changes causes a deadlock. So it being this way is clearly important:

Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, FALSE, FALSE, FALSE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 0, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<{1}>>, <<{2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 4

State 2: <Prerun line 82, col 3 to line 88, col 54 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<TRUE, FALSE, FALSE, FALSE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 0, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<{1}>>, <<{2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 4

State 3: <Send line 92, col 3 to line 113, col 41 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<TRUE, FALSE, FALSE, FALSE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 0, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<{1}>>, <<{2}, {2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 3

State 4: <Send line 92, col 3 to line 113, col 41 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<TRUE, FALSE, FALSE, FALSE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 0, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<{1}>>, <<{2}, {2}, {2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 2

State 5: <Complete line 117, col 3 to line 133, col 32 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, FALSE, FALSE, FALSE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 0, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<>>, <<{2}, {2}, {2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 2

State 6: <Prerun line 82, col 3 to line 88, col 54 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, TRUE, FALSE, FALSE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 1, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<>>, <<{2}, {2}, {2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 2

State 7: <Prerun line 82, col 3 to line 88, col 54 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, TRUE, FALSE, TRUE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 1, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<>>, <<{2}, {2}, {2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 2

State 8: <Prerun line 82, col 3 to line 88, col 54 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, TRUE, TRUE, TRUE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 1, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<>>, <<{2}, {2}, {2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 2

State 9: <Send line 92, col 3 to line 113, col 41 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, TRUE, TRUE, TRUE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 1, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<{1, 2}>>, <<{2}, {2}, {2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 2, 0>>
/\ fuel = 1

State 10: <Complete line 117, col 3 to line 133, col 32 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, FALSE, TRUE, TRUE>>
/\ scheduled = <<TRUE, TRUE, TRUE, TRUE>>
/\ priority = <<0, 1, 0, 0>>
/\ mute = <<{}, {}, {}, {}>>
/\ queue = <<<<{1, 2}>>, <<{2}, {2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 2, 0>>
/\ fuel = 1

State 11: <Complete line 117, col 3 to line 133, col 32 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, FALSE, FALSE, TRUE>>
/\ scheduled = <<TRUE, TRUE, FALSE, TRUE>>
/\ priority = <<0, 1, -1, 0>>
/\ mute = <<{}, {3}, {}, {}>>
/\ queue = <<<<{1, 2}>>, <<{2}, {2}>>, <<>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 1

State 12: <Prerun line 82, col 3 to line 88, col 54 of module backpressure>
/\ blocker = <<0, 0, 0, 0>>
/\ running = <<FALSE, TRUE, FALSE, TRUE>>
/\ scheduled = <<TRUE, TRUE, FALSE, TRUE>>
/\ priority = <<0, 0, -1, 0>>
/\ mute = <<{}, {3}, {}, {}>>
/\ queue = <<<<{1, 2}>>, <<{2}, {2}>>, <<>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 1

State 13: <Acquire line 64, col 3 to line 78, col 45 of module backpressure>
/\ blocker = <<2, 0, 0, 0>>
/\ running = <<FALSE, TRUE, FALSE, TRUE>>
/\ scheduled = <<FALSE, TRUE, FALSE, TRUE>>
/\ priority = <<0, 0, -1, 0>>
/\ mute = <<{}, {3}, {}, {}>>
/\ queue = <<<<>>, <<{2}, {2}, {1, 2}>>, <<>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 1

State 14: <Send line 92, col 3 to line 113, col 41 of module backpressure>
/\ blocker = <<2, 0, 0, 0>>
/\ running = <<FALSE, TRUE, FALSE, TRUE>>
/\ scheduled = <<FALSE, TRUE, FALSE, TRUE>>
/\ priority = <<0, 0, -1, 0>>
/\ mute = <<{}, {3}, {}, {}>>
/\ queue = <<<<>>, <<{2}, {2}, {1, 2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 3, 0, 0>>
/\ fuel = 0

State 15: <Complete line 117, col 3 to line 133, col 32 of module backpressure>
/\ blocker = <<2, 0, 0, 0>>
/\ running = <<FALSE, FALSE, FALSE, TRUE>>
/\ scheduled = <<FALSE, FALSE, FALSE, TRUE>>
/\ priority = <<0, -1, -1, 0>>
/\ mute = <<{}, {3}, {2}, {}>>
/\ queue = <<<<>>, <<{2}, {1, 2}>>, <<{3}>>, <<{4}>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 0

State 16: <Complete line 117, col 3 to line 133, col 32 of module backpressure>
/\ blocker = <<2, 0, 0, 0>>
/\ running = <<FALSE, FALSE, FALSE, FALSE>>
/\ scheduled = <<FALSE, FALSE, FALSE, TRUE>>
/\ priority = <<0, -1, -1, 0>>
/\ mute = <<{}, {3}, {2}, {}>>
/\ queue = <<<<>>, <<{2}, {1, 2}>>, <<{3}>>, <<>>>>
/\ mutor = <<0, 0, 0, 0>>
/\ fuel = 0

27760996 states generated, 7028036 distinct states found, 280309 states left on queue.
The depth of the complete state graph search is 18.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 24 and the 95th percentile is 3).