Contract-oriented programming

The CO2 middleware currently supports two kinds of contracts:

  • first-order binary session types;
  • timed session types (TST)

In this page we illustrate TSTs with the help of a small case study, an online store which receives orders from customers. The snippets of code illustrated here are in the Java language.

Timed Session Types

Timed session types extend binary session types with clocks and timing constraints, similarly to the way timed automata extend (untimed) finite state automata.

Guards

Guards describe timing constraints, and they are conjunctions of simple guards of the form t d, where t is a clock, d ∈ N, and is a relation in <, <=, =, >=, >. For instance, the guard t<60,u>10 is true whenever the value of clock t is less than 60, and the value of clock u is greater than 10.

Send and receive

A TST describes the behaviour of a single participant A at the end-point of a session. Participants can perform two kinds of actions:

  • a send action !a{g;t1,...,tk}

    stipulates that A will output a message with label a in a time window where the guard g is true. The clocks t1,...,tk will be reset after the output is performed

  • a receive action ?a{g;t1,...,tk}

    stipulates that A will be available to receive a message with label a at any instant within the time window where the guard g is true. The clocks t1,...,tk will be reset after the input is received.

When g = true, the guard can be omitted. For instance, consider the contract store1 between the store and a customer, from the point of view of the store.

store1 = "?order{;t} . !price{t<60}"

The store declares that it will receive an order at any time. After it has been received, the store will send the corresponding price within 60 seconds.

Internal and external choices

TSTs also feature two forms of choice:

  • !a1{g1;R1} + ... + !an{gn;Rn}

    This is an internal choice, stipulating that A will decide at run-time which one of the output actions !ai{gi;Ri} (with 1 i n) to perform, and at which time instant. After the action is performed, all clocks in the set Ri = t1,...,tk are reset.

  • ?a1{g1;R1} & ...& ?an{gn;Rn}

    This is an external choice, stipulating that A will be able to receive any of the inputs !ai{gi;Ri}, in the declared time windows. The actual choice of the action, and of the instant when it is performed, will be made by the participant at the other endpoint of the session. After the action is performed, all clocks in the set Ri = t1,...,tk are reset.

With these ingredients, we can refine the contract of our store as follows:

store2 = " ? order {; t } . (! price {t <60} + ! unavailable {t <10}) "

This version of the contract deals with the case where the store receives an unknown or invalid product code. In this case, the internal choice allows the store to inform the buyer that the requested item is unavailable.

Recursion

The contracts shown so far can only handle a bounded (statically known) number of interactions. We can overcome this limitation by using recursive TSTs. For instance, the contract store3 below models a store which handles an arbitrary number of orders from a buyer:

store3 = "REC 'x' [?addtocart{t<60;t}.'x' \
             & ?checkout{t<60;t}.( \
                   !price{t<20;t}.( \
                       ?accept{t<10} & ?reject{t<10}) \
                 + !unavailable{t<20})]"

The contract store3 allows buyers to add some item to the cart, or checkout. When a buyer chooses addtocart, the store must allow him to add more items: this is done recursively. After a checkout, the store must send the overall price, or inform the buyer that the requested items are unavailable. If the store sends a price, it must expect a response from the buyer, who can either accept or reject the price.

Online Tool

Try our online tool: http://co2.unica.it/tst/.

PDF Documentation: http://co2.unica.it/tst/syntax_tutorial.pdf.

Context

Action labels are grouped into contexts, which can be created and made public through the middleware APIs. Each context defines the labels related to an application domain, and it associates each label with a type and a verification link. The type (e.g., int, string) is that of the messages exchanged with that label. The verification link is used by the runtime monitor (described later) to delegate the verification of messages to a trusted third party. For instance, the middleware supports Paypal as a verification link for online payments.

Compliance

Besides being used to specify the interaction protocols between pairs of ser- vices, TSTs feature the following primitives:

  • a decidable notion of compliance between two TSTs;
  • a decidable procedure to detect if a TST admits a compliant one;
  • a computable canonical compliant construction.

