Contents

1 Preamble

1.1 Conversations and Protocols

This document presents concrete description examples of various interaction scenarios written in the first layer of scribble. scribble is a language for describing the structures and behaviours of communicating processes at a high level of abstraction, offering an intuitive and expressive syntax built on a rigorous mathematical basis. While the language can potentially be used for many purposes, our initial primary application area is description, validation and execution of the whole class of financial protocols and applications which use them.

Our central philosophy in designing scribble, as a high-level language for describing communication-centred applications, is to enable description which is free from implementation details but which allows efficient and flexible implementation. The key idea to achieve these seemingly contradictory requirements is the use of the unit of abstraction called “conversation,” known as session in the literature on theories of processes and programming languages.

A conversation in the present context means a series of interactions among two or more participants which follow a prescribed scenario of interactions. This scenario is the type (signature) of that conversation which we call protocol. A protocol is a minimal structure which guarantees type-safety of conversations, and has been known as session type [3, 10, 2, 1, 5, 4] in theories of processes which in turn is based on theories of types for programming languages. [9] At runtime, a conversation is established among its participants, and the participants get engaged in communications in its context following a stipulated protocol.

A single distributed application may be engaged in two or more conversations, even simultaneously. For example, during a commercial transaction, an application running for a merchant may be engaged in two conversations at the same time, one for a credit transfer and another for a debit transfer protocol. Another example is a travel agency who interacts with its customer electronically following a certain protocol and, to meet the demands of the customer, interacts with other service providers (for example airline companies), each following a distinct protocol. The agency’s conversation with its customer and those with other services will interleave.

We specify a protocol using a type language of scribble (just as types in ML are specified using a type language of ML). This type language constitutes the most abstract level of the description layers in scribble. On its basis, the immediately upper layer of description defines what we call conversation models (which correspond to class models in UML). Conversation models serve many purposes including a foundation for a design-by-contract (DBC) framework, which starts from augmenting conversation models with assertions written in a logical language. Further we have languages for describing detailed behaviour, reaching executable descriptions, some of which may as well take the form of integration with existing programming languages. These languages as a whole contribute to flexible and comprehensive descriptions of the structure of message exchange (choreography) among communicating agents. Example descriptions in some of these languages will be treated in the sequels to the present note.

The language for protocols is the most abstract and terse: at the same time, it is also a rich description language for conversation scenarios, as well as offering a basis for the remaining layers. Protocols are also a basis of diverse forms of static and dynamic validation. Thus understanding this language is the key to understanding the present description framework as a whole.

1.2 Applications

The first and foremost objectives of scribble is to allow scribbling of structures of interactions intuitively and unambiguously. Just like we are sure what is the intended behaviour of our programs and models for sequential computation, we want to be sure what our description for interactional applications means in a simple and intuitive syntax.

scribble is based on theories of processes, in particular the π-calculus [8, 6, 7]. This is not a place to discuss the nature of this theoretical basis but it is worth noting that this theory enables us to mathematically identify what is the (interactional) “behaviour” embodied in a given description. Thus we can rigorously stipulate what each description means. While the meaning of sequential programs is relatively intuitive to capture, this may not be so for interactional software: thus this theory pins down the tenet of descriptions of interactional behaviour, bootstrapping all endeavours in the present enterprise.

Another theoretical underpinning of the design of scribble is the study on session types [3, 10, 2, 1, 5, 4] mentioned already, which present in-depth study of type languages for conversations and their use in static validation, abstraction concerns and runtime architecture.

Starting from clarity and precision in description, scribble (together with its theoretical basis) is intended to be used for several purposes, some of which we summarise in the following.

∙

Describe protocols of conversations for applications clearly, intuitively and precisely; statically validate if the resulting descriptions are consistent; with unambiguous shared understanding on the meaning of resulting descriptions.

∙

Generate code prototypes and associated runtime parameters (e.g. an FSA for monitoring) from stipulated protocols, with a formal guarantee that code/data exactly conform to the protocols.

∙

Describe conversation scenarios of a distributed application which use these protocols, as conversation models. Statically validate if the resulting models use protocols correctly, as well as other significant properties.

∙

Elaborate protocols and conversation models with assertions (logical formulae) to specify their properties, for enriched behavioural constraints/models.

∙

Develop (and debug) endpoint applications which realise given conversation models with incremental validation that the resulting programs conform to the stipulated protocols and conversation models.

∙

Statically validate if they have specific desirable properties (such as deadlock-freedom) leveraging high-level conversation structures.

∙

Dynamically validate (monitor) if runtime message exchanges of an application precisely follow the stipulated protocols/models: with a formal guarantee that all and only violations of the stipulated scenario are detected; automatically generate such a monitor from protocols/conversation models.

∙

Offer a tractable and unambiguous specification of software tools and infrastructure needed for achieving these goals.

We note that the central point of having a theoretical basis in scribble is first of all to allow these ideas themselves (for example validation) to “make sense”: we can share clearly what they mean and what they do not mean. And all of this should be built on the clarity of the behavioural description in the first place.

1.3 Copyright

Languages by their very nature are hoped to be used widely: scribble is no exception. For this reason the use of a general language has never been taxed since ancient times, either natural or programming. scribble is therefore free (as in freedom). All ideas in this document are free (as in freedom). For the document itself we only ask it to be treated as decently as other scientific documents: our purpose is to share ideas.

1.4 Caution

This compilation only lists signatures (or types) for conversations, not direct behavioural description. While it may look we are describing dynamic behaviour, what is indeed described is the static structure underlying dynamic behaviour, just as signature in class models extracts the static core of dynamic behaviour of objects.

1.5 Legend

The presentation is organised centring on concrete examples described in scribble. Each subsection (except a few whose titles are prefixed with “Note”) treats one example. Each example is preceded, when necessary, by a brief note; and is followed by illustration and comments. We refer to the example in Section 6.1 as Example 6.1. There are 29 examples divided into 11 sections: the last section treats fairly complex examples from a real world financial protocol.

2 Declaration and Interaction

2.1 Example: Hello World

The following is the signature for a hello-world program:

Comment 2.1.1 (Structure of Protocol)  
A protocol (or protocol definition) consists of:

(1)

preamble, mainly consisting of import clauses (none in this example, illustrated in Example 3.1 later).

(2)

protocol definition (Lines 1–8 above)

The protocol definition starts from (in Line 1 above) the keyword protocol, followed by the protocol name (GreetWorld in this example): then the main part, the protocol body, comes (lines 2-7 above), enclosed by curly braces.

Comment 2.1.2 (Declaration)  
Lines 3 and 4 give participant and channel declarations, respectively. Line 3 says that this protocol uses two participants, You and World. it uses declaration of multiple participants:

which is the same thing as:

As in Line 3, Line 4 uses declaration of multiple channels which can be similarly decomposed. The keyword at indicates that the channel is located at the participant for the latter to receive messages through the former. So Line 4 says that the protocol uses the channel chWorld which is located at the participant World. We can write “@” for “at”: so Line 4 can also be written:

Comment 2.1.3 (Interaction)  
Line 6 defines an interaction signature or often simply interaction which reads:

In general an interaction has the following syntax:

where Ch is a channel name and Part1 and Part2 are participant names. These two participant names and a channel name should be declared beforehand. This one line depicts abstractly the following situation:

• Part1 asynchronously sends a message which has an operator (selector) OpName and arguments of types Type1,..., TypeN, to a target channel Ch;
• this message will travel through network and arrives at Ch which should be located at Part2; and
• eventually the message is received by Part2.

Later we present syntactic conventions to omit part of the syntax of interaction without losing precision — for “fast scribbling”.

Comment 2.1.4  
Channel declarations can be further elaborated with one or more modes, on which we discuss in Section 2.3.

Comment 2.1.5  
A protocol is often called signature of a conversation.

2.2 Note: Participants and Channels

A language abstraction (such as “while” in imperative languages) serves both as a tool for describing the application concerns and as a basis of implementation. In other words a good abstraction should capture the desired behaviours cleanly and without losing generality; and should serve as an effective medium to efficiently realise these desired behaviours by mapping them to an available execution mechanism.

Participants and channels (and other constructs which use them such as interactions) are intended to be such abstractions. One rough but useful way to think of participants and channels are as follows:

∙

Participants represent, abstraction-wise, corporations, divisions, departments, groups or individuals, who are responsible for taking communication actions in distributed applications. System-wise they represent network endpoints and may be designated by standard addresses or names used in global networks (ranging from IP addresses to public URLs to X.509 certificate).

∙

Channels located at some participant are logical entities which serve as multiple destinations within that participant (consider them as different mailboxes which a participant can access to and retrieve his/her messages from). A sending action is targeted to a specific channel. System-wise a channel serves as a means for multiplexing communications to some endpoint: as such, two channels allow parallel message processing as well as parallel monitoring as desired.

We consider participants as fundamental abstraction. From the abstraction concerns, many application domains (say financial protocols) demand a point of focus for capabilities and responsibilities in communication actions. From the implementation concerns, a conversation is system-wise realised by the behaviour of endpoints so that abstraction of endpoints plays an essential role for a consistent abstraction framework.

Channels are built on this abstraction. Since channels are logical there is no need to map distinct channels at some participant to physically distinct channels (at the OS/Network level), though implementation can choose to do so.

