readPair(int i,j){local a,b,v,w; 1 eng(v){ 16deg()[ {I*(cid→(y.(i,j))} 2 local x,t,s,bi 17 local h,t,s,v,bi 1 while(true){ 3 x :cons(v,null) 18 while (true){ *(cid(:(i,j))e true)} 4 while (true) 19 h :Head;t :Tail; <a:=m[i].d;v:=m[i].v;> t :Tail;s :t.next; 20 s :h.next; v'.(I A readCell(i,a,v;v))*(cid(,(i,j))true) 6 if (t Tail){ 21 if (h Head) 3 <b :m[j].d;w :m[j].v;trylinself;> > f(s=nu11)[ 22 if (h=t){ {.(I A readCell(i,a,v:)A readCell(j,b,w;))*afterTry} b:=cas(&(t.next),s,x);23 if (s null) if (v m[i].v){ 9 if (b){ 24 return EMPTY; I*(cid(end,(a,b))true) 10 cas(&Tail,t,x); 25 cas(&Tail,t,s); commit(cid(end,(a,b))); 11 return; 26 Felse [I *(cid-(end,(a,b)))} 12 }else cas(&Tail,t,s); 27 v :s.val; 6 return (a,b); 13 28 b:=cas(&Head,h,s); I *(cid-(end,(a,b)))} 14 29 if(b)return v; 7 15] 30]] Auxiliary definitions: readCell(i,d,v:)(cell(i,d,v)v(cell(i,)A))*true Figure 13.MS Lock-Free Queue Code absRes(cid一(end,(a,b)Ar'=)v(cid一(end,(-,b)Au'≠v) after Try cid一(，(i,j)⊕absRes⊕true 6.2 MS Lock-Free Queue Figure 12.Proof Outline of readPair in Pair Snapshot The widely-used MS lock-free queue [23]also has future-dependent LPs.We show its code in Fig.13. The queue is implemented as a linked list with Head and Tail and reason about the instrumented code by applying our inference pointers.Head always points to the first node (a sentinel)in the list, rules,just like the usual partial correctness verification in LRG.In and Tail points to either the last or second to last node.The eng our experience,handling the auxiliary commands usually would method appends a new node at the tail of the list and advances not introduce much difficulty over the plain verification with LRG. Tail,and deq replaces the sentinel node by its next node and Below we sketch the proofs of three representative examples:the returns the value in the new sentinel.If the list contains only the pair snapshot,MS lock-free queue and the CCAS algorithm. sentinel node,meaning the queue is empty,then deq returns EMPTY The algorithm employs the helping mechanism for the enq 6.1 Pair Snapshot method to swing the Tail pointer when it lags behind the end of As discussed in Sec.2.3.the pair snapshot algorithm has a future- the list.A thread should first try to help the half-finished enq by dependent LP.In Fig.12,we show the proof of readPair for the advancing Tail (lines 12 and 25 in Fig.13)before doing its own current thread cid.We will use y for its abstract operation,which operation.But this helping mechanism would not affect the LP of atomically reads the cells i and j at the abstract level. enq which is statically located at line 8 when the cas succeeds. First,we insert trylinself and commit as highlighted in Fig.12 since the new node already becomes visible in the queue after being The commit command says,when the validation at line 4 succeeds, appended to the list,and updating Tail will not affect the abstract we must have cid(end,(a,b))as a possible speculation.This queue.We simply instrument line 8 as follows to verify eng: actually requires a correct instrumentation of trylinself.In Fig.12 b :cas(&(t.next),s,x);if (b)linself; we insert it at line 3.It cannot be moved to other program points since line 3 is the only place where we could get the abstract return On the other hand,the original queue algorithm [23]checks value (a,b)when executing y.Besides,we cannot replace it by Head or Tail (line 6 or 21 in Fig.13)to make sure that its value a linself,because if line 4 fails later,we have to restart to do the has not been changed since its local copy was read (at line 5 original abstract operation. or 19),and if it fails,the operation will restart.This check can After the instrumentation,we can define the precise invariant 7. improve efficiency of the algorithm,but it makes the LP of the deq the rely R and the guarantee G.The invariant I simply maps every method for the empty queue case depend on future executions.That memory cell (d,v)at the concrete level to a cell with data d at the LP should be at line 20,if the method returns EMPTY at the end abstract level.as shown below: of the same iteration.The intuition is,when we read null from I兰④esiz-(目d,v.cel(a,d,v） h.next at line 20 (indicating the abstract queue must be empty there),we do not know how the iteration would terminate at that where cell(i,d,v)兽（回→(d,v)*(片d) time.If the later check over Head at line 21 fails,the operation Every thread guarantees that when writing a cell,it increases the would restart and line 20 may not be the LP.We can use our try- version number.Here we use [G]I short for (GVId)+ldA (II). commit instrumentation to handle this future-dependent LP.We GWrite]r Write,v.cell(i,v)x cell(i,+1) insert trylinself at line 20,as follows: <s The rely R is the same as the guarantee G. :h.next;if (h t&&s null)trylinself;> Then we specify the pre-and post-conditions,and reason about Before the method returns EMPTY,we commit to the finished ab- the instrumented code using our inference rules.The proof follows stract operation,i.e.,we insert commit (cid(end,EMPTY))just the intuition of the algorithm.Note that we relax cid(,(i,j)) before line 24.Also,when we know we have to do another itera- in the precondition of the method to cid(,(i,j))true to tion,we can commit to the original DEQ operation,i.e.,we insert ensure the loop invariant.The latter says,cid may just start (or commit(cidDEQ)at the end of the loop body. restart)its operation and have not done yet. For the case of nonempty queues,the LP of the deq method is The readPair method in the pair snapshot algorithm is "read- statically at line 28 when the cas succeeds.Thus we can instrument only"in the sense that the abstract operation does not update the ab linself there,as shown below. stract object.This perhaps means that it does not matter to linearize b :cas(&Head,h,s);if (b)linself;> the method multiple times.In Sec.6.3 we will verify an algorithm with future-dependent LPs,CCAS,which is not "read-only".We After the instrumentation,we can define /R and G and verify can still "linearize"a method with side effects multiple times the code using our logic rules.The invariant I relates all the nodes 468readPair(int i, j) { local a, b, v, w; {I ∗ (cid (γ, (i, j)))} 1 while(true) { {I ∗ (cid (γ, (i, j)) ⊕ true)} 2 < a := m[i].d; v := m[i].v; > {∃v . (I ∧ readCell(i, a, v; v )) ∗ (cid (γ, (i, j)) ⊕ true)} 3 < b := m[j].d; w := m[j].v; trylinself; > {∃v . (I ∧ readCell(i, a, v; v ) ∧ readCell(j, b, w; )) ∗ afterTry} 4 if (v = m[i].v) { {I ∗ (cid (end, (a, b)) ⊕ true)} 5 commit(cid (end, (a, b))); {I ∗ (cid (end, (a, b)))} 6 return (a, b); {I ∗ (cid (end, (a, b)))} 7 }}} Auxiliary definitions: readCell(i, d, v; v ) def = (cell(i, d, v) ∨ (cell(i, , v ) ∧ v = v )) ∗ true absRes def = (cid(end, (a, b)) ∧ v =v)∨(cid(end, ( , b)) ∧ v =v) afterTry def = cid (γ, (i, j)) ⊕ absRes ⊕ true Figure 12. Proof Outline of readPair in Pair Snapshot and reason about the instrumented code by applying our inference rules, just like the usual partial correctness verification in LRG. In our experience, handling the auxiliary commands usually would not introduce much difficulty over the plain verification with LRG. Below we sketch the proofs of three representative examples: the pair snapshot, MS lock-free queue and the CCAS algorithm. 6.1 Pair Snapshot As discussed in Sec. 2.3, the pair snapshot algorithm has a future￾dependent LP. In Fig. 12, we show the proof of readPair for the current thread cid. We will use γ for its abstract operation, which atomically reads the cells i and j at the abstract level. First, we insert trylinself and commit as highlighted in Fig. 12. The commit command says, when the validation at line 4 succeeds, we must have cid (end,(a, b)) as a possible speculation. This actually requires a correct instrumentation of trylinself. In Fig. 12, we insert it at line 3. It cannot be moved to other program points since line 3 is the only place where we could get the abstract return value (a, b) when executing γ. Besides, we cannot replace it by a linself, because if line 4 fails later, we have to restart to do the original abstract operation. After the instrumentation, we can define the precise invariant I, the rely R and the guarantee G. The invariant I simply maps every memory cell (d, v) at the concrete level to a cell with data d at the abstract level, as shown below: I def = i∈[1..size].(∃d, v. cell(i, d, v)) where cell(i, d, v) def = (m[i] → (d, v)) ∗ (m[i] ⇒ d)) Every thread guarantees that when writing a cell, it increases the version number. Here we use [G]I short for (G ∨Id) ∗ Id∧(I I). G def = [Write]I Write def = ∃i, v. cell(i, , v) cell(i, , v + 1) The rely R is the same as the guarantee G. Then we specify the pre- and post-conditions, and reason about the instrumented code using our inference rules. The proof follows the intuition of the algorithm. Note that we relax cid (γ,(i, j)) in the precondition of the method to cid (γ,(i, j)) ⊕ true to ensure the loop invariant. The latter says, cid may just start (or restart) its operation and have not done yet. The readPair method in the pair snapshot algorithm is “read￾only” in the sense that the abstract operation does not update the ab￾stract object. This perhaps means that it does not matter to linearize the method multiple times. In Sec. 6.3 we will verify an algorithm with future-dependent LPs, CCAS, which is not “read-only”. We can still “linearize” a method with side effects multiple times. 1 enq(v) { 2 local x, t, s, b; 3 x := cons(v, null); 4 while (true) { 5 t := Tail; s := t.next; 6 if (t = Tail) { 7 if (s = null) { 8 b:=cas(&(t.next),s,x); 9 if (b) { 10 cas(&Tail, t, x); 11 return; } 12 }else cas(&Tail, t, s); 13 } 14 } 15 } 16 deq() { 17 local h, t, s, v, b; 18 while (true) { 19 h := Head; t := Tail; 20 s := h.next; 21 if (h = Head) 22 if (h = t) { 23 if (s = null) 24 return EMPTY; 25 cas(&Tail, t, s); 26 }else { 27 v := s.val; 28 b:=cas(&Head,h,s); 29 if(b) return v; } 30 } } Figure 13. MS Lock-Free Queue Code 6.2 MS Lock-Free Queue The widely-used MS lock-free queue [23] also has future-dependent LPs. We show its code in Fig. 13. The queue is implemented as a linked list with Head and Tail pointers. Head always points to the first node (a sentinel) in the list, and Tail points to either the last or second to last node. The enq method appends a new node at the tail of the list and advances Tail, and deq replaces the sentinel node by its next node and returns the value in the new sentinel. If the list contains only the sentinel node, meaning the queue is empty, then deq returns EMPTY. The algorithm employs the helping mechanism for the enq method to swing the Tail pointer when it lags behind the end of the list. A thread should first try to help the half-finished enq by advancing Tail (lines 12 and 25 in Fig. 13) before doing its own operation. But this helping mechanism would not affect the LP of enq which is statically located at line 8 when the cas succeeds, since the new node already becomes visible in the queue after being appended to the list, and updating Tail will not affect the abstract queue. We simply instrument line 8 as follows to verify enq: < b := cas(&(t.next), s, x); if (b) linself; > On the other hand, the original queue algorithm [23] checks Head or Tail (line 6 or 21 in Fig. 13) to make sure that its value has not been changed since its local copy was read (at line 5 or 19), and if it fails, the operation will restart. This check can improve efficiency of the algorithm, but it makes the LP of the deq method for the empty queue case depend on future executions. That LP should be at line 20, if the method returns EMPTY at the end of the same iteration. The intuition is, when we read null from h.next at line 20 (indicating the abstract queue must be empty there), we do not know how the iteration would terminate at that time. If the later check over Head at line 21 fails, the operation would restart and line 20 may not be the LP. We can use our try￾commit instrumentation to handle this future-dependent LP. We insert trylinself at line 20, as follows: < s := h.next; if (h = t && s = null) trylinself; > Before the method returns EMPTY, we commit to the finished ab￾stract operation, i.e., we insert commit(cid (end, EMPTY)) just before line 24. Also, when we know we have to do another itera￾tion, we can commit to the original DEQ operation, i.e., we insert commit(cid DEQ) at the end of the loop body. For the case of nonempty queues, the LP of the deq method is statically at line 28 when the cas succeeds. Thus we can instrument linself there, as shown below. < b := cas(&Head, h, s); if (b) linself; > After the instrumentation, we can define I, R and G and verify the code using our logic rules. The invariant I relates all the nodes 468