Operational semantics of transactions(6)

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

ruleName:

condition

actions

The abstract setting for transactions can be now defined by the following rules:

BOT:

Status(Self)=undef

Status(Self):=active

Queue(Self):=Content(Self)

CreateOwnDB()

This rule specifies the instantiation of the local space of the transaction after it has been scheduled. RUN:

Status(Self)=active

IF Queue(Self)=∅

THEN

CASE Top(Queue(Self))OF

read(loc):ReadOwnDB(loc)

write(loc,val):WriteOwnDB(loc,val)

compute(expr,loc):

WriteOwnDB(loc,compute(expr,loc)) ENDCASE

Queue(Self):=Pop(Queue(Self))

ELSE Status(Self):=ready2commit

ENDIF

The RUN state rule for transactions specifies the run of the transaction.This run is modeled without consideration of concurrent writes to the stable database.Concurrent writes appear in the state ICtrue.We shall show later how we can cope with this situation by introducing a central location log space for transactions.

READY2COMMIT:

Status(Self)=ready2commit

IF OwnDB|=Σ

THEN Status(Self):=ICtrue

ELSE Status(Self):=ICfalse

ENDIF

The READY2COMMIT state rule checks whether a consistent state can be reached if the local mod-ification data of the transaction are written to the stable database.

FAILED:

(Status(Self)=failed∨Status(Self)=ICfalse)

Status(Self):=aborted

In the abstract setting,the FAILED rule simply transfers the status of the transaction to aborted.We will discuss in the next subchapters the refinement of this rule.

ABORTED:

Status(Self)=aborted

IF CanReschedule(Self)THEN

Status(Self):=undef

FreeOwnDB()

The ABORTED rule transfers the state of the transaction to the inactive state.From there it becomes active again.The activation is triggered by the monitored function CanReschedule. ICTRUE:

Status(Self)=ICtrue

PrepareMergeDB()

Status(Self):=committed

If the transaction is completed and does not invalidate the integrity constraints we can prepare the states for writing data to locations in the stable database.This state will be modified due to problems of isolation.

COMMITTED:

Status(Self)=committed

MergeOwnDB()

FreeOwnDB()

Status(Self):=done

Program(Self):=undef

The COMMITTED rule checks out the transac-tion.The data which are in the queue for writing are now written in parallel to the stable database.

For completeness we do now define an abstract version of the interface operations. CreateOwnDB:

OwnDB(Self):=globalDB

initOwnDB(Self):=globalDB

MergeOwnDB:

for all x∈Location:

OwnDB(Self,x)=initOwnDB(Self,x)

globalDB(x):=OwnDB(Self,x) FreeOwnDB:

//do nothing here

ReadOwnDB(where:Location):

return OwnDB(Self,where)

WriteOwnDB(where:Location,val:Value):

OwnDB(Self,where):=val

3.4Operational Semantics for Transactions

in the In-Private Setting

Operational semantics of transaction can be refined in a large variety of ways.We shall demonstrate this va-riety for transactions in the in-private setting.These variations demonstrate the advantage of the abstract definition discussed in section3.3.The transactions which are enabled to run are supported by:

Current database:The current database Cur-rentDB(transaction,location)keeps all those data that are used in the working space and that are related to data on the same location at the secondary storage device.

Flash data:The moment of writing may depend on the actual conditions of the machine.There-fore,we write data which may be transferred to the database in the secondary storage device to Ready2Write(location).