We assume the following two conditions are satisfied in the channel-based communications under consideration.

∙

(Asynchrony) There is no wait in sending actions.

∙

(Message Order Preservation)  The order of two messages from the same participant to the same channel is preserved.

These two conditions may be achieved by a message transport layer possibly in combination with runtime systems at endpoints and are natural assumptions under the available transports, be it in Internet, high-performance LAN or on-chip interconnect.

2.3 Note: Modes for Channels

Since channels are logical we can think of different ways to use this abstraction. For example we have the declaration which says that we consider only one channel to a specific participant:

which says World only owns a single channel, chWorld. This unique elaboration allows us to even omit a participant name when one likes to do fast scribbling, as we shall see later.

Or we may consider fixing a sender for some channel:

which says chWorld is located at World to which only You will send to. We can stipulate a set of senders as:

which specify I and You as possible senders for chWorkd.

Logically speaking, we can also think of channels via which messages can be received by several participants (consider a mailbox which can be read by several principals). For our current problem domain, financial protocols, we consider that the use of such channels is not necessary and is not advantageous (note their inclusion necessitates a mechanism to multiplex a message queue among geographically separate endpoints: this is certainly not impossible but it may lead to more error-prone models/programs and may incur a heavy runtime in the presence of choice constructs which we introduce later). Nevertheless we can think of the notation for this most unrestricted case:

or one may specify multiple participants for senders and/or receivers, as:

Note this is not about multi-casting: in multi-casting, each message is duplicated and distributed to each recipient, while in this case each message is received by one of the recipients and is not duplicated.

Other modes for channels (used by prefixing as those discussed above) include:

∙

once: can be used at most once.

∙

repeated: can be used zero or more times (default).

∙

linear: can be sent from one at one time (default).

∙

shared: can be sent from many at one time.

∙

sharedlinear: can be sent from many at one time but only one of them will be processed.

∙

collective: represents individual channels of a collection of participants (enabling multicasting).

These modes have their origins in theories of processes on the one hand and in practice of communication-based applications on the other.

3 Sequencing and Choice

3.1 Example: Buyer-Seller Protocol (1)

This is a well-known simple two-party protocol, through which we introduce two of the key control constructs, sequence and choice. This example also shows the way to import data and document types.

Comment 3.1.1 (Import)  
Line 1 imports two data types, Invoice and Order. Since these are given without name space notations, their definitions are parametrised and are bound to concrete data types by an enclosing context. We can also refer to document types using URLs (or any element in a specified name space), as discussed in Section 3.5.

Comment 3.1.2 (Sequencing)  
Line 6 is the first interaction described in the protocol, saying that Buyer sends an order to Seller via chSeller. Line 6 and the next choice construct (from Line 7 to Line 11) are combined by the sequencing “;” (this operator appeared before but not substantially). In general a sequencing is written as, with I1 etc being sentences in a protocol:

Informally a sequencing is interpreted as follows: in I1;I2, if the same participant appears in both I1 and I2, then their actions should be ordered temporarily for that participant. In particular if none of the participants overlap between I1 and I2, there is in fact no order specified. This interpretation is faithful to the asynchronous semantics of communications as discussed in a separate work (this point is informally illustrated in more detail in the scribble’s blog titled “Example (1) asynchrony”).

Comment 3.1.3 (Choice) From Line 7 to Line 12 we use a choice construct. In Line 7 we see:

which declares that this choice is chosen by participant Seller (which should be declared beforehand). This is followed by two choice branches which consists of a block¹ from Line 7 to Line 9 and a block from Line 9 to Line 11, which are combined by the keyword or in Line 9. The choice in Lines 7–12 reads:

Note that, in this choice, both of the initial actions in its branches are from Seller to the same channel chBuyer. This is the most tractable form of a choice, where the receiver (Buyer) has only to expect differing messages at a single channel. We shall later explore other kinds of choices with different kinds of locality.

There are only two branches in the choice construct in the example. In fact a choice construct can have an arbitrary number of branches:

where the order of the branches in a choice is irrelevant so that we can permute them without changing the meaning.

Comment 3.1.4 (if-then-else and choice)  
In programming, the choice in Example 3.1 may as well be realised as a concrete behaviour using the “if-then-else” construct: for example, Seller may look at its stock record and if there is an enough stock to meet the order will decide to send “invoice” or, if not, the “out-of-stock” message to Buyer. In comparison:

• The choice construct in protocols describes all possible interactions in abstract, without mentioning concrete details of how one branch is chosen over the other;
• In contrast, the if-then-else construct in programs describe specific algorithmic behaviour concerning corresponding choice point concretely.

Note (1) offers just enough information to constrain (2) so that interactions proceed without such hazards as mismatch in document types etc. On this basis a model may as well describe, in principle, anything between (1) and (2).

3.2 Example: Buyer-Seller Protocol (2)

This will be the same protocol as Example 3.1 except we use a “Fast Scribbling” notation which omits the receiver, using locatedness of channels.

Comment 3.2.1 (Fast Scribbling, 1)  
The protocol given above is precisely the same as Example 3.1 except in interactions at Lines 6, 8 and 10, where we omit receivers’ names, relying on the declaration in Line 4 to fill respective appropriate receivers. This does not change the meaning of the protocol: we formally regard these two protocols to be eqivalent. The general rule of this omission is simple: when a channel is located at a single participant, as is usually the case and as in this example, we can omit the receiver’s name. This omission does not lose precision: moreover it does not seem to lose legibility either (at least from our experience). The example above hopefully shows that this abbreviation does not lose clarity: this would be because one can easily see flow of information from the description.

Comment 3.2.2 (Virtue of Redundancy)  
One may wonder what can be the benefit of not omitting the receiver when a channel is located. Surely it is redundant to mention it, but suppose you happen to type in, under the same declaration as Line 4 above:

Then your editor can immediately check either the channel name chSeller is wrong, its declaration is wrong, or the recipient participant Broker is wrong. Thus by a piece of redundant information your editor can give an alarm which is not possible otherwise. We may also recall such redundancy is used in all typed programming and modelling languages.

3.3 Example: Buyer-Seller Protocol (3)

The following is essentially the same protocol as Example 3.1 except that it does not use an operator name in the first interaction: instead it uses the name of a data type (hence the protocol is different from Example 3.1, exactly speaking).

Comment 3.3.1 (Interaction without Operator Name)  
In some interactions (in fact in many financial protocols), the use of operator names may look redundant and is in fact logically unnecessary. In such cases we allow the following format:

which means:

For legibility we only allow single message interaction in this notation which practically does not lose expressiveness. This is used in Line 8 of the example above. A finite state automata underlying static and dynamic validation of protocols are induced from these types used as part of messages, serving as their labels. We can use any “designated name” (see Section 3.5) as the name of a data type usable as such a label.

3.4 Note: Further Fast Scribbling

In Example 3.2, we have seen that we can omit the recipient of an interaction without losing any information when the involved channel is located. Here we discuss several more notational conventions for fast scribbling.

The following notes are given as additional comments for Example 3.2.

Comment 3.4.1 (Omitting Sender)  
Assume that the sender of channel chSeller is uniquely fixed in Example 3.2 using from (see §2.2) as follows:

then we can also abbreviate the interaction syntax so that we can omit a sender, as in:

or when we only use the type name for a selector:

We do not recommend this practise except for a personal scribbling or when we describe a series of interactions at the same channel, since the resulting description tends to read cryptic.

Comment 3.4.2 (Omitting Channel)  
As another constraint on chSeller, suppose that, in Example 3.2, the channel is uniquely located at participant Seller (see §2.2) with the declaration say

Then we can do an abbreviation in a different way: this time we omit the target channel, writing:

or in the case when we use only the type name:

In both cases the description automatically entails that the used channel is chSeller. One may observe that this notation is isomorphic to (taking the second one):

which is the familiar notation from cryptographic protocols. This correspondence allows us, on the one hand, to map many informal protocols written without channels onto the present notation faithfully; and on the other to present a class of protocols (as above) in the familiar notation.

3.5 Note: Details of Import Statement

Importing Opaque Data Types.  Practical communication-centred applications, now and in future, treat many kinds of data and document types. Even restricted to financial protocols, we have to treat a wide range of document formats. The ability to flexibly and precisely specify these data formats at a desired level of abstraction is fundamental for their practical usage as a basis of conversation-based models and applications built on them, including conformance validation and precise monitoring.

The import statements we have introduced has the following shape:

Above Invoice is a data type name, called designated name, which will be bound to some data type or document type at (say) compilation time, via the following itinerary:

1. If the protocol is used in some name space (by the enclosing environment — induced by say an enclosing program) and the name Invoice is bound to some data format, then that is its real format — but its type name in an interaction signature is still Invoice.
2. If there is no binding for Invoice, then a compiler tries to find Invoice (perhaps with some suffix such as Invoice.sdd) in the current directory. If it is found then that is its real format — but its type name in an interaction signature is still Invoice.
3. If this does not succeed, then we do not know the real format which Invoice stands for: however the need to do such a binding only occurs when one needs manipulation of data items of this type — hence as far as we do not need it for current task at hand (e.g. validation, compilation, ...) we can leave its treatment for later: we take the late binding approach.