These primitives are exploited by the CO2 middleware to establish sessions between services: more specifically, the middleware only allows interactions between services with compliant contracts. Intuitively, compliance guarantees that, if all services respect all their contracts, then the overall distributed application (obtained by composing the services) will not deadlock. Below we illustrate the primitives of TSTs by examples.

Informally, two TSTs are compliant if, in the interactions where both participants respect their contract, the deadlock state is not reachable. For instance, recall the simple version of the store contract:

store1 = "?order{;t} . !price{t<60}"

and consider the following buyer contracts:

buyer1 = "!order {;u} . ?price{u<70}"
buyer2 = "!order {;u} . (?price{u<70} & ?unavailable)"
buyer3 = "!order {;u} . (?price{u<30} & ?unavailable)"
buyer4 = "!order {u<20} . ?price{u<70}"

We have that:

  • store1 and buyer1 are compliant:

    indeed, the time frame where buyer1 is available to receive price is larger than the one where the store can send;

  • store1 and buyer2 are compliant:

    although the action ?unavailable enables a further interaction, this is never chosen by the store store1.

  • store1 and buyer3 are not compliant,

    because the store may choose to send price 60 seconds after he got the order, while buyer2 is only able to receive within 30 seconds.

  • store1 and buyer4 are not compliant.

    Here the reason is more subtle: assume that the buyer sends the order at time 19: at that point, the store receives the order and resets the clock t; after that, the store has other 60 seconds to send price. Now, assume that the store chooses to send price after 59 seconds (which fits within the declared time window of 60 seconds). The total elapsed time is 19+59=78 seconds, but the buyer is only able to receive before 70 seconds.

Compliance can be checked using the middleware Java APIs. We show how to do this through the Groovy interactive shell (see Installation and Download).

You can check the compliance as follows:

cS1 = new TST(store1)
===> ?order{;t}.(!price{t<60})

cS1.isCompliantWith(new TST(buyer1))
===> true

cS1.isCompliantWith(new TST(buyer3))
===> false

Consider now the second version of the store contract:

store2 = "?order{;t} . (!price{t<60} + !unavailable{t<10})"

The contract store2 is compliant with the buyer contract buyer2 discussed before, while it is not compliant with:

buyer5 = "!order{;u} . (?price{u<90})"
buyer6 = "!order{;u} . (?price{u<90} + ?unavailable{u>5,u<12})"

The problem with buyer5 is that the buyer is only accepting a message labelled price, while store2 can also choose to send unavailable. Although this option is present in buyer6, the latter contract is not compliant with store2 as well. In this case the reason is that the time window for receiving unavailable does not include that for sending it (recall that the sender can choose any instant satisfying the guard in its output action).

Duality

To illustrate some less obvious aspects of compliance, consider the following buyer contract:

buyer7 = "!order{u<100} . ?price{u<70}"

This contract stipulates that the buyer can wait up to 100 seconds for sending an order, and then she can wait until 60 seconds (from the start of the session), to receive the price from the store.

Now, assume that some store contract is compliant with buyer7. Then, the store must be able to receive the order at least until time 100. If the buyer chooses to send the order at time 90 (which is allowed by contract buyer7), then the store would never be able to send price before time 70. Therefore, no contract can be compliant with buyer7.

The issue highlighted by the previous example must be dealt with care: if one publishes a service whose contract does not admit a compliant one, then the middleware will never connect that service with others. To check whether a contract admits a compliant, we can query the middleware APIs:

cB7 = new TST(buyer7)
===> !order{u<100} . ?price{u<70}

cB7.hasCompliant()
===> false

Recall from Introduction that the CO2 middleware also allows a service to accept another service’s contract, as per item (5). For instance, assume that the store has advertised the contract store2 above. When the buyer uses the primitive accept, the middleware associates the buyer with the canonical compliant of store2, constructed through the method dualOf, e.g.:

