An Assertional Characterization
of Serializability*
E. Robert McCurley
Fred B. Schneider
TR 89-1039
September 1989
Department of Computer Science
Cornell University
Ithaca, NY 14853-7501
*This material is based on work supported by the Office of Naval Research under contract
NOOOI4-86-k-0092, the National Science Foundation under grant no OCR-8701 103, and
Digital Equipment Corporation. Any opinions, findings, and conclusions or recommendations
expressed in this publication are those of the authors and do not reflect the views of these agencies.
An Assertional Characterization of
serializability*
E. Robert McCuriey
School of Information and Computer Science
Georgia Institute of Technology
Atlanta, Georgia 30332
Fred B. Schneider
Department of Computer Science
Cornell University
Ithaca, New York 1?853
September 28, 1989
Abstract
Serializability is usually defined operationally in terms of sequences
of operations. This paper gives another definition of serializability--H
in terms of sequences of states. It also shows how this definition can
be used to prove correctness of solutions to the concurrency control
problem.
1 Introduction
A database system is a computer system that stores information. Consis-
tency constraints restrict system states to those that are meaningful; trans-
actions are designed so that each individually transforms the database from
- This material is based on work supported in part by the Office of Naval Research un-
der contract N00014-86-K-0092, the National Sdence Foundation under Grant No. CCR
8701103, and Digital Equipment Corporation. Any opinions, findings, and conclusions or
recommendations expressed in this publication are those of the authors and do not reflect
the views of these agencies.
one consistent state to another. For example, in a database for a banking
application, a consistency constraint might relate cash-on-hand to the sum
of the account balances; a transaction for a deposit would adjust both an
account balance and cash-on-hand, preserving the consistency constraint.
During concurrent execution of transactions, operations can interleave in
ways that leave the database in an inconsistent state. Avoiding such states
is called the concurrency control problem. The traditional solution to this
problem is based on serializability [EGLT76], which asserts that transactions
executing concurrently "behave like" they are run serially, one after another.
If, when run in isolation, each transaction transforms the database from
one consistent state to another and if transactions are seriallzable, then
concurrent execution of those transactions will also transform the database
from one consistent state to another. Thus, implementing serializability
solves the concurrency control problem.
Seriallzability is usually defined (operationally) in terms of sequences,
called schedules, that list operations in the order they run. This would seem
to preclude use of programming methodologies based on assertions about
states--Hso called asseflional reasoning. It is tempting to regard this as a
fundamental limitation of such methodologies. In this paper, we show this
view to be erroneous. We give an assertional characterization of seriallzabil-
ity and show how this definition can be used to prove correctness of solutions
to the concurrency control problem.
We proceed as follows. In Section 2, we present a database system
model and give a formal definition of seriallzability. Two ways to specify
seriallzability using formulas of a Hoare-style programming logic are given
in Section 3. In Section 4, we discuss possible extensions to our database
system model and their implications. We conclude, in Section 5, with a
comparison of our definition and previous ones.
2 Serializability
2.1 System Model
A database system ? can be represented by a triple (V, C, T?, where V is
a set of variables, C is a predicate on V, and
T: [ro II . II
is a concurrent program in which each transaction Tj is a program that
references only variables of V-
2
Variables ill V represent the state of the database, including but not
limited to the part that actually contains application data.1 C is the con-
sistency constraint of the database. A state is consistent iff C is true in
that state. Each transaction r? is assumed to terminate in a consistent state
when run aione starting in one.
An example of a database system is given in Figure 1. ?o models a
database that maintains an unordered collection of records, represented by
variable s of type set. Variables ?....., rn??i are sequences, containing
records that have or will be inserted into 8, and consistency constraint Co
requires 8 to contain a subset of these. Each transaction Addi adds the
records of ?flj to 8. Variable tj of Addi is locai to the transaction, hence
excluded from V0. In the guard of the loop, linil denotes the length of the
sequence ?flj. Angle brackets "(" and ")" surround operations that execute
atomically.
2.2 Serializability
?o=(Vo: 8,??,???,??N--H1,
C0: 8C?(inoU...UinN?1),
T0: [Ad?? ... II AddN?l]
Add?: (ti:=O);
doti#Iinil
(8:=8uini(tj));
od
Figure 1: Database System ?o.
Seriallzability of ? = ( V, C, T? can be understood in terms of an abstract
database system ?` = ( V', C', T'? where V' and C' are the same as V and
C of?, and
T':			[ro' II . II r?'?iJ ,			(1)
is the concurrent program in which each r: is (r2-), a transaction that exe-
cutes the same operations as r? but as a single atomic operation. Executions
`A commit flag is an example of an element of V that does not contain application
data.
3
of T' are serial, meaning that transactions are executed one after another
without interleaving.
Recall that serializability asserts that every (potentially interleaved) exe-
cution of T "behaves like" some (serial) execution of T'. Since if one system
T implements another one T', then every behavior of T can be viewed as
a behavior of T', serializability of T is equivalent to T implementing T'
[Lam88].
2.3 Defining "Implements"
111 [Pri87, GP85j, a formal definition in terms of predicate transformers is
given for when one program implements another. This definition is a gen-
eralization of that presented in [Hoa72j and can be summarized as follows.
Let S' be a program operating on variables X, and let P be a predicate
on X such that S' is guaranteed to terminate when run in an initial state
satisfying F. Let S be a program 011 variables Y (disjoint from X), which
is intended to implement s,.
Programs S' and S are called the abstract and concrete programs, re-
spectively. The correspondence between the states of these programs is
represented by a predicate I on X and Y, called a coupling invariant. It
often takes the form X = F( Y), where F is a function that maps any state
of s to the state of S' that it implements.
The property that S implements S' is formalized as
(P A I) ? wp(S, wp*(S',I)).
(2)
Here, wp(S, R) denotes the weakest precondition of S with respect to R
[Dij76], the set of states in which any execution of S is guaranteed to ter-
minate in a state satisfying R, and wp*(S', R) denotes the angelic weakest
precondition of S' with respect to R, the set of states in which some exe-
cution of S' wffl terminate in a state satisfying R.2 Thus, (2) specifies a
correspondence between the effect of concrete program S and that of the
abstract program S1, when both programs are viewed as predicate trans-
formers. In particular, (2) asserts that concrete program S changes its
variables in a way that is consistent--Has defined by I--Hwith some execution
of the abstract program it implements.
2The relationship between wp and wp is as follows:
wp(S, true) ? (wp*(S,R) ? ?wp(S, ?R)).
For deterrainistic S, wp(S, R) ? wp?(S,R).
4
2.4 Serializability as "Implements"
Serializability of? = ( V, C, T) can be formalized in terms of?'= ( V', C', T'?
using (2) by taking T' of (1) to be the abstract program and T to be the
concrete program. To do so, however, variables V' in C' and T' must be
replaced by fresh variables ??.?? ,VM' 1 disjoint from V. Henceforth, we
assume that V and V' are disjoint.
For P in (2) we take C' and for I we take A,jE v Vj = v: giving the fol-
lowing characterization of serializability.
Definition: ? is serializable if and only if
(C'A A Vi=v:')?wp(T,wp*(T', A vi=v:()).
?Ev			?Ev
(3)
Some simplification of (3) is possible. Since .?.... ,r?'?1 run serially in
T', any execution of T' will be equivalent to some execution of a sequential
program p in the set
S( T'): .......			?? is a transaction of T', 0< i <N?.
Thus, for any predicate R,
wp*(T',R) ? V wp*(p,R).			(4)
pES( T')
Substituting the right-hand side of (4) into (3) gives the equivalent formuia
(C'A A vi=v?)?wp(T, V wp*(p, A vi=v:.)). (5)
?EV			pEs(T')			VjEV
When transactions of T' are deterministic, (3) can be further simplified.
Each p E S( T') is now deterministic. Since wp and wp* are equivalent for
deterministic programs, (5) is equivalent to
(C' A A vi=vD ? wp(T, V wp(p, A vi=v:.)). (6)
?Ev			pEs(T')			?EV
3 Proof Techniques for Serializability
3.1 Hoare's Logic
Verifying that a database system ? satisfies any of (3), (5) or (6) presents
a difficuit problem: the weakest precondition of a concurrent program such
5
as T is a complicated predicate that is difficult to evaluate. Hoare's logic
[Hoa69] provides all alternative and often more tractable formalism for rea-
soning about concurrent programs. A t'ipLe is a formula
?PJSfQJ			(7)
where S is a program and P and Q are predicates on variables of S. Predi-
cates P and Q are called asseflions with P designated the precondition and
Q the postcondition of S.
The triple (7) has the following interpretation:
If execution of S begins in a state satisfying P and s terminates,
then the state reached will satisfy Q.
Since this interpretation implies nothing about the termination of S, a triple
specifies partial correctness. Axioms and inference rules of Hoare's logic
for a simple sequential programming language can be found in [Hoa69j.
Additional axioms and rules for concurrent programs are given in [oG76].
3.2 Effective Criteria Serializability
The relationship between a triple and wp is
Q ? wp(S, R)			iff			fQJS?R) and term(S, Q)
(8)
for any predicates Q and R and any program S, where terrn(S, Q) specifies
that S is guaranteed to terminate when started in a state satisfying Q. Thus,
our definition of serializability in Section 2.4 and formulas (3), (5) and (6)
imply the following theorem and corollary.
Theorem 1 Let ? = ( V, C, T) be a database system and ?` a correspond-
ing abstract system. ? is serializable if and only if
T1.1: (C' A A v?=v1,.JTf V wp*(p, A vi=vDY,
VjEV			pE8(T')			?jEV
T1.2: term(T,C' A A vj=v8,).
?E v
Corollary 2 If the transactions of T' are deterministic, then ? is serializ-
able if and only if
6
02.1: ?C'A A Vi=V:'JTf V wp(p, A v:=v1,)1,
?EV			pES(T')			VjEV
02.2: term( T, C' A A v1 =
VjE V
The conditions of Theorem 1 and Corollary 2 provide effective criteria for
verifying--Husing assertional reasoning?enalizability of database systems.
Validity of Ti.1 and C2.1 can be established using the logic of [OG76];
validity of Ti.2 and C2.2 can be established using temporal logic [Pnu8i,
MP8lj.
3.3 An Example
Returning to the example of Figure 1, note that transactions of ??` are
deterministic since those of ?o are. Thus, Corollary 2 can be used to verify
serializability of ?o as follows. We first prove condition C2.1,
(C01A A vi=vg'JT0( V wp(p, A Vi=Vj')) (9)
ViEV0			ViEV0
We abbreviate the formal proof of(9) with the following proofotttine [OG76J:
(C01A 8=81 A (Vi: O<i<N: ??i=in?)Y
(10 A (Vi:			O<i<N: Ai=?)
[Po(Ad?)			II . II PO(AddN?l)]			(10)
(10 A (Vi:			O<i<N: Ai=inj)J
( v WP(P?A?iEV0Vi=Vi1)?
pE8( T01)
Here, each PO(Addj) is the proof outline shown in Figure 2 below, and
10:			_
(Vi: O<i<N: ?CAjCinj)
As=(s'U U Aj) A (Vi: O<i<N: ini=in?)
O<i<N
is an assertion that remains true throughout execution of T0. Variables
A0,.. .,AN?1 are auxiiiary variables [OG76, McC89]. They have type set
and represent the difference between 8 and 51 Since they are used for
purposes of proof only, they need not be implemented.
In verifying serializability of ??, we next prove condition C2.2 of Corol-
lary 2--Hthat T0 terminates when started in a state satisfying Col A A?E v0 Vj =
7
flo A Aj=?
flo A O?<ti<IiniI A ?i=ini(O..ti?1)?
doti#Iinil
flo A O<?4<jifljJ A ?i=ini(O..tj?1)J
( s,Ai:=suina(ti),Aiuini(ti)?;
flo A OSti<Iiflil A Ai=inj(O..tj)J
( t?:=t?+1?
flo A 0< ti < linil A Aj = ini(O..ti?1)J
od
flo A Ai=ifljj
Figure 2: PO(Addj)
v,'. Since the loop in each Addi executes exactly ?flj iterations, Addj ex-
ecutes a bounded number of operations, each of which is an assignment
that is guaranteed to terminate. Consequently, each Addj terminates, and
it follows that T0 terminates.
By Corollary 2, therefore, ?o is a serializable database system. Notice
that an explicit concurrency control mechanism was not needed to achieve
this serializability, even though transactions shared access to variable s.
This, then, illustrates how our work can be used to prove correctness of so-
lutions to the concurrency control problem when the semantics of individual
transactions contribute to the sdution.
The preceding example is misleading. Although effective, the criteria
given by Theorem 1 and its corollary are not practical for verifying serializ-
ability of a database system. For all but the simplest database systems, the
assertions used will be too large for a proof of Ti.1 or C2.1 to be tractable,
due to the number and complexity of serial executions p E S( T'). For ex-
ample, consider the database system ?i of Figure 3. ?i is obtained from
?o by adding variables outb,. . ., OttN?1 and transactions Lis?, . . . , ListN?l
that write the contents of 8 to these variables. The consistency constraint
has been strengthened to require that contents written by a List transaction
contain all or none of the elements being added by an Add transaction. This
has made it necessary to synchronize transactions in order to prevent listing
8 when only part of some ?flj has been added. Synchronization is accom-
plished using locking [KS79, Kor83j. Transactions synchronize by acquiring
8
?i=(Vi:
C1:
Add?:
S,?nO,...,?flN?1,ouo,...,outN?l,
C0 A (Vi,j: O<i,j<N: oit?ninj=in? V Ottiflinj=?)
A (Vi,M: O<i<N: ?tocked(Add?,M) A ?1ocked(List?,M))
T1: [Ad?? ... AddN?l Lis? o+. II Li8tN?lj ?
(lock(S)?;			List?:			(lock(X)?;
(out?:=s?;
doti$Iinil			(unlock(X)?
(8:=sUini(tj)?;
od;
(unlock(S))
Figure 3: Database System ?i.
and releasing a lock, which can have either shared or exclusive mode, denoted
by 5 and X, respectively. An X-lock is incompatible with other locks, so a
transaction attempting to acquire either an 5-lock or an X-lock will block
until no other transaction holds an X-lock.3 To ensure that transactions
terminate when run in isolation, the consistency constraint requires that
transactions hold no locks initially. We denote the fact that a transaction
r? holds an M-lock by the predicate iocked(r?,M).
Corollary 1 requires
?C11A A vi=vs'J7?if V wp(p, A vi=v1f)J
?EVi			PES(T1,)			ViEV1
to be valid. In the postcondition of the analogous triple (9) for T0, all dis-
juncts wp(p, AviE Vo V? = v2,.) were equivalent. For ?i of Figure 3, the number
of different disjuncts will be exponential in N, making it painful to verify.
3.4 Simpler Criteria for Serializability
When transactions are deterministic (as they are in t0 and ?i), simpler
criteria for serializability can be formulated by promoting abstract transac-
tions from their passive role in the postcondition of C2.1 to a more active
3The semantics of operations on a have allowed shared-mode locks to be used in trans-
actions Addj, even though they modify a.
9
one. Let r be a transaction of ? and let r' be the corresponding transaction
of an abstract system for ?. All augmentation of r is a program r* obtained
by substituting (a; r'? for some atomic operation a that runs exactly once
in any terminating execution of r. An augmentation of T is a program
T*: [ro* II			II rN*?1]
in which each T1* is an augmentation of Tj. The following theorem shows
that serializability can be characterized using triples for augmentations.
Theorem 3 Let ? = ( V, C, T? be a database system with deterministic
transactions and let ?` = ( V', C', T') be an abstract system for ?. Let T*
be an augmentation of T using transactions of T'. ? is serializable if
T3.1: fC'A A vi=v2,)T*f A Vi=Vj'?,
?Ev			?Ev
T3.2: term(T,C' A A vi=v?').
ViE V
Proof Due to Corollary 2, it suffices to show that conditions T3.1 and T3.2
imply 02.1 and 02.2. Since T3.2 and C2.2. are identical, it suffices to show
T3.1 and T3.2 imply C2.1.
Assume T3.1 holds and consider a terminating execution of T that starts
in a state satisfying the precondition of C2.1. Any such execution can be
formally represented by a history of the form
o: so4?s1?82...sM?1048M,
where so is the initial state, and ?i--H1 Sj denotes that atomic action a?
transforms state ?i--Hi to state Sj. To show that 02.1 is valid, it suffices to
show that 8M satisfies the postcondition of 02.1.
For any execution a of T, the construction of T* implies that there is a
corresponding history
a*. 8o*?8i*?8;...sM*?ia4*sM*
of T* in which 50* = so and a*s. is either Qj or (a?;r'), where r' is the abstract
transaction used to form the r* that contains a*?. Validity of T3.1 implies
that 8M* satisfies A?i?vVi=Va'
Since V and V' are disjoint, the abstract transactions in a* can be pulled
from their atomic operations and permuted with operations a? to obtain a
history
10
1			? r0, ?
N--Hi
a:			8o'?8i' ? 82'???8M' 1			8M? 8M+1???8M+N-1			8M'+N
of T followed by T' in which 86=80, 8M'+N = 8M* and r6,...,r?' 1 are the
abstract transactions of T' ill the order they appear in a
Transactions are assumed to be deterministic, and the subsequence of
a' from 86 to 8M' has the same initial state and operations as the original
execution sequence a. Consequently, 8M' = 8M The subsequence of a' from
8M' to 8M'+N is one of the p E S( T'). Since 8M'+N = 8M* satisfies AviE v Vj = Vj?
8M' satisfies wp(p, AviE y Vj = Vj'), from which it follows that 8M satisfies the
postcondition of C2.1.			0
The conditions given by Theorem 3 are simpler to verify than those of
Theorem 2 or Corollary 2, due to shorter assertions in the proof of T3.1.
However, this simpllcity has been acquired at the expense of completeness.
The conditions of Theorem 1 and its corollary are equivalent to serializabil-
ity, while those of Theorem 3 only imply it. An example of a serializable
database system for which T3.1 cannot be proven is given in [McC88].
3.5 Example Revisited
Theorem 3 can be used to prove ?? of Figure 3 serializable, as follows. The
following augmentations of each Addi and Listi are used:
Add,*:			List,*:
(lock(S)?;
( t?:=O?;
doti$Iinil
(8:=8Uinj(tj));
od;
(unlock(S);Add,'.?
We first prove T3.1,
(C11A A vi=v,'JTi*(A vi=v,'),
ViE V1			VjEY
using the proof outllne
(lock(X) ?;
(on4:=s;List:');
(unlock(X)')
11
fC11 A AviEViV?=V:'J
?I1 A (Vi: O<i<N: Ai=?J
[Po(Ad?)II... Po(Add)???1)
PO(List0*) I. .11 PO(ListN*?1)]
?I1 A (Vi: O<i<N: Aj=?J
fAviE v1 Vj =
(11)
In (11), PO(Add1*.) and PO(Li&tt*) are the proof outlines shown in Fig-
ures 4 and 5, and 11 is
I0
A(Vi: O<i<N: o?i=ou?)
A (Vi: O<i<N: Aj$? ? locked(Adc4,S))
A(Vi,j: O<i,j<N: ?(1ocked(Add?,S) A tocked(List?,X)))
A(Vi,j: O<i#j<N: ?(1ocked(List1,X) A locked(List1,X)))
Auxiliary variables .0...., AN?1 play the same role here as in the previous
example. The proof of (11) is straightforward and is omitted here.
Condition T3.2 requires T1 to terminate when started in a state satis-
fying C? A A?E ?1 Vj = V,. The argument for this is analogous to that used
to prove termination of ?o except for the possibility of deadlock introduced
by the addition of locking. Deadlock is impossible, however, since locking is
two-phase [EGLT76].
4 Extensions
4.1 Modes of Termination
The database system model presented in Section 2.1 ignores certain aspects
of actual database systems. One of these is the potential for transactions
to abort. An aborting transaction typically executes a recovery protocol in
which operations are run that undo the effects of its changes to the database,
thereby giving the effect that it never ran.
We can incorporate this mode of transaction termination into our system
model by including in each transaction Tj an operation modeling its recovery
protocol and including in V a Boolean variable commit?, initially false, that
Tj sets to true if and only if it terminates without executing its recovery
protocol. This change in the system model necessitates a change in the
12
fri A Aa=? A ?iocked(Add?,S)?
(lock(S));
fli A A1=? A tocked(Add?,S)?
fli A O<ti<Ii%I A Ai=ifli(O..tj--Hi) A tocked(Add?,S)?
doti#Iinil
fli A O<ti<Iinil A Ai=ini(O..ti--Hi) A iocked(Add1,S)?
( s,Ai:=suin?(t?),A?uin1(t?));
fli A O<?ti<IiniI A Ai=iflj(O..tj) A Thcked(Add?,S)?
( t?:=t?+1)
fli A O<4<?IiniI A Ai=ifl:(O..tj--H1) A 1ocked(Add?,S))
od;
fli A Aj=inj A Thcked(Add?,S)J
(unlock(s); Aj ?; Add11.)
fli A Aj=? A ?tocked(Add?,S)J
Figure 4: PO(Add2*)
definition of serializability as well. Our definition specifies in (3) that every
execution of T corresponds to some execution of T'. However, there can
be executions of T in which transactions abort for reasons that are not
encountered in a serial execution (e.g., deadlock), and no execution of T'
wffl correspond to these.
This problem is circumvented by chosing
T11: [ro? II			II
as the abstract concurrent program for ?` (instead of T'), where each trans-
action
r?N:			(if trte .`			skipfi)
executes one of r2, or skip when run, the choice being made nondetermin-
istically. If skip is selected, all variables, including commit:, will be left
unchanged, giving the same effect as if r:. ran but aborted. Every execution
in S( T") will now be equivalent to some serial execution pin the set
SS(T'): f?o;...;??iI0<k<?N,?isatransactionofT',0<i<ky.
13
fli A ?1ocked(List?,X)J
(1ock(X)?;
fil A tocked(List?,X)J
(otttj:=s; Lis??;
fli A 1ocked(List?,X)J
(unlock(X)
fli A ?iocked(List?,X)J
Figure 5: PO(List?*.)
There are several consequences of replacing T' by T". One is that S( T')
must be replaced by SS( T') ill (5) and formulas derived from it. Conse-
quently, all implementation of ? that aborts every transaction will be seri-
alizable under our definition, violating constraints on transaction progress
that are often assumed of databases. This can be avoided by specifying
these constraints ill addition to serializabillty.
Another consequence of using abstract transactions of T" is that even
when transactions of T are deterministic, those of T" are not, and conse-
quently cannot be used in augmentations to prove serializability as described
in Section 3.4. Transactions of T' can still be used in augmentations, how-
ever, as long as each r1, is restricted to positions where it runs if and only if
m commits. The proof of Theorem 3 is virtually unchanged by this restric-
tion, guaranteeing that serializability is still ensured by conditions T3.1 and
T3.2.
4.2 Views
In our definition of serializabillty, the choice of the coupling invariant reflects
an implicit assumption that transaction behavior is characterized by the
entire system state. This may be too strong. Parts of the state of a real
database system will be invisible to users of the system and need not be
included when considering behavior. For example, the set 8 of database ?i
might be implemented nsing an array a that stores elements in contiguous
locations. The order of elements in this array should not be considered when
determining whether or not execution is serializable.
The visible aspects of the database system state are an abstraction of the
system state. This can be modeled by using a function on system states that
14
maps indistinguishable states to a common abstract representation. We call
such a function a view fLLnction. We can incorporate a view function f into
our definition of serializability by replacing the original coupling invariant
A,iEVVi=V:' by A?Evf(Vi)=f(V:') in (3), together with formulas derived
from it.
5 Discussion
We have defined serializability in terms of concurrent execution of transac-
tions implementing serial execution. By choosing an assertional character-
ization of "implements", serializability was expressed using Hoare's logic.
This makes it possible to verify concurrency control mechanisms using that
logic.
There are many other definitions of serializability [Pap86J. What most
of these definitions have in common is that serializability is defined as a
property of system schedules, sequences of operations resulting from partic-
ular system executions. Schedule-based definitions of serializability fall into
two broad categories based on how schedule behavior is characterized: state
based and conflict based.
In state-based definitions, system behavior is described in terms of how
schedules transform one state to another. Definitions differ with respect
to the parts of the state considered significant. A schedule is final-state
serializable if it and some serial schedule transform identical initial states to
final states that agree on the value of all shared variables. A schedule is view
serializable if the final states agree on the values obtained by read operations
as well. Both final-state and view serializable schedules can be expressed by
our definition of serializability by suitable choice of system variables.
Conflict-based definitions of serializability describe behavior somewhat
indirectly, using conflict relations (also known as dependency relations) on
operations of the schedule. An operation a1 conflicts with another oper-
ation a2 in the same schedule (written al <a2) if (i) the operations are
from different transactions, (il) a1 precedes a2, and (iii) a1 and a2 do not
commute with each other (i.e., the same initial state can produce different
final states when the operations are run in different orders). The conflict
relation on operations is extended to one on transactions. This, then, is
used to determine the set of serial schedules exhibiting the same behavior: a
schedule is conflict serializable if it and some serial schedule have the same
conflict relation on transactions.
15
?2=(V2:			(x,y,out,b?,
C2: O<b<1 A x+y=1OO,
T2: [UpdatexY ListX]
UpdateXY: Qo:
ListX: ?0:
Figure 6: Database System ?2
(x,y:=x+b*17,y--Hb*17);
a?:			(x,y:=z+b*17,y--Hb*17?
(out z)
Because schedule-based definitions of serializability consider operation
sequences and system states independently, some database systems consid-
ered serializable under our definition are not considered serializable by the
schedule-based definitions above. The (somewhat contrived) database sys-
tem ?2 of Figure 6 is an example. There, variables x, y, and out hold integer
values, while b holds a binary value. Transaction UpdateXY subtracts 17
from y and adds it to x, using the value of b to control the order in which this
occurs. (b denotes the complement of b.) Using the techniques of Section 3,
it is not difficult to prove ?2 serializable according to our definition.
Consider the schedule
a0;P0;a1.			(12)
Note that the value read by ListX depends on the state in which execution
begins: out gets the same value as it does from the serial schedule oto; a1; p0 if
b =1 initially, while out gets the same value as from Po; a0; a1 if b = 0. Thus,
schedule (12) is neither final-state nor view serializable since these require
(12) to "behave like" one of the serial schedules for all initial states. Nor is
(12) conflict serializable, since the conflict relation on UpdateXY and ListX
has a cycle. Thus, although ?2 is serializable according to our definition, it
is not serializable by the schedule-based definitions of serializability.
In [Cas81], a definition of serializability similar to ours is given. This
definition uses operators of Concurrent Dynamic Logic (CDL) instead of
weakest preconditions to express the "implements" relationship between T
and its serial model T'. Our definition is more general than the CDL defi-
ultion, however, because the coupling invariant can be written in terms of a
view function. Our definition also provides more useful criteria for verifying
serializability, since Hoare's logic offers a variety of formal techniques for
deriving and verifying triples that CDL currently lacks.
16
Acknowledgment
David Gries and Phil Hutto read and provided helpful comments on an
earlier version of this paper.
References
[Cas81]
M. Casanova. The Concurrency Control Problem for Database
Systems, volume 116 of Lecture Notes in Computer Science.
Springer-Verlag, New York, New York, 1981.
[Dii76] E. W. Dijkstra. A Discipline of Programming. Prentice Hall, In-
glewood, New Jersey, 1976.
[EGLT76] K. P. Eswaran, J. N. Gray, R. A. Lorie, and I. L. Traiger. The
notions of consistency and predicate locks in a database system.
Communications of the ACM, 19(11):624?33, Nov. 1976.
[GP85]
D. Gries and J. Prins. A new notion of encapsulation. In Proceed-
ings SIGPLAN Symposium on Language Issues in Programming
Environments, pages 131--H139, Jun. 1985.
[Hoa69] C. A. R. Hoare. An axiomatic basis for computer programming.
Communications of the ACM, 12(10):576--H580, Oct. 1969.
[Hoa72] C. A. R. Hoare. Proofs of correctness of data representations. Acta
Informatica, 1:271--H281, 1972.
[Kor83] H. F. Kortli. Locking primitives in a database system. Journal of
the ACM, 30(1):55--H79, Jan. 1983.
[KS79]
Z. Kedem and A. Silberschatz. Controffing concurrency using lock-
ing. In IFEE Foundations of Computer Science, pages 274--H285.
IEEE, 1979.
[Lam88] L. Lamport. A simple approach to specifying concurrent systems.
Communications of the ACM, 32(1):3245, Jan. 1988.
[McC88] E. R. McCurley. An Assertional Characterization of Serializability
and Locking. PhD thesis, Cornell University, 1988.
17
[McC89]
[MP81]
R. McCurley. A valid rnle for au::li?ary variable transformations.
Technical Report GIT-ICS-89/11, Georgia Institute of Technology,
1989.
Z. Manna and A. Pnueli. Verification of concurrent programs, part
I: The temporal framework. Technical Report STAN-CS-81-S36,
Stanford University, 1981.
[OG76] 5. 5. Owicki and D. Gries. An axiomatic proof technique for par
allel programs. Acta Informatica, 6:319--H340, 1976.
[Pap86] C. H. Papadimitriou. The Theory of Database Concnrrency Con-
troL Computer Science Press, 1986.
[Pnu8i] A. Pnueli. The temporal semantics of concurrent programs. The-
oretical Computer Science, 13:4560, 1981.
[Pri87] J. F. Prins. Paflial Impiementations in Program Derivation. PhD
thesis, Cornell University, 1987.
18