1 local b :false,p,ci 1 lock L1; (MName）f∈String (ThrdID)t E Nat while (!b){ 2 local r :L2; (p,c):=find(e); 心 h11e(r1=0)[ (Epr）E:=x|n|E+E| lock p;lock c; unlock Li; (BExp)B ::true false E=E!B... 5 b :validate(p,c); 5 lock L1; (Instr)c:=:=E:=[E][E]:=E I print(E)1... 6 if (!b){ 6 x:=L2; 1 unlock c;unlock p; > () C ::=skip l c lx :f(E)I return E I (C) 8 心 lock L2; C;C if(B)C else C while(B)C} update(p,c,e); 9 unlock L2; (Prog)W ::skip let II in C...C 10 unlock c;unlock p; 10 unlock L1; (ODecl)Π，T={fh(r1,C1),.,fn(rn,Cn)} (a)optimistic list (b)rollback (S1ore)s,s∈ar⊥nt (Heap)h,h∈Nat一lmt Figure 2.Examples with multiple locks. (Mem)o,2:=(s,h) (PState)S::=(c;0o;...) successfully acquires the lock,which allows it to eventually finish Figure 3.The language syntax and state model. the dfInc method.Thus the system as a whole progresses Nevertheless,as explained in Sec.2.2.2,we have to make sure the queue jump(which is a special form of delay)is a"good"one. levels constitute a tuple (mk,...,m2,m).It is strictly descending We follow the token-transfer ideas [16.24]to support disci- along the dictionary order. plined queue jumps.We explicitly specify in the rely/guarantee The stratified -tokens naturally prohibit the circular delay conditions which steps could delay the progress of other threads problem discussed in Sec.2.2.2 with the object in Fig.2(b).The (jump their queues).To prohibit unlimited queue jumps without deadlock-free optimistic list in Fig.2(a)can now be verified.We making progress,we assign a finite number m of -tokens to an classify its delaying actions into two levels.Actions at level 2(the object method,and require that a thread can do at most m delaying highest level)update the list,which correspond to line 9 in Fig.2(a), actions before the method finishes. and each method can do only one such action.Lock acquirements Whenever a step of thread t'delays the progress of thread t. are classified at level 1,so a thread is allowed to roll back and we require t'to consume one -token.At the same time,thread t re-acquire the locks when its environment updates the list. could increase O-tokens so that it can loop more rounds.Besides we redefine the definite progress condition to allow the metric E 3. Programming Language (about the length of the queue)to be increased when an environment Figure 3 gives the syntax of the language.A program W consists of thread jumps the queue at the cost of a -token. multiple parallel threads sharing an object II.We say the threads are 2.3.4 Allowing Rollbacks for Optimistic Locking the clients of the object.An object declaration II is a mapping from a method name f to a pair of argument and code (method body) The ideas we just explained already support simple deadlock-free The statements C are similar to those in the simple language used objects such as dfInc in Fig.1(b),but they cannot be applied to for separation logic.The command print(E)generates exterally objects with optimistic synchronization,such as optimistic lists [13] observable events,which allows us to observe behaviors of programs. and lazy lists [11]. We assume it is used only in the code of clients.We use (C)to Figure 2(a)shows part of the optimistic list implementation. represent an atomic block in which C is executed atomically Each node of the list is associated with a TAS lock,the same lock To simplify the presentation,we make several simplifications as in Fig.1(b).A thread first traverses the list without acquiring any here.We assume there is only one concurrent object in the system locks (line 3).The traversal find returns two adjacent node pointers Each method of the object takes only one argument,and the method p and c.The thread then locks the two nodes (line 4),and calls body ends with a return E command.Also we assume there is no validate to check if the two nodes are still valid list nodes (line 5) nested method invocation.For the abstract object specification I, If validation succeeds,then the thread performs its updates(adding each method body is an atomic operation(C)(ahead of the return or removing elements)to the list (line 9).Otherwise it releases the command),and executing the code is always safe and never blocks two node locks (line 7)and restarts the traversal. The model of program states S is defined at the bottom of Fig.3 For this object,when the validation fails,a thread will release To ensure that the client code does not touch the object state,in S the locks it has acquired and roll back.Thus the thread may acquire we separate the states accessed by clients (oe)and by the object the locks for an unbounded number of times.Since each lock ()Here S may also contain auxiliary data about the control stacks acquirement will delay other threads requesting the same lock and for method calls.Execution of programs is modeled as a labeled each delaying action should consume one -token,it seems that transition system(W,S)(W',S').Here e is an event (either the thread would need an infinite number of -tokens.which we observable or not)produced by the transition.We give the small-step prohibit in the preceding subsection to ensure deadlock-freedom, transition semantics in TR [22]. even though this list object is indeed deadlock-free. Below we often write X,s and h for the notations at the abstract We generalize the token-transfer ideas to allow rollbacks in order level to distinguish from the concrete-level ones (o.s and h). to verify this kind of optimistic algorithms,but still have to be careful to avoid the circular delay caused by the "bad"rollbacks in 4. Fig.2(b),as we explain in Sec.2.2.2. Program Logic LiLi Our solution is to stratify the delaying actions.Each action is LiLi verifies the linearizability of objects by proving the method now labeled with a level k.The normal actions which cannot delay implementations refine abstract atomic operations.The top level other threads are at the lowest level 0.The -tokens are stratified judgment is in the form of D,R,GP)I<T.(The oBJ rule for accordingly.A thread can roll back and do more actions at level k this judgment is given in Fig.7 and will be explained later.)To verify only when its environment does an action at a higher level k',at the an object II,we give a corresponding object specification I(see cost of a k'-level -token.Note that the -tokens at the highest level Fig.3),which maps method names to atomic commands.In addition are strictly decreasing,which means a thread cannot roll back its we need to provide an object invariant (P)and rely/guarantee actions of the highest level.In fact,the numbers of -tokens at all conditions (R and G)for the refinement reasoning in a concurrent 3891 local b := false, p, c; 2 while (!b) { 3 (p, c) := find(e); 4 lock p; lock c; 5 b := validate(p, c); 6 if (!b) { 7 unlock c; unlock p; } 8 } 9 update(p, c, e); 10 unlock c; unlock p; (a) optimistic list 1 lock L1; 2 local r := L2; 3 while (r != 0) { 4 unlock L1; 5 lock L1; 6 r := L2; 7 } 8 lock L2; 9 unlock L2; 10 unlock L1; (b) rollback Figure 2. Examples with multiple locks. successfully acquires the lock, which allows it to eventually finish the dfInc method. Thus the system as a whole progresses. Nevertheless, as explained in Sec. 2.2.2, we have to make sure the queue jump (which is a special form of delay) is a “good” one. We follow the token-transfer ideas [16, 24] to support disci￾plined queue jumps. We explicitly specify in the rely/guarantee conditions which steps could delay the progress of other threads (jump their queues). To prohibit unlimited queue jumps without making progress, we assign a finite number m of -tokens to an object method, and require that a thread can do at most m delaying actions before the method finishes. Whenever a step of thread t 0 delays the progress of thread t, we require t 0 to consume one -token. At the same time, thread t could increase ♦-tokens so that it can loop more rounds. Besides, we redefine the definite progress condition to allow the metric E (about the length of the queue) to be increased when an environment thread jumps the queue at the cost of a -token. 2.3.4 Allowing Rollbacks for Optimistic Locking The ideas we just explained already support simple deadlock-free objects such as dfInc in Fig. 1(b), but they cannot be applied to objects with optimistic synchronization, such as optimistic lists [13] and lazy lists [11]. Figure 2(a) shows part of the optimistic list implementation. Each node of the list is associated with a TAS lock, the same lock as in Fig. 1(b). A thread first traverses the list without acquiring any locks (line 3). The traversal find returns two adjacent node pointers p and c. The thread then locks the two nodes (line 4), and calls validate to check if the two nodes are still valid list nodes (line 5). If validation succeeds, then the thread performs its updates (adding or removing elements) to the list (line 9). Otherwise it releases the two node locks (line 7) and restarts the traversal. For this object, when the validation fails, a thread will release the locks it has acquired and roll back. Thus the thread may acquire the locks for an unbounded number of times. Since each lock acquirement will delay other threads requesting the same lock and each delaying action should consume one -token, it seems that the thread would need an infinite number of -tokens, which we prohibit in the preceding subsection to ensure deadlock-freedom, even though this list object is indeed deadlock-free. We generalize the token-transfer ideas to allow rollbacks in order to verify this kind of optimistic algorithms, but still have to be careful to avoid the circular delay caused by the “bad” rollbacks in Fig. 2(b), as we explain in Sec. 2.2.2. Our solution is to stratify the delaying actions. Each action is now labeled with a level k. The normal actions which cannot delay other threads are at the lowest level 0. The -tokens are stratified accordingly. A thread can roll back and do more actions at level k only when its environment does an action at a higher level k 0 , at the cost of a k 0 -level -token. Note that the -tokens at the highest level are strictly decreasing, which means a thread cannot roll back its actions of the highest level. In fact, the numbers of -tokens at all (MName) f ∈ String (ThrdID) t ∈ Nat (Expr) E ::= x | n | E + E | . . . (BExp) B ::= true | false | E = E | !B | . . . (Instr) c ::= x := E | x := [E] | [E] := E | print(E) | . . . (Stmt) C ::= skip | c | x := f(E) | return E | hCi | C; C | if (B) C else C | while (B){C} (Prog) W ::= skip | let Π in C k. . .kC (ODecl) Π, Γ ::= {f1 ❀ (x1, C1), . . . , fn ❀ (xn, Cn)} (Store) s, s ∈ Var * Int (Heap) h, h ∈ Nat * Int (Mem) σ, Σ ::= (s, h) (PState) S ::= (σc, σo, . . .) Figure 3. The language syntax and state model. levels constitute a tuple (mk, . . . , m2, m1). It is strictly descending along the dictionary order. The stratified -tokens naturally prohibit the circular delay problem discussed in Sec. 2.2.2 with the object in Fig. 2(b) . The deadlock-free optimistic list in Fig. 2(a) can now be verified. We classify its delaying actions into two levels. Actions at level 2 (the highest level) update the list, which correspond to line 9 in Fig. 2(a), and each method can do only one such action. Lock acquirements are classified at level 1, so a thread is allowed to roll back and re-acquire the locks when its environment updates the list. 3. Programming Language Figure 3 gives the syntax of the language. A program W consists of multiple parallel threads sharing an object Π. We say the threads are the clients of the object. An object declaration Π is a mapping from a method name f to a pair of argument and code (method body). The statements C are similar to those in the simple language used for separation logic. The command print(E) generates externally observable events, which allows us to observe behaviors of programs. We assume it is used only in the code of clients. We use hCi to represent an atomic block in which C is executed atomically. To simplify the presentation, we make several simplifications here. We assume there is only one concurrent object in the system. Each method of the object takes only one argument, and the method body ends with a return E command. Also we assume there is no nested method invocation. For the abstract object specification Γ, each method body is an atomic operation hCi (ahead of the return command), and executing the code is always safe and never blocks. The model of program states S is defined at the bottom of Fig. 3. To ensure that the client code does not touch the object state, in S we separate the states accessed by clients (σc) and by the object (σo). Here S may also contain auxiliary data about the control stacks for method calls. Execution of programs is modeled as a labeled transition system (W, S) e 7−→ (W0 , S 0 ). Here e is an event (either observable or not) produced by the transition. We give the small-step transition semantics in TR [22]. Below we often write Σ, s and h for the notations at the abstract level to distinguish from the concrete-level ones (σ, s and h). 4. Program Logic LiLi LiLi verifies the linearizability of objects by proving the method implementations refine abstract atomic operations. The top level judgment is in the form of D, R, G ` {P}ΠΓ. (The OBJ rule for this judgment is given in Fig. 7 and will be explained later.) To verify an object Π, we give a corresponding object specification Γ (see Fig. 3), which maps method names to atomic commands. In addition, we need to provide an object invariant (P) and rely/guarantee conditions (R and G) for the refinement reasoning in a concurrent 389