Readers?Writers Problem 4

• Modifikácia usera

  declare t: int, b: boolean
  
  always t = N ? (nr + N.nw)
  initially b = false
  assign
  nr := nr + 1 if t ? 1 ? ?b {started read}
  
   nr := nr ? 1 {end read}
   nw, nq, b := nw + 1, nq ? 1, false
  if t ? N ? nq > 0 {started write}
   nw := nw ? 1 {end write}
   b := nq > 0 {set b}

end

• Dôkaz (5), cize nq > 0 ? nw = 1 plynie z (4) a (6)?(9):

  b ? nq > 0 (6)
  
  nq > 0 ensures nw = 1 ? b (7)
  b ? nr = 0 ensures nw = 1 (8)
  b ? nr = k ? k > 0 unless b ? nr < k (9)
  (uz sme neformálne urobili predtým)

• chceme ukázat, ze nq > 0 ? nw = 1:

  b ? nr = k ? k > 0 ? b ? nr < k (PSP 4, 9)
  

• aplikujeme indukciu

  b ? nr = 0 ? b (10)
  

• tranzitivita s (8) a (10): b ? nw = 1 (11)

• kombináciou (7) a (11) dostávame výsledok.

Previous slide

Next slide

Back to first slide

View graphic version