Specifying and proving serializability in temporal logic

Specifying and Proving Serializability in Temporal Logic  Shmuel Katz Doron Peledy AT&T Bell Labs Department of Computer Science 600 Mountain Avenue The Technion Murray Hill, NJ 07974, USA Haifa 32000, Israel Amir Pnueli Department of Applied Mathematics The Weizmann Institute of Science Rehovot 76100, Israel Abstract Serializability of database transactions is rst de ned within the framework of linear temporal logic. For commutativity{based serializability, an alternative speci cation is given in a temporal logic whose semantic interpretation is especially tailored for reasoning about equivalence classes of histories. Both past operators and prophecy variables are used in the speci cation of serializability, which includes the possibility of aborting a transaction. We provide a formal veri cation system for serializability. Within it, proving serializability of transactions executing a concurrency control algorithm is done along the same lines as proving properties of concurrent programs.

1 Introduction Concurrency control of database systems involves executing user requests reliably and guaranteeing no interference among them. Such requests, called transactions, should behave as if executed atomically, one at a time. However, transactions are constructed from ner operations that may interact with the operations of other transactions. Failure situations may also occur, preventing transactions from proceeding, requiring some recovery measures to be taken. The atomic{like behavior of transactions in concurrency control algorithms is sometimes called This research was supported in part by the European Community ESPRIT Basic Research Action project 3096 (SPEC). y This research was carried out while the rst author was with the Department of Computer Science, The Technion. 

1

serializability. It demands that each execution, seen as an interleaved sequence of operations, behave as if transactions execute one after the other. Concurrency control and serializability [5] bring together researchers from both database theory and distributed programming. Many attempts have been made to formalize serializability, resulting in a variety of distinct notions. Verifying that a particular protocol or regime guarantees serializability has also been considered within diverse formalisms using dierent models and techniques. In this paper, we address the problem of specifying and verifying serializability within the framework of Temporal Logic. We show that formalizing serializability needs a temporal logic with expressive power beyond that normally used for reasoning about concurrent programs. One aspect in formalizing serializability demands, for example, the use of equivalence classes of interleaving sequences, since serializability is essentially the assertion that one of the sequences from each equivalence class behaves in a serial manner. The kind of speci cation that is usually given in the literature uses explicit referencing of equivalent execution sequences. Some examples are the de nitions of serializability in [25, 5] and the recent formalizations which generalize serializability to abstract data types (rather than considering only read{write operations) [30]. The style of reasoning appropriate for such a speci cation also involves the explicit use of execution sequences. A typical proof of serializability for a concurrency control algorithm requires showing inductively that each nite execution sequence is equivalent to a sequence that is serial, i.e., satis es some desired properties [31, 11, 32]. We give an alternative speci cation method for the common variants that we call commutativitybased serializability, using a temporal logic that hides the use of equivalence classes of sequences by embedding the classes into the semantic interpretation of the temporal states. This kind of serializability covers most known concurrency control algorithms. In this way, speci cations use the modals of the logic, instead of explicit assertions about equivalence classes of execution sequences. A formal proof system with simple reasoning on the set of program variables (in the style of [20]) is given. The veri cation method presented herein allows verifying a concurrency control algorithm at various levels of abstraction. By using operations in which details not relevant to the generic algorithm are abstracted out, an abstract version of a concurrency control algorithm can be veri ed. On the other hand, a precise detailed implementation can also be treated. Lamport has motivated, during the twenty sixth Lake Arrowhead Workshop, \How will we specify concurrent systems in the year 200", held in September 1978, a study of speci cation and veri cation methods for serializability by dierent formalisms [18]. This resulted in a special issue of Distributed Computing on speci cation of concurrent systems [29], containing contributions by Manfred Broy, Reino Kurki-Suonio, and by Simon Lam and Udaya Shankar. We consider the ability to provide a relatively complete state-based proof system, similar to Manna{Pnueli style of veri cation as the main contribution of our framework over those suggested in the special issue. This is achieved by restricting ourselves to commutativity{based serializability. We claim that this restriction is still general enough to capture most existing concurrency control algorithms. By comparing it to other mothods it illustrates the observation that additional generality in sepci cation can come at the cost of excessive complexity of the related veri cation method. This paper is organized as follows: In Section 2, some preliminary de nitions are presented, and serializability is speci ed in Linear Temporal Logic [20]. In Section 3, the speci cation for

2

commutativity-based serializability is written using the temporal logic ISTL [12], where the states are interpreted as equivalence classes of nite execution sequences. Proof rules especially suited for this kind of serializability are presented. In Section 4, two examples of veri cation of concurrency control algorithms are outlined. Section 5 summarizes the speci cation and veri cation method.

2 Preliminaries A database system can be modeled by a set of atomic operations which test and modify a given set of variables ~y. A global state J is an interpretation that assigns a value from some prede ned domain to each variable in ~y. The state space of global states is denoted by S . A database system DS is a triple hT; ~y; i where T is a set of operations or transitions, ~y is a set of variables, called the concrete variables, and  is a predicate called the initial condition. Each operation  2 T is associated with a pair hen ; fi where en is a predicate (the enabling condition) and f (the transformation) is a tuple of j ~y j terms over some xed rst order language. We allow j ~y j to be in nite. However, only a nite number of variables can be changed by executing any single operation , i.e., for only a nite number of indexes 1  i j ~y j, f(yi) 6= yi. This allows a nite representation for the operations. The predicates  and en for each  2 T contain no free occurrences other than the variables of ~y. The same holds for the variables used in the terms f. The enabling condition en controls when the operation  may execute and the eect of the operation is to simultaneously assign the j ~y j expressions f(~y) into the set of variables ~y. Transformations of various programming models into such a set of operations appear in [20]. The notation '[f(~y)=~y] (also written '(f(~y))) means the result of substituting in ' for each 1  i j ~y j, the ith term f(yi) instead of each free occurrence of yi in '. The predicate transformer wp(') = en(~y) ^ '[f(~y)=~y] is called the weakest precondition [7]. For a predicate ', wp(') returns the predicate that is satis ed exactly by states from which  can execute and produce a state satisfying '. A transition formula ' is a classical (non{temporal) assertion with variables taken from the set ~y [ ~y0 [ fopg, where ~y0 are the primed versions of the variables ~y. Such an assertion is interpreted over a triple hJ; ; J 0i 2 S  T  S such that the ~y variables have values assigned to them by the state J , ~y0 have values assigned by J 0, and op has the value . We write hJ; ; J 0i j= ' if ' is true under the appropriate substitutions. In order to reason about generic concurrency control algorithms (i.e., algorithms that are not completely speci ed), an assertional method that allows partial speci cation of the system is appropriate. In the framework of serializability, the partiality of the speci cation stems from the fact that only limited relevant information is given about the operations. In order to allow this genericity, we allow the operations to be parametric. For example, if some unspeci ed value is assigned to a variable x, then we use the parametric assignment x := n. The veri cation is done with respect to all such n that can be assigned to x. When a speci c implementation of the algorithms is given, it is possible that only a subset of the 3

values can actually be assigned to x. The actual implementation of the generic algorithm can also strengthen the enabledness conditions of some operations. Both changes implied by implementing the algorithm maintain the validity of serializability as can be easily seen from the semantic model to be used.

De nition 2.1 A history (a nite execution sequence) of a database system is a pair h = hJ; wi where J is an interpretation of ~y called the initial interpretation of h, and w 2 T . Let n =j w j, w = 12 : : : n be a sequence of occurrences of operations of T (that is, operations can occur more than once). We require that J j=  (J satis es the initial condition). Furthermore, there exists a sequence of interpretations J0; J1 ; : : :; Jn with J0 = J such that for each 1  i  n, 1. Ji?1 j= en , and i

2. Ji = f (Ji?1 ). i

The last global state obtained in this way is called the nal interpretation of h, and is denoted finh .

A transaction is a set of operations. The order among the operations is consistent with the enabling condition and transformation associated with each operation, and with the initial state. TheS set of transactions of a system is denoted by Tran. Thus, the set of program operations T is T 2Tranf j  2 Tig. i

2.1 Variables A database contains concrete variables y of two types:

Local variables, each of which is associated with a single transaction. Such a variable is

modi ed and used only by the operations of that transaction. Without loss of generality, we can assume that each transaction Ti has the same set of local variables separated from the variables of other transactions by indexing with i. Global variables, which are shared by all the transactions.

Both types of concrete variables are used to implement some abstract set of variables ~yA. The user of the database is only concerned with the manipulation of these abstract variables. It is the responsibility of the database system that the representation captures the intended semantics of the abstract variables. The state of the system consists of the concrete variables. We assume the logic to be de ned over a many{sorted interpretation. Thus, i; j are quanti ed over the natural numbers (which serve for indexing the transactions). Similarly, in the following formulas y is assumed to be quanti ed over the abstract database variables ~yA , and u over a domain DB of database values. The speci cation of serializability will relate the abstract variables with their values in the various transactions using the concrete state function expi[y]. For each abstract variable y and 4

transaction i, expi[y] is a function from states to values from DB. Thus, one can write expi[y](J ), where J is a state. The database implementor usually suplies a term, based on the concrete variables, that enable calculating the value of the function expi[y](J ) from the values assigned to the concrete variables in the state s. This expression can depend on

 the interpretation of the global variables,  the index i of a transaction Ti, and  the interpretation of the local variables of a transaction Ti. The expression used to calculate expi[y] is supplied by the implementor together with the algorithm. We often abuse notation by using expi[y] to stand for both the state function and the suplied term that is provided in order to calculate it. Note that the name of the variable y is used in denoting the function expi[y], and this is indicated by enclosing it in brackets. The need for i as another argument of this function stems from the fact that in some implementations, a single abstract variable has multiple versions at the same time for the dierent transactions. When a transaction Ti has not yet started, or has already terminated, the value of expi[y] is irrelevant. The initial value of a variable y is exp0[y]. The use of an abstract set of variables is common in many uses of database systems. Frequently, several copies of the same variable are held simultaneously, so that dierent transactions might refer to dierent versions of the same abstract variable. This may enhance the concurrency among transactions, allow recoverability of the variable's value after failures, and increase

exibility in concurrency control. As an example, consider a database implementation where each transaction receives a unique timestamp that is an indication of its startup time. An abstract variable y is represented as a global list of triples hu; wr; rdi called versions, where u is a value, wr is the timestamp of the transaction that has written this version, and rd is the maximal timestamp of a transaction that has read this version. Then, given the value of the list of triples, an index i of the current transaction issuing an operation, and its timestamp ti, it is possible to de ne expi[y] as the u component of the version hu; wr; rdi with maximal wr that is still less than, or equal to ti. This abstraction function is actually taken from the multiversion timestamp algorithm [5], and is further elaborated in Section 4.2.

2.2 External and Internal Operations The speci cation of serializability is concerned with the order of the operations that manipulate (read and write) the abstract variables. Thus, the database system operations T can be partitioned into external operations Ext and internal operations Int. External operations manipulate or refer to the abstract variables, while internal operations cannot refer to them. The label of an occurrence of an external operation is its type (read, write, etc.), along with the transaction's index, and the relevant abstract variable and value. Thus, the ve types of external operations with their corresponding labels are: 5

begini This operation initiates the transaction Ti. readi[y; u] A read operation obtains the value u of the abstract variable y in Ti. writei[y; u] A write operation changes the value of the abstract variable y into u by an

assignment based upon the local variables of Ti. aborti An abort operation terminates transaction Ti abnormally. Operations from aborted transactions have no eect on the values of abstract variables read by transactions that commit. commiti A commit operation terminates a transaction Ti normally.

Given a history h, an execution of a transaction Ti in h is the sequence of occurrences of operations from Ti appearing in h. An execution of a transaction in a history h can be committed (terminated with a commit operation), aborted (terminated with an abort operation), or active (neither of the above, but a begin for Ti has occurred in h). Transition formulas can be used to specify transitions and their labeling. In order to relate to the labels of operations, the following constructs should be available: 1. Predicates that de ne the type of the operation op, such as Read(op) (for a read operation), Commit(op) (for a commit operation) and Int(op) (for an internal operation). 2. A function tran(op) that returns the transaction number (the index) of the operation op. 3. A function var(op) that returns the abstract variable involved in the operation op. (When the label of op does not involve an abstract variable, var(op) is de ned arbitrarily.) Then, we can de ne transition formulas such as

Ri[x; u] =4 (tran(op) = i) ^ Read(op) ^ (var(op) = x) ^ (expi[x] = u) .

Wi[x; u] =4 (tran(op) = i) ^ Write(op) ^ (var(op) = x) ^ (exp0i[x] = u)

A primed expression (or formula) means the expression (formula) where all the system variables are replaced by their primed version. The function label(op) can be de ned similarly to return the label of the operation op. Our view of an abstract variable (to be further explained later) requires the following restrictions:

 A begin, a read, a commit, or an internal operation do not modify the value of any of the abstract variables.  A writei[y; u] operation modi es only the value of the abstract variable y. 6

 For each transaction, none of its external operations is allowed to occur before a begin, or after a commit or an abort operation. In order to ensure that expi[y] satis es these restrictions, we de ne the transition formula restrict =4 ((Int(op) _ Read(op)) ! 8i8y (expi[y] = expi0[y])) V ((Begin(op) _ Commit(op)) ! 8i8y (i 6= tran(op) ! expi[y] = expi0[y])) V (Write(op) ! 8y8i(y 6= var(op) ! expi[y] = expi0[y])) must be an invariant of the database system. (Notice that splitting the requirement from begin, read, commit and internal operations into cases is needed since the value of expi[y] does not have to be de ned outside of the transaction Ti.) Intuitively, serializability means that the sequence of occurrences can be re-arranged to form a sequence where the committed transactions are totally ordered. Several details should be noted:

 read{write consistency must be maintained in the permuted sequence, i.e., a read operation reads the last value written to the same variable (or to the initial value, if no previous write for that variable occurred).  read{write consistency is required only from the external operations of the transactions

that have committed. This corresponds to two observations: rst, the eect of the aborted transactions should not in uence serializability of the rest of the operations; second, transactions that are active (have not yet committed or aborted) can still be aborted later and therefore their eect is not taken into account.  Some restrictions may be imposed on rearranging operations. One such restriction requires that the internal order of the operations inside each transaction be maintained. This requirement can be weakened by an implementation that allows concurrency within transactions. On the other hand, it can be strengthened by an implementation that assigns transactions to sequential processors, imposing a total order among the operations of dierent transactions that are executed on the same processor.

2.3 Specifying Serializability in Linear Temporal Logic The syntax of the Linear Temporal Logic that will be used is extended with transition formulas, inspired by Lamport's temporal logic of actions [17]. Beside the set of state variables (sometimes also called exible variables, which will be used to denote the program's concrete and abstract variables, the logic uses another disjoint set of static variables. The dierence between state variables and static variables, as will be re ected in the following de nition, is that static variables are not allowed to change from state to state.

De nition 2.2 An extended LTL structure A is a quadruple hQ; T; q^; i where Q is a set of elements, T is a set of transitions, q^ is some distinguished element of Q,  is an alternating sequence of elements from Q and operations from T , 0 1 1 2 2 : : :, starting with 0 = q^.

7

A labeling function L assigns to each element q 2 Q an interpretation over the state variables, and for each static variable an interpretation xed over all elements.

Denote by L(q) the interpretation of the state and the static variables for the element q. The length of a sequence  is denoted j  j (! if it is in nite). The syntax of the extended LTL formulas  is as follows (notice that the until operator U is unnecessary in this framework, and therefore not de ned):  if ' is a transition formula, then ' 2 .  if '; 2  then ' _ ; :'; 2' 2 .  if ' 2  and z is a variable, then 9z ' 2 . The semantics of extended LTL is standard, except for the de nition of transition formulas and quanti cation:

 (A; L; i) j= T  (A; L; i) j= '  (A; L; i) j= '  (A; L; i) j= ' _  (A; L; i) j= :'  (A; L; i) j= 2'  (A; L; i) j= 9z'

() () () () () ()

j  j> i + 1 and hL(i ); i+1; L(i+1)ij= ', if ' is a transition formula. L(i ) j= ', if ' is a state formula. (A; L; i) j= ' or (A; L; i) j= . not (A; L; i) j= '. for each j  i, (A; L; j ) j= ' there exists a labeling function L^ , which diers from L by at most the assignment given to z, and (A; L^ ; i) j= '.

Notice that (1) quanti cation is allowed over state variables as well as static variables [3], and (2) classical formulas are a special case of transition formulas. An LTL formula ' is satis ed by an LTL structure A = hQ; T; q^; i and a labeling function L i (A; L; 0) j= '. A database system DS = hT; ~y; i generates a set of structure and labeling function pairs, such that for each such pair A = hQ; T; q^; i and L, with Q a set of database system states, T the set of database system operations, q^ a state satisfying the initial condition , and  = 0 1 1 2 2 : : : is a maximal sequence of states such that 0 = q^, and for each 0 < i 0 ?! x := x ? 1i, with
; = (x 6= 0 ^ x 6= ?1). If x is 0 or ?1, executing  changes the enabledness of , and so the two are not independent. Two additional restrictions are needed in order to preserve the labeling. Let Ri[x] be a read operation that involves the variable x, Wi[x] be a write operation that involves x, and any operation from T . Then the two additional restrictions can be formalized as 3R. (
R [x]; (~y) ^ enR [x] (~y) ^ en (~y) ) ! (expi[x](~y) = expi[x](f (~y) )) [the value of x calculated by transaction Ti is the same before and after executing from a state where
R [x]; holds], and i

i

i

3W. (
W [x]; (~y) ^ enW [x] (~y) ^ en (~y) ) ! (expi [x](fW [x] (~y) ) = expi [x](fW [x] (f (~y) ) ) ) [the value of x calculated by transaction Ti is the same after executing Wi[x] and after executing both and Wi [x] from a state where
W [x]; holds]. i

i

i

i

i

The predicate
; is used to identify the context (i.e., the set of global states) where  and are commutative. That is, when
; is true, if both the operations are executed in some order, the order of their execution can be reversed, obtaining the same result. Two histories, h and h^ are equivalent i their initial interpretations are the same and one of the strings is obtained from the other by repeatedly commuting adjacent operations only when the commutativity among them holds. When
; is false, the histories hJ;  i and hJ; i are not considered equivalent, even if  and are commutative when executed from the state J . For an extensive discussion on
; , see [13]. We can formally de ne now the equivalence between histories, based on independence between program operations. 11

De nition 3.2 The histories h = hJ; vi and ^h = hJ; wi are equivalent (denoted h  ^h) i there exists a sequence of histories hJ; v1i; hJ; v2i; : : :; hJ; vn i with v1 = v and vn = w and for each 1  i < n there exist v; v^ 2 T ; ; 2 T such that vi = v v^, vi+1 = v v^ and for h = hJ; vi; finh j=
; . An equivalence class of histories is called conditional trace. From the above requirement of the relation I , the same nal interpretation is shared by all histories of the same equivalence class of histories. Hence, we may let fin denote the nal interpretation of an equivalence class of histories . The semantics of a database system can be de ned as the set of conditional traces obtained from a set of independence conditions. Conditional traces will be called simply traces in the sequel. We sometimes identify a trace with its nal interpretation, writing  j= ' instead of fin j= '. The pre x relation 1 v 2 between traces 1 = [J; v], and 2 = [j; w] is de ned to hold i hJ; wi  hJ; vvi, for some v 2 T . It is said that 1 is subsumed by 2. If in addition, the length of v is shorter than the length of w by exactly one, it is said that 2 is an immediate successor of 1 (or that 1 is an immediate predecessor of 2). When v =  for some  2 T , it is said that 2 is the {successor of 1 (or that 1 is the {predecessor of 2). A directed set of traces  satis es that for each pair of traces ;  2 , it contains also a trace that subsumes both. A run is a maximal directed set of traces.

3.2 Using Interleaving Set Temporal Logic The logic ISTL (Interleaving Set Temporal Logic) deals with global states that correspond to partial order executions [12], or similarly, traces corresponding to runs [22]. Its modals resemble those in the branching time logic CTL [9] in its interpretation over abstract structures. It is also related to POTL [27] in the introduction of past operators. The version used here also adopts the transition formulas from Lamport's TLA [17].

De nition 3.3 Syntax

We inductively de ne two sets of formulae: ? (state formulae) and  (path formulae). State Formulas (?):  true 2 ?  if ' is a classical formula, then ' 2 ?.  if '; 2 ? then ' _ ; :' 2 ?.  if ' 2  then E ' 2 ?.  if ' 2 ? and z is a variable, then 9z ' 2 ?. Path Formulas ():  if ' 2 ?, then ' 2 .  if ' is a transition formulas, then ' 2 .  if ' 2 ? then ' 2 .  if '; 2  then ' _ ; :' 2 .  if '; 2  then ('U ); ('S ); X '; Y ' 2 .

12

De nition 3.4 An ISTL structure A is a quadruple hQ; T; q^; i where Q, T , q^ are as in

De nition 2.2, and  is a set of sequences, all starting with the state q^. A labeling function L for L is also de ned similarly to 2.2.

De nition 3.5 The de nition of satisfaction of ISTL formulas appears in Figure 1. Satisfaction of a state formula under a labeling function L and state q 2 Q:  (L; q) j= true  (L; q) j= ' () L(q) j= ', for ' a classical formula.  (L; q) j= ' _ () (L; q) j= ' or (L; q) j= .  (L; q) j= :' () not (L; q) j= '.  (L; q) j= E ' () there exists a path  2  and an integer 0  i 0 and (L; ; i ? 1) j= '. Figure 1: Semantics of ISTL

Abbreviations. false = :true , ' ^ = :( (:') _ (: ) ), ' ! = (:') _ , ' $ = (' ! ) ^ ( ! ' ), A' = :E (:'), F ' = (true U '), G' = :(true U (:') ), P ' = (true S '), H ' = :(true S (:') ), 8y ' = :9:'. 9!z'(z) = 9z'(z) ^ 8z0( (z0 6= z) ! :'(z0) ), where z0 does not appear free in ' (this is the exists one quanti er). A useful notation is the entailment operator [21] \)", where ' ) = AG(' ! ).

De nition 3.6 For every ' 2 ?, a structure A = hQ; T; q^; i, and a labeling function L, (A; L) j= ' i (L; q^) j= '. If (A; L) j= ' for every structure A and labeling function L, it is said that ' is valid.

For example, (A; L) j= EGF asserts that there exists a path in which holds in nitely often. For each run , a temporal structure A = hQ; T; q^; i and a labeling function L can be constructed, where Q is the set of traces of the run, q^ is the trace [J; "] of Q,  is the set of 13

maximal sequences, each of the form  = 0 1 1 2 2 : : :, where all the traces on the sequence are from Q, 0 = q^, and for each 0 < i j  j, i is the i{successor of i?1. The labeling function L assigns for each variable in each state of Q its value according to the nal interpretation of the trace generating the state. A formula is said to be valid for a database system if A j= ' for every structure A and labeling function L associated with the runs of the database system.

3.3 Specifying Serializability A backwards path for  is a nite sequence of traces 0 1 1 2 : : : n n, such that  = 0, n = [J; "] for some interpretation J , and for each 0 < i  n, i?1 is the i{successor of i. Then, hJ; n n?1 : : : 1i is a history that belongs to . The observation that a path can be viewed either as a sequence of traces, or as a sequence of operation occurrences is crucial to the speci cation. It allows asserting the existence of an appropriate permutation of the histories at each trace  by specifying the existence of a backwards path from . This backwards path can be identi ed using temporal past modals. In particular, it is the appropriate permutation of the histories in  that satis es restrictions such as sequentialily (transaction by transaction) and read{write consistent behavior.

3.3.1 No failure assumption To develop the speci cation of serializability, let us begin with two constraining assumptions that are not reasonable in the general case and thus will be abandoned later. Nevertheless, they will allow a systematic development of the ideas. Assume rst that none of the transactions is allowed to abort. Furthermore, assume that each execution is nite, ending with a state where no transaction remains active. In order to de ne serializability formally, we de ne the predicate quiescent i to hold when the transaction Ti is not active. That is, Ti has already terminated or has not yet started. When a concrete system is given, the predicate quiescent i can be written precisely, using the set of variables, function and relation symbols appropriate for that system. An example that illustrates how this can be done will be given in the next section. A state in which no transaction is active is denoted by the predicate quiescent (quiescent =4 8i quiescent i). The initial states, satisfying , are obviously quiescent. We assume that  cannot hold in states that are not initial (i.e., it is impossible to reach again a state satisfying  during an execution of the database system). This requirement can easily be achieved using auxiliary variables. Alternatively, we can replace  with AY false (which holds exactly in states that initiate the execution). Recall that p ) q means AG(p ! q), and so relates to every state. From any state in which all of the transactions are quiescent, there must be a backwards path that reaches the starting state and satis es two restrictions: Going backwards is done transaction by transaction. That is,

quiescent ) E (sequential S ) 14

(1)

where sequential is de ned as

quiescent _ 9!i :quiescenti: This speci cation relies on the fact that in the computation model of transactions, at most one transaction can change its state from active to non-active (quiescent) or vice versa, by executing a single operation. This property of the model can be written as

8i 8j ( (:(quiescenti $ quiescent0i) ^ i 6= j ) ) (quiescentj $ quiescent0j) ) : The sequence of reads and writes is consistent. Thus, there should exist a state function M (for memory) that returns for each abstract variable in each state a value that is consistent with the order of the reads and writes. Initially 8x (M[x] = exp0[x]).

quiescent ) E ( (Y consistent) S )

(2)

where consistent is de ned as 8i 8x 8u( (Ri[x; u] ! ( (M[x]= u) ^ (M0[x]= u) ) )^ (Wi[x; u] ! (M0[x] = u) )^ ( (:Write(op) _ var(op) 6= x) ! (M[x]= M0[x]) ) ) : These formulas must be combined into a single assertion so that both requirements refer to the same backwards sequence.

9exp 9M (8x (M[x]= exp0[x] ) V AG restrict V (quiescent ) E ( (sequential ^ (Y consistent) ) S ) ) ) : Notice that as in the LTL case, quantifying over exp and M implies that the temporal logic is de ned over a second order logic. However, when verifying a speci c implementation, the occurrences of these functions within the formula are replaced by the user-supplied expressions for expi[y], over the database concrete variables, and the resulting formula to be veri ed is then in rst order temporal logic.

3.3.2 Adding Aborts and Active Transactions The next step is to abandon the assumption about the non-existence of aborted transactions. The general de nition of serializability requires sequentiality and consistency only from operations that belong to committed transactions. The mapping M ignores aborted transactions by recording in M only the eect of the operations that belong to transactions that will commit. In order to tell whether an operation belongs to a transaction that is about to commit or abort, we assume there is a prophecy function ignore, such that for each transaction Ti, ignorei returns a boolean value consistent with the future behavior of the transaction, and remains xed throughout the execution. That is, Ti may abort only if ignorei holds, and it may commit only 15

if ignorei does not hold. This can be speci ed by asserting that the state function ignorei satis es (encommiti ) :ignorei) ^ (enabort ) ignorei ). The state predicates ignorei can be incorporated into the database system as boolean prophecy variables. These are auxiliary variables [6, 24] which predict the future. Their de nition appears in [1], and in a dierent form in [23]. Here we only need to use static prophecy variables, i.e., variables whose value does not change during the execution. Unlike history variables, which accumulate information about the history of the computation, prophecy variables guess the future. Thus, these variables can in uence the enabledness of an operation, based on a previous guess. The guessing must be constrained in such a way that the set of execution sequences of the database system is not altered. States of the transformed database system (the database system after adding the prophecy variables) are called augmented states, while sequences of augmented states are augmented sequences. The part of an augmented state or augmented sequence that contains only the interpretation of the original variables is called the projection of the state or the sequence (on the set of original variables), respectively. When adding prophecy variables in our context, it is required that (a) for each nite augmented sequence, its projection forms a legal sequence of the original database system, and (b) for each nite sequence, there exists a corresponding augmented sequence with prophecy variables. These requirements are maintained when applying the restrictions given in [1], without the requirement that for each database system state there corresponds a nite set of augmented states. This is problematic in our context because the number of transactions is not bounded, but is not needed since we care here only about nite sequences. A standard construction, where the conjunct ignorei is added to the enabling condition of aborti, and the conjunct :ignorei is added to the enabling condition of commiti, expresses the requirements from prophecy variables. This construction is exempli ed in the next section. Having developed the machinery, we are ready to provide the speci cation. First, observe that the aborted transactions can be interleaved with non-aborted transactions in various ways. Therefore, we cannot assume as before that there exists a backwards path that retracts transaction by transaction. Instead, we require that this is true only for the non-aborted part. Furthermore, the consistency requirement ignores the reads and the writes of the aborted transactions as if they never occurred. We previously assumed that each execution is nite, ending in a state where no transaction remains active. If this is no longer assumed, the computation might be in nite with active transactions appearing in every global state. Observe that active transactions should be treated like aborted ones. This means that the eect of their read and write operations on transactions that commit is ignored. Now, for every global state there exists a guess where all the active transactions Ti have ignorei = true . We rede ne the predicate quiescent to agree with these guesses by setting quiescent =4 8i (:quiescenti ! ignorei). Note that quiescent is now a restriction on the values of ignorei, but that every history will satisfy it for some such assignment of values. Now at most one transaction that is going to commit may be active on the backwards path from a quiescent state at any given time (but an arbitrary number of active transactions that are going to abort). Thus, sequential should be rede ned in formula (1) as (quiescent _ i

16

9!i (:quiescenti ^ :ignorei) ).

The formula (2) must take care of the consistency between read and write operations that belong to transactions that are committed. This is achieved by rede ning consistent to be

8i 8x 8u( ( (Ri[x; u] ^ :ignorei) ! ( (M[x]= u) ^ (M0[x]= u) ) )^ ( (Wi[x; u] ^ :ignorei) ! (M0[x] = u) )^ ( (:Write(op) _ (var(op) = 6 x) _ ignorei) ! (M[x] = M0[x] ) ) ) Again, the reformulated requirements (1) and (2) should be combined to refer to the same representative sequence, as follows:

9exp 9ignore9M (8x (M[x]= exp0[x] ) V 8i ( (encommitV ):ignorei) ^ (enabort )ignorei) ) V

AG restrict (quiescent ) E ( (sequential ^ (Y consistent) ) S ) ) ) i

i

(3)

3.4 Proof Rules for Verifying Serializability The proof rules in this subsection are closely related to the proof system developed in [26] for the logic ISTL [12]. The formulas '; ;  stand for classical formulas, while  stands for a transition formula. The typical formula of an operation  is  = en ^ (~y0 = f(~y) ) ^ (op = ). This is a transition formula describing the connection between interpretations J and J 0 such that J 0 is obtained from J by executing . The rule INV is used to prove that an assertion  is an invariant of the database system (recall that  is the initial condition). The case that  is an implication is useful as a premise in other rules when entailment is expected. (Recall that 0, which appears in premise I2 of INV, is the primed version of the formula , and that a classical formula  can be used here as a special case of a transition formula.) INV

I1  !  I2 ( ^  ) !  0, for each  2 T I3  ! 

AG

The rule SINCE, has a consequent appropriate for proving the formulation for serializability in (3) in Section 3.3.2. It is based upon nding a formula  stronger than  (S3). When  holds in a trace , there exists an immediate predecessor ^ of , such that ^ satis es either  or (S2). Furthermore, the pair of traces ^ and  together with the operation  that causes the transition between them satisfy the transition formula . Each state  j= ' satis es either or  (S1). A trace satisfying must be reached, as each backwards sequence is nite. 17

SINCE

S1 ' ) ( _ ) S2  ) EY ( ( _ ) ^ ) S3  ) 

' ) E ( ( ^ Y )S )

The completeness of the rule relies on complete proof rules for properties of the form ' ) EY given below. Then,  can be chosen to be a formula that is satis ed by nal interpretations of traces  that begin a backwards path containing a trace  j= . We want exactly those  such that on the part of the path from  to , all the traces except possibly  satisfy , and all adjacent pairs of traces in the sequence, together with the relevant operation, satisfy . Such an  satis es the premises of the proof rule. Notice that the ability of adding auxiliary variables to the database system is essential to the completeness of this rule, and the rule BACK in the sequel [26]. Proving S2 of rule SINCE uses the following proof rules. CASE2

CASEN

' ) ( '1 _ '2 ) '1 ) EY  '2 ) EY  ' ) EY 

' ) 9 '^ ( ) '^ ( ) ) EY  ' ) EY 

The rule CASE2 allows proving ' ) EY  by splitting the traces satisfying ' into two sets, '1{traces (i.e., traces whose nal interpretation satisfy '1) and '2{traces, proving the entailment for each subset separately. If it is necessary to separate the traces into n sets, this rule can be applied repeatedly. The rule CASEN allows splitting the traces satisfying ' in a parametric manner. This is useful when the formula ' needs to be decomposed into a number of cases which is not nite or not constant. The basic rule that allows proving a property of the form ' ) EY  is BACK. Let T  T be a set of operations, B1 B2 B3 B4 B5

BACK

') wp () ) , for each 62 T wp (wp () ) )
; , for each  2 T ; 62 T  ) : ('0 ^ ) ) , for each  2 T ' ) EY 