Binding should be determined when one wishes to check compatibility among descriptions of distributed applications: if two programs use the protocol but in fact eventually use different data formats then this can cause a problem. But validation and compilation may as well be done earlier and generically: we believe incremental and staged approach in compilation will help us deal with this issue.

Importing External Data Types.  Next we consider the cases when we bind early: we directly specify externally defined data/document types, refining the syntax of import above. Consider for example the use of XML data types. This can be an XML schema (for the whole XML document) or an XML data types (say for elements). Below we consider the latter case which easily extends to the former. Assume we wish to import a data type called RequestTradeConfirmation with target namespace ² (say) http://www.fpml.org/2007/FpML-4-3 from a file (say) RequestTradeConfirmation.xsd located in the current directory. We can then write:

The statement above reads:

The part xmlschematype is called type kind: since its use is an integral part of import clauses, it should be part of compiler and runtime infrastructures. The management of type kinds in such infrastructures can be done following general rules which we shall discuss elsewhere. One of the purposes of importing data type is to statically check whether models and programs manipulate data properly: this is why it becomes important to have these data kinds properly managed.

Above, note the designated name becomes RequestTradeConfirmation rather than the qualified name. Note also that the last RequestTradeConfirmation is not enclosed in the quotation marks: it is the name inside the system and as such cannot overlap with any other designated names. Designated names are used as labels (literals) for various static and dynamic validations and serve as a basis for execution. The source field (the field after from) can include a URL.

If the as field (above RequestTradeConfirmation) is omitted then the canonical name becomes the qualified name of the data type (prefixed with the namespace). Even in this case, one may refer to this data type with the local name RequestTradeConfirmation as far as there is no ambiguity. Such convention can be stipulated for each type kind.

In the case above, the “xsd” suffix of the file name safely allows us to regard the target of import as an XML data type, ,enabling us to infer the data kind even if the statement lacks it:

which gives a use of the registered data types.

It is also convenient to be able to import multiple types collectively: For this purpose we can write:

without specifying an intended data type name, in which case all data types are imported from the source. The qualified names of imported types become their designated names. In such cases it would also be convenient to be able to use an alias for a target namespace as in the standard practice of XML so that we do not have to use qualified names without name collision (designated names stay to be the qualified names).

As a non-XML example, suppose we wish to use a Java class which includes a class called Invoice. Then we can write:

where we specify the code base name in the from field and the package hierarchy (including the directory hierarchy) in the name space part. If no code base is specified then it is taken from a directory specified by the environmental variable: in the usual case this will be the current directory where compilation is being done.

Using Public Data Types There are two rules of thumb for a safe practice for the use of document types for protocols, especially for protocols with public nature such as financial protocols, to guarantee maximum compatibility.

(1)

Use the public document type as much as possible (for the initial “namespace” part).

(2)

Use the formal repository for (1), if any, as the source of its specification (the from field).

The key merit of these two rules of thumb is portability: your protocols, hence your models and programs based on them, can be used, validated and run at any place guaranteeing compatibility with the other participants in the protocol, as far as the other participants also adhere to the rules and (2) is accessible. If (2) causes an issue in efficiency and accessibility but the data format is a well-known one then we can also make resort to the format without the from field:

In this case the source file will be accessed following a local rule in a given environment: if it is a well-known document format and is stable, then it is worth maintaining the definitions locally in (say) an organisation or in a local machine so that they conform to the public repository.

Another way to gain portability is the use of meta data so that we can leave a data type abstract while constraining some of its features. For example we may want a concrete data type to be communicated on the fly. If no constraint is given for its usage, we can use a pure nominal type. If however we do need constraints, we may use meta data specification languages such as RDF and OWL. This may be done with the keyword satisfying followed by the location of a specification file. The concrete syntax needs be defined for each specific data kind.

4 Three Party Protocols

4.1 Example: Buyer-Broker-Seller Protocol (1)

In this section we show three examples which in fact use the same constructs as in Sections 2 and 3 except there are three participants involved in the protocols: in addition to Buyer and Seller we have Broker.

Comment 4.1.1 (Buyer-Broker-Seller Protocol)  
We illustrate the basic scenario of the protocol above.

1. Buyer orders goods to Broker (Line 6).
2. Broker may choose to order the same goods to Seller (Line 8), or Broker may choose to send instantly an out-of-stock message to Buyer (Line 17).
3. If the former is the case then there are two possibilities:
4. First, Seller may (for example if it has the goods) send an invoice to Broker (Line 10) which in turn sends an invoice to Buyer (Line 11).
5. Or alternatively Seller may send an out-of-stock message to Broker (Line 13) which in turn sends the same message to Buyer (Line 14).

Note that, by locatedness of channels, we can omit all recipient participants from the interactions, cf. Example 3.2. Note that the distinction between document names (e.g. Order and OutOfStock) is used for making the choice meaningful: this means these names play an essential role both for static validation and at runtime, just like method names (selectors) in objects.

4.2 Example; Buyer-Broker-Seller Protocol (2)

The following example is precisely the same as Example 4.1 except a position of declaration for Seller and its channel.

Comment 4.2.1 (inner declaration)  
The only difference from Example 4.1 is in Lines 8 and 9 where we declare the participant Seller and its channel chSeller only when they become necessary (in Line 11), unlike in Example 4.1 where both are declared at the outset together with others. In spite of the difference, we regard this protocol as identical to Example 4.1 in terms of their denotation (i.e. what they mean: hence in static validation and code generation). A signature only specifies the core interaction structure, not dynamic details, so that it is a good idea to treat such variations as abstractly as possible. Such local declaration is especially useful in large protocols.

Comment 4.2.2 (another use of inner declaration)  
The equivalence between Example 4.1 and Example 4.3 does not prevent implementations to use such an inner declaration as a hint for efficiency or economy: for example it shows that Seller can participate in this conversation as late as the declared point (note this information can also be inferred from Example 4.1). Thus we obtain both freedom in descriptions and flexibility in implementations.

An alternative interpretation is to consider that an inner declaration fixes the place where a participant may join this conversation: this interpretation however contradicts with the purpose of conversation signature since, regardless of the timing of participation, the resulting scenario inside a conversation remains the same. For this reason such a detail is better described in a modelling and programming language when there is a need.

Comment 4.2.3  
There are cases when an inner declaration of channels cannot be replaced by an outer declaration: this is the case when we use the former as part of a recursive protocol, or when we need to use the same sub-protocol repeatedly inside a protocol, see Section 10.2.

4.3 Note: Treatment of Ill-Formed Protocols

A protocol description can sometimes be loose:

 
In the protocol above, the choice is located at Broker: however the immediately following actions are done by Seller in each branch. This has causal anomaly since the immediately following actions cannot be done except by Broker (we omit detailed analysis), hence we may conclude that some such actions are missing from the description. Such an incomplete description may be called ill-formed. When contrarily all natural causality constraints are met, a protocol is well-formed. We may allow such ill-formed description under the assumption that they are to be completed later (e.g. an editor may flag those places to be “completed”). Note that, for the well-formedness of choices as in this example, we need to locate choice at a participant.

5 Repetition and Recursion

Repetition and recursion are used to describe recurring behaviour. They have the following syntax respectively:

The first syntax describes a repetition of the conversation in the block. The second syntax uses a label label (whose use directly comes from type variables in standard recursive types) to explicitly repeat the whole block from arbitrary points inside the block.

5.1 Example: Repetition

Below we refine the Buyer-Seller protocol in Example 3.3.

Comment 5.1.1 (Repetition)  
The protocol, whose Line 6 introduces the repeat construct located at Buyer, reads as follows.

Thus this repetition construct allows Buyer and Seller to repeat the same conversation unboundedly. The locatedness at Buyer means the decision to repeat or not is the responsibility of Buyer. Note the protocol does not say how Buyer will notify Seller about this decision, on which we discuss in Comment 5.1.2 given next. To explicitly specify an exit, we can use the labelled recursion discussed next or the escape construct discussed in Section 8 later.

Comment 5.1.2 (Implicit Interaction in Repetition)  
A natural implementation of a repetitive conversation following the above protocol will let Buyer notify Seller when the latter decides to quit the loop (cf. Comment 5.1.1), necessitating the use of implicit interactions. On this topic we shall discuss in Section 9.

5.2 Example: Recursion (1)

We now consider a version of Buyer-Seller protocol with recursion.

Comment 5.2.1 (Recursion)  
In Line 6, the recursion (prefixed by the keyword recur) is introduced, located at Buyer (hence the decision to recur lies in Buyer) and labelling the recursion block (Lines 6-19) as Transaction. In Line 15, this label is used for recursion, by simply citing it. As a whole the protocol reads:

The difference between repeat and recur is that, in the latter, recurrence is no longer implicit: it now needs to be explicitly specified (as in Line 15) or else the block will exit the recursion block. The use of the recursion label should always be local to (inside) the labelled block.

Comment 5.2.2 (Recursion and Global Escape)  
The construct is useful to exit from an internal loop to an external loop or even to the outside of loops, since as default (i.e. if there is no recur statement) the repetition in the conversation structure is absent. The code remains structured due to the rigid nesting.

5.3 Example: Recursion (2)

We next consider a recursion which has multiple exit and recurring points. The protocol depicts the negotiation between Buyer and Seller: Buyer wishes to negotiate down the price and always tries to continue negotiation as far as he is unhappy about the price.

