Global snapshots 3

• cur ? nejaký stav, ktorý sa vyskytuje vo výpocte po tom, co bolo zaznamenávanie ukoncené

• pozadujeme, aby existovali postupnosti u, v také, ze

  [init] u [rec] ? [rec] v [cur]
  

• stavové premenné:

  x.done ? platí práve vtedy, ked x bolo zaznamenané
  

• zaznamenávanie je ukoncené, ak ??x platí x.done

• zaznamenaná hodnota je ulozená do x.rec

• stav rec je teda daný hodnotami ? ?x:: x.rec ?

• stav cur je daný momentálnymi hodnotami x

• invariant a progress podmienka:

  invariant ? ?x:: x.done ?
  
  ? ? ?u, v: [init] u [rec] ? [rec] v [cur] ?
  begun ? ? ?x:: x.done ?

• neformálne:

  • zaznamenávanie sa skoncí v konecnom case
  • [rec] je na nejakej „ceste“ medzi [init] a [cur]

• Program P1

  initially ? ||x:: x.done = false ?
  
  add ? ||x:: x.rec, x.done = x, true if begun ? ?x.done ?

end{P1}

• P1 je vhodný pre sekvencné pocítace, nevhodný pre asynchrónne pocítace

Previous slide

Next slide

Back to first slide

View graphic version