1 CCAS(o,n){ 11 Complete(d){ 2 local r,d; 12 local b; Then we can define I,R and G,and verify the code by applying 3 d :cons(cid,o,n); 13 b:=flagi the inference rules.The invariant I says,the shared state includes 4 r :cas(&a,o,d)i 141f(b) flag and a at the abstract and the concrete levels;and when a is a 5 while(IsDesc(r)){ 15 cas(&a,d,d.n); 16 descriptor d,the descriptor and the abstract operation of the thread 6 Complete(r); else 2 d.id are also shared. r :cas(&a,o,d); 17 cas(&a,d,d.o); 8】 18] The rely R and the guarantee G should include the action 9 if(r =o)Complete(d); 19 SetFlag(b){flag :b;} over the shared states at each line.The action at line 4 (or 7)is 10 return r; interesting.If it succeeds,both the descriptor d and the abstract operation will be transferred from the local state to the shared part. Figure 14.CCAS Code This puts the abstract operation in the pending thread pool and enables other threads to help execute it. The action at line 13 guarantees TrylinSucc V TrylinFail,which in the concrete linked list to the abstract queue.R and G specify demonstrates the use of our logic for both helping and speculation. the related transitions at both levels,which simply include all the actions over the shared states in the algorithm.The proof is similar TrylinSucc (t,o,n.(flagtrue*notDone(t,o,n)) x(f1ag户true*endSucc(t,o,n)⊕ld to the partial correctness proof using LRG,except that we have to where notDone(t,o,n)gt一(CCAS,o,m)*a÷o specify the abstract objects and operations in assertions and reason about the instrumented code.We show the full proof in TR [18]. endSucc(t,o,m)些t一(end,o)*a→n TrylinFail is symmetric for the case when flagfalse.Here 6.3 Conditional CAS we use R ld (defined in Fig.8)to describe the action of trylin Conditional compare-and-swap (CCAS)[31]is a simplified version It means,after the action we will keep the original state as well of the RDCSS algorithm [12].It involves both the helping mecha- as the new state resulting from R as possible speculations.Also, nism and future-dependent LPs.We show its code in Fig.14. in TrylinSucc and TrylinFail.the current thread is allowed to help The object contains an integer variable a,and a boolean bit execute the abstract CCAS of some thread t. flag.The method SetFlag (line 19)sets the bit directly.The The subtle part in the proof is to ensure that,no thread could method CCAS takes two arguments:an expected current value o of cheat by imagining another thread's help.In any program point the variable a and a new value n.It atomically updates a with the of CCAS,the environment may have done trylin and helped the new value if flag is true and a indeed has the value o;and does operation.But whether the environment has helped it or not,the nothing otherwise.CCAS always returns the old value of a. commit at line 15 or 17 cannot fail.This means,we should not The implementation in Fig.14 uses a variant of cas:instead confuse the two kinds of nondeterminism caused by speculation of a boolean value indicating whether it succeeds,cas(a,o,n) and by environment interference.The former allows us to discard returns the old value stored in a.When starting a CCAS,a thread wrong guesses,while for the latter,we should consider all possible first allocates its descriptor (line 3),which contains the thread id environments (including none). and the arguments for CCAS.It then tries to put its descriptor in a (line 4).If successful (line 9),it calls the auxiliary Complete 7.Related Work and Conclusion function,which restores a to the new value n (line 15)or to the In addition to the work mentioned in Sec.I and 2,there is a large original value o(line 17),depending on whether flag is true.If body of work on linearizability verification.Here we only discuss it finds a contains a descriptor (i.e.,IsDesc holds),it will try to the most closely related work that can handle non-fixed LPs. help complete the operation in the descriptor (line 6)before doing Our logic is similar to Vafeiadis'extension of RGSep to prove its own.Since we disallow nested function calls to simplify the linearizability [32].He also uses abstract objects and abstract language,the auxiliary Complete function should be viewed as a atomic operations as auxiliary variables and code.There are two macro. key differences between the logics.First he uses prophecy variables The LPs of the algorithm are at lines 4,7 and 13.If a contains a to handle future-dependent LPs,but there has been no satisfactory different value from o at lines 4 and 7,then CCAS fails and they are semantics given for prophecy variables so far.We use the simple LPs of the current thread.We can instrument these lines as follows: try-commit mechanism,whose semantics is straightforward.Sec- <r :=cas(&a,o,d);if(r!=o&!IsDesc(r))linself;> ond the soundness of his logic w.rt.linearizability is not specified and proved.We address this problem by defining a new thread- If the descriptor d gets placed in a,then the LP should be in the local simulation as the meta-theory of our logic.As we explained Complete function.Since any thread can call Complete to help in Sec.2,defining such a simulation to support non-fixed LPs is one the operation,the LP should be at line 13 of the thread which will of the most challenging issues we have to solve.Although recently succeed at line 15 or 17.It is a future-dependent LP which may be Vafeiadis develops an automatic verification tool [33]with formal in other threads'code.We instrument line 13 using trylin(d.id) soundness for linearizability,his new work can handle non-fixed to speculatively execute the abstract operation for the thread in d. LPs for read-only methods only,and cannot verify algorithms like which may not be the current thread.That is,line 13 becomes: HSY stack,CCAS and RDCSS in our paper. b :flag;if (a d)trylin(d.id);> Recently,Turon et al.[31]propose logical relations to ver- ify fine-grained concurrency,which establish contextual refinement The condition a=d requires that the abstract operation in the de- between the library and the specification.Underlying the model a scriptor has not been finished.Then at lines 15 and 17,we commit similar simulation is defined.Our pending thread pool is proposed the correct guess.We show the instrumentation at line 15 below concurrently with their"spec thread pool".while the speculation (where s is a local variable),and line 17 is instrumented similarly. idea in our simulation is borrowed from their work,which traces back to forward-backward simulation [21].What is new here is <s :cas(&a,d,d.n); if(s d)commit(d.id(end,d.o)*ad.n); a new program logic and the way we instrument code to do re lational reasoning.The set of syntactic rules,including the try- That is,it should be possible that the thread in d has finished the commit mechanism to handle uncertainty,is much easier to use operation,and the current abstract a is the new value n. than the semantic logical relations to construct proofs.On the other 4691 CCAS(o, n) { 2 local r, d; 3 d := cons(cid, o, n); 4 r := cas(&a, o, d); 5 while(IsDesc(r)) { 6 Complete(r); 7 r := cas(&a, o, d); 8 } 9 if(r = o) Complete(d); 10 return r; } 11 Complete(d) { 12 local b; 13 b := flag; 14 if (b) 15 cas(&a, d, d.n); 16 else 17 cas(&a, d, d.o); 18 } 19 SetFlag(b){ flag := b;} Figure 14. CCAS Code in the concrete linked list to the abstract queue. R and G specify the related transitions at both levels, which simply include all the actions over the shared states in the algorithm. The proof is similar to the partial correctness proof using LRG, except that we have to specify the abstract objects and operations in assertions and reason about the instrumented code. We show the full proof in TR [18]. 6.3 Conditional CAS Conditional compare-and-swap (CCAS) [31] is a simplified version of the RDCSS algorithm [12]. It involves both the helping mecha￾nism and future-dependent LPs. We show its code in Fig. 14. The object contains an integer variable a, and a boolean bit flag. The method SetFlag (line 19) sets the bit directly. The method CCAS takes two arguments: an expected current value o of the variable a and a new value n. It atomically updates a with the new value if flag is true and a indeed has the value o; and does nothing otherwise. CCAS always returns the old value of a. The implementation in Fig. 14 uses a variant of cas: instead of a boolean value indicating whether it succeeds, cas(&a,o,n) returns the old value stored in a. When starting a CCAS, a thread first allocates its descriptor (line 3), which contains the thread id and the arguments for CCAS. It then tries to put its descriptor in a (line 4). If successful (line 9), it calls the auxiliary Complete function, which restores a to the new value n (line 15) or to the original value o (line 17), depending on whether flag is true. If it finds a contains a descriptor (i.e., IsDesc holds), it will try to help complete the operation in the descriptor (line 6) before doing its own. Since we disallow nested function calls to simplify the language, the auxiliary Complete function should be viewed as a macro. The LPs of the algorithm are at lines 4, 7 and 13. If a contains a different value from o at lines 4 and 7, then CCAS fails and they are LPs of the current thread. We can instrument these lines as follows: <r := cas(&a, o, d); if(r!=o && !IsDesc(r)) linself;> If the descriptor d gets placed in a, then the LP should be in the Complete function. Since any thread can call Complete to help the operation, the LP should be at line 13 of the thread which will succeed at line 15 or 17. It is a future-dependent LP which may be in other threads’ code. We instrument line 13 using trylin(d.id) to speculatively execute the abstract operation for the thread in d, which may not be the current thread. That is, line 13 becomes: < b := flag; if (a = d) trylin(d.id); > The condition a=d requires that the abstract operation in the de￾scriptor has not been finished. Then at lines 15 and 17, we commit the correct guess. We show the instrumentation at line 15 below (where s is a local variable), and line 17 is instrumented similarly. < s := cas(&a, d, d.n); if(s = d) commit(d.id (end, d.o) ∗ a⇒d.n); > That is, it should be possible that the thread in d has finished the operation, and the current abstract a is the new value n. Then we can define I, R and G, and verify the code by applying the inference rules. The invariant I says, the shared state includes flag and a at the abstract and the concrete levels; and when a is a descriptor d, the descriptor and the abstract operation of the thread d.id are also shared. The rely R and the guarantee G should include the action over the shared states at each line. The action at line 4 (or 7) is interesting. If it succeeds, both the descriptor d and the abstract operation will be transferred from the local state to the shared part. This puts the abstract operation in the pending thread pool and enables other threads to help execute it. The action at line 13 guarantees TrylinSucc∨ TrylinFail, which demonstrates the use of our logic for both helping and speculation. TrylinSucc def = (∃t, o, n. (flag ⇒ true ∗ notDone(t, o, n)) (flag ⇒ true ∗ endSucc(t, o, n))) ⊕ Id where notDone(t, o, n) def = t (CCAS, o, n) ∗ a ⇒ o endSucc(t, o, n) def = t (end, o) ∗ a ⇒ n TrylinFail is symmetric for the case when flag ⇒ false. Here we use R ⊕ Id (defined in Fig. 8) to describe the action of trylin. It means, after the action we will keep the original state as well as the new state resulting from R as possible speculations. Also, in TrylinSucc and TrylinFail, the current thread is allowed to help execute the abstract CCAS of some thread t. The subtle part in the proof is to ensure that, no thread could cheat by imagining another thread’s help. In any program point of CCAS, the environment may have done trylin and helped the operation. But whether the environment has helped it or not, the commit at line 15 or 17 cannot fail. This means, we should not confuse the two kinds of nondeterminism caused by speculation and by environment interference. The former allows us to discard wrong guesses, while for the latter, we should consider all possible environments (including none). 7. Related Work and Conclusion In addition to the work mentioned in Sec. 1 and 2, there is a large body of work on linearizability verification. Here we only discuss the most closely related work that can handle non-fixed LPs. Our logic is similar to Vafeiadis’ extension of RGSep to prove linearizability [32]. He also uses abstract objects and abstract atomic operations as auxiliary variables and code. There are two key differences between the logics. First he uses prophecy variables to handle future-dependent LPs, but there has been no satisfactory semantics given for prophecy variables so far. We use the simple try-commit mechanism, whose semantics is straightforward. Sec￾ond the soundness of his logic w.r.t. linearizability is not specified and proved. We address this problem by defining a new thread￾local simulation as the meta-theory of our logic. As we explained in Sec. 2, defining such a simulation to support non-fixed LPs is one of the most challenging issues we have to solve. Although recently Vafeiadis develops an automatic verification tool [33] with formal soundness for linearizability, his new work can handle non-fixed LPs for read-only methods only, and cannot verify algorithms like HSY stack, CCAS and RDCSS in our paper. Recently, Turon et al. [31] propose logical relations to ver￾ify fine-grained concurrency, which establish contextual refinement between the library and the specification. Underlying the model a similar simulation is defined. Our pending thread pool is proposed concurrently with their “spec thread pool”, while the speculation idea in our simulation is borrowed from their work, which traces back to forward-backward simulation [21]. What is new here is a new program logic and the way we instrument code to do re￾lational reasoning. The set of syntactic rules, including the try￾commit mechanism to handle uncertainty, is much easier to use than the semantic logical relations to construct proofs. On the other 469