Comment 5.3.1 (Multiply-Located Recursion)  
In Line 7, the recursion is located at both Buyer and Seller, allowing both to decide to recur. Lines 20 and 25 show the use of recursion by respective participants. As a whole the protocol depicts the following situation:

Note that either Seller or Buyer can decide to recur, in Lines 20 and 25, respectively. Further there are multiple exit points, again by Seller and Buyer, in Lines 16 and 28. Having multiple repetition and exit points in this way is made possible by the flexibility of recursion.

Comment 5.3.2 (Implicit Interaction in Recursion)  
Whichever of Buyer and Seller decides to exit/repeat the recursion, the other party needs be notified that the Transaction recursion block is to be repeated (or not): if this information is not communicated, the scenario one party is following and the one the other party is following can become inconsistent. This is another example where the use of an implicit interaction may become necessary (cf. Comment 5.1.2), though in fact the given interactions are enough to share the decision in the protocol given above. General discussions on implicit interactions are given in Section 9.

Comment 5.3.3 (Further on Escape)  
The use of recursion in Example 5.3 allows a loop with multiple exits and multiple resumption points. What recursion cannot realise is to describe the conversation in which the interacting parties can escape from a repeated conversation to another conversation at any point of the loop: but the more complex the conversation inside a loop becomes, the more convenient it becomes to escape from the loop at any point of the loop. The construct to describe such conversation patterns will be discussed in Section 8.

6 Parallel

In many conversations we wish to perform two or more independent conversations in parallel. This is realised by the parallel construct.

6.1 Example: Buyer with Two Sellers (1)

We first treat a simple example where one buyer interacts with two sellers.

Comment 6.1.1 (Parallel)  
In Line 4, two channels (chBuyerA and chBuyerB) are located at Buyer. In Lines 6 and 7, Buyer sends a message to SellerA and another to SellerB sequentially; then from Line 8, there is the parallel construct which describe two parallel conversations, one between Buyer and SellerA using channels chSellerA and chBuyerA (from Line 9 to Line 14), and the other isomorphic one between Buyer and SellerB using channels chSellerB and chBuyerB (from Line 16 to Line 21). Note that two parallel conversations use two disjoint sets of channels for their conversation: in particular messages to Buyer are handled by two distinct channels. This disjointness prevents communicated messages from getting mixed up, which is why Buyer is using two channels.

Comment 6.1.2 (Parallel and Message Mix-up, 1)  
A mix-up of messages which may be asynchronously arriving at a participant, can be prevented in several ways.³

• Distinct channels, as in Example 6.1 above.
• Distinct operator names (or data types).
• Distinct values.

Among the three, (3) is not desirable since we cannot guarantee the lack of confusion statically, i.e. at a compile time. On the other hand, the solutions (1) and (2) have the merit in that such a guarantee can be done at the signature (protocol) level. Once this is done, any program or model which conforms to the protocol is guaranteed to be confusion-free.⁴

Between (1) and (2), (1) is robust in that the design (including its change) can be done systematically by preparing disjoint channels for conversations which may possibly run in parallel. (2) may be less robust since there may always be the chances that two parallel threads of conversations wish to use the same document types etc., though for smaller protocols this method will also work. The static checking is equally easy in both cases.

Comment 6.1.3 (Parallel and Message Mix-up, 2)  
Yet another solution to prevent a mix-up may use the names of senders (in the case above, SellerA and SellerB). However this solution assumes that each message carries the name of its sender as part of its fields; and that this name precisely corresponds to a participant. While the former may be manageable, the latter is problematic since if we assume a uniform correspondence scheme then it will prevent a late binding of participants to real organisational entities. In contrast, channels are abstractions which are maintained inside a conversation: in particular, the representation of channels is maintained purely inside each conversation instance (see Section 2.2).

Comment 6.1.4 (simple multi-casting)  
Lines 6 and 7 may as well be written:

which has the same semantics as Lines 6 and 7 since we are assuming communication is asynchronous. A later version will discuss an example with full-fledged multiparty channel.

6.2 Example: Buyer with Two Sellers (2)

We consider a variant of the previous example.

Comment 6.2.1 (Parallel and Synchronisation, 1)  
In Example 6.1, we first have two interactions (Lines 6 and 7), followed by two parallel conversations (one from Line 9 to Line 14 and another from Line 16 to Line 21).

In Example 6.2, the initial two interactions are now merged into respective parallel conversations: so the original Line 6 is now found in Line 8 of Example 6.2, similarly Line 7 is found in Line 16 of Example 6.2.

In the present case, these two protocols (as far as we do not mind the order of two initial sending actions by Buyer) may in fact be regarded as being logically identical as far as we regard send actions to be purely asynchronous (i.e. they demand no synchronous ack — which we presume to be the standard assumption). If however a sending action demands a synchronous ack, Example 6.1 has an extra sequencing, hence two are logically distinct.

Comment 6.2.2 (Parallel and Synchronisation, 2)  
We show a case in which the distinction we discussed in Comment 6.2.1 is evident. Consider that the initial two sending actions are replaced by:

Then putting the above four lines before the parallel conversations in Example 6.1, on the one hand, and distributing them to the parallel blocks, on the other, are surely distinct in terms of the ways communication actions are done and therefore how they are observed: there is strictly less (potential) asynchrony in the former.

6.3 Example: Buyer with Two Sellers (3)

We next consider the case when we synchronise after the parallel construct, taking a speculative conversation by Buyer.

Comment 6.3.1 (Parallel and Synchronisation, 3)  
Note Lines 12-18 describe a conversation after the parallel construct. We outline the scenario of this protocol:

In this case it makes a good case that Buyer waits until both parallel conversations complete, which is precisely what the protocol above dictates.

Comment 6.3.2 (Parallel and Symmetry)  
The parallel construct, as in choice, induces symmetry among its component blocks: however we order them, they are regarded (logically) identical.

7 Protocol inside Protocol

There are a couple of ways to “run” protocols inside a protocol. The first one simply uses the definition of another protocol, just like one uses a class in another class. Another is to define a protocol inside another protocol and run it. If we name an inner protocol, then this is like an inner class in Java. If we do not name it, it is like an anonymous class. We illustrate these three cases by simple examples, touching a subtle feature of channel declaration which we have not discussed so far.

7.1 Example: Running Inner Protocols

The following defines logically the same protocol as Example 6.2.

Comment 7.1.1 (“Run”)  
We use the verb “run” for protocols following the standard usage of English. The term “run” however does not have any dynamic meaning: we can always textually replace a run statement with its content. Although an implementation can use it as a hint for e.g. a lazy establishment of a conversation, this is an implementation concern, not a description/modelling concern.

Comment 7.1.2 (Sub-Protocol and Main Protocol)  
If a protocol runs another protocol, we often say the latter is a sub-protocol of the former. An outermost protocol is called the main protocol.

Comment 7.1.3 (Inner Protocol)  
From Line 15 to Line 27, an inner protocol Order is defined (whose name coincides with Order as an imported document type but which does not lead to confusion because their types and usage are different). Except prefixing the keyword protocol with another keyword inner in Line 15, the format of the definition is precisely the same as in independent protocol definitions.

Comment 7.1.4 (Instantiating Protocols, 1)  
Lines 8 and 9, as well as Lines 11 and 12, run the subprotocol Order. Since two parallel blocks use the common conversation structure, this shared use contributes to clarity and economy.

