Specifying Transaction Control to Serialize Concurrent Program Executions

TL;DR

This paper introduces a language-independent transaction controller and operator that transform concurrent program executions into serializable transactions, ensuring correctness and broad applicability through formal specifications in Abstract State Machines.

Contribution

It defines a formal transaction controller and operator applicable to various programs, guaranteeing serializability and correctness in concurrent executions.

Findings

Proves that concurrent runs under the transaction controller are serializable.

Provides a formal specification of the transaction controller and operator.

Applicable as a plug-in for specifying concurrent system components.

Abstract

We define a programming language independent transaction controller and an operator which when applied to concurrent programs with shared locations turns their behavior with respect to some abstract termination criterion into a transactional behavior. We prove the correctness property that concurrent runs under the transaction controller are serialisable. We specify the transaction controller TaCtl and the operator TA in terms of Abstract State Machines. This makes TaCtl applicable to a wide range of programs and in particular provides the possibility to use it as a plug-in when specifying concurrent system components in terms of Abstract State Machines.

Equations

$${\Delta }_i=\bigcup _{M\in \mathcal{M}}{\Delta }_i(M)\cup {\Delta }_i(\text{sc}TaCtl).$$

$${\Delta }_i^{\prime \prime }=\bigcup _{M\in \mathcal{M}-\{M_1\}}{\Delta }_i(M)\cup \{(\ell ,v)\in {\Delta }_i(\text{sc}TaCtl)\mid (\ell ,v)\text{does not concern M1}\}.$$

Full text

1 Introduction

This paper is about the use of transactions as a common means to control concurrent access of programs to shared locations and to avoid that values stored at these locations are changed almost randomly. A transaction controller interacts with concurrently running programs (read: sequential components of an asynchronous system) to control whether access to a shared location can be granted or not, thus ensuring a certain form of consistency for these locations. A commonly accepted consistency criterion is that the joint behavior of all transactions (read: programs running under transactional control) with respect to the shared locations is equivalent to a serial execution of those programs. Serialisability guarantees that each transaction can be specified independently from the transaction controller, as if it had exclusive access to the shared locations.

It is expensive and cumbersome to specify transactional behavior and prove its correctness again and again for components of the great number of concurrent systems. Our goal is to define once and for all an abstract (i.e. programming language independent) transaction controller TaCtl which can simply be “plugged in” to turn the behavior of concurrent programs (read: components $M$ of any given asynchronous system $\cal M$) into a transactional one. This involves to also define an operator $TA(M,\hbox{\sc TaCtl})$ which forces the programs $M$ to listen to the controller TaCtl when trying to access shared locations.

For the sake of generality we define the operator and the controller in terms of Abstract State Machines (ASMs) which can be read and understood as pseudo-code so that TaCtl and the operator $TA$ can be applied to code written in any programming language (to be precise: whose programs come with a notion of single step, the level where our controller imposes shared memory access constraints to guarantee transactional code behavior). On the other side, the precise semantics underlying ASMs (for which we refer the reader to [5]) allows us to mathematically prove the correctness of our controller and operator.

We concentrate here on transaction controllers that employ locking strategies such as the common two-phase locking protocol (2PL). That is, each transaction first has to acquire a (read- or write-) lock for a shared location, before the access is granted. Locks are released after the transaction has successfully committed and no more access to the shared locations is necessary. There are of course other approaches to transaction handling, see e.g. [6, 14, 15, 17] and the extensive literature there covering classical transaction control for flat transactions, timestamp-based, optimistic and hybrid transaction control protocols, as well as non-flat transaction models such as sagas and multi-level transactions.

We define TaCtl and the operator $TA$ in Sect. 2 and the TaCtl components in Sect. 3. In Sect. 4 we prove the correctness of these definitions.

2 The Transaction Operator $TA(M,\hbox{\sc TaCtl}$)

As explained above, a transaction controller performs the lock handling, the deadlock detection and handling, the recovery mechanism (for partial recovery) and the commit of single machines. Thus we define it as consisting of four components specified in Sect. 3.

• $\hbox{\sc TaCtl}={}$

LockHandler

DeadlockHandler

Recovery

Commit

The operator $TA(M,\hbox{\sc TaCtl})$ transforms the components $M$ of any concurrent system (asynchronous ASM) ${\cal M}=(M_{i})_{i\in I}$ into components of a concurrent system $TA({\cal M},\hbox{\sc TaCtl})$ where each $TA(M_{i},\hbox{\sc TaCtl})$ runs as transaction under the control of TaCtl:

• $TA({\cal M},\hbox{\sc TaCtl})=((TA(M_{i},\hbox{\sc TaCtl}))_{i\in I},\hbox{\sc TaCtl})$

TaCtl keeps a dynamic set $TransAct$ of those machines $M$ whose runs it currently has to supervise to perform in a transactional manner until $M$ has $Terminated$ its transactional behavior (so that it can Commit it).111In this paper we deliberately keep the termination criterion abstract so that it can be refined in different ways for different transaction instances. To turn the behavior of a machine $M$ into a transactional one, first of all $M$ has to register itself with the controller TaCtl, read: to be inserted into the set of currently to be handled $TransAct$ions. To Undo as part of a recovery some steps $M$ made already during the given transactional run segment of $M$, a last-in first-out queue $history(M)$ is needed which keeps track of the states the transactional run goes through; when $M$ enters the set $TransAct$ the $history(M)$ has to be initialized (to the empty queue).

The crucial transactional feature is that each non private (i.e. shared or monitored or output) location $l$ a machine $M$ needs to read or write for performing a step has to be $LockedBy(M)$ for this purpose; $M$ tries to obtain such locks by calling the LockHandler. In case no $newLocks$ are needed by $M$ in its $currState$ or the needed $newLocks$ can be $Granted$ by the LockHandler, $M$ performs its next step; in addition, for a possible future recovery, the machine has to Record in its $history(M)$ the current values of those locations which are (possibly over-) written by this $M$-step together with the obtained $newLocks$. Then $M$ continues its transactional behavior until it is $Terminated$. In case the needed $newLocks$ are $Refused$, namely because another machine $N$ in $TransAct$ for some needed $l$ has $W\mbox{-}Locked(l,N)$ or (in case $M$ wants a W-(rite)Lock) has $R\mbox{-}Locked(l,N)$, $M$ has to $Wait$ for $N$; in fact it continues its transactional behavior by calling again the LockHandler for the needed $newLocks$—until the needed locked locations are unlocked when $N$’s transactional behavior is Commited, whereafter a new request for these locks this time may be $Granted$ to $M$.222As suggested by a reviewer, a refinement (in fact a desirable optimization) consists in replacing such a waiting cycle by suspending $M$ until the needed locks are released. Such a refinement can be obtained in various ways, a simple one consisting in letting $M$ simply stay in $waitForLocks$ until the $newLocks$ $CanBeGranted$ and refining LockHandler to only choose pairs $(M,L)\in LockRequest$ where it can $\hbox{\sc GrantRequestedLocks}(M,L)$ and doing nothing otherwise (i.e. defining $\hbox{\sc RefuseRequestedLocks}(M,L)=\;\mathrel{\mathbf{skip}}$). See Sect. 3.

