An Assertional Characterization of Serializability and Locking* Ernest R. MoCurley Ph.D. Thesis 88-894 January 1988 Department of Computer Science Cornell University Ithaca, NY 14853-7501 *This material is based on work supported in part by the Office of Naval Research under contract NoOOi4-86-K-0o92 and the National Science Foundation under Grant No. COR-87o1 103. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author and do not reflect the views of the Office of Naval Research or the Nationa Science Foundation. AN ASSERTIONAL CHAR?ACTEMzATIoN OF SERIALIZABILITY AND LOCKING A Thesis Presented to the Faculty of the Graduate School of Cornell University in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy by Ernest Robert NicCurley January 1988 Oc Ernest Robert McCurley 1988 ALL RIGHTS RESERVED An Assertional Characterization of Serializability and Locking Ernest Robert McCurley, Ph.D. Cornell University t988 The problem of synchronizing transactions in a database system so that concurrent execution transforms the system from one consistent state to another is called the Con- currency Control Problem. Over the past 20 years, a property of concurrent execution called serializability has evolved as a universal paradigm for solving the Concurrency Control Problem. Up until now, most work on serializability has been characterized by an emphasis on sequences of operations. Researchers studying programming logics and methodologies have developed a different approach to characterizing the semantics of concurrent programs. This approach is called assertional reasoning, and emphasizes the system state instead of sequences of operations. This dissertation describes the ex- tension of the formalisms and tools of assertional reasoning to the Concurrency Control Problem. Proposed is a definition of serializability that generalizes previous definitions in many respects. Two methods are described by which this definition of serializability can be specified in an assertional programming logic using formulas called proof out- lines. As a consequence of specifying serializability with proof outlines, it becomes possible to formally verify serializability. The use of an assertional programming logic eliminates the need to explicitly consider transaction interleavings, simplifying verifica- tion. Another consequence of specifying serializability with proof outlines is the ability to derive synchronization protocols for serializability. This possibility is realized in the form of a method for deriving locking protocols from assertional specifications. The method is based on a novel view of locking, in which locks held by transactions reflect properties of the system state. Using this method, semantic information available dur- ing the derivation process can be used to obtain locking protocols permitting greater concurrency among transactions than locking protocols obtained by more traditional methods. Examples are given throughout the dissertation to illustrate the methods described. Biographical Sketch Rob McCurley was born on July 5th, 1958, in a suburb of Los Angeles, California, third child and only son of loving parents Ernest and Alice McCurley. In his first year o+ of life, he moved with his parents to Atlanta, Georgia, where he grew up in the heart of the New South. He graduated from Peachtree High School in the spring of 1976. In the fall of 1976, he enrolled at the University of Georgia. There, he studied mathematics and fell in love with his future wife, Janet Bless. The university awarded him a B.S. in Mathematics, magna cum laude, in spring of 1980. He enrolled as a graduate student at Cornell University in the fall of 1980, where he studied the science of computers and learned the true meaning of winter. On the happy day of March 27,1982, he and Janet were married. Cornell awarded him a M.S. in Computer Science in 1983. 111 To Janet. lv Acknowledgement s I would like to thank Fred Schneider for his immeasurable contributions to both the form and content of this dissertation. As my advisor, Fred has spent much time and effort trying to teach me how research is conducted. I hope he realizes how much I appreciate his patience. I would also like to thank the other members of my special committee, John Hopcroft and Richard Shore, for their time and helpful comments on early drafts of this dissertation. I am grateful for the support of the Office of Naval Research under contract N00014- 86-K-0092 and for the support of the National Science Foundation under Grant No. CCR-8701103 during the course of this research. There are many people I would like to thank for their friendship. In particular, I would like to thank Tim and Jeanne Lansing for moral support, traveler's assistance, and restraint in harassing me; Doug and Maureen Howe for many pleasurable evenings of dinner and conversation; and Jacob Aizikowitz for listening to my musings and grumblings about research and other topics. Finally, I would like to thank my family, especially my parents. Though they must have thought I was crazy at times, they loved and supported me when I doubted v myself. However, the person I am most grateful to is my wife Janet. Her love and encouragement have meant everything to me; without them, I would have given up long ago. vi Table of Contents 2 Introduction 1.1 Consistency and Concurrency 1.2 Serializable Schedules 1.3 Related Work 1.3.1 Operation Types 1.3.2 Transaction Synchronization 1.3.3 Locking 1.3.4 Definitions of Serializability 1.3.5 Alternatives to Serializability 1.4 Reasoning About Concurrency 1.5 Overview of Dissertation 2.7 2.8 3 Serializability 2.1 Database System Model 2.2 Serializability 2.3 Serializability with Proof Outlines 2.4 An Example 2.5 A More Tractable Method . . 2.6 Examples of the Second Method . 2.6.1 An Alternate Proof of Serializability for ?1 . 2.6.2 Sequence Variables with Set Semantics . Incompleteness of the Second Method for Proving Serializability Discussion. . . 2.8.1 Comparing System Models 2.8.2 Comparing Definitions of Serializability . . Deriving Locking Protocols 3.1 Proofs of Concurrent Programs 3.2 Interference and Synchronization 3.3 Exclusion Invariants 4 6 7 7 9 9 11 14 16 19 20 20 24 27 38 49 54 54 58 62 65 65 65 70 71 73 75 vii 3.4 3.5 3.6 Using Locking to 5trer'gthen Assertions Selectively An Example . . Discussion . . . - 3.6.1 Comparing Locking Protocols . . - 3.6.2 Locks and Local State . Concluding Remarks 4.1 Summary and Discussion 4.2 Topics for Further Research 4 A Axioms and Inference Rules of Proof Outline Logic B The Weakest Precondition Predicate Transformer Bibliography 78 83 o+ - 103 103 - - 105 107 - - 107 110 112 116 120 vii' List of Figures 1.1 Deposit and Interest Transactions. 2.1 2.2 2.3 2.4 2.5 2.6 2.7 2.8 2.9 2.10 3.1 3.2 3.3 3.4 3.5 3.6 3.7 3.8 3.9 3.10 3.11 3.12 3.13 Database System ?O. Synchronized Database System V?1 Proof Outline Po(r:) Augmented Database System ?1* Proof Outline Po(r?). Database System ?2. Augmented Database System ?2*. Proof Outline for Po(r:.) for Tt* of ?? Database System ?3. Database System ?A 5 Database System V?5 for an Idealized Banking Application. Synchronized Database System (A6,?6?. Augmented Database System VJ;* Version 1 of PO(r?) . . . . . Version 1 of PO(r1*) Version 2 of ?(;* . . . Version 2 of PO(r0*) . . . Version 2 of PO(r1*). Version 3 of A6 . . . . . Version 3 of ?(3* Version 3 of PO(m*) . . . . . Version 3 of PO(rf). Serializable Database System (A6,vJ;?. . . Ix 23 42 45 55 58 59 60 61 63 66 85 86 87 89 89 92 93 94 97 99 101 102 104 Chapter 1 Introduction Many computer applications involve information that must be stored, retrieved, and modified. For example, a bank must maintain customer account balances and update them as deposits and withdrawals are made; a university must record information about course offerings and student grades Database systems are computer systems that store and maintain large amounts of information. Information in a database system is typically stored on magnetic disk storage devices rather than in primary memory because of their high capacity for data storage and relative involatility. It is accessed through one or more processors ?onnected to these storage devices. Information stored in a database can be viewed as modeling some aspect of the application it supports. For example, a banking database system might store a list of numeric values to model balances of customer accounts. As events, such as deposits and withdrawals, transform the application state, the database state is transformed 2 accordingly by running programs called transactions. The correspondence between an application and a database system imposes certain restrictions on the database system state. A bank might require account balances to be non-negative, which restricts the stored values that model these balances to be ?on-negative. Restrictions imposed by an application on the database system state are called consistency constraints. A consistency constraint can be thought of as a predicate on the database system, although in practice such predicates are often too complex to be written explicitly. States that satisfy the consistency constraint are called consistent states. Database systems are started in a consistent state and transactions are constructed so that they model the events to which they correspond, thereby guaranteeing that each transaction individually will transform the system from one consistent state to another. A serial e?ecution of transactions is one in which transactions are executed one at a time, starting one only after the preceding one competes. By a simple inductive argument on the number of transactions, any serial execution will transform the system from one consistent state to another. Concurrent execution of transactions, in which one or more transactions are started b1efore previous ones complete, has an advantage over over serial execution. In some systems, a large portion of transaction execution time is spent waiting for responses from relatively slow 1/0 devices (such as a user terminals or storage devices). By running transactions concurrently, the time that one transaction spends waiting can be used to run operations from another transaction that is not waiting, thereby increasing the rate at which transactions are processed. 3 Unfortunately, without synchronization, concurrently executed transactions can in- terleave in ways that leave the database in an inconsistent state. The problem of syn- chronizing transactions so that concurrent execution transforms the system from one consistent state to another is called the Concurrency Control Problem. Over the past 20 years, a property of concurrent execution called serializability has evolved as the basis for solving the Concurrency Control Problem. Until now, however, most work on serializability has been characterized by an emphasis on sequences of operations. The definition of serial execution of transactions is an example of this style of characteriza- tion. The view that locking protocols exclude operations from executing concurrently is another example. A different approach to analyzing the semantics of both sequential and concurrent programs has been developed by researchers studying programming logics and method- ology. The approach is called assertional reasoning and emphasizes system states rather than operation sequences. This thesis describes the application of assertional reason- ing to database systems. We give an assertional characterization of serializability; it generallzes previous definitions of serializability. Our approach to defining serializabil- ity not only allows the correctness of synchronization protocols for serializability to be proven formally, but also allows semantics of an application to be incorporated into the - derivation of synchronization protocols that allow a high degree of concurrency among transactions. We illustrate this benefit by giving an assertional characterization of locking and a method for deriving locking protocols from specifications. 4 1.1 Consistency and Concurrency A simple example illustrates the Concurrency Control Problem. Consider a database system that models bank accounts numbered from 0 to N. The database stores account balances as values in an array a[O.. NJ, with a[iJ holding the balance of account number i Another variable ba holds the value of bank assets. As is typical of database systems, these values are stored on magnetic disk. Disk drives typically provide two types of operations for accessing values: read and write. Let r(?,t) denote a read operation that copies the value of z (stored on disk) into a computer memory location denoted t; let w(x,e) denote a write operation that evaluates expression e involving values in computer memory and copies the resulting value back to x on disk. The requirement that bank assets match the amount deposited in accounts induces a consistency constraint ba ? a[iJ, specifying that ba equals the sum of values in a[O.. NJ. As customers make deposits and transfer funds within accounts, transactions must be run to update the values in a[O. NJ and ba while leaving the system in a consistent state. Using read and write operations, the transaction DEP(a[iJ,x) of Figure 1.1 incre- ?ents a[iJ and ba to reflect a deposit of amount x to that account. The transaction reads the balance of a[iJ into memory and writes the updated balance back, sub- sequently updating ba in the same way to ensure that the consistency constraint will hold afterwards. In a similar manner, transaction INT(a[j],y) of Figure 1.1 increments a[jJ and ha by y*a[jJ, reflecting the accumulation of interest at rate y by account 5. 5 DEP(a[ij,x): r(ati],tO); INT(a[jJ,y): ?(a[j],t2); w(a[ij,tot z); w(a[j],t2+y *t2); r(ba,t1); r(ba,t3); w(ba,t1?x) w(ba,t3+y*t2) Figure 1.1: Deposit and Interest Transactions. Suppose that a deposit of d to account s is made at about the same time interest at rate r is begin credited to that account. If DEP(a[sj,d) and INT(a[sJ,r) run concurrently and without synchronization, transaction operations can interleave in the following order: aO: r(a[s],tO); r(a[sJ,t2); w(a[s],tot d); w(a?],t2tr*t2); r(ba,tl); w(ba, tit d); r(ba,t3); w(ba,t3sr*t2). A sequence of transaction operations like ?O that denotes an interleaving resulting from concurrent execution is called a schedule. The use of the statement composition oper- ator ";" between operations allows the schedule to be viewed as a sequential program having the same effect as the particular concurrent execution it is modeling. When con- current execution produces schedule cTO, the update w(a[s],tO+d) by DEP(a[sj,d) is overwritten by INT(a[s],r), effectively losing the deposit into a[sj. As a consequence, ff0 will leave ba d + ? a[i], an inconsistent state. 6 1.2 Serializable Schedules As ff0 illustrates, not all schedules in which transactions interleave transform a database system from a consistent to an inconsistent state. One type of schedule that preserves consistency is a serializable schedule. A serializable schedule is one that "behaves like" some serial schedule--Ha schedule that denotes a serial execution of transactions.1 Since serial execution of transactions transforms a database from one consistent state to another, execution resulting in a serializable schedule will do so as well. An example of a serializable schedule of DEP(a[sJ,d) and INT(ats],r) is ff1: r(a[s],tO); w(a[s], tO + d); r(a[s],t2); w(a[sJ,t2+r* t2); r(ba,ti); w(ba,ti+d); r(ba,t3); w(ba,t3+r*t2). For any given initial values of a[O. NJ and ba, ff1 leaves the same final values as the serial schedule 1We describe more formally what it means for one schedule to "behave like? another in Section 1.3.4. 7 a2: r(a[s],tO); w(a[sl, to s d); i'(ba,tl); w(ba,tl ?d); r(a[s], t2); w(a[s],t2+r*t2); r(ba,t3); w(ba,t3tr*t2). The consistency-preserving properties of senalizable schedules imply that the Concur- rency Control Problem can be solved by synchronizing transactions to ensure that every schedule is serializable. 1.3 Related Work A great deal of research has been published about serializability. Several different database models have been considered and several different definitions of serializability have been proposed. 1.3.1 Operation Types One way in which database system models differ is in the types of operations that dan be used to construct transactions. Many models [BBGLS83,BC83,BG8?,BSW79, GW82,G83,G78,P79,R83,SLR76,T585,Y84] assume that transactions are constructed from read and write operations as the ones described in Section 1.1 were. This reflects the use of storage devices, such as disks, that implement these operations in hardware. More recently, models have been devised for systems that support operations other than read and write. For example, a model with operations that traverse and manipulate 8 search structures is considered in [GS85j and one with operations on abstract data types such as queues and sets is considered in [SS84J and [W84]. The model of [K83] does not place any restrictions at all on the operations from which transactions are constructed. Although system models with a greater variety of operations tend to make analysis of concurrent execution more complicated than in read-write models, they do make it possible to describe more accurately the semantics of concurrent execution. Many models also make assumptions about the way operations are ordered within transactions. In ?P79] and ?BSW79J, for example, transactions consist of a single read operation followed by a single write operation, each of which accesses several variables at the same time. In [Y84], transactions can contain several read and write operations but the operations are assumed to be ordered so that no transaction writes to the same variable twice or reads a variable it has previously written. Such restrictions on transaction structure simplify analysis. In addition to assumptions about organization, different models make different as- sumptions about the degree to which semantics of individual operation are known. In [P79J, only the set of variables accessed by a write operation is considered when ana- lyzing its behavior; the function used to compute the value it stores is left unspecified. The same is true in [Y84j. In contrast, the models of [SS84j and [W84j specify not only the variables that operations access, but also details of how these operations transform these variables from one state to another. As with restrictions on operation type and order, weaker assumptions about operation semantics simplify analysis of concurrent execution. However, models that make stronger assumptions about semantic infor- mation allow use of this information when deriving synchronization for serializability, 9 usually allowing more concurrency than models that make weaker assumptions. 1.3.2 Transaction Syncbronization Another area of difference in various database system models is the way in which trans- action synchronization is represented. In some models, synchronization is implicit--H transactions do not execute synchronizing operations directly but send requests for operations to a system process called a schedule? [P79J. The scheduler considers the history of requests when deciding whether to delay or grant a pending request. An ex- ample of implicit synchronization is timestamp o?ering [BG81j, in which a timestamp is assigned to each transaction as it begins to execute. Each request submitted to the scheduler is marked with the timestamp of the transaction submitting it. The scheduler then uses these timestamps to order requests. In other database system models, trans- action synchronization is ezplicit--Hsynchronizing operations appear among transaction operations for manipulating data. 1.3.3 Locking A form of synchronization used in many database system models is locking [G78,K83, Y84,KS79j. In database systems that use locking for synclironization, transactions ,?cquire and release entities called locks. In some systems using locking, transactions explicitly execute operations to acquire and release locks, while in others, locks are acquired and released implicitly as transactions execute operations. A locking protocol characterizes how locks can be used to synchronize transactions. A locking protocol specifies to 0 a set of possible modes, or types, that locks can have, 0 a compatibihty relation indicating what locks can be held concurrently, and 0 a set of locking rules transactions must follow when acquiring and releasing locks. Synchronization results from mediation of lock acquisition and release requests ac- cording to the compatibility relation, delaying requests that are inconsistent with the compatibility relation. Previous research on synclironization in database systems has focused on developing locking protocols that allow as much concurrency as possible among transactions, but restrict possible schedules to serializable ones. Several protocols have been proposed. One area of difference between them is the set of lock modes assumed. The set of lock modes is usually derived from the set of operations that the database system model permits. Each lock mode typically specifies the operation with which it is associated and the process that has acquired it. Lock compatibility relations have traditionally been derived from the semantics of the operations with which they are associated. Exclusive locks are used whenever the net effect of concurrently executing transactions can depend on how operations of a par- \icular type interleave. For example, the value left in a[s] by transactions DEP(a[sJ,d) and INT(a[sJ,r) of Section 1.1 depends on how the write operations w(a[s],t0?d) and w(ba,titd) in DEP interleave with w(a[sJ,t2$r*t2) and w(ba,t3+r*t2) in INT. Consequently, the lock mode associated with write operations would by exclusive. If both transactions consisted of only read operations, every interleaving would produce the same result, which implies that the lock mode associated with read operations need l1 not be exclusive. Locking rules for acquiring and releasing locks generally require a transaction to have acquired and not yet released a lock for an operation before it can execute that operation. Several additional restrictions on lock acquisition and release have been proposed. For example, lock acquisition and release is often required to be two-pha?e [ECLT76J, which means that a transaction never acquires additional locks once it has released any lock. This divides transaction execution into a lock acquiring phase and a lock releasing phase. A two-phase locking rule is shown to be sufficient to guarantee only serial schedules for the model used in [EGLT76]. The necessity of two-phase locking in the absence of restrictions on transaction structure is also discussed there. In models where more is known about the structure of access to data, locking rules that are not two-phase have been proposed. In [BS77j, for example, a protocol for transactions that traverse and modify B-trees that does not obey the two-phase restriction on lock acquisition and release is presented. This approach is generalized in [GS85] to obtain locking rules that are not two-phase when transaction operations are structured to traverse more general types of linked data structures. .3.4 Definitions of Serializability As with database system models, several different definitions of serializability have been proposed. These definitions differ primarily in the formal definition of when a schedule "behaves like" a serial schedule. One of the earliest formal definition of serializability, found in [EGLT76j, falls into 12 a class of definitions that has subsequently been called conflict serializability [P86J. In conflict serializability, behaviors of schedules are compared according to certain conflict relations that they induce. A schedule a induces the conflict relation CRj on pairs of operations in a, where (a?,a1) ? CR? if and only if aj and a? are from different transactions, aj appears before a? and both operations cannot be run in the other order and produce the same result. The conflict relation CR? is extended to transactions by defining (ri,rj) E CRff if and only if (aj,a1) c CR? for some operation aj from Tj and a? from Tj. A conflict relation CR? reflects the potential for one transaction to influence the behavior of another in the concurrent execution represented by the schedule a. Thus, the behavior of two schedules can be compared by comparing there associated conflict relations. Two schedules a and a1 are conflict equivalent if and only if CRff and CRji are the same relations on transactions. A schedule a is conflict serializable if and only if it is conflict equivalent to some serial schedule a1. An equivalent definition sometimes given is that a is conflict serializable if and only if CR? is acyclic, since this ensures at least one serial schedule shares the same conflict relation. As the second formulation of conflict serializability illustrates, whether or not a ?articular schedule is conflict serializable depends directly on the strength of the conflict relation: the more conflicting operations there are in a schedule a, the more likely CR? is to contain a cycle and hence fail to be conflict serializable. For this reason, operation semantics are used to define conflict relations that relate as few operations as possible. In models with read and write operations, the conflict relation is defined so that (a?,a1) E CRff whenever aj and a? reference the same variable and at least 13 one is a write operation. This is because pairs of operations on different variables or pairs of operations that only read the same variable cannot influence each other. In models such as [K83] and [GS85], the greater degree to which operation semantics are specified permits weaker conflict relations to be specified. For example, two operations that change the value of the same variable do not necessarily conflict as they would if they were simply considered to be instances of write operations. Another class of serializability definitions involves those that compare schedules on the basis of how they transform a system from one state to another. This class is sometimes subdivided into finai-state serializability and view seriaiizability [P86j In both of these subclasses, a schedule "behaves like" another if and only if both transform identical initial states to identical final states. However, final-state and view serializability differ as to what portion of the system state is used to compare the effect of schedules. In the definition of final-state serializability found in [K83J, system states are corn- pared according to the value of only those variables that are shared by transactions. However, it is argued in [Y84] that final-state serializability is inappropriate for mod- els in which transactions contain read operations because it ignores the values copied into a transaction's local storage by read operations and does not take into account - the possibility that transactions might read inconsistent values and behave erratically or present inconsistent output to users of the database system. View serializability is therefore proposed in [Y84] as a more appropriate definition of serializability. When comparing the effect of schedules, view serializability includes in the system state the values read by transactions in addition to the values of shared variables. 14 In [P79j, the relationship between conflict and view serializability is explored. It is proven that every conflict-serializable schedule is also view serializable. In light of this result, view serializability would seem to be a preferable definition because of its generality. However, it is also shown in [P79j that the complexity of the general problem of deciding whether a schedule is view serializable as a function of its length is NP-complete. This makes it improbable that efficient algorithms can be constructed for synchronizing arbitrary sets of transactions. Because a schedule can be determined to be conflict serializable in time polynomial in its length, conflict serializability is more often used in practice as the basis for concurrency control. 1.3.5 Alternatives to Serializability Some have suggested that requiring every schedule to be equivalent to some serial schedule is too strict a requirement for database systems (e.g. [L76]). The Concurrency Control Problem requires only that transactions transform the database system from one consistent state to another. Every serializable schedule will accomplish this, but in some cases there may be non-serializable schedules that do so as well. An alternative is proposed in [G83]. There, every schedule is required to be se- manticatty consistent rather than serializable. A schedule CT is semantically consistent CT transforms the system from one consistent state to another, and o+ there is a serial schedule CT? such that for every initial consistent state, CT and ?? leave the same values in a specified set of RS variables (for Requiring Serializab- ility). 15 Since the RS variables need not include every variable of the consistency constraint, the first requirement is not redundant. This approach has the advantage of allowing more concurrency than if schedules are required to be serializable. A simple example of a database system that models an airline reservation system is given in [C83] to illustrate this. The system contains four variables SX, SY, TX and TY. The value of SX denotes the number of passengers on a flight FX, while TX denotes the type of plane scheduled to handle that flight: either "small" or "large". Variables SY and TY denote the same information for a flight FY. The consistency constraint for the system is (SX>1OO? TX--H"larg&')A(SY>lOO? TY--H¶arg&'). The RS variables are SX and SY Two transactions are considered, one that reserves a seat on both flights: RX Y: Ri: Increment SX by 1. If SX ? loo, change TX to "large". R2: Increment SY by 1. If SY > loo, change TY to "large". and one that cancels a seat on both flights: CXY: Ci: Decrement SX by 1. C2: Decrement SY by 1. ?uppose that both RXY and CXY run concurrently in an initially consistent state with SX SY 99 and TX TY "small" producing the schedule ?3: Ri, Ci, C2,R2. This schedule will leave SX SY 99, TX "large" and TY "small", which is also a consistent state. It also leaves the RS variables SX and SY with the same values as 16 either of the two possible serial schedules. Consequently, a3 is semantically consistent. However, ff3 is not serializable under any of the definitions described previously and would not be allowed in a database system requiring serializability. Thus, an advantage of replacing serializability by the weaker requirement of semantic consistency is that more concurrency among transactions is possible. A disadvantage of this approach is that analysis of synchronization requirements for semantic consistency can be more complicated than for serializability because of the details of the consistency constraint and operation semantics that must be considered. 1.4 Reasoning About Concurrency A database system can be viewed as a concurrent program a collection of sequential programs that run concurrently. Properties of concurrent programs can be viewed in terms of safety and tiveness. A safety property is one that specifies that one of a given set of "bad" states is never reached. An example of a safety property is partial correctness, which says that execution that begins in one of a given set of initial states does not terminate in a state outside of a given set of final states. A liveness property is one that specifies that some set of "good" states are eventually reached. An example of a liveness property is termination, which says that execution that begins in one of a given set of initial states eventually terminates. As the schedules considered previously indicate, execution of a concurrent program can produce any of a number of different interleavings of its constituent operations. The interleavings that are possible depend on the atomic operations that constitute the concurrent program. An atomic operation is one that indivisibly runs to completion 17 once started. Following [L8oj, an atomic operation that executes program text S is denoted (S ?. In the sequel, we will write S in Guarded Command Notation [D76] but require that 3 is deterministic. For all but the simplest concurrent programs, the number of different schedules is apt to be too large for safety and liveness properties to be verified by considering every possible schedule. To address this problem, a more tractable approach to reasoning about concurrent programs has been developed. It is based on the use of a formal logical system relating program behavior to predicates on program states. Proof Outline Logic [SA87] is one programming logic for expressing and proving safety properties of concurrent programs. A proof ontiine is a formula fQ?StR1 where Q and R are predicates on the system state and are called assertion?; 3 is an annotated program, a program in which each atomic operation (a is preceded by zero or more assertions. An assertion that immediately precedes (a? in the proof outline is called the precondition of (a) and is denoted pre( (a)). An assertion that immediately follows (a) is called the postcondition of (a) and is denoted post((a)). A proof outline f Q) 3 fR? specifies the safety property that if 3 is started at some &tomic operation (a) in a state that satisfies pre((a)), then at any point reached during execution, the state will satisfy the assertion or assertions that appears at that point. Proof Outline Logic provides a set of axioms and inference rules for inferring valid proof outlines. These axioms and rules include those of Predicate Logic [S67] along with axioms and rules given in [SA87] that are specific to Proof Outline Logic. A summary of these rules can be found in Appendix A of this dissertation. 18 Dijkstra's weakest precondition predicate transformer [D76J, a function that maps one assertion to another, is often used in conjunction with Proof Outline Logic to reason about programs. For S an operation or program and R a predicate, the predicate wp(S,R) (read the weakest precondition of S with respect to R) denotes the largest set of states in which execution of S is guaranteed to terminate leaving R true. From the semantics of proof outlines and wp, it follows that fwp(S,R)?S fRJ is a valid proof outline for any S and R. Thus, a precondition of S that allows a given postcondition R to be asserted can be computed using wp. A summary of general properties of wp along with rules for computing wp(S,R) can be found in Appendix B. Assertionai reasoning is the name given to the style of characterizing program semantics in terms of assertions on the program state. When compared to other ap- proaches to reasoning about concurrent programs, an apparent disadvantage of asser- tional reasoning is the level of detail at which the analysis is carried out. Of course, this is also an advantage since it is possible to capture detailed semantic information that is ignored in other formal systems. Another advantage of assertional reasoning is that properties of concurrent programs are often specified most naturally in terms ?f properties of the states reached during execution. For example, a solution to the Concurrency Control Problem requires every execution that begins in a consistent state to leave a consistent state. This is an assertional property since it specifies a prop- erty of the system state (consistency) at points during execution (before and after). Yet another advantage of assertional reasoning is the ability not only to prove that a given program satisfies a particular specification, but also to derive programs from 19 their specification, using the inference rules of the logic to motivate refinement of the program. 1.5 Overview of Dissertation This thesis describes the application of assertional reasoning to the Concurrency Con- trol Problem. Chapter 2 presents a new definition of serializability that is based on assertional reasoning and generalizes previously proposed definitions in several respects. A method for using Proof Outline Logic to specify and prove that database systems satisfy this definition of serializability is then presented. Chapter 3 presents an as- sertional view of locking and describes a method for deriving locking protocois. This method is then used to derive synchronization for a database system modeling a sim- ple banking application. Finally, Chapter 4 summarizes the thesis and draws some conclusions from the research presented here. Chapter 2 s erializability As discussed in Section 1.3, there is no standard system model or definition of serial- izability. In this chapter, we describe the system model used in the remainder of this dissertation. We then propose a definition of serializability that generalizes previous definitions of serializability in several ways. Finally, we demonstrate how this definition can be formulated in Proof Outline Logic. 2.1 Database System Model Concurrent execution of a set of transactions T0,. . - ,TN?1 is denoted cobegin r0 o+. II rN?1 coend. (2.1) A necessary condition for an atomic operation (S? in (2.1) to run is that it be enabled, which means that the control point before (S has been reached and the system state be one in which S will run to completion. During execution of (2.1), however, it is possible for more than one operation to be enabled at the same time. Consequently, a scheduling 20 21 policy must be given to specify how operations are selected for execution from among those that are enabled. We will assume in the remainder of this dissertation that concurrent execution of transactions follows a weakly fair scheduling policy [SA87]--H no operation that becomes and remains enabled will be forever delayed. Execution of (2.1) terminates when every transaction has terminated. A transac- tion r? can terminate in two ways. One is for r? to complete by executing an operation (end(r?)) and halting. The other way in which Tj can terminate is to abort. A trans- action aborts when conditions such as deadlock, system failure, or unexpected input make it undesirable or impossible for it to complete. Tj aborts by executing an op- eration (abort(r?)? and halting. Operation (abort(rj)? typically implements recovery operations to cancel the effect of operations previously executed by Tj. A database system ? can be specified by a 4-tuple (V, C, T,z?, where V (v0,... ,v?? is a vector of variables, C is a predicate on V, T fro,. . . ,TN?IJ is a set of sequential programs and _ is an equivalence relation on the domain of V (the cross product of the domains of the variables of V). Variables of V characterize the state of ?. Any system state can be written as a vector of constants V' (v01,... ,v?1?, where each v: is the value of the corresponding variable Vj in that state. For any predicate P on V, P is true in state V' if and only if PvV1 true.1 Predicate C in the specification of ? is a predicate that implies the consistency constraint of ?; a state is consist?nt if C is true in that state. Each Tj E T models a transaction of ?. An e:ecution of ? is an execution of the concurrent program lp?o?t denotes the result obtained by simultaneously replacing all occurrences of v? by the corre- e0 sponding e??. 22 cobegin To I - - - I TN?1 coend, (2.2) and a schedule of ? is the sequence of atomic operations resulting from a terminating execution of (2.2). We assume that each Tj will complete leaving C true when executed in isolation starting with C true. For each r? C T, we will assume that V contains a \`oolean variable cfj, called the completion flag of Tj, such that cfj true if and only if Tj has completed. This models information that is typically found in system logs. The equivalence relation in the specification of ? is a binary relation on the domain of V and partitions the states of ? into equivalence classes. Each equivalence class contains the states that cannot be distinguished from one another by the appli- cation supported by ?. This provides an abstraction that hides aspects of the system state that are irrelevant to the application being supported. To limit the amount of information that can be hidden _ is requires to satisfy two adequacy constraints: ACi. For all system states ?? and V11, (V'--H--H V") ? (Vi: 0 ? i ? N: cf?' cf?11). AC2. For all system states V' and V11, (V'=--H V11)?(cvV??cvV11). ACi ensures that states in which different sets of transactions have completed are distinguishable. AC2 ensures that consistent states and inconsistent states are distin- guishable. An example a database specified as a 4-tuple is ?O of Figure 2.1. ?X) models an application in which a series of independent events move elements one at a time from the 23 ?O--H--H(VO,CO,TO,0? V0--H(q0,q1,xo,..?,x??1,cfo,..?,cf??1?, CO--H(q1.qOzQA?qO>(?k: O?k?N: cf?--HJa1se)), Sl?: (z?,qO:--HqO(O),qO(t..)?; S2j: (q1:--Hq1.x??; S3?: (end(Tj)) (VO'0 VOfl)?(qOt??qOflA q1fzq?fl? A cf?'c4") O?k<:N Figure 2.1: Database System ?X). head of one queue to the rear of another, as in a factory where parts are transferred from one assembly line to another, VO contains two sequence variables qO and qi modeling the two queues, and a variable xj for each r? in TO to hold the item removed from qO and not yet appended to qi The following notation is used for sequence variables: Is the number of elements in s, s(i) the ith element of s for 0 ? i ? I?I s(i . .j) the subsequence of consecutive elements from the ith to the jth for 0 ? i ?j ? Is (and the empty sequence if an abbreviation for s(i.. IsI?1). s1?s2 the catenation of si and s2. The conjunct qi `qO Q in the consistency constraint CO specifies that queue el- ements are not lost in the transfer, while the second conjunct2 qO ? (# k: 0 ? k ? 2(# i: R: P) denotes the number of values i in range R that satisfy P. 24 N: cI? false) specifies that qO contains enough elements for every transaction that has not completed to remove one. Each transaction Tj C TO models the transfer of one element from the first queue to the second, using a local variable Zj for temporary storage of the element removed. For simplicity, we assume that transactions of ?O terminate only by completing. The operation S12 moves the first element of qO into Zj? and S2? then moves it to the rear of qi; S3j has no effect other than ensuring that cfj true. The equivalence relation 0 specifies that two states VO' and ???? are equivalent when each of qO and qi contain the same sequence of elements in both states, and the same transactions have completed. The values of temporary variables ?` `?N--H1 are ignored by =o since the particular order in which transactions run is insignificant in this application. 2.2 Serializability Recall that wp(S,R) denotes the set of states in which execution of 5 will terminate leaving R true. Using wp, it is possible to formalize the property that a schedule ? "behaves like" like a serial schedule. Definition 2.2.1 (Serializable Schedule) Let ? (V C T ? be a database sys- tem and let SER( T) denote the set of serial schedules for ?, each schedule consisting of zero or more transactions of T. Let ? be a vector of new variables each having the same domain as the corresponding one in V. A schedule ? of ? is a serializable schedule of ? if and only if: 25 ?(CA wp(?V--HV))?( v wp(&,v?Vr)). ?`cSER( T) 5 Definition 2.2.1 can be interpreted as lollows. A state satisfying the antecedent is one satisfying the consistency constraint and in which execution of ?(#k: O?k?2: ??zfr1se)AqO(2..)?qO Aql.qO(O).qO(1)--Hq? A true--H--Hc40--Hc41 q0(2..)--Hq?Aq1.qO(O).qO(1)zq?Atruecf0?cf1 From this it follows that # (CO A wp(ff4, VO?--H0 ?o)) ? wp(?5, VO?--H--H0 ?) and since ?5 c SER( To), #(COAwp(?4,VO?--Ho?)) ? (? v wp(&,VO0V6)). Therefore, ff4 is serializable according to our definition. Definition 2.2.1 for serializable schedules can be extended to obtain a definition for serializable database systems. Definition 2.2.2 (Serializable System) Database system ? (V, C, T,--H? is a se- riatizable system if and only if concurrent execution of transactions that begins with ??C true always terminates and every resulting schedule is serializable. 0 Note that although the schedule ff4 is serializable, ?X) is not a serializable system since ff6: S10;S11;S21;S20;S30;S31 is not a serializable schedule. 27 2.3 Serializability with Proof Outlines Definition 2.2.1 characterizes serializability using wp. It is also possible to characterize serializability using proof outlines. Two benefits result from such a formulation. The first is that Proof Outline Logic then can be used to verify formally the serializability of a database system. The second, explored more fully in Chapter 3, is that it becomes possible to derive synchronization protocols that ensure serializability. A Proof Outline Logic characterization of serializability is formulated by intro- ducing auxiliary variables and operations on them that allow the behavior of serial schedules to be characterized by assertions. Let ? (V, C, T,=) be a database system with variables and transactions TztTo,...,TN?lY. Define a vector of new variables 4ith each new variable v? having the same type as the corresponding variable vk in V. Each ? is called the shadow variable corresponding to vk. With these shadow variables, construct a set of new transactions 28 where each r% is obtained from ri E T by replacing all reference to vk c V by a reference to the corresponding v? C V. Each r? is called the shadow transaction corresponding to T?. Let SER(?) denote the set of serial schedules consisting of zero or more transac- tions of T. The isomorphism between V and ? and between each r? C T and r? C T implies that for any serial schedule a' E SER( T), there is a serial schedule & E SER( T) that transforms V in the same way that a transforms V - This isomorphism between schedules of SER( T) and SER(?) makes it possible to construct a proof outline that is valid if and only if a satisfies Definition 2.2.1. Theorem 2.3.1 (Schedule Serializability with Proof Outlines) Schedule a of database system ? (V, C, T,z? is a serializable schedule if and only if SSO(a): fCAV--HV? a f v wp(&,V?)? ??SER(T) is valid. 5 Proof of Theorem 2.3.1 From the interpretation of SSO(a) and of the weakest pre- condition predicate transformer, SSO(a) is a valid proof outline if and only if w(cA V--H?Awp(?true))?wp(a, v wp(&,V?--H--H?)). (2.3) &cSER( T) Thus, the theorem follows if a is a serializable schedule of ? if and only if (2.3). This is proven in Lemma 2.3.4 proven below. 0 The proof of Lemma 2.3.4 will frequently rely on inferences that are justified by 29 the following two lemmas. The first states that substituting subformulas of A with equivalent ones results in a formula that is equivalent to A. Lemma 2.3.2 Let A' be obtained from A by replacing some occurrences of B1, Bn by B?', ..., B?1 respectively. If ?Bi?Bi',...,WBn?Bn', then WA if and only if WA' 0 Proof of Lemma 2.3.2 By induction on the structure of A. See [S67J for details. 0 The second lemma characterizes the distributivity of wp over conjunction with a predicate B when B does not contain variables referenced by S. Lemma 2.3.3 For any program S and predicates A and B, if S does not change any variable of B, then W(wp(S,A) A B)?wp(S,A A B). 0 Proof of Lemma 2.3.3 By definition, wp(S,B) represents the set of all states such that execution of S begun in any one of them is guaranteed to terminate in a state satisfying B. Since S does not change any variable of B, then wp(S,B) is the set of states in which S is guaranteed to terminate and in which B is true. Thus, 30 #(wp(S,true) A B)?wp(S,B). By Predicate Logic, wp(S,A) can be conjoined to both sides of (2.4) giving #(wp(S,4) A wp(S,true) A B)?(wp(S,4) A wp(S,B)). Distributivity of Conjunction from Appendix B implies that wp(S,A) A wp(S,true))?wp(S,A A true). Substituting the right side for the left in (2.5) gives #(wp(S,A A true) A B)?(wp(S,A) A wp(S,B)). Distributivity of Conjunction also implies that wp(S,A) A wp(S,B)) ? wp(S,A A B). Substituting the right side for the left in (2.6) gives ?(n;p(S,A A true) A B)?(wp(S,4 A B)). Since (A A true) ? A, ?(wp(S,A) A B)?wp(S,A A B). (2.4) (2.5) (2.6) (2.7) 0 Using these lemmas, the equivalence of the serializability of ? and the validity of (2.3) can be proven. 0 Lemma 2.3.4 a is a serializable schedule of ? if and only if (2.3). 31 Proof of Lemma 2.3.4 By Definition 2.2.1, a is serializable under if and only if #(CAwp(a,VE?))?( v wp(&,V?z?fr (2.8) (T'CSER( T) From Predicate Logic, WP?(VV: V??V?PvY) for any predicate P. Taking v wp(&,V--HV)J, cSER(T) and applying Lemma 2.3.2, (2.8) if and only if #(CAwp(?V=?V))?(VV: v--HM?( v wp(&,V--HV))?). (2.9) ff1CSER( T) From the construction of the shadow transactions and definition of SER(?), W( V wp(&?V?b!fv?( v wp(&,?--HV)). (T1CSER(T) Thus, (2.9) if and only if #(CAwp(a,V--HV))?(VTh v-M?( v wp(&,?7Vb). ffCSER(?) From Predicate Logic, when variables of V are not free in P, #(P?(vTh Q))?(VV: P?Q). Taking P [CAwp(a,v?V)j and Q--H[V-??( v wp(a%V-Th)], &eSER( T) (2.10) (2.10) if and only if 32 WY?(CAwp(ff,V--H-?b?(V--H??( v wp(&,??--H?)))). ff?SER(T) From Predicate Logic, W (v?: P) if and only if K P Taking P--H[(CAwp(QV--HTh)?(V--H??( v wp(&,V--Th))], ??sER(T) (2.11) if and only if W(CAwp((r,V--HTh)?(V??( v wp(ff,MThTh ff?SER(T) From Predicate Logic, Taking P Q--H[V-?] and R [ v wp(&,??--V)], (TESER(?) (2.12) if and only if W(cAwp(cT,v?zThAvTh?( v wp(&,??)). ??SER(T) By the commutativity of conjunction in the antecedent, (2.13) if and only if W(CAV--HMAwp(cr,VE?))?( v wp(&,?--HTh). (TCSER(T) (2.11) (2.12) (2.13) (2.14) From Predicate Logic, 33 [7((P A ? R)?((P A Q) ? (Q AR)). Taking P Q R [CA VzVJ, --H [wp(? v --H V)] and --H [ v ?ESER( T) (2.14) if and only if K(CA v--H VAwp(J,v--HVb? (2.15) (wp(?v--H--HV)?( v wp(&,V--H--HV))). Since ? does not reference any free variable of ( V wp(&,? --H--H V)), it follows ??sER(T) by Lemma 2.3.3 that #(wp(?v--HV)?( v wp(&,V=--Hv))) ?cSER(T) tvp(QV--HVA( v wp(&,VzV))). (7CSER(T) Thus, (2.15) if and only if K(CA vvAwp(?VzV))? lvp(ff,VzVA( v wp(&,??--HV))). vqO, then delaying each Si? until vqO+ 1 t?j ensures that the timestamp of each r? is greater than vqO when r? accesses qO. This is what is required by condition TS1. 5Guarded Command Notation semantics specify that if B S fi executes s if started with B true and will fail to terminate if started with B false. Since atomic operations run to completion once started, execution of (if B s fi) delays until B becomes true. 41 Now consider operation S15 in a transaction r5 j ? i that runs after Sl?. Note that assignment vqO:--Ht??' in Sl? leaves vqO> ts_ Since vqo#lzts5 ? ts5?vqO, then ts5 vqO will be true when Sij runs. The assignment vqO:--H tsj in Sl? ensures that vqO > tsj after Sl? runs. Since (vqO+1 ts5 A vqO? Isi) ? ts5 ? tsj, then delaying each Sl? until vqO +1 tsj ensures that the timestamp of r5 cannot be less than the timestamp of r? when S1j runs after Si?. This is required by condition TS2. 0 By Lemma 2.4.1, access to qO will satisfy TS1 and TS2 if vqO+1 tsj is chosen as the guard for each Sl?. By a similar analysis, it can be shown that access to qi will satisfy TS1 and TS2 if vql + 1 tsj is chosen as the guard for each S2?. Because of the synchronization that has been added to transactions, the conjunct vqO--Hvql clock has been added to the consistency constraint Cl to ensure that transactions complete yvhen executed in isolation starting in a consistent state. In addition, the definition of --H? has been changed to ensure that continues to satisfy adequacy constraint AC2. This gives the synchronized database system ?1 of Figure 2.2. We can now apply Method 2.3.6 to prove that ?1 is serializable. First we define shadow variables Vi: q0,q1,zo,...,x??i,cf0,...,cf??1,c1ock,v?,v?,t?0,...,t???1 42 = (Vi, Ci, T1,=--H1? V1=(q0,q1,xo,...,x??i,cfo,...,cf??1,clock,vqO,vq1,ts0,...,ts??1? Cl=fql-qO= Q A qOI?(#k: O?k?N: ??=false)A vqO=vql=clockj, Tl=fro',...,TN' 11, T' SO? i I. (cThck,ts?:=clock+1,clock?1); S1?: S2?: S3?: (ifvqO+1=ts? :j,qO,vqO:=qO(O),qO(1..),ts,.fi?; (ifvqltl tsj H q1,vq1:=q1.x?,ts? fi?; (end(r?) (Vi' i Vi") ? (qO' = qO" A qi' = qi" A o?kAN OO. Thus, qO contains at least one element when Sli has been reached. In addition, pre(Sl?) ? (13 A vqO < clock), (I3AvqO?t;qO+1?clock), --H ((Vv: vqO?v?clock: (?k: O?k?N: CLOCKklA VQOkZOAvtsk)) AvqO?vqO+1 ?clock). Since vqO ? vqO +1 ? clock implies that vqO +1 satisfies the range of the universal quan- tifier in 13, the quantified expression can be instantiated with vqO + 1 substituted for v. Thus, pre(Sl?) ? (3k: 0 ? k ? N: CLOCKk 1 A VQOk 0 A vqOt 1 tsk) A qO ? 0. It follows from the interpretation of FSDO(?1) that when execution of ?1 starts with CiA Vi Vi and reaches Sl?, there is some 4 such that CLOCKk 1 A VQOk 0 A vqO+ 1 tsk A IqO >0. Since CLOCKk 1 A VQ0k 0 implies that the control point before 51k has been reached and 48 (vqO+lts? A Iqol >0) ? wp(Sl?,true), then Sik In rk will be enabled when Sl? is reached. Thus, condition T2 will be satisfied when Slj has been reached. Suppose that 52i has been reached. Note that pre(S2?) ? (14 A vql ? vqO), ? (13 A vql ?vq1t1 4 vqo), --H ((Vv: vq1?v4vqO: (3k: O?k?N: VQOk--H1A VQlkOAv--Htsk)) Avq1?vq1+14vqO). Since vqi ? vql +14 vqO implies that vqi $ 1 satisfies the range of the universal quan- tifier in 14, the quantified expression can be instantiated with vql $ 1 substituted for v, from which it follows that pre(52j) ? (3k: 04k ? N: VQOk --H--H1 A VQ1k 0 A vql $ 1 tsk). it follows from the interpretation of FSD0(?1) that when execution of ?1 starts with Ci A Vi Vi and reaches S2j, there is some transaction rk' such that VQOk 1 A VQi?0Avq1$1ts?. Since VQ0k1A VQik--H0 implies that the control point before 52k has been reached and vqi+1 tsk ? wp(S2?,true), then 52k in rk' will be enabled when S2? has been reached. Thus condition T2 will be satisfied when S2i has been reached. Finally, suppose that S3? has been reached. Since wp(S3?,true) --H--H true 49 S3j will be enabled and condition T2 will be satisfied. Thus, execution of ?1 satisfies conditions T1 and T2 of Lemma 2.4.2 when started with Ci A Vi ?i true, and consequently will terminate. 0 2.5 A More Tractable Method The preceding example ?1 with Method 2.3.6 is misleading in one respect. Because of the uniformity of transactions in T1, all serializable executions of ?1 leave the same values in qO and qi. For an arbitrary serializable database system ?, however, the size of assertions in the proof of SDO(?) can be proportional to the number of different serial schedules. If ? contains N transactions, there are ? (Nk) possible serial O?kN o?kOA?q?--HLQ1+ CLOCKk VQOk A q?jffi N CLOCKk o (# k: 0 ? k ? N: q? false) and the equivalence relation --Ho has been replaced by the weaker relation (V2' --H2 V2") ? (fqO'J fqO11? A fq1'? fql11J A A cf?' O?(#k: O?k?N: cf?--Hfalse). O (P A B). This gives the following method for using locking to strengthen assertions. Method 3.4.2 (Selectively Strengthening Assertions) Let FPO(?): fQjcobeginpO(r0) I II PO(r??i)coendtRJ be a full proof outline for database system ? and let P be an assertion in one of the PO(r?). To strengthen P to an assertion P' such that P' ? (P A B), do the following. 1. Choose Local Predicates. Choose a predicate LP local to r? such that P ? LP 81 and for each 0 fflj # i ? N choose a predicate LQj local toT1 such that P ? (B v V LQ1). O?#i?N 2. Guarantee Exclusion Invariants. Use Method 3.3.2 to strengthen A so that ?(LP A LQ1) isinvaflantforeachO?j#i?N. TakeP'--H--H(PA A ?(LPALQ1). 0 Using Method 3.4.2 to help eliminate interference by selectively strengthening as- sertions, our method for proving the serializability of a database system (Method 2.5.3) can be transformed into a method for deriving synchronization that ensures it is seri- alizable. Method 3.4.3 (Deriving Synchronization for Serializability) To derive a lock- ing protocol A=(M,LC,R? for database system ??--H(V,C,T,z') such that (A,?? is serializable, do the following. 1. Approximate (A,?). Choose an initial version of A and modify ? as necessary to follow A. 2. Define Shadow Variables and Transactions. Define shadow variables ? and shadow transactions T corresponding to the variables V and and transactions T of ?. 3. Form Synchronized Augmented System. Construct an augmented system 82 4. Derive Synchronization. Strengthen the locking protocol A so that it becomes possible to construct the valid, full proof outline FSDi(V?*): fCAVzV? cobeginP0(?0*)fI... PO(TN*?1) coend as follows. (a) Construct Sequential Proof Outlines. Construct valid proof outlines Po(r0*),...,Po(rk?1) satisfying hypotheses Hi and H2. (b) Eliminate Interference. While hypothesis H4 remains unsatisfied, do the following i. Enumerate and check the interference freedom formulas. ii. Choose an invalid NI(o,A) for a in PO(ri) and A in PO(rj) and do one of the following. o+ Strengthen pre(a). If possible, replace p?(a) by stronger asser- tion pre(a)' such that fpre(a)' A AiafA? is valid, strengthening assertions that precede pre(a)' enough that PO(r2) remains valid as required by hypothesis Hi but not enough that hypothesis H2 is invalidated. If hypotheses Hi and H2 prohibit strengthening pre(a) enough to eliminate interference, use Method 3.4.2 to selectively strengthen pre(a) without invalidating these hypotheses. o+ Weaken A. If possible, replace A by a weaker assertion A' such that the interference freedom formula fpre(a) A A'?a(A'? is valid, weakening assertions that follow A' enough that PO(rj) remains 83 valid as required by hypothesis Hi but not enough that hypoth- esis H3 becomes unattainable. If hypotheses Hi and H3 prohibit weakening A enough to eliminate interference, use Method 3.4?2 to selectively strengthen an assertion following A so that A can be weakened without invalidating these hypotheses. (c) Check that the resulting proof outlines satisfy hypothesis 113. 5. Infer SDi(?*). Using the Assertion Deletion Rule, Infer SDi(?*): fCA v--H?? cobeginr0* II II rk?i coend from FSDi(?*). 6. Prove Termination. Prove that execution of ?? terminates when started with C A V V true. 3.5 An Example 0 ;?To illustrate use of Method 3.4.3 to derive locking protocols for serializability? we consider a database system that supports a simple banking application. In deriving synchronization for serializability, we will illustrate another point as well. This example was first used in [L76] to argue that serializability is inappropriate as a correctness criteria because of the restrictions it imposes on concurrency among transactions. We 84 will show that choosing an equivalence relation more accurately reflecting the semantics of the banking application makes it possible to derive a locking protocol that does ensure serializability while at the same time ensures a high degree of concurrency among transactions. Database system "? of Figure 3.1 models a simple banking application. Variables V5 include an array a[0. NJ that models account balances. For j >0, array element a[jj holds the balance of a customer account; a[0] holds the balance of a dummy account that is equal to minus the sum of customer accounts, modeling the bank's financial obligation to its customers. This implies a consistency constraint that the elements of a sum to zero. Transaction T0 models an auditor that inspects account balances to determine if funds have embezzled. The auditor accomplishes this by copying account balances into a ledger 1 for inspection at a later time. V5 contains an array l[0. . N] modeling the ledger used by the auditor to record account balances. Transaction r1 models a sequence of deposits, withdrawals and transfers. (A deposit to or withdrawal from an account a[j] would be implemented by a transfer between that account and the bank's account a[OJ.) Here, r1 is shown performing only two such updates, to simplify ?nalysis. To ensure that array references by r1 are within a's range of subscripts, C5 bounds variables cO, dO, cl and dl. States equivalent under 5 are those in which corresponding elements of a[O. . and variables cO, dO, cl and dl have the same value, and in which elements of 1[O. NJ sum to the same value.3 The latter property of ? reflects that only the sum of ledger 3This value is 0 for consistent states. 85 ?5(V5,C5,T5,--H--H5?, V5z(a[O..N],1[O..N],k,cO,dO,tO,cl,dl,tl,cfo,cA?, C5--H--H(N>?OAO--H Z a[jj AO?cO?dO?NAO?cl?dlffiN), T5 --H fr0,r1?, r?--H--H AO: (k,1[O]:--HO,a[O]?; dok#N Al: (k,1[kl]:zktl,a[k+l]) od; A2: (end(r0)), r1 --H--H TO: (a[cOj,a[dOJ:--Ha[cOj+ tO,a[doj --H tO); Ti: (a[cl],a[dlj:=a[cl]$tl,a[dl] --H tl); T2: (end(r1)), (VS' ? VS") ?(a'[O..N]a11[O..NJA ? 1'[jjz ? O fIoA POA k/N? Al: (k,1[ktlj:--Hk+l,a[kslJ? flO A PO? od; fIOA ? Oj?N A2: (end(r0);r%? fIOA z `[i]--H--H OO. wp(DO,R)--H(?k: O?k: Hk(R)). Composition Rule. wp(Sl;S2,R) wp(Sl,wp(S2,R)). Bibliography [BBG LS83] [BG81] [BG83] [BS77] [BSW79] [C73j ?C81] C. Beeri, P. Bernstein, N. Goodman, M. Lai, and D. Shasha. A con- currency control theory for nested transactions. In Second Annual A CM Symposium on Principles of Distributed Computing, pages 45--H62, ACM, 1983. P. Bernstein and N. Goodman. Concurrency control in distributed data- base systems. ACM Computing Surveys, 13(2):185--H221, Jun. 1981. P. Bernstein and N. Goodman. Concurrency control for multiversion data- base systems. ACM Transactions on Database Systems, 8(4):465--H483, 1983. R. Bayer and M. Schkolnick. Concurrency of operations on B-trees. Acta Informatica, 9:1--H21, 1977. P. Bernstein, D. Shipman, and W. Wong. Formal aspects of serializability in database concurrency control. IEEE Transactions on Software Engi. neeiing, SE-5(3):203--H216, May 1979. M. Clint. Program proving: coroutines. Acta Informatica, 2:50--H63, 1973. The Concurrency Control Problem for Database Systems. in Computer Science, Springer-Verlag, New York, New M. Casanova. Lecture Notes York, 1981. [D76j E. W. Dijkstra. A Discipline of Programming. Prentice Hall, Inglewood, New Jersey, 1976. [EGLT76j 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--H633, Nov. 1976. 120 121 [FL79J [G78j [G81] [G83j [GS85J [GW82J [H79J [HW86j [K83J [KS79j jL76] [L80J M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194--H211, 1979. J. Gray. Notes on database operating systems. In R. Bayer, R. Gra- ham, and G. Seegmuller, editors, Operating Systems: an Advanced Course, Springer-Verlag, 1978. D. Gries. The Science of Programming. Springer-Verlag, New York, New York, 1981. H. Garcia-Molina. Using semantic knowledge for transaction process- ing in a distributed database. ACM Transactions on Database Systems, 8(2):186--H213, Jun. 1983. N Goodman and D. Shasha. Semantically-based concurrency control for search structures. In Principles of Distributed Systems, pages 8--H19, ACM, 1985. H. Garcia-Molina and G. Wiederhold. Read-only transactions in a dis- tributed database. ACM Transactions on Database Systems, 7(2):209--H234, Jun. 1982. D. Harel. First Order Dynamic Logic. Volume 68 of Lecture Notes in Computer Science, Springer-Verlag, New York, New York, 1979. M. P. Herlihy and J. M. Wing. A:ioms for Concurrent Objects. Technical Report CMU-CS-86-154, Carnegie-Mellon University, Oct. 1986. H. F. Korth. Locking primitives in a database system. Journal of the ACM, 30(1):55--H79, Jan. 1983. Z. Kedem and A. Silberschatz. Controlling concurrency using locking. In lEEF Foundations of Computer Science, pages 274-285, IEEE, 1979. L Lamport. Towards a Theory of Correctness for Multi. user Data Base Systems. Technical Report CA- 7610-0712, Massachusetts Computer As- sociates, Oct. 1976. L Lamport. The `Hoare logic' of concurrent programs. Acta Informatica, 14:21--H37, 1980. 5. 5. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319--H340, 1976. [OG76J 122 [P79J [P86J [P87] [R83] [567] [5A87J [5LR76] [S584] [TS85] [W84] [Y84J C. H. Papadimitriou. Serializability of concurrent updates. Journal of the ACM, 26(4):631--H653, Oct. 79. C. H. Papadimitriou. The Theory of Database Concurrency Control. Com- puter Science Press, 1986. D. Peleg. Concurrent dynamic logic. Journal of the A CM, 34(2):45O--H479, Apr. 87. D. P. Reed. Implementing atomic actions on decentralized data. A CM Transactions on Computer Systems, 1(1):3--H23, Feb. 1983. J. R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967 F. B. Schneider and G. R. Andrews. Concurrent programming: centralized and distributed. In Current Trends in Concurrency, Springer-Verlag, 1987 R. E. Stearns, P. M. Lewis, and D. J. Rosenkrantz. Concurrency control for database systems. In 17th Symposium on Foundations of Computer Science, pages 19--H32, 1976. P. M. Schwarz and A. Z. Spector. Synchronizing shared abstract types. A CM Transactions on Computer Systems, 2(3):223--H250, Aug. 1984. A. Tuzhilin and P. Spirakis. A semantic approach to correctness of con- current transaction executions. In Proceedings of Principles of Distributed Computing, pages 85--H95, 1985. W. E. Weihl. Specification and Implementation of Atomic Data Types. Ph.D. dissertation, Massachusetts Institute of Technology, 1984. M. Yannakakis. Serializability by locking. Journal of the A CM, 31(2):227- 244, Apr. 1984.