Theodus/backpressure-model

Issues

• possible deadlock?

  #24 opened 4 years ago by sophiaIC
  2

• Q22: high level proof of deadlock freedom -- assuming that `Obstacle` is acyclic

  #8 opened 4 years ago by sophiaIC
  0

• Need necessary conditions for High Priority

  #22 opened 4 years ago by sophiaIC
  2

• Send doesn't change the priority or muted cowns

  #23 opened 4 years ago by lukecheeseman
  1

• Send only sets a mutor when first receiver has high priority

  #21 opened 4 years ago by lukecheeseman
  6

• A stronger blocker invariant?

  #20 opened 4 years ago by lukecheeseman
  1

• new notation for the model

  #19 opened 4 years ago by sophiaIC
  2

• proposing that `LowPriorityImpliesNotAcquired`

  #18 opened 4 years ago by sophiaIC
  1

• `HighPriorityInUnbockedQueue` -- what does the name express?

  #16 opened 4 years ago by sophiaIC
  1

• proposing that we drop `BehaviourAcquisition`

  #15 opened 4 years ago by sophiaIC
  1

• What happened to `WillScheduleCown`

  #14 opened 4 years ago by sophiaIC
  1

• Remove "Termination" from the properties to be model-checked

  #13 opened 4 years ago by sophiaIC
  2

• Q19: requiring weaker definition of Terminated

  #5 opened 4 years ago by sophiaIC
  2

• proposing to amalgamate `HighPriotityInUnblockedQueue` and `HighPriorityHasWork`

  #17 opened 4 years ago by sophiaIC
  0

• summary of meeting on 29.10

  #12 opened 4 years ago by sophiaIC
  0

• Q23: another problematic configuration

  #10 opened 4 years ago by sophiaIC
  0

• Q24: Summary of meeting on 20.10.2020

  #11 opened 4 years ago by sophiaIC
  5

• Q16: cycles in the mute-sets

  #2 opened 4 years ago by sophiaIC
  2

• Should CurrentMessage return empty set?

  #9 opened 4 years ago by lukecheeseman
  0

• Q21: removing temporal requirements from `PROPERTIES`

  #7 opened 4 years ago by sophiaIC
  0

• Q18: Is the union of AcquiredBy and MutedBy acyclic?

  #4 opened 4 years ago by sophiaIC
  2

• Q20: Acyclic AcquiredByMutedByWithPrioMinus1

  #6 opened 4 years ago by sophiaIC
  5

• Q17: implications of `priority[c]=1`

  #1 opened 4 years ago by sophiaIC
  10

• Q18: mut-sets disjoint

  #3 opened 4 years ago by sophiaIC
  1