As a consequence deadlocks may occur, namely when a cycle occurs in the transitive closure $Wait^{*}$ of the $Wait$ relation. To resolve such deadlocks the DeadlockHandler component of TaCtl chooses some machines as $Victim$s for a recovery.333To simplify the serializability proof in Sect.3 and without loss of generality we define a reaction of machines $M$ to their victimization only when they are in $ctl\_state(M)=\;$TA-$ctl$ (not in $ctl\_state(M)=waitForLocks$). This is to guarantee that no locks are $Granted$ to a machine as long as it does $waitForRecovery$. After a victimized machine $M$ is $Recovered$ by the Recovery component of TaCtl, so that $M$ can exit its $waitForRecovery$ state, it continues its transactional behavior.

This explains the following definition of $TA(M,\hbox{\sc TaCtl})$ as a control state ASM, i.e. an ASM with a top level Finite State Machine control structure. We formulate it by the flowchart diagram of Fig. 1, which has a precise control state ASM semantics (see the definition in [5, Ch.2.2.6]). The components for the recovery feature are highlighted in the flowchart by a colouring that differs from that of the other components. The macros which appear in Fig. 1 and the components of TaCtl are defined below.

The predicate $NewLocksNeededBy(M)$ holds if in the current state of $M$ at least one of two cases happens:444See [5, Ch.2.2.3] for the classification of locations and functions. either $M$ to perform its step in this state reads some shared or monitored location which is not yet $LockedBy(M)$ or $M$ writes some shared or output location which is not yet $LockedBy(M)$ for writing. A location can be $LockedBy(M)$ for reading ($R\mbox{-}Locked(l,M)$) or for writing ($W\mbox{-}Locked(l,M)$). Formally:

• $NewLocksNeededBy(M)={}$

$newLocks(M,currState(M))\not=(\emptyset,\emptyset){}$555 For layout reasons we omit in Fig.1 the arguments of the functions $newLocks$ and $overWrittenVal$.

$newLocks(M,currState(M))=(R\mbox{-}Loc,W\mbox{-}Loc){}$666By the second argument $currState(M)$ of $newLocks$ (and below of $overWrittenVal$) we indicate that this function of $M$ is a dynamic function which is evaluated in each state of $M$, namely by computing in this state the sets $ReadLoc(M)$ and $WriteLoc(M)$; see Sect. 4 for the detailed definition.

$\mathrel{\mathbf{where}}{}$

$R\mbox{-}Loc=ReadLoc(M,currState(M))\cap(SharedLoc(M)\cup MonitoredLoc(M)){}$

$\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\cap\overline{LockedBy(M)}{}$777By $\overline{X}$ we denote the complement of $X$.

$W\mbox{-}Loc=WriteLoc(M,currState(M))\cap(SharedLoc(M)\cup OutputLoc(M)){}$

$\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\cap\overline{W\mbox{-}LockedBy(M)}{}$

$LockedBy(M)=\{l\mid R\mbox{-}Locked(l,M)\mathrel{\mathbf{or}}W\mbox{-}Locked(l,M)\}{}$

$W\mbox{-}LockedBy(M)=\{l\mid W\mbox{-}Locked(l,M)\}$

The $overWrittenVal$ues are the $currState(M)$-values (retrieved by the $eval$-function) of those shared or output locations $(f,args)$ which are written by $M$ in its $currState(M)$. To Record the set of these values together with the obtained $newLocks$ means to append the pair of these two sets to the $history$ queue of $M$ from where upon recovery the values and the locks can be retrieved.

• $overWrittenVal(M,currState(M))=\;\{((f,args),val)\mid{}$

$(f,args)\in WriteLoc(M,currState(M))\cap(SharedLoc(M)\cup OutputLoc(M)){}$

$\mathrel{\mathbf{and}}val=eval(f(args),currState(M))\}{}$

$\hbox{\sc Record}(valSet,lockSet,M)=\;\hbox{\sc Append}((valSet,lockSet),history(M))$

To CallLockHandler for the $newLocks$ requested by $M$ in its $currState(M)$ means to $\hbox{\sc Insert}(M,newLocks)$ into the LockHandler’s set of to be handled $LockRequest$s. Similarly we let CallCommit(M) stand for insertion of $M$ into a set $CommitRequest$ of the Commit component.

• $\hbox{\sc CallLockHandler}(M,L)=\;\hbox{\sc Insert}((M,L),LockRequest){}$

$\hbox{\sc CallCommit}(M)=\;\hbox{\sc Insert}(M,CommitRequest)$

3 The Transaction Controller Components

A CallCommit(M) by machine $M$ enables the Commit component. Using the $\mathrel{\mathbf{choose}}$ operator we leave the order in which the $CommitRequest$s are handled refinable by different instantiations of TaCtl.

Commiting $M$ means to Unlock all locations $l$ that are $LockedBy(M)$. Note that each lock obtained by $M$ remains with $M$ until the end of $M$’s transactional behavior. Since $M$ performs a CallCommit(M) when it has $Terminated$ its transactional computation, nothing more has to be done to Commit $M$ besides deleting $M$ from the sets of $CommitRequest$s and still to be handled $TransAct$ions.888We omit clearing the $history(M)$ queue since it is initialized when $M$ is inserted into $TransAct(\hbox{\sc TaCtl})$.

Note that the locations $R\mbox{-}Locked(l,M)$ and $W\mbox{-}Locked(l,M)$ are shared by the Commit, LockHandler and Recovery components, but these components never have the same $M$ simultaneously in their request resp. $Victim$ set since when machine $M$ has performed a CallCommit(M), it has $Terminated$ its transactional computation and does not participate any more in any $(M,L)\in LockRequest$ or $Victim$ization.

