Global snapshots 10
Efektívne programy na zaznamenanie stavu
Asynchrónna shared-memory:
- predpokladajme, ze premenná y v príkaze t bola zaznamenaná t.j. platí y.done a ze iná premenná x v t nebola zaznamenaná, t.j. ?x.done
- pravidlo R hovorí, ze t nemôze byt vykonané skôr, nez sa x nezaznamená
- zaznamenanie x mozno dorobit zároven s t:
? ||x: t obsahuje x ? ?x.done::
x.rec, x.done = x, true if ? ?y: t obsahuje y:: y.done ??
|| t
- na zaciatku predpokladajme, ze zaznamenávanie je iniciované zaznamenávaním jednej špecifickej premennej first
first.rec, first.done := first, true if begun ? ?first.done
- je isté, ze v konecnom case po zaznamenaní first bude zaznamenaná kazdá premenná, ktorá sa vyskytuje v nejakom príkaze t spolu s first
- definujme
x je_spolu s y ? ? ? príkaz t:: t obsahuje x ? t obsahuje y ?
je_spolu* ? tranzitívny uzáver je spolu
- platí
x.done ? x je_spolu s y ? y.done
x.done ? x je_spolu* s y ? y.done