process STP[self : 0..MAXUID]constant
MAXUID,
MAXTID,
MAXSEQ,
MAXCERT,
MAXSIGN,
MAXHASH,
MAXKEY
input
self_cert : array [0..MAXUID] of 0..MAXCERT
function
Sign(0..MAXKEY, integer) returns 0..MAXSIGN,
Verify(0..MAXKEY, integer) returns 0..MAXSIGN,
Hash(integer) returns 0..MAXHASH,
Unique(0..MAXTID) returns boolean,
Id(0..MAXCERT) returns 0..MAXUID,
Key(0..MAXCERT) returns 0..MAXKEY,
SelfKey(0..MAXCERT) returns 0..MAXKEY
variable
msgtype : set {T-start, T-accept, T-data, T-token, T-commit, T-abort, T-fault},
state : set {null, sending, receiving, ready, committed, aborted},
t_state : array [0..MAXTID] of state init null,
t_other : array [0..MAXTID] of 0..MAXUID,
t_key : array [0..MAXTID] of 0..MAXKEY,
t_data : array [0..MAXTID, 0..MAXSEQ] of integer,
t_seq : array [0..MAXTID] of 0..MAXSEQ,
t_context : array [0..MAXTID] of 0..MAXHASH,
cert : 0..MAXCERT,
data : integer,
sign : 0..MAXSIGN,
context : 0..MAXHASH,
valid : boolean
parameter
tid : 0..MAXTID
begin
(t_state[tid] = null
Unique(tid))
{Action 0}
t_other[tid] := any;
cert := self_cert[t_other[tid]];
sign := Sign(SelfKey(cert), T-start
tid
t_other[tid]);
send T-start(tid, sign, cert) to t_other[tid];
rcv T-start(tid, sign, cert)
{Action 1}
valid := (sign = Verify(Key(cert), T-start
tid
self)
t_state[tid] = null);
if true
![]()
skip;
(valid)
![]()
t_state[tid], t_seq[tid], t_context[tid] := receiving, 0, 0;
t_other[tid], t_key[tid] := Id(cert), Key(cert);
cert := self_cert[t_other[tid]];
sign := Sign(SelfKey(cert), T-accept
tid);
send T-accept(tid, sign, cert) to t_other[tid];
fi
rcv T-accept(tid, sign, cert)
{Action 2}
valid := (sign = Verify(Key(cert), T-accept
tid)
t_state[tid] = null);
if (
valid
![]()
(Id(cert) = t_other[tid]))
![]()
skip;
(valid
Id(cert) = t_other[tid])
![]()
t_state[tid], t_seq[tid], t_context[tid] := sending, 0, 0;
t_key[tid] := Key(cert);
fi
(t_state[tid] = sending)
{Action 3}
cert := self_cert[t_other[tid]];
if true
![]()
data := any;
sign := Sign(SelfKey(cert), T-data
tid
data
t_context[tid]);
send T-data(tid, data, t_context[tid], sign) to t_other[tid];
t_data[tid, t_seq[tid]] := data;
t_context[tid] := Hash(data
t_context[tid]);
t_seq[tid] := t_seq[tid] + 1;
true
![]()
sign := Sign(SelfKey(cert), T-token
tid
t_context[tid]);
send T-token(tid, t_context[tid], sign) to t_other[tid];
t_state[tid] := receiving;
true
![]()
sign = Sign(SelfKey(cert), T-abort
tid);
send T-abort(tid, sign) to t_other[tid];
t_state[tid] := aborted;
true
![]()
sign = Sign(SelfKey(cert), T-commit
tid
t_context[tid]);
send T-commit(tid, t_context[tid], sign) to t_other[tid];
t_state[tid] := ready;
fi
rcv T-data(tid, data, context, sign)
{Action 4}
valid := (sign = Verify(t_key[tid], T-data
tid
data
context)
t_state[tid] = receiving);
if (
valid
![]()
(context = t_context[tid]))
![]()
skip;
(valid
context = t_context[tid])
![]()
t_data[tid, t_seq[tid]] := data;
t_context[tid] := Hash(data
t_context[tid]);
t_seq[tid] := t_seq[tid] + 1;
fi
rcv T-token(tid, context, sign)
{Action 5}
valid := (sign = Verify(t_key[tid], T-token
tid
context)
t_state[tid] = receiving);
if (
valid)
![]()
skip;
(valid
![]()
(context = t_context[tid]))
![]()
cert := self_cert[t_other[tid]];
sign := Sign(SelfKey(cert), T-abort
tid);
send T-abort(tid, sign) to t_other[tid];
t_state[tid] := aborted;
(valid
context = t_context[tid])
![]()
t_state[tid] := sending;
fi
rcv T-commit(tid, context, sign)
{Action 6}
valid := (sign = Verify(t_key[tid], T-commit
tid
context)
![]()
(t_state[tid] = sending
t_state[tid] = null));
if (
valid)
![]()
skip;
(valid
t_state[tid] = aborted)
![]()
cert := self_cert[t_other[tid]];
sign := Sign(SelfKey(cert), T-abort
tid);
send T-abort(tid, sign) to t_other[tid];
(valid
t_state[tid] = committed)
![]()
cert := self_cert[t_other[tid]];
sign := Sign(SelfKey(cert), T-commit
tid
0);
send T-commit(tid, 0, sign) to t_other[tid];
(valid
t_state[tid] = ready)
![]()
t_state[tid] := committed;
(valid
t_state[tid] = receiving)
![]()
if true
![]()
cert := self_cert[t_other[tid]];
sign := Sign(SelfKey(cert), T-abort
tid);
send T-abort(tid, sign) to t_other[tid];
t_state[tid] := aborted;
(context = t_context[tid])
![]()
cert := self_cert[t_other[tid]];
sign := Sign(SelfKey(cert), T-commit
tid
0);
send T-commit(tid, 0, sign) to t_other[tid];
t_state[tid] := committed;
fi
fi
rcv T-abort(tid, sign)
{Action 7}
valid := (sign = Verify(t_key[tid], T-abort
tid)
![]()
(t_state[tid] = null
t_state[tid] = committed));
if (
valid)
![]()
skip;
(valid)
![]()
t_state[tid] := aborted;
fi
rcv T-fault(tid)
{Action 8}
if (t_state[tid] = null
t_state[tid] = committed
t_state[tid] = aborted)
![]()
skip;
(t_state[tid] = sending
t_state[tid] = receiving)
![]()
t_state[tid] := aborted;
(t_state[tid] = ready)
![]()
cert := self_cert[t_other[tid]];
sign := Sign(SelfKey(cert), T-commit
tid
t_context[tid]);
send T-commit(tid, t_context[tid], sign) to t_other[tid];
fi
end