The idea of this theoretical work on transactions is to decompose in
the syntax of a small language the properties that are usually
required together in the definition of a transaction, namely
atomicity, isolation and durability. So, in addition to the classical
symbols for parallel composition, sequential composition and
non-deterministic choice, the language contains a special symbol for
each transactional property, as well as a symbol that expresses a
crash/recovery of the system.
Then we define by means of a rewriting system, convergent on ground
terms, a partial order on the terms of the calculus. Informally a term
t1 is smaller than a term t2 if the set of the possible
behaviours of t1 contains the set of the possible behaviours of
t2.
Finally we say that a machine that can execute terms is `an
implementation of transactions' if it treats sequential composition
and non-deterministic choice in the natural way, and is sound with
respect to the informal meaning of the order relation described above.
The main result of this work would be to show that a process designed
to be consistent, i.e. which is a combination of basic bricks that we
know to be consistent, will actually preserve the consistency of the
system, even in presence of crash/recoveries, when executed by a
machine that implements the transactions.
Then the next step will be to better understand the problems addressed
so far and to see if this work could be useful in practice, because it
is not clear yet what it really means.
If so, we would like to add to the language the notion of
communication, which is required for cooperation between transactions,
as well as the notion of replication. Of course to be useful in this
project we will also have to deal with distribution. That is what we
plan to do in the next months.
[Vincent Cremet, Martin Odersky]