Consider a set of transaction components in which Coordinators help arrange the actions of Transactors, with IDL interfaces:
typedef long TID;
interface Transactor {
boolean join(in TID tid);
boolean commit(in TID tid)
void abort(in TID tid)
};
interface Coordinator : Transactor {
TID begin();
boolean add(in TID tid,in Transactor p) raises (TransError);
};
The overall design is that Coordinators create (via begin) transaction identifiers ( TIDs) that are used to index transactions. Each transaction consists of a group of Transactor members, added via the add operation. As indicated by the use of interface inheritance, members may be other Coordinators. Each Transactor may be asked to join a transaction, and to commit or abort it. The application operations that each component performs within transactions (perhaps bank account updates) are not described in this set of interfaces.
To capture some of this in PSL/IDL, we declare a protocol module, starting off with a declaration of attribute members to represent the handles of all members of a given transaction. There may be several sets of members maintained by each Coordinator, each referenced via its transaction identifier ( tid). The associated constraint precludes the existence of any additional operations or rules that cause p to become a member unless they somehow invoke add. We also declare auxiliary function validtid and corresponding constraint to show how the notion of a valid transaction id is related to event predicates. A transaction identifier tid is valid if it was created as the result of a begin operation, but becomes invalid when the subject of any abort or commit request:
sequence<Transactor> members(Coordinator c, TID tid);
boolean validtid(Coordinator c,TID tid);
rules(Coordinator c, Transactor p, TID t){
inv { contains(members(c,t), p) -->
out(reply[<c->add(p,t)>](TRUE)) }
inv { validtid(c, tid) --> out(reply[<c->begin()>](tid)) }
inv { in(<c->abort(tid)>) --> !validtid(c, tid) }
inv { in(<c->commit(tid)>) --> !validtid(c, tid) }
};
Two sample protocol rules are also shown in the accompanying PSL/IDL-G declaration. The first rule says that on receiving a begin request, the Coordinator replies with a tid value that has never been used before. This statement, along with the above constraints on validtid amount to a promise that each tid value returned by begin is unique and valid for the length of the transaction.
The main ``thread'' in the second rule says that upon receiving an add request for a Transactor p with a valid tid, a coordinator invokes p's join operation. If it then receives a TRUE reply, p is then a member of members and the operation completes successfully. The other cases are ``error paths''; one causing an exception, and the other a simple FALSE reply. Additional situations and relations would surely be included in a more realistic specification. For example, it may describe cases dealing with the possibility that !live(p) (i.e., if p were not a live handle), the use of timeouts, and so on.
We may also rework a more specialized version of the add rule by parameterizing over both the Coordinator and the Transactor roles. The accompanying partial PSL/IDL-G declaration of rules addp(Coordinator c, Transactor p) assumes for simplicity that p replies FALSE to join only if it is already a member of the transaction. For emphasis, situations describing the view of the Transactor are shaded. One sense in which this protocol is more committal is that rather than relying on a one-to-one delivery rule to match the p->join request with its reception (and similarly for the join reply), this version directly connects the associated situations for these particular communication partners. Such rules may be seen as the specification analog of multimethods[17].
Along a different dimension, we could have presented a less committal version by omitting various situations if we happened not to care about them for the sake of this protocol declaration, and then perhaps inserted them later as refinements. For example, the join reply and its acceptance might have been elided without changing the ordering requirements of the remaining situations.