Constraints

Some conditions must always hold, across all possible contexts. PSL constraint rules limit the set of possible system states to those in which listed expressions hold. For a trivial example, if we declared attribute notOpen(File f), we would want to claim that its value is always equal to !isOpen(f). The PSL notation for static constraints is based on the `` '' necessity operator of temporal and modal logic[19,64]. The expression p indicates that p invariantly holds for all time, over all possible worlds. In PSL/IDL rules declarations, brace-demarcated expressions describing necessary restrictions among attribute values are prefaced by inv. For example:

rules f1(File f) { inv {notOpen(f) == !isOpen(f)} };

Constraints may be used to describe system-wide messaging policies. For example, CORBA (like most systems) enforces the policy that either a normal reply or an exceptional reply can be issued for procedural request req, but at most one of these. Using the PSL construct unique( expr), which is false if there is more than one match to expr, these constraints may be expressed as:

inv { out(reply[req]()) --> !out(throw[req](x)) }

inv { out(throw[req](x)) --> !out(reply[req]()) }

inv { unique(reply[req]()) }

inv { unique(throw[req](x)) }

Relating Attributes to Events. Once a predicate describing the occurrence of an individual event becomes true, it never becomes false. Thus, event predicates ``latch'' from left to right in PSL linked situations. For any event predicate e, if e holds in A, then it also holds in all successors of A. For example, the following two rules for simple relays are equivalent:

{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)}

Such unconstrained attributes are notoriously troublesome in practice [43,11,17]. When attributes are not tied to events, there are no global rules stating how values change as a function of events. Any required variation or invariance in the values of unconstrained attributes across time must be explicitly tracked in individual protocol rules. Constraint rules may be used to avoid such problems, by linking the values of arbitrary attributes to the occurrence particular events. For example, supposing that our unrealistically simple File may be opened and closed only once, we might supply constraints indicating how attribute isOpen varies with open and close events:

rules f1(File f) { 
 inv { isOpen(f) -->   out(reply[<f->open()>]()) }
 inv { out(reply[<f->close()>]()) -->  !isOpen(f) }
};

Here, the first constraint says that if a file is open, then it must have at some time replied to an open request (but not necessarily vice versa). The second says that if the file has ever replied to a close request, then it must not be open. These might be buttressed with a description of a FileFactory operation that guarantees that isOpen is true upon reply of its result. On the other hand, if a File could be implemented by a special kind of object that is initially open upon construction without requiring an explicit open operation, then the first constraint would have to be weakened or eliminated.

To further illustrate, consider an Account interface, along with a protocol module declaring abstract bal and serialNo, along with simple postcondition style rules stating that mkAcc initializes them, getBalance returns bal, setBalance changes bal, and getSerialNo reports serialNo. A set of inv rules adds further constraints:

interface Account {
 void  setBalance(in float b);
 float getBalance();
 long  getSerialNo();
}; 

interface AccountFactory { 
 Account mkAcc(in long s, in float b); 
}; 

protocol module accountm {
 float bal(Account a); 
 long  serialNo(Account a);
 rules (Account a, AccountFactory f, long s, float b) {
  {in(<f->mkAcc(s, b)>)}  pair
   {out(reply(a)), live(a), bal(a) == b, serialNo(a) == s}
  {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)))}

  inv {(bal(a) == b) --> 
       out(reply[<f->mkAcc(x,b)>](a)) ||
       out(reply[<a->setBalance(b)>]()) }
  inv {(serialNo(a) == s) --> 
      out(reply[<f->mkAcc(s,b)>](a)) }
  inv {unique(out(reply[<f->mkAcc(s,b)>](a)) }
  inv {unique(in(s = <a->setBalance(b)>), !out(reply[s]())) }
 };
};

The four invariants establish the following constraints:

1. The setBalance and mkAcc 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 is expressed by relating bal to values associated with replies from either of the two operations.
2. The serialNo is always the one established by the factory operation. Note that because roles need not bear a one-to-one relation to implementation objects, it is not possible in PSL to ascribe such ``initial'' properties to roles that hold across all instantiations. Instead, factory[53] operations are used to establish instances for which particular properties hold.
3. Initialization occurs at most once per account.
4. The processing of setBalance requests is not subject to arbitrary interleavings (i.e., that they proceed serially), thus precluding multithreaded implementations. The restriction that no two setBalance operations operate concurrently can be expressed by saying that any message that has been received but not replied to is unique.