next up previous
Next: Methods and Tools Up: PSL: Protocols and Pragmatics Previous: PSL





Even though protocols describe multi-participant interactions, PSL declarations are frequently ``one-sided'', describing a role with respect to a single interface. This captures the modularity of protocols in which a participant's interactions do not vary with respect to the types or states of others that it interacts with. For example, here is a fragment of a protocol for a simple File:

rules filep(File f) { // ...
 {in(R = < f->read() >)} && {
   case {isOpen(f)} enable {char c, out(reply[R](c)), 0 <= c, c <= 127}
   case {default}   pair   {out(throw[R](NotOpen x))}

Here, the use of linking the ``normal'' read reply indicates that a situation in which a reply is generated occurs only when a file is open and receives a read request, but may not occur at all so far as can be determined from the perspective of the roles parameterized within the current rules declaration. For example, there may be ``downstream'' errors stemming from internal invocations that are not visible at this scope or level of specification. However, if a reply occurs, the return value c is subject to the listed constraints that amount to a guarantee that the return value is a 7-bit character value.

In contrast, the ``exceptional'' reply situation is linked via , indicating that (only) when a read request is received by a file that is not open, an exception reply to the request is always generated. This does not indicate that this is the only context in which the NotOpen exception is thrown. It says instead that this is the only context in which it is thrown as a reply to read. If for some reason we had wanted to make the weaker claim that NotOpen is possible but not guaranteed, we would have used . Had we wanted to make the differently weaker claim that NotOpen is always issued not only here, but perhaps also in some other context (i.e., even if the file is open) we would have used the operator.


One-sided protocol descriptions can be useful even when interactions are focused upon fixed sets of communications partners. For example, consider a transaction framework in which Coordinators help arrange the actions of Transactors. The IDL interfaces are:

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:

sequence<Transactor> members(Coordinator c, TID tid);

rules(Coordinator c,Transactor p,TID t){
 inv {contains(members(c,t),p) --> out(reply[<c->add(p,t)>](TRUE))}

We next 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:

boolean validtid(Coordinator c,TID tid);

rules valid(Coordinator c, TID tid) {
 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 describe some of the dynamics. 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:

rules coord(Coordinator c) {
 {in(<c->begin()>), long tid,  empty(members(c, tid)),
 pair  {out(reply(tid))}

The rule for add contains a main ``thread'' saying 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 p were not a live handle, the use of timeouts, and so on.)

 {in(A = <c->add(tid, p)>)} && {
    case {!validtid(c,tid)} pair  {throw(tx)}
    case {default} lead {out(J = <p->join(tid)> )} enable 
           {in(reply[J](ok))} && {
            case {!ok}     lead {out(reply[A](FALSE))} 
            case {default} lead {out(reply[A](TRUE)), 
                                 contains(members(c,tid), p)}}}

Multiple Participants


Protocols including situations describing multiple participants are used when the perspectives and responsibilities of all parties need to be taken into account simultaneously, often because one party responds in special ways to another that do not apply to interactions with other kinds of participants. Such rules may be seen as the specification analog of multimethods [19]. For example, we may rework a more committal version of the add rule:

For clarity, situations describing the view of the Transactor are shaded. This rule assumes for simplicity that p replies FALSE to join only if it is already a member of the transaction. 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.

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.

Rules in such PSL declarations often represent ``snippets'' [64] of a longer or fuller protocol. It is normally possible to show a more complete view of a protocol by linking situations described in one scope to those in others. This may entail exploitation of global axioms such as the one-to-one delivery rule when available to match ins with outs, along with special rules for matching the obligations and expectations of particular partners [18]. For example, the multi-participant view of add may be constructed given the single forms of Coordinator ::add and Transactor ::join. The resulting timethread [13] is a path linking initial situations to terminal ones. Such timethreads can be valuable tools for informally validating protocols.

Design Patterns


The elements of many common object-oriented design patterns [21] consist of protocols common to all participants in a framework. For example, in the Observer pattern, Subjects maintain representations of things they are modeling, along with operations to reveal and change this represented state. Observers display (or otherwise use) the state represented by Subjects. When a Subject's state is changed, it merely informs one or more Observers that it has changed. Observers are responsible for determining the nature of the changes, and whether they require re-display. The version illustrated here is one of the variants described in [21] in which the Subject sends a handle to itself as an argument to notify when it is changed. The Observer uses this handle to probe for values, and performs a redisplay only if the state actually differs from that held in a cache.

The static structure may be described in PSL/IDL, as well as in an IDL dialect of the OMT [61] notation often used for design patterns in which attributes are listed along with operations:

interface Subject {
  StateType   currentVal();
  void        changeVal(in StateType v);
  void        attach(in Observer ob);
  void        detach(in Observer ob);

interface Observer {
  void        display(in StateType v);
  oneway void notify(in Subject s);

protocol module {
  StateType          Val(Subject);
  sequence<Observer> Obs(Subject);
  StateType          CachedState(Observer);

Informally, the main notification protocol is that when a Subject s receives a changeVal request, it makes sure that its abstract state Val(s) has been set, and for each member o in its set of Observers, sends a notify message to the observer, and then replies to whoever called changeVal. When the Observer o receives the notification, it probes s by asking for its currentVal. If the returned value differs from the value recorded as CachedState, the Observer sends itself a display request. The details of what happens when an Observer receives that display request aren't important to this aspect of the protocol.

In the corresponding PSL/IDL-G specification, situations primarily viewing an Observer's role are shaded. Note that the declaration and use of Observer o in the first situation means that the Observer roles of the protocol are taken (perhaps concurrently) by all observers of Subject s:



Recall the equivalence of our first relay rules in Section 3.6:

{in(m1)} lead {out(m2)}
{in(m1)} lead {in(m1), out(m2)}

This ``latching'' property of event predicates does not necessarily hold for arbitrary attributes. For example, if there were an unconstrained attribute ok(Relay r), and we required that ok(r) persist as true across these two situations, we would have to write:

{in(m1), ok(r)} lead {out(m2), ok(r)}

Constraint rules may be used to avoid such problems. Constraint rules add requirements that do not otherwise come ``for free'' in open protocol specifications. Consider, for example, interfaces describing Accounts that maintain balances:

interface Account { // ...
 void  setBalance(float b);
 float getBalance();
 long  getSerialNo();

interface AccountFactory { // ...
 Account makeAcc(long sn, float initbal);

As a start, we can declare a protocol module with abstract attributes bal and serialNo, along with simple postcondition-style rules stating that makeAcc initializes bal and serialNo, getBalance ``reads'' bal, setBalance ``writes'' bal, and getSerialNo reports serialNo:

protocol module accountm {

 float bal(Account a); 
 long  serialNo(Account a);

 rules (AccountFactory f) {
  {in(<f->makeAcc(sn, initbal)>)}
  {out(reply(a)), live(a), bal(a) == initbal, serialNo(a) == sn}

 rules (Account a) {
  {in(<a->getBalance()>)}  pair {out(reply(bal(a))}
  {in(<a->setBalance(b)>)} pair {out(reply()), bal(a) == b}
  {in(<a->getSerialNo()>)} pair {out(reply(serialNo(a))}



It is useful here to add a further constraint saying that the setBalance and makeAcc operations are the only ones that affect the value of attribute bal. Without such a constraint, there is no requirement that this reasonable and often implicitly assumed encapsulation property holds. This may be expressed by relating bal to values associated with replies from either of the two operations:

rules (Account a, AccountFactory f, float b) {
 inv {(bal(a) == b) --> 
         out(reply[<f->makeAcc(s,b)>](a)) || 


A similar tactic may be used to describe attributes whose values are fixed forever upon initialization. For example, to claim that the serialNo is always the one established by the factory operation, and further claim that initialization occurs at most once per account:

rules (Account a, AccountFactory f, long s)  {
 inv {(serialNo(a) == s) --> out(reply[<f->makeAcc(s,b)>](a))}
 inv {unique(out(reply[<f->makeAcc(s,b)>](a))}


We could further require that processing of setBalance requests is not subject to arbitrary interleavings (i.e., that setBalance operations proceed serially), thus precluding multithreaded implementations. Again, without such a constraint, there is nothing forcing this interpretation. The restriction that no two setBalance operations operate concurrently may be expressed by saying that any message that has been received but not replied to is unique:

rules (Account a, float b) {
 inv {unique(in(s = <a->setBalance(b)>), !out(reply[s]()))}


The relative ordering approach to protocol specification does not directly admit the use of global timing constraints. However, it is very much possible to describe constraints with respect to one or more timers. (The physical/temporal implementation properties of timers of course remain outside the scope of PSL.)

One way to impose such constraints is via ``client-side'' protocol rules. For example, assuming the existence of a Timer with attribute ticks, we could state that any AccountUser client issuing a getBalance receives a reply within N time units:

rules (AccountUser client, Account a, Timer tm) {
 {out(m = <a->getBalance()>) by(client), long t1 == ticks(tm)} 
 {in(reply[m](b)) by(client), long t2 == ticks(tm), t2 - t1 <= N}

Interactions with timers may also be specified. For example, an AccountUser may invoke getBalance in conjunction with a time-out alarm set for N time units of a Timer. If the client receives the reply before the time-out, it somehow uses the value. One part of such a specification is:

rules (AccountUser client, Account a, Timer tm) {
 {out(to=<tm->alarm(N)>)by(client), out(gb=<a->getBalance()>)by(client)}
 {case {in(reply[gb](b)), use(client,b)} enable {in(reply[to]())} 
  case {in(reply[to]())}                 enable {in(reply[gb](b))} 

These kinds of idiomatic constructions are obvious candidates for simpler expression and support in PSL.

next up previous

Doug Lea@Sat Jun 3 07:20:05 EDT 1995