Faulty channels 2

• správa je stratená, ak sender zapíše do x prv, nez to receiver precítal

• správa je zduplikovaná, ak receiver znova cíta x bez toho, ze by sa medzitým obsah x zmenil

• podobne platí strata/duplikovanie pre y

• predpokladáme, ze sender posiela postupnost 1, 2, 3… (teda správy ocíslujeme a namiesto správ posielame len ich císla)

• nech

  ks – posledné císlo poslané senderom
  
  kr – posledné císlo prijaté receiverom

• initially ks = 1 ? kr = 0

• invariant kr ? ks {prijíma sa len to, co bolo poslané}

• kr = n ? kr = n + 1 {nakoniec sa prijmú všetky správy}

• pozadovaný program musí splnat túto špecifikáciu a naviac jeho príkazy sa dajú rozdelit do dvoch skupín (pre sender a receiver):

  • ks vie cítat a písat len sender (sRW)
  • kr vie cítat a písat len receiver (rRW)
  • x, y sa môzu vyskytovat v oboch skupinách
  • do x vie priradovat len sender
  • do y vie priradovat len receiver

Previous slide

Next slide

Back to first slide

View graphic version