• $\hbox{\sc Commit}={}$

$\mathrel{\mathbf{if}}CommitRequest\not=\emptyset\mathrel{\mathbf{then}}{}$

$\mathrel{\mathbf{choose}}M\in CommitRequest\;\hbox{\sc Commit}(M){}$

$\mathrel{\mathbf{where}}{}$

$\hbox{\sc Commit}(M)={}$

$\mathrel{\mathbf{forall}}l\in LockedBy(M)\;\;\hbox{\sc Unlock}(l,M){}$

$\hbox{\sc Delete}(M,CommitRequest){}$

$\hbox{\sc Delete}(M,TransAct){}$

$\hbox{\sc Unlock}(l,M)={}$

$\mathrel{\mathbf{if}}R\mbox{-}Locked(l,M)\mathrel{\mathbf{then}}R\mbox{-}Locked(l,M):=false{}$

$\mathrel{\mathbf{if}}W\mbox{-}Locked(l,M)\mathrel{\mathbf{then}}W\mbox{-}Locked(l,M):=false$

As for Commit also for the LockHandler we use the $\mathrel{\mathbf{choose}}$ operator to leave the order in which the $LockRequest$s are handled refinable by different instantiations of TaCtl.

The strategy we adopt for lock handling is to refuse all locks for locations requested by $M$ if at least one of the following two cases happens:

• some of the requested locations is $W\mbox{-}Locked$ by another transactional machine $N\in TransAct$,
• some of the requested locations is a $WriteLoc$ation that is $R\mbox{-}Locked$ by another transactional machine $N\in TransAct$.

This definition implies that multiple transactions may simultaneoulsy have a $R\mbox{-}Lock$ on some location. It is specified below by the predicate $CannotBeGranted$.

To RefuseRequestedLocks it suffices to set the communication interface $Refused$ of $TA(M,\hbox{\sc TaCtl})$; this makes $M$ $Wait$ for each location $l$ that is $W\mbox{-}Locked(l,N)$ and for each $WriteLoc$ation that is $R\mbox{-}Locked(l,N)$ by some other transactional component machine $N\in TransAct$.

• $\hbox{\sc LockHandler}={}$

$\mathrel{\mathbf{if}}LockRequest\not=\emptyset\mathrel{\mathbf{then}}{}$

$\mathrel{\mathbf{choose}}(M,L)\in LockRequest{}$

$\hbox{\sc HandleLockRequest}(M,L){}$

$\mathrel{\mathbf{where}}{}$

$\hbox{\sc HandleLockRequest}(M,L)={}$

$\mathrel{\mathbf{if}}CannotBeGranted(M,L){}$

$\mathrel{\mathbf{then}}\;\hbox{\sc RefuseRequestedLocks}(M,L){}$

$\mathrel{\mathbf{else}}\;\hbox{\sc GrantRequestedLocks}(M,L){}$

$\hbox{\sc Delete}((M,L),LockRequest){}$

$CannotBeGranted(M,L)={}$

$\mathrel{\mathbf{let}}L=(R\mbox{-}Loc,W\mbox{-}Loc),Loc=R\mbox{-}Loc\cup W\mbox{-}Loc{}$

$\mathrel{\mathbf{forsome}}l\in Loc\;\;\mathrel{\mathbf{forsome}}N\in TransAct\setminus\{M\}{}$

$W\mbox{-}Locked(l,N)\mathrel{\mathbf{or}}{}$

$(l\in W\mbox{-}Loc\mathrel{\mathbf{and}}R\mbox{-}Locked(l,N)){}$

$\hbox{\sc RefuseRequestedLocks}(M,L)=(Refused(M,L):=true){}$

$\hbox{\sc GrantRequestedLocks}(M,L)={}$

$\mathrel{\mathbf{let}}L=(R\mbox{-}Loc,W\mbox{-}Loc){}$

$\mathrel{\mathbf{forall}}l\in R\mbox{-}Loc\;\;(R\mbox{-}Locked(l,M):=true){}$

$\mathrel{\mathbf{forall}}l\in W\mbox{-}Loc\;\;(W\mbox{-}Locked(l,M):=true){}$

$Granted(M,L):=true$

A $Deadlock$ originates if two machines are in a $Wait$ cycle, otherwise stated if for some (not yet $Victim$ized) machine $M$ the pair $(M,M)$ is in the transitive (not reflexive) closure $Wait^{*}$ of $Wait$. In this case the DeadlockHandler selects for recovery a (typically minimal) subset of $Deadlocked$ transactions $toResolve$—they are $Victim$ized to $waitForRecovery$, in which mode (control state) they are backtracked until they become $Recovered$. The selection criteria are intrinsically specific for particular transaction controllers, driving a usually rather complex selection algorithm in terms of number of conflict partners, priorities, waiting time, etc. In this paper we leave their specification for TaCtl abstract (read: refinable in different directions) by using the $\mathrel{\mathbf{choose}}$ operator.

• $\hbox{\sc DeadlockHandler}={}$

