5 Analysis

Having specified the system, we would now like to analyze it. Although there are many things that might in principle be checked, one particularly important property is whether the link connector that we defined above is consistent. By ``consistent" we mean whether it describes a protocol that is deadlock-free in the presence of reconfigurations carried out by the ``Configuror".

We can check this property directly using Wright's tools for consistency checking. When we do this we discover that the connector is, in fact, not deadlock-free. Indeed, if a reconfiguration (``control.ChangeOK") occurs after the client has sent a request (``c.request"), but before it has been transmitted to the server (``s.request"), the connector will deadlock. On the other hand, we do not have to worry about reconfiguration when the Link is transmitting a reply back to the client. In this case we can postpone its treatment until the end of the transaction.

These results have an intuitive explanation. In a concrete implementation, if the active server goes down in the middle of a request transmission (between ``c.request" and ``s.request"), the reconfiguration must be taken into account or the connector will try to send the request to the wrong server. But, if the active server goes down in the middle of a reply transmission (between ``s.reply" and ``c.reply"), the Link connector can still send the reply to the client, before reconfiguring its attachments with the servers.

This specification and its analysis can help the programmer modify the original Link definition to achieve a fault tolerant one. In practice, the code dealing with reconfiguration (e.g., switching the communication channel) should not be simply inserted in the original Link definition as a new fourth case, but it must also be interleaved with the transmission of a request. A correct version of Link's Glue is detailed in Figure 9.

  

Figure 9: Dynamic Wright Specification: Deadlock Free Link Connector

Finally, this example reveals a point about fault-tolerance: this kind of system requires a buffer to handle transient states. In our case, the request is stored in the connector until a stable configuration with a working server is reached.