# Thursday, November 24, 2005

Introducing synchronization contracts

In the last year, during my thesis period and later, I have heard a lot of interest from the software research community around contracts. Maybe I'm biased, since my thesis was on contracts, but Don Box claimed more than once that Indigo (now WCF) is based on contracts, and Singularity, the new prototipe of managed OS from Microsoft Research, is based as contracts as well.
In the same period, we also had an increasing interest in concurrency; the most evident sign is the interest raised by Herb Sutter's article "The free lunch is over".

The idea expressed in my thesis is: why do not use contracts to specify concurrency constraints? We can use them to check if a desired temporal behaviour is met, or if an undesiderable sequence of events happens. But we can do even more: we can enforce a desired temporal behaviuor, generating synchronization code from the contract isself.

If you are interested in this technique, let me explain it in some more details: in a contractual aware language, the correctness of a program can be expressed and enforced through contracts. Contracts are assertions on a single method (pre-conditions and post-conditions) or over a whole class (class or object invariants). In their simplest form, those assetions are expressed in boolean logic, but there are various "levels" for contracts:
  • basic or syntactic contracts (for example: XML schemas, IDL);
  • assertion-based contracts (for example: Eiffel);
  • behavioral contracts (assertions are not only on methods or classes, but on the control flow as well);
  • synchronization contracts (like the previous ones, but able to work in a concurrent environment, i.e. to check temporal behaviour);
  • QoS contracts (like the previous ones, but with the possibility to specify also numerical constraints (throughput, mean response time, etc.)).
Therefore a contract aware language is often a dialect of an original programming languages with few additional keywords for expressing assertions.

A compiler for a language supporting concurrent contracts, therefore, will automatically generate checks to see at run-time if a undesiderable sequence of events happens. To express assertions from which the check will be generated we use temporal logics, an extension of boolean logic that adds operators for specifying temporal behaviour.

How it works? We mutuate techinques from formal cheching techniques. The temporal logics we use (LTL -linear temporal logic- and PLTL -LTL with Past-) are mutuated from this field as well.
The life of an object can be seen as an execution trace, i.e. a sequence of traversed states. From its "birth" (construction) to its "death" (finalization and destruction) an object has an internal state, and this state is altered by external events through callings to its method, using the interface it provides.

We can check if a particular assertion holds by examining the sequence of state the object traversed. Moreover, since the satisfaction of a Past LTL formula can be defined in a recursive manner, for those formulas we can do it only looking at the previous execution step.
For LTL formulae, instead, we make use of well-known algorithms to translate every formula in a finite state automaton.

This is for the checking side, but we wished to push it a little further...