cS2 = new TST(store2)
===> ?order{;t} . (!price{t<60} + !unavailable{t<10})

cB2 = cS2.dualOf()
===> !order{;t} . (?price{t<60} & ?unavailable{t<10})

Intuitively, if a TST admits a compliant one, then its canonical compliant is constructed as follows:

  1. output labels !a are translated into input labels ?a, and vice versa;
  2. internal choices are translated into external choices, and vice versa;
  3. prefixes and recursive calls are preserved;
  4. guards are suitably adjusted in order to ensure compliance.

Consider now the following contract of a store which receives an order and a coupon, and then sends a discounted price to the buyer:

store4 = "?order{t<60} . ?coupon{t<30;t} . !price{t<60}"

In this case store4 admits a compliant one, but this cannot be obtained by simply swapping input/output actions and internal/external choices.

cS4 = new TST(store4)
cB4 = new TST("!order{t<60} . !coupon{t<30;t} . ?price{t<60})")
cS4.isCompliantWith(cB4)
===> false

Indeed, the canonical compliant construction gives:

cB5 = cS4.dualOf()
===> !order{t<30} . ?coupon{t<30;t} . ?price{t<60}

Run-time monitoring of contracts

In order to detect (and sanction) contract violations, the CO2 middleware monitors all the interactions that happen through sessions. Here we illustrate how runtime monitoring works, by making a store and a buyer interact.

To this purpose, we split the paper in two columns: in the left column we show the store behaviour, while in the right column we show the buyer. We assume that both participants call the middleware APIs through the Groovy shell, as shown before. Note that the interaction between the two participants is asynchronous: when needed, we will highlight the points where one of the participants performs a time delay.

Both participants start by creating a connection waitForReceive with the middleware:

usr = "testuser1@gmail.com"
pwd = "testuser1"
co2 = new CO2ServerConnection(usr,pwd)
usr = "testuser2@gmail.com"
pwd = "testuser2"
co2 = new CO2ServerConnection(usr,pwd)

Then, the participants create their contracts, and advertise them to the middleware through the primitive tell. The variables pS and pB are the handles to the published contracts.

cS = new TST(store2)
pS = cS.toPrivate(co2).tell()
cB = new TST(buyer2)
pB = cB.toPrivate(co2).tell()

Now the middleware has two compliant contracts in its collection, hence it can establish a session between the store and the buyer. To obtain a handle to the session, both participants use the blocking primitive waitForSession:

sS = pS.waitForSession()
sB = pB.waitForSession()

At this point, participants can query the session to see who is “on duty” (namely, one is on duty if the contract prescribes her to perform the next action), and to check if they have violated the contract:

sS.amIOnDuty()
===> false
sS.amICulpable()
===> false
sB.amIOnDuty()
===> true
sB.amICulpable()
===> false

Note that the first action must be performed by the buyer, who must send the order. This is accomplished by using the send primitive. Dually, the store waits to receive the message, using the waitForReceive primitive:

msg = sS.waitForReceive()
msg.getStringValue()
===> 0123
sS.amIOnDuty()
===> true
// send at an arbitrary time}
sB.send("order", "0123")

sB.amIOnDuty()
===> false

Since there are no time constraints on sending order, this action can be successfully performed at any time; once this is done, the texttt{waitForReceive} unlocks the store. The store is now on duty, and it must send price within 60 seconds, or unavailable within 10 seconds. Now, assume that the store tries to send unavailable after the deadline:

// wait more than 10 seconds

sS.send("unavailable")
===> ContractException
msg = sB.waitForReceive()

===> ContractViolationException:
    "The other participant is culpable"

On the store side, the send throws a ContractException; on the buyer side, the waitForReceive throws an exception which reports the violation of the store. At this point, if the two participants check the state of the session, they find that none of them is still on duty, and that the store is culpable:

session.amIOnDuty()
===> false
session.amICulpable()
===> true
session.amIOnDuty()
===> false
session.amICulpable()
===> false