Operational semantics of transactions(4)

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

a transition constraint preserving transformation

T (S C )=

T (S C )if T (S C )|=Σ

S C if T (S C )|=ΣThe transaction can be thus understood as an invari-ant state transition.

Transactions T 1and T 2are competing if read (T 1)∩write (T 2)=∅or read (T 2)∩write (T 1)=∅or write (T 2)∩write (T 1)=∅.The sets read (T i )and write (T i )consists of the locations of objects which are read or written by the transaction T i .

Parallel execution of transactions T 1 T 2is cor-rect if either the transactions are not competing or the effect of T 1 T 2(S C )is equivalent to T 1(T 2(S C ))or to T 2(T 1(S C ))for any database S C .If paral-lel execution is correct transaction execution can be scheduled in parallel.

Logical semantics of transactions is defined by consistency (each transaction preserves transition

constraints)and

parallelization (transaction can be executed in par-allel).

We observe that atomicity is not considered.Atomic-ity is declared by granularity of transitions.Further-more,we are not concerned with durability.Durabil-ity is not a logical property but rather a property of storage.2.4

Operational semantics of transactions

Instead of using an abstract interpretation and a set of models,an abstract Moore-automaton M =(Z,f,I,Z final )is used with the set Z of states,its subset Z final of final states,the state transition func-tion f ,and the initialization function I which assigns a starting state I (p,d )=z p,d ∈Z to each program p and each input d .The interpretation of the pro-gram p and the input d is the sequence of states z p,d =z 0,z 1,...,z i ,...with z i =f (z i −1)for i ≥1.If the sequence is finite for n p,d and z n p,d ∈Z final then the program p is correct for d .If f (z i )is un-defined for some i and z i ∈Z final then the program does not have a meaning for d .If the sequence is in-finite with z i ∈Z final for all i ∈N then the program is not terminating for d .

A variety of approaches has been developed for definition of operational semantics:

Scheduling,access and recovery models:Transactions

are executed in parallel and independent from each other.In order to support this require-ment,access,scheduling and recovery models are developed (Biskup 1995).

Given a set of transactions T 1,...,T n .A sched-ule S (T 1,...,T n )of T i =o i,1,...,o i,n i ,1≤i ≤n is assignment of moments S (o i,j )of time to the operations of the transactions which preserves the order of operations within each transaction.Now an access plan can be specified for the ob-jects to be used in transactions.An access plan is roughly called conflict-free if no transaction reads a value which is under change by another transaction.

This approach has the advantage that the trans-action machine is constructed.The disadvantage is the complexity of the constructive approach.Any change in transaction policy or constraint enforcement policy imposes a severe number of changes in the definitions.

Abstract automata models are widely used for pro-gramming languages.Such abstract models have the advantage that refinement of requirements is reflected by refinement of abstract automata.For this reason,this approach is preferable if we are able to to define such abstract automata.Operational semantics for transactions must be based on parallel execution of processes.Therefore,we need a machine that allows to model parallel exe-cution.3Defining Operational Semantics Through Abstract State Machines (ASM)

3.1

Functional Semantics for Transactions using ASM

Abstract state machines (ASM)M (Gurevich 1997,Gurevich 2000,St¨a rk,Schmid &B¨o rger 1996)provide a framework for specification of parallel execution.Abstract state machines are defined by a number of rules

IF condition DO actions

which can be applied to a state space in parallel .The condition or guard is an arbitrary first-order for-mula.

The notion of the state space is the classical no-tion of mathematical structures (?)where data are abstract objects collected in relations or characteris-tic functions.The state space consists of static func-tions (which never change during any run)and dy-namic functions.Controlled functions are dynamic functions which are updateable only by ASM rules.Monitored functions are only updated by the envi-ronment.Interaction functions are updatable both by the ASM and the environment.Derived functions are neither updatable by the ASM nor by the envi-ronment but are defined in terms of other functions.Actions are updates of the state space,i.e.,func-tions of the form

f (t 1,...,t n ):=t

whose execution is changing the value of the lo-cation loc represented by the function f at the given parameters.The notion of the ASM run is the same as the computation notion of transition systems.An ASM computation step in a given state is the simultaneous execution of all rules whose guard is true in the state if these updates are consistent.An update set U is consistent if there are no pairs f (t 1,...,t n ):=t and f (t 1,...,t n ):=t in U with t =t .The firing a consistent update set U in a state A results in a new state B in which controlled and interaction functions are changed by the update set.

Simultaneous execution allows to abstract from ir-relevant details of sequential execution and to use syn-chronous parallelism.We observe that,therefore,the model fits very well to transaction execution.

ASM semantics has been been used for definition of semantics of object-oriented models in (Gottlob et al.1991)and for defining database recovery in (Gurevic …… 此处隐藏：4148字，全部文档内容请下载后查看。喜欢就下载吧 ……