Operational semantics of transactions(5)

Mathematics is forcing towards a consistent framework of theory development. Computer Science is an engineering discipline and sometimes suffers from ad-hoc definitions. Transactions are a concept that is commonly used in the database area. It is often def

•The application functionΞof application of M assigns a state of M to the empty set of oper-ations.The functionΞassigns a state to each initial segment of M.The stateΞ(X)is the re-sult of performing all operations in X.

The application function is restricted by the co-herence condition:

If x is a maximal operation in afinite initial seg-ment X of M and Y=X\{x},then the trans-action T with x∈T is an active transaction in Ξ(Y)andΞ(X)is obtained fromΞ(Y)by per-forming x atΞ(Y).

3.2Models of Modification of Database Sys-

tems.

Modification in-place:Any modification caused by an operation of the transaction to the data in the secondary memory is directly written to the lo-cation of those data.In order to be able to undo

a modification in the case of failure of the trans-

action the changes are recorded.The undo thus applies to the case that the transaction fails or aborts.

Modification in-private:The transaction keep their lo-cal spaces.The local space can be abandoned if the transaction fails or aborts.If the transaction commits then the data of local space which are associated to the data in the secondary memory areflushed to the secondary memory.

Shadow modification:With the start of the transac-tion,a shadow page which is identical to the cur-rent page is allocated.This shadow page shows the state of data before the transaction.The transaction works on the original page.If the transaction fails the shadow is used for recovery.

If the transaction commits the shadow page is removed.

3.3Abstract Operational Semantics for

Transactions using ASM

The concurrency control can be solved by a large variety of approaches.Database books usually dis-cuss one or some of the approaches and introduce the transaction concept on the basis of those approaches. It is,however,not necessary,to introduce transac-tions on the basis of a specific solution.Furthermore, transaction machines also implement one or some of possible solutions.The transaction model is,however, far more general than the specific solution provided by a given DBMS.In the sequel we shall discuss two of the approaches.

We require that each of the solutions is a refine-ment of the relation˘Ξ

−→.The refinement of the transaction relation should be conservative,i.e.,all properties valid for˘Ξ

−→must be preserved.

Conceptually,each transaction is working over a local copy of the database and writing the results of its work into the global database at the end.In order to cover all approaches for databases in the abstract presentation,we introduce the following abstract op-erations:

CreateOwnDB for creating a local copy of the global database,

PrepareMergeDB for preparing the merging into the global database,

MergeOwnDB for merging the results into the global database,

FreeOwnDB for housekeeping at the end of the lo-cal database,ReadOwnDB for reading values from the local database,and

WriteOwnDB for writing values to the local database.

These operation are refined in the sequel for sev-eral approaches of transaction implementation.

The State Space for Transactions.We distinguish between

Status of the transaction:The status of the transac-tion Status(transaction)is either undef(denot-ing inactivity of transactions in the queue),ac-tive(denoting that a transaction is currently run-ning),commit(denoting that a transaction has been committed),ready2commit(denoting that a transaction is ready for committing),failed(de-noting that the transaction has failed),or done (denoting that a transaction has been success-fully completed).See also the state transition diagram below.

Content of the transaction:Syntactically,transac-tions are sequences of basic computations, retrieval and modification operations.The content Content(transaction)of the transaction is used for recharging the queue of operations to be performed by the database system.

The content of a transaction is given by a queue Queue(transaction)of operations to be performed.

Persistent database space:The database is kept per-sistently.Any change to the database must pre-serve transition constraints.We use the Sta-bleDB for representing the persistent database.

The General State Transition Diagram for Transac-tions..The diagrams discussed above cannot cap-ture the entire picture of transaction processing.We use additional states for the definition of transactions:

Ready2Commit:The effect of application of the transaction is checked against the database. ICtrue:If data under change are kept within the lo-cal space of the transaction the space is prepared for writing to the database.

Failed:The local space is used recovering from fail-ure of the transaction.

Inactive:The transaction is ready for execution but not yet scheduled.

The state model of the transaction displayed in Figure 1is extended to the model shown in Figure4.

r r

r r

r r j

r r

r r

r j

T

T

'

'

T

'

©

E

s

BOT

Run

Failed

Aborted

Inactive

Ready2Commit

ICtrue

Committed

EOT

Figure4:The States of a Transaction

We use a Z-like notation for specification of the rule

ruleName:IF condition DO actions,i.e.,