next up previous
Next: Conversation Protocol Negotiation Up: Conversation Protocols Previous: Instantaneous Description

Compatibility Semantics


In order to ensure the correct exchange of utterances during a conversation, there are important, desirable properties such as termination, liveliness, deadlock and race condition free that CPs must verify. In what follows we concentrate exclusively on the two last properties, since to guarantee both termination and liveliness it suffices to assume that every CP whose set of final states is non-empty does not remain forever in the same state.

First we formulate our notion of CP compatibility, following the notion of protocol compatibility proposed by Yellin and Strom in [12], whose work provides, in fact, the foundations of our analysis.

CPs can be assigned two different semantics: asynchronous or synchronous. Although asynchronous semantics may facilitate implementation, it makes generally harder reasoning about certain properties, such as deadlock which has proven undecidable under these semantics[12]. On the contrary, under synchronous semantics, reasoning about such properties is easier, though an implementation technique must map these semantics to a particular implementation. For our purposes, we have decided for a synchronous semantic for CPs and, consequently, for devising the adequate mechanisms for implementation. Such a type of semantic requires to assume that a speaker can send an utterance to the other speaker only if that is willing to receive the utterance. Therefore, we must assume that the finite state controls of both CP instances advance synchronously, and hence that sending and receiving an utterance are atomic actions. Upon this assumption, Yellin and Strom introduced the following notion of compatibility of protocols: ``Protocols tex2html_wrap2473 and tex2html_wrap2474 are compatible when they have no unspecified receptions, and are deadlock free''. On the one hand, in terms of CPs, the absence of unspecified receptions implies that whenever the finite state control of a CP instance corresponding to one of the speakers is in a state where a utterance can be sent, the finite state control of the CP instance of the other speaker must be in a state where such utterance can be received. On the other hand, deadlock free implies that the finite state control of both CP instances are either in final states or in states that allow the conversation to progress. Interestingly, the authors prove the existence of an algorithm for checking protocol compatibility. By applying such algorithm, it can be proved that under synchronous semantics a CP instance tex2html_wrap2340 and its symmetric view tex2html_wrap2341 are always compatible. From this follows that two CP instances are compatible if both belong to the same CP class, and both have the same speakers but different polarity. In this way, the complete agreement on the order of the utterances exchanged between the speakers is guaranteed.

Concerning the implementation, observe that the atomicity of sending and receiving utterances cannot be guaranteed. Nonetheless, when compatible CP instances lack mixed states, the unspecified receptions and deadlock free properties can still be guaranteed. But the presence of mixed states can lead to race conditions that prevent both speakers from agreeing on the order of the messages, and therefore unexpected receptions and deadlocks might occur. In order to avoid such situations, low-level synchronization mechanisms must be provided in accordance with the interpretation given to message sending and receiving in Section 3.1.

For this purpose, we consider that the speakers adopt different conflict roles --either leader or follower-- when facing mixed states. The leader will decide what to do, whereas the follower will respect the leader's directions. By extending CP instances with a new attribute --which can take on the values leader or follower-- we include the role to be played by each speaker in front of mixed states. Besides, we consider two special symbols --TRY and OK-- that alter the interpretation of message sending. Thus, on the one hand when a message is sent under the TRY semantics, the receiver tries to directly accept the message without requiring previous admission. On the other hand, the OK symbol confirms that the TRY was successful. Then given a CP tex2html_wrap2477 for each mixed state tex2html_wrap2478 the CP instance corresponding to the follower will be augmented in the following way:

tex2html_wrap2479 such that tex2html_wrap2480 then a new state tex2html_wrap2481 will be added tex2html_wrap2482 and the following transitions will be added:

  1. tex2html_wrap2483
  2. tex2html_wrap2484
  3. tex2html_wrap2485 then tex2html_wrap2486

Therefore, when the leader is in a mixed state and sends an utterance, the follower admits it and subsequently accepts it. Conversely, when the follower is in a mixed state and sends an utterance, the leader, upon reception, determines if it is admitted or not. Figure 4 illustrates how the CP instance on the left should be augmented to deal with the mixed state tex2html_wrap2461 .



Figure 4: Augmented CP instance

Notice that the conflict role played by each speaker must be fixed before the CP becomes completely instantiated. This and other properties of CP instances need be negotiated by the speakers as explained in the next section.

next up previous
Next: Conversation Protocol Negotiation Up: Conversation Protocols Previous: Instantaneous Description

World Wide Web
Wed Mar 10 11:44:57 MET 1999