$\mathrel{\mathbf{if}}Deadlocked\cap\overline{Victim}\not=\emptyset\mathrel{\mathbf{then}}\mbox{ // there is a Wait cycle}{}$

$\mathrel{\mathbf{choose}}toResolve\subseteq Deadlocked\cap\overline{Victim}{}$

$\mathrel{\mathbf{forall}}M\in toResolve\;Victim(M):=true{}$

$\mathrel{\mathbf{where}}{}$

$Deadlocked=\{M\mid(M,M)\in M^{*}\}{}$

$M^{*}=\mbox{ TransitiveClosure}(Wait){}$

$Wait(M,N)=\;\mathrel{\mathbf{forsome}}l\;Wait(M,l,N){}$

$Wait(M,l,N)={}$

$l\in newLocks(M,currState(M))\mathrel{\mathbf{and}}N\in TransAct\setminus\{M\}\mathrel{\mathbf{and}}{}$

$W\mbox{-}Locked(l,N)\mathrel{\mathbf{or}}(l\in W\mbox{-}Loc\mathrel{\mathbf{and}}R\mbox{-}Locked(l,N)){}$

$\mathrel{\mathbf{where}}newLocks(M,currState(M))=(R\mbox{-}Loc,W\mbox{-}Loc){}$

Also for the Recovery component we use the $\mathrel{\mathbf{choose}}$ operator to leave the order in which the $Victim$s are chosen for recovery refinable by different instantiations of TaCtl. To be $Recovered$ a machine $M$ is backtracked by $\hbox{\sc Undo}(M)$ steps until $M$ is not $Deadlocked$ any more, in which case it is deleted from the set of $Victim$s, so that be definition it is $Recovered$. This happens at the latest when $history(M)$ has become empty.

• $\hbox{\sc Recovery}={}$

$\mathrel{\mathbf{if}}Victim\not=\emptyset\mathrel{\mathbf{then}}{}$

$\mathrel{\mathbf{choose}}M\in Victim\;\hbox{\sc TryToRecover}(M){}$

$\mathrel{\mathbf{where}}{}$

$\hbox{\sc TryToRecover}(M)={}$

$\mathrel{\mathbf{if}}M\not\in Deadlocked\mathrel{\mathbf{then}}Victim(M):=false{}$

$\mathrel{\mathbf{else}}\;\hbox{\sc Undo}(M){}$

$Recovered={}$

$\{M\mid ctl\mbox{-}state(M)=waitForRecovery\mathrel{\mathbf{and}}M\not\in Victim\}{}$

$\hbox{\sc Undo}(M)={}$

$\mathrel{\mathbf{let}}(ValSet,LockSet)=youngest(history(M)){}$

$\hbox{\sc Restore}(ValSet){}$

$\hbox{\sc Release}(LockSet){}$

$\hbox{\sc Delete}((ValSet,LockSet),history(M)){}$

$\mathrel{\mathbf{where}}{}$

$\hbox{\sc Restore}(V)={}$

$\mathrel{\mathbf{forall}}((f,args),v)\in V\;f(args):=v{}$

$\hbox{\sc Release}(L)={}$

$\mathrel{\mathbf{let}}L=(R\mbox{-}Loc,W\mbox{-}Loc){}$

$\mathrel{\mathbf{forall}}l\in Loc=R\mbox{-}Loc\cup W\mbox{-}Loc\;\hbox{\sc Unlock}(l,M)$

Note that in our description of the DeadlockHandler and the (partial) Recovery we deliberately left the strategy for victim seclection and Undo abstract leaving fairness considerations to be discussed elsewhere. It is clear that if always the same victim is selected for partial recovery, the same deadlocks may be created again and again. However, it is well known that fairness can be achieved by choosing an appropriate victim selection strategy.

4 Correctness Theorem

In this section we show the desired correctness property: if all monitored or shared locations of any $M_{i}$ are output or controlled locations of some other $M_{j}$ and all output locations of any $M_{i}$ are monitored or shared locations of some other $M_{j}$ (closed system assumption)999This assumption means that the environment is assumed to be one of the component machines., each run of $TA({\cal M},\hbox{\sc TaCtl})$ is equivalent to a serialization of the terminating $M_{i}$-runs, namely the $M_{i_{1}}$-run followed by the $M_{i_{2}}$-run etc., where $M_{i_{j}}$ is the $j$-th machine of $\cal M$ which performs a commit in the $TA({\cal M},\hbox{\sc TaCtl})$ run. To simplify the exposition (i.e. the formulation of statement and proof of the theorem) we only consider machine steps which take place under the transaction control, in other words we abstract from any step $M_{i}$ makes before being Inserted into or after being Deleted from the set $TransAct$ of machines which currently run under the control of TaCtl.

First of all we have to make precise what a serial multi-agent ASM run is and what equivalence of $TA({\cal M},\hbox{\sc TaCtl})$ runs means in the general multi-agent ASM framework.

4.0.1 Definition of run equivalence.

Let $S_{0},S_{1},S_{2},\dots$ be a (finite or infinite) run of the system $TA({\cal M},\hbox{\sc TaCtl})$. In general we may assume that TaCtl runs forever, whereas each machine $M\in\mathcal{M}$ running as transaction will be terminated at some time – at least after commit $M$ will only change values of non-shared and non-output locations101010It is possible that one ASM $M$ enters several times as a transaction controlled by TaCtl. However, in this case each of these registrations will be counted as a separate transaction, i.e. as different ASMs in $\mathcal{M}$.. For $i=0,1,2,\dots$ let $\Delta_{i}$ denote the unique, consistent update set defining the transition from $S_{i}$ to $S_{i+1}$. By definition of $TA({\cal M},\hbox{\sc TaCtl})$ the update set is the union of the update sets of the agents executing $M\in\mathcal{M}$ resp. TaCtl:

[TABLE]

$\Delta_{i}(M)$ contains the updates defined by the ASM $TA(M,\hbox{\sc TaCtl})$ in state $S_{i}$111111We use the shorthand notation $\Delta_{i}(M)$ to denote $\Delta_{i}(TA(M,\hbox{\sc TaCtl}))$; in other words we speak about steps and updates of $M$ also when they really are done by $TA(M,\hbox{\sc TaCtl})$. Mainly this is about transitions between the control states, namely TA-$ctl$, $waitForLocks$, $waitForRecovery$ (see Fig.1), which are performed during the run of $M$ under the control of the transaction controller TaCtl. When we want to name an original update of $M$ (not one of the updates of $ctl\_state(M)$ or of the Record component) we call it a proper $M$-update. and $\Delta_{i}(\hbox{\sc TaCtl})$ contains the updates by the transaction controller in this state. The sequence of update sets $\Delta_{0}(M)$, $\Delta_{1}(M)$, $\Delta_{2}(M)$, …will be called the schedule of $M$ (for the given transactional run).

To generalise for transactional ASM runs the equivalence of transaction schedules known from database systems [6, p.621ff.] we now define two cleansing operations for ASM schedules. By the first one (i) we eliminate all (in particular unsuccessful-lock-request) computation segments which are without proper $M$-updates; by the second one (ii) we eliminate all $M$-steps which are related to a later $\hbox{\sc Undo}(M)$ step by the Recovery component:

1. (i)

Delete from the schedule of $M$ each $\Delta_{i}(M)$ where one of the following two properties holds:

• $\Delta_{i}(M)=\emptyset$ ($M$ contributes no update to $S_{i}$),
• $\Delta_{i}(M)$ belongs to a step of an $M$-computation segment where $M$ in its $ctl\_state(M)=$ TA-$ctl$ does $\hbox{\sc CallLockHandler}(M,newLocks)$ and in its next step moves from control-state $waitForLocks$ back to control state TA$-ctl$, because the LockHandler refused new locks by $Refused(M,newLocks)$.121212Note that by eliminating this $\hbox{\sc CallLockHandler}(M,L)$ step also the corresponding LockHandler step $\hbox{\sc HandleLockRequest}(M,L)$ disappears in the run.

In such computation steps $M$ makes no proper update. 2. (ii)

Repeat choosing from the schedule of $M$ a pair $\Delta_{j}(M)$ with later $\Delta_{j^{\prime}}(M)$ ($j<j^{\prime}$) which belong to the first resp. second of two consecutive $M$-Recovery steps defined as follows:

• a (say $M$-RecoveryEntry) step whereby $M$ in state $S_{j}$ moves from control-state TA-$ctl$ to $waitForRecovery$, because it became a $Victim$,
• the next $M$-step (say $M$-RecoveryExit) whereby $M$ in state $S_{j^{\prime}}$ moves back to control state TA-$ctl$ because it has been $Recovered$.

In these two $M$-Recovery steps $M$ makes no proper update. Delete:

1. (a)

$\Delta_{j}(M)$ and $\Delta_{j^{\prime}}(M)$, 2. (b)

the $((Victim,M),true)$ update from the corresponding $\Delta_{t}(\hbox{\sc TaCtl})$ ($t<j$) which in state $S_{j}$ triggered the $M$-RecoveryEntry, 3. (c)

$\hbox{\sc TryToRecover}(M)$-updates in any update set $\Delta_{i+k}(\hbox{\sc TaCtl})$ between the considered $M$-RecoveryEntry and $M$-RecoveryExit step ($i<j<i+k<j^{\prime}$), 4. (d)

each $\Delta_{i^{\prime}}(M)$ belonging to the $M$-computation segment from TA-$ctl$ back to TA-$ctl$ which contains the proper $M$-step in $S_{i}$ that is UNDOne in $S_{i+k}$ by the considered $\hbox{\sc TryToRecover}(M)$ step; besides control state and Record updates these $\Delta_{i^{\prime}}(M)$ contain updates $(\ell,v)$ with $\ell=(f,(val_{S_{i}}(t_{1}),\dots,val_{S_{i}}(t_{n})))$ where the corresponding Undo updates are $(\ell,val_{S_{i}}(f(t_{1},\dots,t_{n})))\in\Delta_{i+k}(\hbox{\sc TaCtl})$, 5. (e)

the $\hbox{\sc HandleLockRequest}(M,newLocks)$-updates in $\Delta_{l\prime}(\hbox{\sc TaCtl})$ corresponding to $M$’s CallLockHandler step (if any: in case $newLocks$ are needed for the proper $M$-step in $S_{i}$) in state $S_{l}$ ($l<l^{\prime}<i$).

The sequence $\Delta_{i_{1}}(M),\Delta_{i_{2}}(M),\dots$ with $i_{1}<i_{2}<\dots$ resulting from the application of the two cleansing operations as long as possible – note that confluence is obvious, so the sequence is uniquely defined – will be called the cleansed schedule of $M$ (for the given run).

Before defining the equivalence of transactional ASM runs we remark that $TA({\cal M},\hbox{\sc TaCtl})$ has indeed several runs, even for the same initial state $S_{0}$. This is due to the fact that a lot of non-determinism is involved in the definition of this ASM. First, the submachines of TaCtl are non-deterministic:

• In case several machines $M,M^{\prime}\in\mathcal{M}$ request conflicting locks at the same time, the LockHandler can only grant the requested locks for one of these machines.
• Commit requests are executed in random order by the Commit submachine.
• The submachine DeadlockHandler chooses a set of victims, and this selection has been deliberately left abstract.
• The Recovery submachine chooses in each step a victim $M$, for which the last step will be undone by restoring previous values at updated locations and releasing corresponding locks.

Second, the specification of $TA({\cal M},\hbox{\sc TaCtl})$ leaves deliberately open, when a machine $M\in\mathcal{M}$ will be started, i.e., register as a transaction in $TransAct$ to be controlled by TaCtl. This is in line with the common view that transactions $M\in\mathcal{M}$ can register at any time to the transaction controller TaCtl and will remain under its control until they commit.

Definition 1

Two runs $S_{0},S_{1},S_{2},\dots$ and $S_{0}^{\prime},S_{1}^{\prime},S_{2}^{\prime},\dots$ of $TA({\cal M},\hbox{\sc TaCtl})$ are equivalent iff for each $M\in\mathcal{M}$ the cleansed schedules $\Delta_{i_{1}}(M),\Delta_{i_{2}}(M),\dots$ and $\Delta_{j_{1}}^{\prime}(M),\Delta_{j_{2}}^{\prime}(M),\dots$ for the two runs are the same and the read locations and the values read by $M$ in $S_{i_{k}}$ and $S_{j_{k}}^{\prime}$ are the same.

That is, we consider runs to be equivalent, if all transactions $M\in\mathcal{M}$ read the same locations and see there the same values and perform the same updates in the same order disregarding waiting times and updates that are undone.

4.0.2 Definition of serializability.

Next we have to clarify our generalised notion of a serial run, for which we concentrate on committed transactions – transactions that have not yet committed can still undo their updates, so they must be left out of consideration131313Alternatively, we could concentrate on complete, infinite runs, in which only committed transactions occur, as eventually every transaction will commit – provided that fairness can be achieved.. We need a definition of the read- and write-locations of $M$ in a state $S$, i.e. $ReadLoc(M,S)$ and $WriteLoc(M,S)$ as used in the definition of $newLocks(M,S)$.

The definition of $Read/WriteLoc$ depends on the locking level, whether locks are provided for variables, pages, blocks, etc. To provide a definite definition, in this paper we give the definition at the level of abstraction of the locations of the underlying class $\cal{M}$ of component machines (ASMs) $M$. Refining this definition (and that of $newLocks$) appropriately for other locking levels does not innvalidate the main result of this paper.

We define $ReadLoc(M,S)=ReadLoc(r,S)$, where $r$ is the defining rule of the ASM $M$, and analogously $WriteLoc(M,S)$ $=WriteLoc(r,S)$. Then we use structural induction according to the definition of ASM rules in  [5, Table 2.2]. As an auxiliary concept we need to define inductively the read and write locations of terms and formulae. The definitions use an interpretation $I$ of free variables which we suppress notationally (unless otherwise stated) and assume to be given with (as environment of) the state $S$. This allows us to write $ReadLoc(M,S)$, $WriteLoc(M,S)$ instead of $ReadLoc(M,S,I)$, $ReadLoc(M,S,I)$ respectively.

4.0.3 Read/Write Locations of Terms and Formulae.

For state $S$ let $I$ be the given interpretation of the variables which may occur freely (in given terms or formulae). We write $val_{S}(construct)$ for the evaluation of $construct$ (a term or a formula) in state $S$ (under the given interpretation $I$ of free variables).

• $ReadLoc(x,S)=WriteLoc(x,S)=\emptyset\mbox{ for variables }x{}$

$ReadLoc(f(t_{1},\ldots,t_{n}),S)={}$

$\{(f,(val_{S}(t_{1}),\ldots,val_{S}(t_{n})))\}\;\cup\;\bigcup_{1\leq i\leq n}ReadLoc(t_{i},S){}$

$WriteLoc(f(t_{1},\ldots,t_{n}),S)=\{(f,(val_{S}(t_{1}),\ldots,val_{S}(t_{n})))\}$

Note that logical variables are not locations: they cannot be written and their values are not stored in a location but in the given interpretation $I$ from where they can be retrieved.

We define $WriteLoc(\alpha,S)=\emptyset$ for every formula $\alpha$ because formulae are not locations one could write into. $ReadLoc(\alpha,S)$ for atomic formulae $P(t_{1},\ldots,t_{n})$ has to be defined as for terms with $P$ playing the same role as a function symbol $f$. For propositional formulae one reads the locations of their subformulae. In the inductive step for quantified formulae $domain(S)$ denotes the superuniverse of $S$ minus the Reserve set [5, Ch.2.4.4] and $I_{x}^{d}$ the extension (or modification) of $I$ where $x$ is interpreted by a domain element $d$.

• $ReadLoc(P(t_{1},\ldots,t_{n}),S)={}$

$\{(P,(val_{S}(t_{1}),\ldots,val_{S}(t_{n})))\}\;\cup\;\bigcup_{1\leq i\leq n}ReadLoc(t_{i},S){}$

$ReadLoc(\neg\alpha)=ReadLoc(\alpha){}$

$ReadLoc(\alpha_{1}\wedge\alpha_{2})=ReadLoc(\alpha_{1})\cup ReadLoc(\alpha_{2}){}$

$ReadLoc(\forall x\alpha,S,I)=\bigcup_{d\in domain(S)}ReadLoc(\alpha,S,I_{x}^{d})$

Note that the values of the logical variables are not read from a location but from the modified state environment function $I_{x}^{d}$.

4.0.4 Read/Write Locations of ASM Rules.

• $ReadLoc(\mathrel{\mathbf{skip}},S)=WriteLoc(\mathrel{\mathbf{skip}},S)=\emptyset{}$

$ReadLoc(t_{1}:=t_{2},S)=ReadLoc(t_{1},S)\cup ReadLoc(t_{2},S){}$

$WriteLoc(t_{1}:=t_{2},S)=WriteLoc(t_{1},S){}$

$ReadLoc(\mathrel{\mathbf{if}}\alpha\mathrel{\mathbf{then}}r_{1}\mathrel{\mathbf{else}}r_{2},S)={}$

ReadLoc(\alpha,S)\cup\left\{\begin{array}[]{ll}ReadLoc(r_{1},S)&\mathrel{\mathbf{if}}val_{S}(\alpha)=true\\ ReadLoc(r_{2},S)&\mathrel{\mathbf{else}}\end{array}\right.{}

WriteLoc(\mathrel{\mathbf{if}}\alpha\mathrel{\mathbf{then}}r_{1}\mathrel{\mathbf{else}}r_{2},S)=\left\{\begin{array}[]{ll}WriteLoc(r_{1},S)&\mathrel{\mathbf{if}}val_{S}(\alpha)=true\\ WriteLoc(r_{2},S)&\mathrel{\mathbf{else}}\end{array}\right.{}

$ReadLoc(\mathrel{\mathbf{let}}x=t\mathrel{\mathbf{in}}r,S,I)=ReadLoc(t,S,I)\cup ReadLoc(r,S,I_{x}^{val_{S}(t)}){}$

$WriteLoc(\mathrel{\mathbf{let}}x=t\mathrel{\mathbf{in}}r,S,I)=WriteLoc(r,S,I_{x}^{val_{S}(t)})\mbox{ // call by value}{}$

$ReadLoc(\mathrel{\mathbf{forall}}x\mathrel{\mathbf{with}}\alpha\mathrel{\mathbf{do}}r,S,I)={}$

$ReadLoc(\forall x\alpha,S,I)\;\cup\;\bigcup_{a\in range(x,\alpha,S,I)}ReadLoc(r,S,I_{x}^{a}){}$

$\mathrel{\mathbf{where}}range(x,\alpha,S,I)=\{d\in domain(S)\mid val_{S,I_{x}^{d}}(\alpha)=true\}{}$

$WriteLoc(\mathrel{\mathbf{forall}}x\mathrel{\mathbf{with}}\alpha\mathrel{\mathbf{do}}r,S,I)=\bigcup_{a\in range(x,\alpha,S,I)}WriteLoc(r,S,I_{x}^{a}){}$

In the following cases the same scheme applies to read and write locations:141414In $yields(r_{1},S,I,U)$ $U$ denotes the update set produced by rule $r_{1}$ in state $S$ under $I$.

• $Read[Write]Loc(r_{1}\mathrel{\mathbf{par}}r_{2},S)={}$

$Read[Write]Loc(r_{1},S)\cup Read[Write]Loc(r_{2},S){}$

$Read[Write]Loc(r(t_{1},\ldots,t_{n}),S)=Read[Write]Loc(P(x_{1}/t_{1},\ldots,x_{n}/t_{n}),S){}$

$\mathrel{\mathbf{where}}r(x_{1},\ldots,x_{n})=P\mbox{ // call by reference}{}$

$Read[Write]Loc(r_{1}\mathrel{\mathbf{seq}}r_{2},S,I)=Read[Write]Loc(r_{1},S,I)\cup{}$

\left\{\begin{array}[]{ll}Read[Write]Loc(r_{2},S+U,I)&\mathrel{\mathbf{if}}yields(r_{1},S,I,U)\mathrel{\mathbf{and}}Consistent(U)\\ \emptyset&\mathrel{\mathbf{else}}\end{array}\right.

For $\mathrel{\mathbf{choose}}$ rules we have to define the read and write locations simultaneously to guarantee that the same instance satisfying the selection condition is chosen for defining the read and write locations of the rule body $r$:

• $\mathrel{\mathbf{if}}range(x,\alpha,S,I)=\emptyset\mathrel{\mathbf{then}}{}$

$ReadLoc(\mathrel{\mathbf{choose}}x\mathrel{\mathbf{with}}\alpha\mathrel{\mathbf{do}}r,S,I)=ReadLoc(\exists x\alpha,S,I){}$

$WriteLoc(\mathrel{\mathbf{choose}}x\mathrel{\mathbf{with}}\alpha\mathrel{\mathbf{do}}r,S,I)=\emptyset\mbox{ // empty action}{}$

$\mathrel{\mathbf{else}}\;\mathrel{\mathbf{choose}}a\in range(x,\alpha,S,I){}$

$ReadLoc(\mathrel{\mathbf{choose}}x\mathrel{\mathbf{with}}\alpha\mathrel{\mathbf{do}}r,S,I)={}$

$ReadLoc(\exists x\alpha,S,I)\cup ReadLoc(r,S,I_{x}^{a}){}$

$WriteLoc(\mathrel{\mathbf{choose}}x\mathrel{\mathbf{with}}\alpha\mathrel{\mathbf{do}}r,S,I)=WriteLoc(r,S,I_{x}^{a})$

We say that $M$ has or is committed (in state $S_{i}$, denoted $Committed(M,S_{i})$) if step $\hbox{\sc Commit}(M)$ has been performed (in state $S_{i}$).

Definition 2

A run of $TA({\cal M},\hbox{\sc TaCtl})$ is serial iff there is a total order $<$ on $\mathcal{M}$ such that the following two conditions are satisfied:

1. (i)

If in a state $M$ has committed, but $M^{\prime}$ has not, then $M<M^{\prime}$ holds. 2. (ii)

If $M$ has committed in state $S_{i}$ and $M<M^{\prime}$ holds, then the cleansed schedule $\Delta_{j_{1}}(M^{\prime})$, $\Delta_{j_{2}}(M^{\prime}),\dots$ of $M^{\prime}$ satisfies $i<j_{1}$.

That is, in a serial run all committed transactions are executed in a total order and are followed by the updates of transactions that did not yet commit.

Definition 3

A run of $TA({\cal M},\hbox{\sc TaCtl})$ is serialisable iff it is equivalent to a serial run of $TA({\cal M},\hbox{\sc TaCtl})$.151515Modulo the fact that ASM steps permit simultaneous updates of multiple locations, this definition of serializability is equivalent to Lamport’s sequential consistency concept [16].

Theorem 4.1

Each run of $TA({\cal M},\hbox{\sc TaCtl})$ is serialisable.

Proof

Let $S_{0},S_{1},S_{2},\dots$ be a run of $TA({\cal M},\hbox{\sc TaCtl})$. To construct an equivalent serial run let $M_{1}\in\mathcal{M}$ be a machine that commits first in this run, i.e. $Committed(M,S_{i})$ holds for some $i$ and whenever $Committed(M,S_{j})$ holds for some $M\in\mathcal{M}$, then $i\leq j$ holds. If there is more than one machine $M_{1}$ with this property, we randomly choose one of them.

Take the run of $TA(\{M_{1}\},\hbox{\sc TaCtl})$ starting in state $S_{0}$, say $S_{0},S_{1}^{\prime},S_{2}^{\prime},\dots,S_{n}^{\prime}$. As $M_{1}$ commits, this run is finite. $M_{1}$ has been Deleted from $TransAct$ and none of the TaCtl components is triggered any more: neither Commit nor LockHandler because $CommitRequest$ resp. $LockRequest$ remain empty; not DeadlockHandler because $Deadlock$ remains false since $M_{1}$ never $Wait$s for any machine; not Recovery because$Victim$ remains empty. Note that in this run the schedule for $M_{1}$ is already cleansed.

We now define a run $S_{0}^{\prime\prime},S_{1}^{\prime\prime},S_{2}^{\prime\prime},\dots$ (of $TA({\cal M}-\{M_{1}\},\hbox{\sc TaCtl})$, as has to be shown) which starts in the final state $S_{n}^{\prime}=S_{0}^{\prime\prime}$ of the $TA(\{M_{1}\},\hbox{\sc TaCtl})$ run and where we remove from the run defined by the cleansed schedules $\Delta_{i}(M)$ for the originally given run all updates made by steps of $M_{1}$ and all updates in TaCtl steps which concern $M_{1}$. Let

[TABLE]

That is, in the update set $\Delta_{i}^{\prime\prime}$ all updates are removed from the original run which are done by $M_{1}$—their effect is reflected already in the initial run segment from $S_{0}$ to $S_{n}^{\prime}$—or are LockHandler updates involving a $LockRequest(M_{1},L)$ or are $Victim(M_{1}):=true$ updates of the DeadlockHandler or are updates involving a $\hbox{\sc TryToRecover}(M_{1})$ step or are done by a step involving a $\hbox{\sc Commit}(M_{1})$.

Lemma 1

$S_{0}^{\prime\prime},S_{1}^{\prime\prime},S_{2}^{\prime\prime},\dots$* is a run of $TA({\cal M}-\{M_{1}\},\hbox{\sc TaCtl})$.*

Lemma 2

The run $S_{0},S_{1}^{\prime},S_{2}^{\prime},\dots,S_{n}^{\prime},S_{1}^{\prime\prime},S_{2}^{\prime\prime},\dots$ of $TA({\cal M},\hbox{\sc TaCtl})$ is equivalent to the original run $S_{0},S_{1},S_{2},\dots$.

By induction hypothesis $S_{0}^{\prime\prime},S_{1}^{\prime\prime},S_{2}^{\prime\prime},\dots$ is serialisable, so $S_{0},S_{1}^{\prime},S_{2}^{\prime},\dots$ and thereby also $S_{0},S_{1},S_{2},\dots$ is serialisable with $M_{1}<M$ for all $M\in\mathcal{M}-\{M_{1}\}$.

Proof

(Lemma 1)  We first show that omitting in $\Delta_{i}^{\prime\prime}$ every update from $\Delta_{i}(\hbox{\sc TaCtl})$ which concerns $M_{1}$ does not affect updates by TaCtl in $S_{i}^{\prime\prime}$ concerning $M\neq M_{1}$. In fact starting in the final $M_{1}$-state $S_{0}^{\prime\prime}$, $TA({\cal M}-\{M_{1}\},\hbox{\sc TaCtl})$ makes no move with a $Victim(M_{1}):=true$ update and no move of $\hbox{\sc Commit}(M_{1})$ or $\hbox{\sc HandleLockRequest}(M_{1},L)$ or $\hbox{\sc TryToRecover}(M_{1})$

It remains to show that every $M$-step defined by $\Delta_{i}^{\prime\prime}(M)$ is a possible $M$-step in a $TA({\cal M}-\{M_{1}\},\hbox{\sc TaCtl})$ run starting in $S_{0}^{\prime\prime}$. Since the considered $M$-schedule $\Delta_{i}(M)$ is cleansed, we only have to consider any proper update step of $M$ in state $S_{i}^{\prime\prime}$ (together with its preceding lock request step, if any). If in $S_{i}^{\prime\prime}$ $M$ uses $newLocks$, in the run by the cleansed schedules for the original run the locks must have been granted after the first Commit, which is done for $M_{1}$ before $S_{0}^{\prime\prime}$. Thus these locks are granted also in $S_{i}^{\prime\prime}$ as part of a $TA({\cal M}-\{M_{1}\},\hbox{\sc TaCtl})$ run step. If no $newLocks$ are needed, that proper $M$-step depends only on steps computed after $S_{0}^{\prime\prime}$ and thus is part of a $TA({\cal M}-\{M_{1}\},\hbox{\sc TaCtl})$ run step.

Proof

(Lemma 2)  The cleansed machine schedules in the two runs, the read locations and the values read there have to be shown to be the same. First consider any $M\not=M_{1}$. Since in the initial segment $S_{0},S_{1}^{\prime},S_{2}^{\prime},\dots,S_{n}^{\prime}$ no such $M$ makes any move so that its update sets in this computation segment are empty, in the cleansed schedule of $M$ for the run $S_{0},S_{1}^{\prime},S_{2}^{\prime},\dots,S_{n}^{\prime},S_{1}^{\prime\prime},S_{2}^{\prime\prime},\dots$ all these empty update sets disappear. Thus this cleansed schedule is the same as the cleansed schedule of $M$ for the run $S_{n}^{\prime},S_{1}^{\prime\prime},S_{2}^{\prime\prime},\dots$ and therefore by definition of $\Delta_{i}^{\prime\prime}(M)=\Delta_{i}(M)$ also for the original run $S_{0},S_{1},S_{2},\dots$ with same read locations and same values read there.

Now consider $M_{1}$, its schedule $\Delta_{0}(M_{1}),\Delta_{1}(M_{1}),\dots$ for the run $S_{0},S_{1},S_{2},\dots$ and the corresponding cleansed schedule $\Delta_{i_{0}}(M_{1}),\Delta_{i_{1}}(M_{1}),\Delta_{i_{2}}(M_{1}),\dots$. We proceed by induction on the cleansed schedule steps of $M_{1}$. When $M_{1}$ makes its first step using the $\Delta_{i_{0}}(M_{1})$-updates, this can only be a proper $M_{1}$-step together with the corresponding Record updates (or a lock request directly preceding such a $\Delta_{i_{1}}(M_{1})$-step) because in the computation with cleansed schedule each lock request of $M_{1}$ is granted and $M_{1}$ is not $Victim$ized. The values $M_{1}$ reads or writes in this step (in private or locked locations) have not been affected by a preceding step of any $M\not=M_{1}$—otherwise $M$ would have locked before the non-private locations and keep the locks until it commits (since cleansed schedules are without Undo steps), preventing $M_{1}$ from getting these locks which contradicts the fact that $M_{1}$ is the first machine to commit and thus the first one to get the locks. Therefore the values $M_{1}$ reads or writes in the step defined by $\Delta_{i_{0}}(M_{1})$ (resp. also $\Delta_{i_{1}}(M_{1})$) coincide with the corresponding location values in the first (resp. also second) step of $M_{1}$ following the cleansed schedule to pass from $S_{0}$ to $S_{1}^{\prime}$ (case without request of $newLocks$) resp. from $S_{0}$ to $S_{1}^{\prime}$ to $S_{2}^{\prime}$ (otherwise). The same argument applies in the inductive step which establishes the claim.

5 Conclusion

In this article we specified (in terms of Abstract State Machines) a transaction controller TaCtl and a transaction operator which turn the behaviour of a set of concurrent programs into a transactional one under the control of TaCtl. In this way the locations shared by the programs are accessed in a well-defined manner. For this we proved that all concurrent transactional runs are serialisable.

The relevance of the transaction operator is that it permits to concentrate on the specification of program behavior ignoring any problems resulting from the use of shared locations. That is, specifications can be written in a way that shared locations are treated as if they were exclusively used by a single program. This is valuable for numerous applications, as shared locations (in particular, locations in a database) are common, and random access to them is hardly ever permitted.

Furthermore, by shifting transaction control into the rigorous framework of Abstract State Machines we made several extensions to transaction control as known from the area of databases [6]. In the classical theory schedules are sequences containing read- and write-operations of the transactions plus the corresponding read- and write-lock and commit events, i.e., only one such operation or event is treated at a time. In our case we exploited the inherent parallelism in ASM runs, so we always considered an arbitrary update set with usually many updates at the same time. Under these circumstances we generalised the notion of schedule and serialisability in terms of the synchronous parallelism of ASMs. In this way we stimulate also more parallelism in transactional systems.

Among further work we would like to be undertaken is to provide a (proven to be correct) implementation of our transaction controller and the $TA$ operator, in particular as plug-in for the CoreASM [8, 7] or Asmeta [4, 10] simulation engines. We would also like to see refinements or adaptations of our transaction controller model for different approaches to serialisability [14], see also the ASM-based treatment of multi-level transaction control in [15]. Last but not least we would like to see further detailings of our correctness proof to a mechanically verified one, e.g. using the ASM theories developed in KIV (see [1] for an extensive list of relevant publications) and PVS [9, 13, 12] or the (Event-)B [2, 3] theorem prover for an (Event-)B transformation of $TA({\cal M},\hbox{\sc TaCtl})$ (as suggested in [11]).

5.0.1 Acknowledgement.

We thank Andrea Canciani and some of our referees for useful comments to improve the paper.