In Lines 8 and 9, we run the protocol Order instantiating it with Buyer and SellerA declared in Line 4, substituted for Buyer and SellerA respectively (in “A for B”, the former is the value already declared in the running protocol, while the latter is the value to be substituted for in the sub-protocol: thus in “Buyer for Buyer” in Line 8, the first Buyer is what is declared in Line 4; while the second Buyer is what is declared inside Order (in Line 15).

In Lines 8 and 9 as well as Lines 11 and 12, we observe that only participants are instantiated, not channels: this is because, when we declare channels, we assume they are localised (more pedantically they get syntactically bound): even if a channel with the same name is declared elsewhere, there will be no confusion (such freshness is easily maintained at runtime). Thus declared channels are always fresh and distinct from other channels.

For example, in Line 15 of the inner protocol Order, channels chBuyer and chSeller are declared. Once thus declared, channels are never bound to something else.⁵ In contrast, a declared participant needs usually be bound to a “real” endpoint, so that its name is “free” (as in free variables), in that it is waiting to be instantiated.

Comment 7.1.5 (Instantiating Protocols, 2)  
Generally, the run statement can be written as:

where ABC is the name of a protocol, formalparam1..N are those parameters which are free in ABC, while realparam1..N are those parameters which are already declared beforehand.⁶ For usual protocols, free parameters in ABC are simply participant names declared in ABC (we later define open protocols where not all channels are declared, in which case undeclared channels become part of formal parameters). Instantiation can also be done for polymorphism in a way close to generics in Java and C♯.

7.2 Example: Running External Protocols

If we assume that the protocol Order in Example 7.1 is defined elsewhere, we can write the protocol BuyerAndTwoSellersAsync as follows.

Comment 7.2.1  
Except Line 2 imports the protocol Order from outside, and it lacks the original inner protocol definition, Example 7.2 is exactly the same as in Example 7.1.

7.3 Example: Running Anonymous Protocols

An anonymous protocol is useful for clarity and articulation though it is less convenient than the previous two cases since it can only be referred to in the single place, i.e. the place where it is used.

Comment 7.3.1  
The protocol is exactly the same as the one which expands and instantiates the anonymous protocol. For this reason anonymous protocols do not add expressiveness vis-a-vis (among others) inner protocols: however they have their use in analysis and transformation of protocols.

Comment 7.3.2 (Open Protocols)  
Below we consider turning the anonymous protocol above to its open version.

Above we observe:

∙

chBuyer0 is declared to be open: this means that this channel name should be instantiated from the enclosing context. Further the description says that this channel should located at participant Buyer0.

∙

Accordingly The run primitive instantiates, in addition to two participants, chBuyer0 into chBuyer (the latter already declared in the enclosing protocol). Thus we can instantiate not only participants but also a channel.

Open protocols are useful for instantiating the same protocol with one or more common channels (for example in different branches of a choice). When running an open protocol, one convenient notation may combine a channel and a participant as follows:

assuming an open protocol OpenOrder with the same definition as the anonymous one above. This is an economical notation especially when we have only one channel for one participant.

8 Global Escape in Conversation

A frequent pattern in conversation is that some circumstance necessitates a conversation to abort in its middle and finish there, or move to a next conversation. Such an “escape” is structurally close to “exception” though in many cases the cause of such a global escape may not be an error in a computation but rather communication from other parties. We illustrate the idea through examples.

8.1 Example: Criss-Crossing and Global Escape

The first protocol comes from trading and induces a criss-crossing interaction pattern as follows:

A central aspect of this scenario is that at each loop, Seller continues to send a quote without waiting for a message from Buyer: it autonomously continues the sending until it receives a message from Buyer. This means we cannot use a choice at each repetition to represent such a protocol. Global escape however can handle such situations simply and clearly.

 
NB: Among the following comments, only the first one is enough to obtain a general idea. The remaining comments are detailed illustration of its semantic mechanism.

Comment 8.1.1 (Global Escape, 1: RepeatQuote Protocol)  
From Line 5 to Line 14, we find the escape construct, which uses the familiar try-catch keywords. In Line 5, the try-block is introduced which consists of a single repeat block from Line 6 to Line 8, in which Seller repeats sending a quote at each loop (note that, in the loop itself, Buyer only receives a message, so no synchronisation is necessary). The try-block enclosing this loop entails the potential that this try can be interrupted: the potential events which serve as the cause of an interruption is given in the two catch blocks from Line 9 to Line 14.

In the first catch block, we find a single interaction, which is from Buyer to Seller accepting one of the quotes. In the second catch block, we again find a single interaction, but this time it says Buyer wishes to abort the transaction. In the former case, Seller sends an acknowledgement and an invoice to Buyer. In the latter case a conversation ends here (where end is the primitive to explicitly finish a conversation). The interactions mentioned immediately after two catch keywords indicates that, at any time of a conversation, once they take place, the conversation moves to the corresponding catch block. It should be the case that only a single exception takes place at each channel (further details on such interrupting interactions are discussed later).

Note the channel chSeller does not occur in the try block, so that there is no confusion as to whether a message one receives is for the conversation in the try block or for invoking one of the catch blocks. Also note it does not specify as to which state/condition induces an interrupting message: a protocol only specifies the basic skeleton of a conversation structure.

Comment 8.1.2 (Global Escape, 2: General Syntax)  
The general syntax of an escape construct is given as follows, taking the case with a single catch block:

to which one can add further catch blocks as needed. The catch block indicates that, at any time during the conversation in the try-body, if one of the interactions mentioned inside its initial parentheses (called interrupting interactions) takes place, then the original conversation aborts and the conversation in the catch block (for all participants in the conversation) starts. Basic observations:

(1)

This is type/signature declaration rather than behavioural description: it does not say in what state/condition an exception may be thrown.

(2)

An interrupting interaction, hence escape to the catch block, can occur at any point during the try body;

(3)

Interrupting interactions should be disjoint from interactions inside the try block. This can mean one of:

1. Their channels should not overlap with those used by interactions inside the try block;
2. Their signatures (including channels) should not overlap with those used by interactions inside the try block.

Clearly the second condition is more general. On the other hand, being more restrictive, the first one also has the merit in that it may be less error-prone for us to describe (since one only has to distinguish by used channels) and allows a simpler implementation (since the runtime can be alert on specific channels for interrupting messages). As a possible practice for the first approach, one may declare channels for escape separately from ordinary channels (one may use escape keyword).

Note that interrupting interactions can be in any directions: for example in the case of RepeatQuote above, some interrupting message can be sent from Seller to Buyer. This and other factors entail that, for treating the present escape mechanism, we need a synchronisation mechanism among all parties. In general this demands a standard n-party agreement (underlying) protocol, but in many cases we can use a simpler protocol for resolving synchronisation including the issue of priority discussed in the next Comment.

Comment 8.1.3 (Global Escape, 3: Resolving Multiple Interruptions)  
When there are multiple catch blocks, we need to resolve multiple interruptions and their effects. We do not discuss detailed arguments except noting a couple of basic principles:

• We stipulate that a participant will “throw” at most one interrupting exception to a single channel.
• Under the condition of (1), we specify all combinations of possible interrupting messages with distinct effects.

As to (2), for example if there are multiple interruptions but they are just for a single catch block, this is enough. However if there are (say) two interruptions placed in distinct catch blocks then one also has to specify the combined effect as the third catch block.⁷

8.2 Example: Multi-Staged Global Escapes

One of the merits of the present escape mechanism is to enable participants to escape from a conversation to another then from there to another, ad infinitum. We show this by an example which concatenates two RepeatQuote conversations into one: Seller is persistent and does not give up by Buyer’s rejection for the first time.

Comment 8.2.1  
This example depicts the scenario as the previous one except that, after the first try is rejected in Line 12, Seller moves into the second round of a quote conversation in Line 13. The interactions from Line 13 to Line 23 are precisely the same as those of RepeatQuote. When Buyer sends a “no thank you” message, (unfortunately for her) she should be ready for the repeat of quotes, since the protocol is a shared agreement: however she can send another “no thank you” message and the conversation as a whole terminates.

8.3 Example: Andrew Parry’s Protocol

The basic script for the following protocol was contributed by Andrew Parry. It introduces a local interrupt which is not communicated to the other — when communicating an interrupt is vanity.

Comment 8.3.1 (Local Interrupt, 1)  
We focus on the try block from Line 13 to 15:

Here ProductManager waits for the result of its inquiry on a financial product it has issued, coming back as an integer, from Market. While ProductManger is waiting, it is possible that:

1. As in Line 15, Market cannot find any value for the product so raise an interrupt (or other faults which we omit), by which this part of conversation (try-block) is thrown away.
2. As in Line 16, It can take too much time for ProductManger to receive so that it ceases to wait — the conversation is again thrown away.

Note the first situation and the second situation are subtly but importantly different:

1. In the first situation, Market knows this is an escape situation and communicates this to ProductManager so that both parties eventually know that an interrupt has happened.
2. In the second stiuation, it is used only ProductManager who knows it is quitting: Market may send in the end its value or even an interrupt but since there is no remaining interactions it does not matter if Market knows if ProductManager has quit or not (or so we stipulate).

The interrupt declared as local is precisely for the second kind of situation: when only one party escapes and the other is not let know. The runtime surely can have a convention that this is in effect shared but it is not necessary. For monitoring at ProductManager there are two possiblities: it does the reception or it does not and even if it is received it is thrown away. Note that the protocol does not specify a concrete time out value etc.: it simply specifies the basic “type” involved in the concerned conversation.

We illustrate further details of local interrupt in the next Comment.

Comment 8.3.2 (Local Interrupt, 1)  
If the local timeout in the protocol above is to be communicated to Market then it suffices to declare say timeoutFault(void) as an interrupt from ProductManager. The local timeout is only when the protocol finds no need to communicate the existence of its local interrupt. If the other party (or parties) should hear about the escape to have a consistent conversation then a local interrupt causes a problem. In the example above, for example, if Market needs to hear some message from ProductManager to proceed to the next stage then this can cause inconsistency in the next stage of a conversation. For this reason we need to impose the following rule for the use of local interrupt:

In this case ProductManager is only receiving a message so that there is no issue even if it does not receive that message. At ProductManager a local monitor will observe that before receiving the message from Market it moves to the next stage.

The general syntax for a local interrupt is:

This line says that:

One may best consider this corresponds to the familiar “raise” construct in the standard exception handling.

Since this local interrupt is not an observable interaction and moreover such an action may be limited to timeout, there is a doubt if it should be stipulated as part of signature: nevertheless whether it does a local interrupt or not does affect the observation so that the protocol at least should declare there can indeed be a local interrupt or not.

Note that if a try-block consists of many message exchanges (unlike the case above) both parties may as well wish to have timeout exceptions: in this case it is usually necessary that this information is eventually shared so that they both can move to the next stage of the conversation in a well-synchronised manner. In such a case it is not a local timeout but an interrupt which may be described as (say) timeoutFault(void) from Market, ProductManager (standing for the obvious two interrupts). This pattern will be useful in many situations.

Further examples of escape can be found in Section 12.

9 N-Party Choice

We have seen so far several single-party located choices. If we assume underlying protocols can reach an agreement among n-parties, we can generalise this idea to n-party located choices. This is what we shall discuss in this section.

9.1 Example: n-party choice

Here Alice and Bob decide which branch of conversations they should take out of the two options.

Comment 9.1.1 (n-party Choice, 1)  
In Line 4, choice is located in both Alice and Bob. Thus which branch of the conversation is to be chosen should be decided by the collaboration between Alice and Bob. If the first branch is taken, then Bob says hello (Line 5) then Alice says hello (Line 6): if the second branch is taken, then Alice first says hello (Line 8) followed by Bob saying the same (Line 9).

Comment 9.1.2 (n-party Choice, 2: Observability)  
A basic issue in n-ary choice is observability. Taking this example, if these two branches are tried simultaneously, then an observer (consider it as a monitor for checking conformance of interactions to a stipulated agreement) at Alice will observe:

• Alice sending an asynchronous message to Bob
• Alice receiving an asynchronous message from Bob

Similarly when an observer is at Bob’s. This goes against an intuitive meaning of “choice” — only one of the branches should take place.

By locating the choice at both Alice and Bob, the protocol signifies that this choice demands hidden (or implicit) interactions to resolve this issue. Two basic ways this issue can be resolved are:

• Which choice is to be taken is resolved, by hidden exchange of messages, before these two branches are executed: thus an observer only observes, except these hidden exchanges, one of the branches.
• As a refinement to (1), one may also combine the preceding hidden interactions with the initial actions of the two branches. That it, both try to (or are allowed to) send the respective initial messages, and then resolving hidden interactions ensure: once this is resolved, we abort (and rollback for) the discarded branch.
• In (1) we can use agreement on local states: for example if Alice and Bob exchange numbers they have in their local data and if one is bigger than the other then that can be used for a choice. By further combining with (2) we can reach a sophisticated hidden system-level protocol.

In each case, as far as an observer knows about the set-up, she will only observe a consistently scenario. Note that it is co-location at Alice and Bob which allows us to stipulate this is a collaboration between them which decides the choice. An initial action in any branch of the choice should then be done only by one of these mentioned participants.

A further analysis of the observability of the n-ary choice in general is given in the next subsection.

9.2 Note: Plugging In Protocols

One of the key ideas underlying various constructs in scribble is to allow the use of “plug-in” hidden interactions to satisfy:

• Precise monitorability of a conversation: “what you have described should be what you hear”.
• High-level description of interactions in a conversation.

The first principle, (1), says the following natural requirement:

If not, what is the purpose of having a protocol as “signature for a conversation”?

The second principle does not need illustration: we want a conversation structure to be specified cleanly at a high-level of abstraction. As we have suggested so far, however, these two requirements are not always compatible. Concretely we have so far seen such situations in the following constructs:

∙

Repetition/recursion: here a decision as to continue/terminate a loop needs be synchronised among the involved parties but this “system message” is hard to write.

∙

Escape: here a decision as to finishing the try block normally, or taking one of the catch blocks, is again should be synchronised among all parties concerned.

∙

n-party choice: here a decision to take which branch of the choice should again be synchronised by the n parties involved.

In each case, the preceding and ongoing studies in distributed systems and process theory offer a precise system-level protocol ⁸ which resolves the given synchronisation problem. For example, the resolution of a n-party choice can be done by the encoding of a so-called “mixed choice” using asynchronous message passing. Further as we mentioned for the n-party choice in Section 9.1, we can use local data wisely, such as using a counter at each participant to decide the timing of an exit of a loop.

Once a family of system-level protocols to be used for these situations are decided, we obtain exact monitorability under the following assumptions:

1. Usable system-level protocols for a certain situation are validated to be correct and are registered.
2. At the time of establishment (or by some actions during its run), a conversation instance clearly specifies the plugged-in system-level protocol at each point, and messages belonging to systems protocol (we may call them system-level messages) are marked as such at runtime.
3. A monitor is aware of an agreed-upon convention and observes messages accordingly (for example by simply neglecting system-level messages or by transforming the as-is scenario into a revised “real” scenario dynamically).

Note once (a) is done (and we believe having only a handful of efficient protocols is enough), (b) and (c) may not generally incur any visible overhead since no additional mechanism than the standard monitoring is necessary (except the transformation mentioned in (c) which however would only involve a fixed transformation in each construct).

The plug-in architecture we discussed above demands in infrastructural preparation. We believe that the resulting benefit is significantly much more than the efforts needed for such preparation.

10 Continuation Channel and Channel Passing

In this section we discuss how we can use and describe continuation channel passing (a different form of channel passing, which is across conversations, is treated in Section 11). At the end of the section we also discuss how to describe protocols which use an unbounded number of channels.

10.1 Example: Continuation Channel

We can describe a request-reply micro-protocol inside a conversation using a continuation channel.

Comment 10.1.1 (Continuation Channel, 1)  
The interaction statement in Line 7 includes the following phrase:

(In Line 7 it is placed before the from phrase but it can also be placed at the end.) This phrase specifies a continuation channel (also called reply channel): A continuation channel denotes a channel freshly created and passed at the time of sending a message: further this channel can only be used by the receiving participant of this interaction as a sender. Thus Line 7 says:

Line 7 is called the initiating interaction for the continuation channel chContBuyer. ⁹ Similarly Line 8 is the initiating interaction for chContSeller located at Seller.

Comment 10.1.2 (Continuation Channel, 2: Request-Reply)  
Because of the constraint that only its receiver of the initial interaction (for example Seller in the case of chContBuyer above) can use it for sending, a continuation channel can describe a correspondence between interactions, in particular one between a request and a reply. In this sense, one may consider a continuation channel as a “reply-to” field of a mail, which is the origin of the keyword for their declaration. For example chContBuyer is used in Line 10 so that we know Line 10 is a reply to the request in Line 7: note Seller, the sending party of Line 10, is the receiver of Line 7. Similarly we know Line 9 is a reply to the request in Line 8. In this way, continuation channels offer a powerful method to specify precise correspondence between the initiating message and one or more later messages, e.g. between a “request” and its “reply” (or even “replies”). Note also the request in Line 7 and its reply in Line 10 have two intermediate interactions, but their correspondence is still unambiguous. ¹⁰ Specifying a request-reply by a continuation channel has the following merits:

∙

It precisely captures the central meaning of request-reply: the reply can only come as the result of the original request.

∙

The correspondence between a request and its reply is precisely described in a protocol and observable at run-time even when many intermediate interactions occur between them.

∙

It needs no additional mechanism at runtime except what we already have.

∙

Its usage in protocol descriptions is amenable to efficient static checking.

∙

It easily allows generalisations such as multiple replies.

∙

It allows an easy cryptographic extension (use a nonce in combination).

∙

Various feasible notations can be easily mapped to the present abstract syntax.

Regarding the last point, one may consider a graphical interface in which one draws a curved line from a request interaction to a reply interaction (one can use different colours to show different modes). Or one may use a syntactic method, labelling the request interaction as

and marking the reply with this label:

We may as well introduce such a notation as a standard macro to the continuation channels, or a primitive construct whose underlying meaning is given with a corresponding continuation channel.

Comment 10.1.3 (Continuation Channel, 3: Abbreviation)  
In most cases, a continuation channel is located at the sending participant, indicating that the sender of the initial interaction is waiting for a reply. For this reason we have the following abbreviation for Line 7:

(again we can place the replyto-phrase at the end) which automatically means this channel is created at Buyer. The explicit location is however useful when we send out a continuation channel which is not located at the sender. So one may write:

which allows Seller to reply to Broker rather than Buyer.

Comment 10.1.4 (Continuation Channel, 4: Modes (1))  
In the standard request-reply protocol, there can only be at most one reply to a given request. This can be represented by the mode once as follows.

which says that chContBuyer can be used at most once: in other words there is at most one reply to this initiating interaction.

The once mode can also be used with the standard channel declaration (note this is different from unique which says a participant owns only the declared channel). For a continuation channel, we set this mode to be a default: if we do not specify, its mode is automatically set to be once.

Comment 10.1.5 (Continuation Channel, 5: Modes (2))  
As a different mode than once, which may be less frequently used but which may still have a use, one may wish to allow multiple replies to a single request, in which case we can use the repeated mode, as in the phrase:

which is used in an interaction statement as before (with a possible abbreviation of the locating participant). For example, we can refine the interactions in the example above as follows:

in which Seller sends three quotes as the replies to the original request.

Comment 10.1.6 (Continuation Channel, 6: Modes (3))  
Instead of using one continuation channel repeatedly, we can also use multiple continuation channels each of which is used once. For this purpose we introduce the notation for standard multiple channel declaration into an interaction, elaborating the channel with the once mode:

which says that later communications to all these channels (only possible by the receiver of this initiating interaction) are regarded as replies to this initiating interaction; and that each reply channel can be used only once. We can equally use repeated as the mode and further mix multiple modes if one likes.

Using this syntax, we now refine the original interaction sequence in a different way:

in which case all of the three parallel interactions are replies to the original initiating action: further no replies to the original request is now possible.

Comment 10.1.7 (General Channel Passing)  
The continuation channel declaration involves both the creation and the communication of a continuation channel. In the same way, one can also pass the capability of an already existing channel to another party: usually this is done in combination with a continuation channel. For example suppose chCont is a continuation channel which Alice should use for a reply: then she can delegate this capability to Bob as follows.

(void can be a non-trivial message type or operator). This command passes the capability Alice has for chCont to Bob (in this case the sending capability). One seldom passes a receiving capability and this may be considered to be ill-formed depending on application areas. In rare cases when one has both sending and receiving capabilities for a channel and wishes to pass part of the capability one can elaborate delegate with input (for receive) and output (send), as in input delegate.

10.2 Example: Protocol with an Unbounded Number of Channels

For in-depth illustration of the notion of channels and channel declaration, we examine a very simple protocol which, among others, specifies that a conversation may use an unbounded number of channels. Below we have already seen the inner protocol Order in Example 7.1.

Comment 10.2.1 (Channels and Participants)  
When Buyer in Line 5 decides on the first branch of the choice, the sub-protocol Order is run in parallel (Line 6) with the recursion in Line 7 which repeats the whole recursion block starting from Line 4. Thus an unboundedly many conversations are in effect specified. We examine this point in more detail below.

∙

Since participants are not local to (hence, dynamically speaking, are not generated at) each run, we have only Buyer and Seller interacting in the whole conversation, however many times a protocol is spawned.

∙

In contrast, the declaration of channels inside Order in Line 15 has a different meaning (cf. Section 2.2): it specifies that channels should be local to each instance of a conversation (or dynamically speaking are generated fresh at each run). Since the specification does not say how many times the repetition will be done the protocol in effect specifies generation and use of a possibly unbounded number of channels.

A significant point is the nature of channels as entities local to each instance of conversation: this allows a simple and clean description for abstraction as well as making their function easily implementable by rendering a channel as a field in a message. Note that, since in practice we have a bound in the number of repetition in a loop, the above protocol is far from being unpractical: we shall later see essentially the same protocol pattern is used in a real trading protocol.

10.3 Notations for Asynchrony

The recursion expression used in Example 10.2:

shows one of the basic patterns of combining recursion and parallel, where each time a loop is done a new conversation is spawned and, before waiting for its termination, we repeat the loop body (hence spawning) again. Note that this combination is very different from:

which is equivalent to:

each of which waits for the protocol Order to terminate before starting the next loop, which is the only possible semantics if we allow the textual substitution of the run command above with a(n instantiated version of) sub-protocol Order. ¹¹

Because of the significance of this pattern, one may introduce a standard macro notation for a spawning loop as follows:

which uses the notation from Unix’s shell languages for an asynchronous command dispatch. Analogously we may write:

which simply stands for:

In general, for arbitrary statements S1, .., SN,

simply means

On the other hand if we have:

then it stands for:

where aLabel is a fresh label not used inside S.

The significance of such an encoding is that we obtain not only a precise understanding and a meaning of each notation but also we can also carry over all analyses and validation methods for basic constructs for these derived constructs.

11 Dynamic Reconfiguration of Conversation

The description by signature can also include dynamic reconfiguration of conversations: two or more conversations may be merged into one or a conversation may be split into two. The purpose of describing such dynamic restructuring in the framework of signature is to make clear the expected conversation structure at an abstract level, allowing efficient static and dynamic validation of complex interactional models and programs as well as helping effective development of compilers and runtime systems.

11.1 A Scenario of Merging

Suppose we wish to describe an application scenario where:

(A)

There are many Sellers and many Buyers, as well as a Broker.

(B)

Each Seller will first interact with Broker; similarly for each Buyer. Then they will be registered in a database.

(C)

A broker then tries to find pairs who are good matches. If it finds one, it tells each of the pair the channel of the other, so that they can communicate. Then that pair start a conversation.

We can describe this situation with two separate conversations: one for (B), between a Seller/Buyer and a Broker; and the other between a Seller and a Buyer.

If alternatively we wish to describe this situation as a scenario in a unified manner, then we need the following framework:

∙

A conversation in (B) starts independently and separately for each Buyer and each Seller.

∙

Once the match is found between a Seller and a Buyer, we wish their respective conversations to get merged into a conversation in stage (C).

Since we do not know initially which Seller’s conversation will be merged into which Buyer’s conversation, the only way to carry out a merge successfully is for a Seller and a Buyer to share the channel(s) of the other dynamically.

Thus merging means that, operationally, a dynamic sharing of channels between two or more distinct conversations so that, in the resulting conversation, a new pair or new pairs can start interactions. This channel sharing can be done at least in two ways: as part of interaction (i.e. channel passing); and as part of non-interactional IO-operations or a proper operation for merging (which has reflective nature in that they are about combining conversations being done from inside a conversation).

11.2 Example: Merging Conversation (1)

In the following we treat the case where channels are shared through communication.

Comment 11.2.1 (Importing Conversation)  
The interaction statement in Line 10-12 has a new phrase in Line 11:

which states the following:

It is not our interest here how Broker has obtained this information: the only significant point is that Seller (which will participate in a merged conversation) obtains the channel which she is going to use in the merged conversation.

This interaction may be considered to be a substantial point where the merging of a conversation takes place, at least from Seller’s viewpoint. It is at this point that the context of a new conversation is communicated to Seller. How and when the underlying synchronisation is done to establish a conversation is however not the concern to be described in a signature.

In Lines 15 and 16, the protocol of a merged conversation is stared (the protocol BuyerSellerOpen is defined later). This run command uses the shape which is introduced in Comment 7.3.2, Section 7, page §, instantiating both participants and channels. Regarding Line 11 as a declaration of Buyer and chBuyer, all parameters to the run statement have been declared by this point.

We leave BuyerAlone to Appendix A since its structure is precisely symmetric to SellerAlone. We now present the merged conversation BuyerSellerOpen.

Comment 11.2.2 (BuyerSellerOpen)  
BuyerSellerOpen is an open version (cf. Comment 7.3.2, Section 7, page §) of the familiar BuyerSeller protocol from Example 3.1: the only difference from Example 3.1 is that it specifies both channels to be open, so that they can be instantiated by its super-protocol.

Comment 11.2.3 (Merging Scenario)  
Given these protocols including BuyerAlone, the merging at a logical level is performed as follows.

(Stage 1)

An instance of (a conversation conforming to) SellerAlone is started: there may be other instances of this protocol running. Asynchronously the same is happening for BuyerAlone.

(Stage 2)

Broker finds a match, and communicates Buyer’s information to Seller inside SellerAlone; and symmetrically Seller’s information to Buyer inside BuyerAlone.

(Stage 3)

The Buyer and the Seller start interactions in an instance of (a conversation following) BuyerSeller, since they already know each’s communication handle.

The scenario says nothing about how merging is implemented, which in turn allows flexible implementation strategies faithful to its high-level description. For example the merging of two conversations can wait until the first interaction between Buyer and Seller; or it can be done eagerly when both Seller and Buyer issue their desire to have their conversations be merged. Further such issuance itself can be done either eagerly or lazily.

11.3 Example: Merging Conversation (2)

Next we consider the case when the import and export of the merging is stated independently from interactions: this is a static statement but is also directly mappable to a real meta-level operation.

Again BuyerAlone2 is symmetric so is left to Appendix A. The merged protocol BuyerSellerOpen remains the same.

Comment 11.3.1 (merge Statement)  
In Lines 14 and 15, the merging and the associated import and export are stipulated independently from interactions. This statement may be mapped to a merge operation (or a sequence of operations) at the program level: by itself, however, the statement only says that the merging is to be done with an instance of BuyerAlone2, with the specified import and export (strictly speaking, the export phrase is not logically necessary: however it contributes to clarity). Concretely the merge statement in Lines 14/15 reads as:

It assumes the symmetric command in BuyerAlone2:

Note the two statements are precisely dual to each other: by exchanging import and export, located participants and protocol names, one becomes the other.

11.4 Example: Splitting Conversation

Consider a conversation among Buyer1, Buyer2 and Seller is split into two conversations, one between Buyer1 and Seller and another between Buyer2 and Seller.

Comment 11.4.1  
Lines 14-20 give the split statement: it is best considered (and functions) as a parallel with explicitly stating which channels are to be used in each branch. Making the splitting explicit has a merit in that the description is more disciplined in terms of channel usage.

12 A Stock Trading Protocol

12.1 Example: Trade

We treat a fairly large example of protocol descriptions, taking a stock trading protocol (see Section 12.5 later for the illustration of the background of this protocol).

Further illustrating of this protocol as a whole are given given at the end of Section in

We introduce its parts one by one. For ease of reading some of the illustrations are duplicated from the previous sections.

We start from one of the central protocols, in which two participants get engaged in multiple instances of the same conversation.

Comment 12.1.1 (Trade, scenario)  
We first describe the general scenario: in later comments we illustrate the protocol line by line. First DealMaker asks DealTaker for a confirmation of the concerned trade; if it is affirmed then the activity starts, consisting of the following three components done in parallel, based on the content of the concerned trade.

∙

Handling of contracts and issuance of security.

∙

Execution of advertisement.

∙

Enquiries of trade status.

For the first task, there would be repeated parallel instantiations of the sub-protocol HandleContract (defined later) to treat each contract for this deal: after all contracts are handled, DealMaker tells DealTaker of this: and finally DealTaker issues the security. For each of the remaining tasks an appropriate subprotocol is used.

Comment 12.1.2 (Trade, line-by-line, preamble)  
Line 1 imports a document type called TradeDetail either through a binding in an enclosing context or from the default directory or name space, cf. Section 3.5. Line 2 says the name of the protocol is Trade: Line 3 says there are two participants, DealTaker and DealMaker. In Line 4, we only need a single channel at DealTaker declared at this stage: channels for DealMaker are declared incrementally, at the place we need it.

Comment 12.1.3 (Trade, line-by-line, main part)  
In Lines 6 and 7 when confirmation is requested we use a continuation channel discussed in Section 10.

Line 8 is the parallel construct: each block combined with and is run in parallel.

Lines 9-12 uses the repeat construct combined with &, the macro we introduced in Example 10.2 in page §. Line 9 says that to repeat or exit is determined by DealMaker; Lines 10-11 run the sub-protocol HandleContract discussed later (for run command see Section 7). The use of & at the end of Line 11 makes the repetition asynchronous, meaning that there is no sequencing between the termination of the run of the sub-protocol and repetition: in other words the repetition does not wait for the termination of the subprotocol. This will be repeated until each contract in the deal is allocated its handler. As examined in detail in Example 10.2, Lines 9-12 is equivalent to the following recursion:

Line 13 is a communication from DealMakerDealTaker, as a result of which the issue subprotocol is instantiated.

Our description hereafter will focus on the sub-protocol HandleContract rather than the other two.

12.2 Example: HandleContract

This protocol depicts how a protocol is handled, again between DealTaker and DealMaker.

Comment 12.2.1 (Contract Handler)  
Line 2 says it uses two participants DealTaker and DealMaker: these are to be instantiated by its super-protocol.

For a channel, the protocol declares a local channel (of the same name as before but logically distinct) executionCh located at DealTaker (Line 3) and starts from DealMaker reporting to DealTaker it is ready to start the task via executionCh.

Then DealMaker starts two sub-activities in parallel: in one activity, in Lines 7 to 16, DealMaker and DealTaker together decide whether to perform ContractAmendment; ContractNovation with DealTaker as Transferer and DealMaker as Transferor; or ContractNovation with the roles for DealTaker and DealMaker exchanged. Note that by the usage of run statement a participant can obtain the behaviour of two “roles” switched in different choices, so that DealTaker can be either Transferor or Transferee similarly for DealMaker.

In the second component of parallel, which is in Lines 18-19, they carry out Confirmation.

12.3 Example: Quotation (1)

This protocol uses Trade we defined in Example 12.1. It uses the global escape (try-catch) introduced in Section 8 to represent expectation of the unexpected.

Comment 12.3.1 (Quotation, 1)  
Line 1 says the protocol uses Product and Quote as document types. In Line 3 it stipulates the usage of two participants, PriceTaker and PriceMaker. Line 4 says it uses two channels, makerCh located at PriceMaker and takerCh located at PriceTaker.

In Line 6 PriceTaker requests a quote (or quotes) to PriceMaker via channel makerCh. In Line 7 PriceMaker confirms this.

In the rest (Lines 8 to 19) the protocol depicts repetition of an activity and an escape from that repetition. Enclosed in try-catch construct (introduced in Section 8), its try-block is the repetition of the activity where a new quote is sent from PriceMaker to PriceTaker. This continues until the event in the initial part of the catch-block (Line 12) takes place, which is the acceptance of the quote by PriceTaker sent to channel makerCh.

When the acceptance is received, then the conversation escapes from the repetition to the body of the catch-block (Lines 13-18), which is the choice between starting a conversation following the Trade protocol; or reporting to PriceTaker that the quote is already expired.

This protocol has the same “criss-crossing” structure as we found in Example 8.1.

12.4 Example: Quotation (2)

This protocol refines Example 12.3.

Comment 12.4.1 (Quotation, 2)  
There are two differences from Example 12.3:

(1)

The whole try-clause is now under another repetition.

(2)

There are two more catch clauses where PriceTaker can send two additional interrupting messages.

(2-a)

In Line 20, PriceTaker can request to repeat the whole transaction again (for a different product).

(2-a)

In Line 22, PriceTaker can request to abort the whole deal.

Note that it is also possible that PriceMaker sends an interrupt if it uses a different channel or if it uses a different signature (see discussions in Comment 8.1.3, Section 8, page §). However in the above scenario where the repetition consists of a single action from PriceMaker it is hardly needed for PriceMaker to do so.

12.5 Example: QuoteOrExecute

This is the main protocol which uses Quotation and Trade.

Comment 12.5.1 (Quote or Execute)  
In this protocol, Maker either decides whether, in Lines 4-5, it runs a Quotation protocol (or to be precise a conversation instance following that protocol) or, in Lines 7-8, it runs Trade protocol (ditto) using choice in Line 3.

Comment 12.5.2 (Background of Trading Protocols)  
At this point we discuss the business background of the protocols we have introduced in this section. The trading protocols as a whole outline the highlevel interactions that occur between organisations that embark on trading activities. The main activity, depicted in QuoteOrExecute above in this section, can optionally commence with an organisation’s request for quote from a market, or directly proceeding to trade execution, as we have already seen.

If a quote is requested, as depicted in the Quote in Example 12.4, then a number of quotes may be generated and updated before the organisation may decide to accept one. At this stage the protocol proceeds to the trade execution step.

The rest of the conversation is depicted in HandleContract in Section 12.2. Once a trade has been executed (and affirmed - which is just an informal confirmation of the trade details between the trading parties), it may represent a block transaction that has been performed on behalf of a number of clients. Each client is called counterparty. Therefore it will need to be processed to create contracts associated with individual allocations for each counterparty.

Each contract has a lifecycle - they are initially created, and at the end they are ’terminated’ (i.e. sold). However between these two situations the contract may be increased (i.e. more stocks are purchased), partially terminated (also known as decreases, e.g. some of the stock is sold), amendments (i.e. details associated with the contract are modified) and novations (where a contract is transferred from one counterparty to another).

While we have not described in this section, for each of these lifecycle events, it is necessary to perform the confirmation process. This entails the organisation and the counterparty both submitting their understanding of the event to a confirmation service, and when the confirmation service agrees that the details from both organisations match, it informs the bank and counterparty that the event has been confirmed. This confirmation protocol can be described using the Merge construct though we have omitted.

We finish the description of Trade protocols for this version: in a later version we shall be able to present the description of the omitted protocols as well as the discussions on the business background of the protocol.

12.6 Remaining Topics and Further Development

Remaining Topics.  This completes the protocols for Trading and our presentation of examples. In a later version we shall augment our present discussions with full treatment of, among others:

∙

Multicasting channels;

∙

Collective participants; and

∙

Binding to specify an enclosing context for imported document types.

Some of the missing protocols in the trade example may also be augmented and further examples may be treated.

Further Development.  In this first compilation of examples we have only presented descriptions of various example scenarios in the form of signature, not their detailed behaviour. This means our descriptions lack many algorithmic details which one may wish to place:

∙

We did not use any of “if” or “while” or “for” by which we can specify the condition to choose between two choices or to continue or terminate the loop or recursion.

∙

Similarly we did not include the “when” construct which starts an action when a condition becomes true: while we could have considered its abstract version (without its conditional part) this may as well be delegated to models since it does not differ from parallel at the level of interleaving of actions.

∙

We did not use any concrete calculation (which calculates decision, messages etc.).

∙

We did not include concrete message values: we only describe their types. Similarly we did not bind document type names to concrete document types nor did we discuss binding of participant names to real organisational entities.

∙

We did not include any IO-actions such as writing to a database or querying it.

All these concrete descriptions are relegated to languages for models and programs.

The abstract nature of our description in this note is in exact correspondence to that of the class signature in OOPL. Consider a method signature:

It depicts the structure of interaction in objects in as abstractly as possible: it is in fact the minimal structure by whose declarations (and programs’ conformance to them) we can guarantee the type correctness of resulting programs. By this abstract nature it can become a basis of static manipulation of models such as model transformation as well as static and dynamic validation.

In the sequels of this note we shall discuss how we can specify “conversation models” (corresponding to class models) on the basis of these signatures, which can describe more detailed structures as well as behavioural properties. We shall also discuss how we can have “behavioural description” which can now represent full-fledged algorithmic behaviours.

References

A BuyerAlone and BuyerAlone2

B Recovering Method Signature (Reference)

The purpose of this appendix is to show that the current notion of “conversation signature” realised as protocols subsumes that of “method signature”.

We consider two participants named “caller” C and “object” O, as well as their respective channels chC and chO, declaring:

Under this declaration, we can describe a method call as a conversation, as follows:

where the last line uses the type only notation in §3.3. Since C and O are located, we can abbreviate this, cf. §3.2, as follows:

Further since chO and chC are uniquely located channels, we can further combine the abbreviation in Comment 3.4.2 as far as we implicitly assume who are involved participants in each interaction, to obtain:

which is isomorphic to the standard format of a method signature,

thus regaining object signature inside conversation signature. Using the escape we discussed in Section 8 we can easily extend the above encoding to the method signature with exception.

NB: The use of two channels in the translation above can be replaced by a single channel O and a continuation channel if we use the construct introduced in Section 10.