The intuition behind this proof rule is as follows: Let  j= ' and 0 1 1 2 : : : n n be a backwards sequence for . Advancing along the sequence of operations 12 : : :n , some  2 T must be found. As long as no such operation is found,  holds (B1,B2). Such an operation  2 T must occur, as the initial states do not satisfy  (B4), and a backwards sequence is nite. If some  2 T now occurs, it is commutative with all the operations that have occurred so far (B3). 18

Thence,  can be commuted to occur as the last operation in some history of . Finally, a triple h; ; i, where  2 T ,  j= ', and  is the {predecessor of , satis es  (B5). Finally, we allow using any rst order tautology (over an appropriate many{sorted domain) as an axiom. This is needed to achieve relative completeness.

4 Examples 4.1 Two Phase Locking We consider a version of the Two Phase Locking Algorithm [10]. Each transaction that needs to issue a read or a write operation on some abstract variable x must rst acquire a lock lock[x] that grants the transaction exclusive use of the variable. It is said that the transaction locks the variable x. (In a more permissive version, there are exclusive write locks and a sharable read lock, so that more concurrency can be gained). When a transaction does not need to use a variable any more, it may free the lock it gained on it or unlock it. The transactions undertake a regime according to which, once a transaction has started unlocking, it cannot lock any further variables. The version of the algorithm given here is somewhat simpli ed, in order to reduce the details needed in the veri cation (however, without losing the basic intuition of the full{ edged algorithm). The restrictions are: (a) shared read locks are not allowed (as explained above), (b) acquiring locks is done within the read and write operations and not by using separate Lock and Unlock operations, and (c) unlocking occurs when committing or aborting. The code of the external operations of the 2PL algorithm is given in Figure 2. It is written in a free syntax, partially inspired by [18]. The operations B , R, W , C , and A stand for begin, read, write, commit, and abort, respectively. The vector element var[x] is used to hold the last updated value of x. Thus, expi[x] = var[x], for every transaction Ti (including those that will eventually abort). Local variables are not indexed when appearing in the code of an operation. For instance, written in Bi refers to writteni. The global operations are denoted with san{serif letters. The read operations always store the value being read in a local variable val. Similarly, the write operation obtains the value to be written from val. The internal operations of the database system can freely access and modify this variable. Auxiliary variables are added in bold letters. The code that is added to handle the auxiliary variables is put inside  and . Auxiliary variables are local, except for the vector last used that is addressed by the names of the abstract variables. Recall that ignorei are the prophecy variables de ned in Section 3.3.2. The initial condition of this algorithm is 8i (quiescenti ^ :startedi) ^ 8x ( (last used[x] = 0) ^ (var[x] = exp0[x]) ). The commutativity among database system operations is summarized in Table 1. Operations of the same transaction are considered interdependent. Internal (parametric) operations allow assigning arbitrary values to the local variables val and to internal variables that are not mentioned in the above operations. These operations are independent of all the operations of other transactions. 19

Bi : :started ! started := true ; quiescent := false ; written := ; locked := ;  last op := Bi  Ri[x] : :quiescent ^( (lock[x] = i) _ (lock[x] = unlocked) ) ?! lock[x] := i locked := locked [ fxg val := var[x];  last used[x] := i; last op := Ri[x]  Wi[x] : :quiescent ^( (lock[x] = i) _ (lock[x] = unlocked) ) ?! lock[x] := i; locked := locked [ fxg; if x 62 written then written := written [ fxg; saved[x] := var[x] endif var[x] := val;  last used[x] := i; last op := Wi[x]  Ci : :quiescent  ^:ignore ?! for each x 2 locked do lock[x] := unlocked; quiescent := true ;  last op := Ci  Ai : :quiescent  ^ignore ?! for each x 2 written do var[x] := saved[x]; for each x 2 locked do lock[x] := unlocked; quiescent := true ;  last op := Ai  Figure 2: The Two Phase Locking algorithm

Bi Ri[x] Wi[x] Ci Ai

Bj

Wj [y]

Rj [y]

Cj

true true true true true x 6= y x 6= y x 62 lockedj true x 6= y x 6= y x 62 lockedj lockedi\ true y 62 lockedi y 62 lockedi locked j= lockedi\ true y 62 lockedi y 62 lockedi locked = j

Aj

true

x 62 lockedj x 62 lockedj lockedi\ lockedj =  lockedi\ lockedj = 

Table 1: Commutativity for the two phase locking algorithm 20

Proving serializability of 2PL will be sketched below. The memory function M, used in the proof to show consistency, expresses that the eective value of the abstract variable x is held in var[x] when x was last written by a transaction Ti that was or will be eventually committed (i.e., having ignorei = false), and in savedi[x] otherwise. In order to de ne M formally, let the function if be de ned ( a if cond = true if(cond; a; b) = b if cond = false : Now we can de ne M[x] as if

(last used[x] = 0, exp0[x]; if( ignorei ^ x 2 writteni ^:quiescenti; savedi[x]; var[x] ) ), where i = last used[x].

First, as in most correctness proofs, some invariants are proved. This is done using the rule INV. The rst invariant, I1 :: 8i 8x ( (:quiescenti ^ x 2 lockedi) ! ( (last used[x] = i) ^ (lock[x] = i) ) ) asserts that when a transaction Ti is active, no other transaction has accessed any of the abstract variables that Ti has locked and not yet released. This is obvious, as Ti did not perform its unlockings while still active. The second invariant, I2 :: : ! 9i (startedi ^ 8x (x 2 lockedi ! (last used[x] = i) ) ) asserts that in every non{initial state there exists a transaction Ti such that no other transaction has yet accessed the abstract variables that Ti accessed (even in the case that all the transactions are quiescent at the moment). This holds initially. If Ti is the witness (an element which can be instantiated for the existentially quanti ed variable) for such a transaction, and Tj has accessed some variable after Ti accessed it, then Tj becomes immediately the witness for I2. Another useful invariant is I3 :: 8i( (startedi^quiescenti) ! ( ( (last opi = Ci)^:ignorei)_ ( (last opi = Ai) ^ ignorei) ) ). The formulation of serializability (3) has four conjuncts. The rst one, namely 8x (M[x]= exp0[x] ), must be shown to be implied by the initial condition . The second conjunct requires the invariant I4 :: 8i ( (encommit ! :ignorei) ^ (enabort ! ignorei) ) to be proved. This is immediate from the construction of prophecy variables. The third, i.e., AG restricted is a trivial invariant. The fourth conjunct is of the same type as the consequence of rule SINCE. The formula  needed in the premises of SINCE can be chosen in this example to be i

i

 = (: ^ quiescent) _ 9!i (:quiescenti ^ :ignorei) Then, S1 and S3 obviously hold. It remains to prove S2, i.e.,  ) EY ( ( _ ) ^ consistent). First, we decompose the traces satisfying  by a repeated application of the rules CASE2 and CASEN. This is demonstrated in Figure 3 using a tree whose nodes (boxes) contain formulas. The root node contains . The set of traces satisfying a formula in some box of the tree is decomposed into sets of traces satisfying the formulas in its immediate descendant boxes. The proof rule 21

used in decomposing the traces or rather the formula is denoted next to the edges emanating from a box. If CASEN is used, the parameter used for the decomposition is also written. A `' symbol is used to avoid rewriting large formulas, and should be replaced with the formula in the parent node. Each formula ^ in a leaf node can now be used to verify ^ ) EY ( ( _ ) ^ consistent). This is done using the proof rule BACK. The formula  needed (for each ^) in the premises B1|B4 of this rule can be obtained as the conjuncts of ^ that appear underlined in the appropriate box for ^ in Figure 3. (: ^ quiescent) _ 9!j (:quiescentj ^ :ignorej) CASE2

?

: ^ quiescent

? : ^ 8i quiescenti

CASE2

CASEN(j ) using I2

? : ^ quiescent^ 9j (:quiescentj ^ ignorej ) CASEN(j ) using I1

??? ??? quiescent^ : ^ 8i quiescenti :quiescentj ^ ignorej ^ ^startedj ^ 8x (x 2 lockedj ! 8x (x 2 lockedj ! (last used[x] = j ) ) (last used[x] = j ) ) ?CASE2, using I3 ? CASEN() ^ (last opj=Cj ) ^ (last opj=Aj ) ? ? ? ^ (last opj=) ^ignorej ^:ignorei T = fCig T = fAig T = fg

? 9!j (:quiescentj ^:ignorej )

CASEN(j ) using I1

??? :quiescentj ^ :ignorej ^ 8x (x 2 lockedj ! (last used[x] = j ) ) CASEN()

??? ^ (last opj=) T = fg

Figure 3: Sketch for proving serializability for 2PL

4.2 Multi-Version Timestamp Order Another example for a commutativity{based algorithm is the MVTO algorithm [4]. It allows transactions to be serialized according to the total order among the timestamps that each transaction gets upon starting. The algorithm implements each variable by holding a set version[x] of triples hu; wr; rdi for it, as demonstrated in the introduction. When a transaction with timestamp t wants to read a variable x, it chooses the triple hu; wr; rdi from x's set with the greatest wr that is still smaller than t. (The set is never empty, as it is initialized with a single triple fhexp0[x]; 0; 0ig for some initial value exp0[x].) If t > rd, it changes the rd component into t. Thus, expi[x] = xv:u, where xv 2 version[x] ^ (xv:t = maxfxt:wr j xt 2 version[x] ^ xt:wr  tig). 22

Bi : :started ! started := true ; quiescent := false ;  written := ;  last started := last started + 1; t := last started; depends upon := ;  last op := Bi  Ri[x] : :quiescent ^ (depends upon \ aborted = ) ?! xt := the triple xv 2 version[x] with maximal xv:wr s.t. xv:wr  t xt:rd := max(xt:rd; t); val := xt:u; if xt:wr 6= t then depends upon := depends upon [ fxt:wrg;  last op := Ri[x]  Wi[x] : :quiescent ^ (depends upon \ aborted = ) ^ :9xv (xv 2 version[x] ^ xv:wr < t < xv:rd) ?! if 9xt (xt 2 version[x] ^ (xt:wr = t) ) then xt:u = val else version[x] := version[x] [ fhval; t; tig;  written := written [ fxg; last op := Wi[x]  Ci : :quiescent ^ (depends upon  committed)  ^:ignore ?! committed := committed [ ftg;  last op := Ci  Ai : :quiescent  ^ignore ?! aborted := aborted [ ftg; for each object x 2 written do for each element xv 2 version[x] do if xv:wr = t then version[x] := version[x] n fxvg;  last op := Ai  Figure 4: The multiversion timestamp algorithm When a transaction Ti with timestamp t wants to write the value u^ to x, the concurrency control algorithm checks rst if there exists a tuple hu; wr; rdi such that wr < t < rd in x's set. The existence of such a tuple prevents Ti from issuing the write operation since then the read by the transaction with timestamp rd should have been from the newly generated version by Ti. In this case, Ti aborts. Otherwise, Ti adds a new tuple hu^; t; ti to the set of x. The initial condition of this algorithm is

8i(quiescenti^:startedi)^8x( (version[x] = fhexp0[x]; 0; 0ig)^(aborted = )^(committed = ) ) The algorithm appears in Figure 4. The predicate
; is listed below, according to the dierent possibilities. The cases not listed (for example,  = Ai, = Aj ), have
; = true .

; 2 i: Operations of the same transaction are always interdependent. Thus,
; = false . 23

 = Wi[x]; = Rj [x];i 6= j : Here the dependency is
; = (ti > tj )_(maxft j xv 2 version[x]^ (xv:wr = t) ^ t  tj g > ti). That is, either the read is issued by a transaction with a smaller timestamp than the transaction that issued the write, or the write produces a version that is earlier than the one that is being read.  = Ci; = Cj ; i 6= j : Two commits are commutative if neither transaction reads a version that the other has prepared. Thus,
; = ti 62 depends uponj ^ tj 62 depends uponi .  = Ri [x]; = Aj ; i 6= j : A read and an abort are commutative if the read refers to a version that was not created by the transaction that is aborted. That is,
; = (maxft j xv 2 version[x] ^ (xv:wr = t) ^ t  tig 6= tj ). A detail that is important to the veri cation of the algorithm is the memory function M imposing the read{write consistency. It is de ned such that

M[x] = xv:u; where xv:wr = maxft j xv 2 version[x] ^ ( (t = 0) _ 9i ((xv:wr = ti) ^ startedi ^ :ignorei) ) g: That is, M returns the latest version of x that is or will be eventually committed.

Veri cation in this case is simple and will be described only in general terms. The proof is based on the observation that a backwards sequence exists in which the operation extracted from a trace in the sequence (resulting in the next trace in the sequence) is the last executed operation (last opi) of a transaction Ti, according to the following rules: 1. Ti has the maximal timestamp, and has committed, or otherwise, 2. Ti has the maximal timestamp among the transactions that satisfy one of the following properties:  last opi = Wi[x] and no transaction has read this version of x yet,  last opi = Ri[x] and the transaction that has written this version of x has not yet aborted,  last opi = Ai and no transaction Tj with a greater timestamp has read an earlier version of some abstract variable (with a smaller timestamp) than the version written by Ti (this would imply that unless Ai was issued, Tj would have read the version prepared by Ti), or  last opi = Bi or last opi 2 Int.

5 Conclusions We have seen two alternative methods to specify serializability. The rst one is written in linear temporal logic and includes direct assertions about sequences of operations. The speci cation explicitly uses the history of execution, and requires a function and predicates de ned for such histories. 24

The alternative speci cation method presented is given in ISTL . It is limited to the speci cation of concurrency control algorithms based upon commutativity. This includes most of the familiar algorithms. This speci cation makes more extensive use of the modals of the logic, instead of referring explicitly to variables containing the entire history of the computation. The consistency and sequentiality requirements use assertions about the relation between successive states in some equivalent history of computation. This kind of speci cation, based upon the (partial order) semantics of conditional traces, is appealing because the veri cation can be done locally. That is, the veri cation requires proving invariants and calculating predicate transformers (no actual ISTL reasoning is needed). Such proofs can also be checked with the help of computerized veri ers. This diers from many proofs in the literature, which begin by proving a series of lemmas about equivalent sequences of operations. The use of state assertions based on the value of the system variables also allows for the formal veri cation of speci c implementations, in addition to verifying general concurrency control algorithms.

References [1] M. Abadi, L. Lamport, The Existence of Re nement Mappings, Proceedings of the 3rd Annual Symposium on Logic in Computer Science, 1988, 165-175. [2] B. Alpern, F.B. Schneider, De ning Liveness, Information Processing Letters 21, 1985, 181-185. [3] H. Barringer, R. Kuiper, A. Pnueli, A Really Abstract Concurrent Model and its Temporal Logic, 13th ACM Symposium on Principles of Programming Languages, 173-183. [4] P. A. Bernstein, N. Goodman, Multiversion Concurrency Control: Theory and Algorithms, ACM Transactions on Database Systems 8, 465-483, 1983. [5] P. A. Bernstein, V. Hadzilacos, N. Goodman, Concurrency control and Recovery in Database Systems, Addison-Wesley, 1987. [6] M. Clint, Program proving: Coroutines, Acta Informatica 2, 1973, 50{63. [7] E.W. Dijkstra, Guarded Commands, Nondeterminancy and Formal Derivation of Programs, Communications of the ACM, 18(1975), 453-457. [8] E. A. Emerson, E. M. Clarke, Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons, Science of Computer Programming 2, 1982, 241-266. [9] E.A. Emerson, J.Y. Halpern, "Sometimes" and "Not Never" Revisited: on Branching Versus Linear Time Temporal Logic, Journal of the ACM 33(1986), 151-178. [10] K. P. Eswaran, J. N. Gray, R. A. Lorie, I. L. Traiger, The Notions of Consistency and Predicate Locks in a Relational Database System, Communications of the ACM 8, 624633, 1976. 25

[11] M. P. Herlihy, J. M. Wing, Axioms for Concurrent Objects, 14th ACM Symposium on Principles of Programming Languages, 1987, 13-26. [12] S. Katz, D. Peled, Interleaving Set Temporal Logic, 6th ACM Symposium on Principles of Distributed Computing, Vancouver, Canada, August 1987, 178-190; revised version in Theoretical Computer Science, Vol 75, No. 3, 263-288. [13] S. Katz, D. Peled, De ning Conditional Independence Using Collapses, Theoretical Computer Science, vol. 101(1992), pp. 337-359. [14] L. Lamport, On Interprocess Communication, Part I: Basic Formalism, Distributed Computing 1 (1986), 77-85. [15] L. Lamport, A Simple Approach to Specifying Concurrent Systems, Communications of the ACM, 32, 32-45. [16] L. Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems, 5, 190-222. [17] L. Lamport, A Temporal Logic of Actions, Research Report SRC57, Digital Equipment Corporation, Systems Research Center, April 1990. [18] 1987 Lake Arrowhead Workshop, How Will We Specify Concurrent Systems in the Year 2000? Report and Call for Papers. [19] O. Lichtenstein, A. Pnueli, L. Zuck, The Glory of the Past, Proceedings of Conference on Logics of Programs, LNCS 193, Springer-Verlag, 196-218. [20] Z. Manna, A. Pnueli, How to Cook a Temporal Proof System for Your Pet Language. Proceedings of the 10th ACM Symposium on Principles on Programming Languages, Austin, Texas, 1983, 141-151. [21] Z. Manna, A. Pnueli, The Anchored Version of the Temporal Framework, School/Workshop on Linear Time, Branching Time and Partial order in Logics and Models, The Netherlands, Lecture Notes on Computer Science 254, 201-281. [22] A. Mazurkiewicz, Trace semantics, Proceedings of an advanced course, Bad Honnef, September 1986, Lecture Notes in Computer Science, 255. [23] E. R. Olderog, K. R. Apt, Fairness in Parallel Programs, The Transformational Approach, ACM Transactions on Programming Languages and Systems 10, 420-455. [24] S. Owicki, A consistent and Complete Deductive System for the Veri cation of Parallel Programs, Proceedings of the 8th Annual Symposium on Theory of Computing, 1976, 7386. [25] C. H. Papadimitriu, The Theory of Concurrency Control, Computer Science Press, Rockville, MD, 1986. 26

[26] D. Peled, A. Pnueli, Proving Partial Order Liveness Properties, in M. S. Paterson (Ed.), International Colloquium on Automata, Languages and Programming, Warwick University, England, July 1990, Lecture Notes in Computer Science 443, Springer{Verlag, 553-571. [27] S. Pinter, P. Wolper, A Temporal Logic for Reasoning about Partially Ordered Computations, Proceedings of the 3rd ACM Symposium on Principles of Distributed Computing, Vancouver, B. C., August 1984, 23-27. [28] A. Pnueli, Applications of Temporal Logic to the Speci cation and Veri cation of Reactive Systems, a survey of current trends, in J.W. de Bakker, W.P. de Roever, and G. Rozenberg (eds.) Current Trends in Concurrency, LNCS 224, Springer-Verlag, 1986. [29] F.B.Schneider (Ed.), Special Issue on Speci cation of Concurrent Systems, Distributed Computing, Vol. 6, No. 1, Springer{Verlag, 1992. Special issue [30] W. E. Weihl, Local Atomicity Properties: Modular Concurrency Control for Abstract Data Types, ACM Transactions on Programming Languages and Systems 11, 249-283. [31] W. E. Weihl, Commutativity{Based Concurrency Control for Abstract Data Types, IEEE Transactions on Computers 37, 1488-1505. [32] J. M. Wing, Verifying Atomic Data Types, in J. W. deBakker, W. P. deRoever, G, Rozenberg (Eds.), Re nement of Distributed Systems, Lecture Notes in Computer Science 430, Springer{Verlag, 731-758.

27