For each process the local state consists of
TMBegin(None)
B1 do loc := glb
B2 while odd(loc)
B3 return None
TMRead(A(addr))
R1 val = mem(addr)
R2 if (glb = loc)
R3 return V(val)
R4 return Aborted
TMWrite(AV(addr,val))
W1 if even(loc)
W2 if ! CAS(glb, loc, loc +1)
W3 return Aborted
W4 else loc := loc + 1
W5 mem(addr) := val
W6 return None
TMEnd(None)
E1 if odd(loc)
E2 glb := glb+1
E3 return None
The individual steps of the algorithms are written as operations, which modify the global state mem and glb, and one local state (four values pc, loc, a, v). Primed values (glb' etc.) denote the values after the step. The individual steps are written as indexed operations. They fall into 3 categories.
Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.