304 Background The key rule in rely-guarantee reasoning is the following (PAR)rule: R1,G1上{P}C{Q1} G1→R2 R2,G2F{P2}C2{Q2} G2→R1 (PAR) RI A R2,G1VG2H{PIA P2}C1lC21Q1AQ2} Here CiC2 is the parallel composition of the two threads Ci and C2 The rule says that,we can verify CillC2 by separately verifying each thread Ci,showing its behaviors under the rely condition Ri indeed satisfy its guarantee Gi.To ensure that parallel threads can collaborate, the guarantee of each thread needs to satisfy the rely of the other (i.e.,Gi=R2 and G2=R).After parallel composition,the threads should be executed under their common environment (i.e.,RIA R2) and guarantee all the possible transitions made by them (i.e.,GI VG2). 2.4.2 Relational Reasoning and Linearizability Verification Consider the counter object inc implemented with a test-and-set (TAS) lock in Figure 2.1(b).Verifying linearizability of inc requires us to prove that it has the same abstract behaviors as INC in Figure 2.1(e),which increments the counter x atomically. Following previous work(Liang and Feng,2013;Liang et al.,2014; Vafeiadis,2008),one can extend the rely-guarantee logic to verify contextual refinement between concurrent programs.Since linearizability is equivalent to contextual refinement where the abstract specifications are atomic operations,and,as explained in Subsection 2.3,we wish to establish similar results for the different progress properties,a program logic supporting contextual refinement verification can be applied to verify linearizability and progress properties. Using the counter object inc as an example,the judgment to verify it is in the form of R,GHP A arem(INC)}inc{Q A arem(skip)}. It looks similar to the traditional rely-guarantee logic,but we want to do relational reasoning here to show inc refines INC.The pre-and post-conditions are now relational assertions specifying the consistency relation between the program states at the concrete and the abstract
304 Background The key rule in rely-guarantee reasoning is the following (par) rule: R1, G1 ` {P1}C1{Q1} G1 ⇒ R2 R2, G2 ` {P2}C2{Q2} G2 ⇒ R1 R1 ∧ R2, G1 ∨ G2 ` {P1 ∧ P2}C1 kC2{Q1 ∧ Q2} (par) Here C1 kC2 is the parallel composition of the two threads C1 and C2. The rule says that, we can verify C1 kC2 by separately verifying each thread Ci , showing its behaviors under the rely condition Ri indeed satisfy its guarantee Gi . To ensure that parallel threads can collaborate, the guarantee of each thread needs to satisfy the rely of the other (i.e., G1 ⇒ R2 and G2 ⇒ R1). After parallel composition, the threads should be executed under their common environment (i.e., R1 ∧ R2) and guarantee all the possible transitions made by them (i.e., G1 ∨ G2). 2.4.2 Relational Reasoning and Linearizability Verification Consider the counter object inc implemented with a test-and-set (TAS) lock in Figure 2.1(b). Verifying linearizability of inc requires us to prove that it has the same abstract behaviors as INC in Figure 2.1(e), which increments the counter x atomically. Following previous work (Liang and Feng, 2013; Liang et al., 2014; Vafeiadis, 2008), one can extend the rely-guarantee logic to verify contextual refinement between concurrent programs. Since linearizability is equivalent to contextual refinement where the abstract specifications are atomic operations, and, as explained in Subsection 2.3, we wish to establish similar results for the different progress properties, a program logic supporting contextual refinement verification can be applied to verify linearizability and progress properties. Using the counter object inc as an example, the judgment to verify it is in the form of R, G ` {P ∧ arem(INC)}inc{Q ∧ arem(skip)}. It looks similar to the traditional rely-guarantee logic, but we want to do relational reasoning here to show inc refines INC. The pre- and post-conditions are now relational assertions specifying the consistency relation between the program states at the concrete and the abstract
2.4.Verifying Progress Properties 305 sides.We also use an assertion arem(C)to specify as an auxiliary state (also known as a ghost state)the abstract operation C to be refined by the concrete program.So the precondition says inc needs to refine INC, and the assertion arem(skip)in the postcondition says there is no more abstract operations to be refined at the end of inc (so the execution of inc indeed fulfills the action INC). Similarly,the rely and guarantee conditions R and G are also lifted to the relational setting.They now specify state transitions at both the concrete and the abstract sides.That is,transitions are made over state pairs consisting of the concrete and abstract states,so R and G are relational assertions over pairs of state pairs. Readers can refer to previous work (Liang and Feng,2013;Liang et al.,2014;Vafeiadis,2008)for more details about relational rely- guarantee logic.In LiLi we extend the relational reasoning to verify contextual refinements equivalent to different progress properties.The focus of this tutorial to address the challenges for progress reasoning, which we first give an overview in the next subsection. 2.4.3 Challenges of Progress Verification Progress properties of objects such as deadlock-freedom and starvation- freedom have various termination requirements of object methods.They must be satisfied with interference from other threads considered,which makes the verification challenging. Non-Termination Caused by Interference In a concurrent setting,an object method may fail to terminate due to interference from its environment.Below we point out there are two different kinds of interference that may cause thread non-termination, namely blocking and delay.Let's first see a classic deadlocking example. DL-12: DL-21: lock L1;lock L2; lock L2;lock L1; unlock L2;unlock L1; unlock L1;unlock L2; The methods DL-12 and DL-21 may fail to terminate because of the cir- cular dependency of locks.This non-termination is caused by permanent
2.4. Verifying Progress Properties 305 sides. We also use an assertion arem(C) to specify as an auxiliary state (also known as a ghost state) the abstract operation C to be refined by the concrete program. So the precondition says inc needs to refine INC, and the assertion arem(skip) in the postcondition says there is no more abstract operations to be refined at the end of inc (so the execution of inc indeed fulfills the action INC). Similarly, the rely and guarantee conditions R and G are also lifted to the relational setting. They now specify state transitions at both the concrete and the abstract sides. That is, transitions are made over state pairs consisting of the concrete and abstract states, so R and G are relational assertions over pairs of state pairs. Readers can refer to previous work (Liang and Feng, 2013; Liang et al., 2014; Vafeiadis, 2008) for more details about relational relyguarantee logic. In LiLi we extend the relational reasoning to verify contextual refinements equivalent to different progress properties. The focus of this tutorial to address the challenges for progress reasoning, which we first give an overview in the next subsection. 2.4.3 Challenges of Progress Verification Progress properties of objects such as deadlock-freedom and starvationfreedom have various termination requirements of object methods. They must be satisfied with interference from other threads considered, which makes the verification challenging. Non-Termination Caused by Interference In a concurrent setting, an object method may fail to terminate due to interference from its environment. Below we point out there are two different kinds of interference that may cause thread non-termination, namely blocking and delay. Let’s first see a classic deadlocking example. DL-12 : DL-21 : lock L1; lock L2; lock L2; lock L1; unlock L2; unlock L1; unlock L1; unlock L2; The methods DL-12 and DL-21 may fail to terminate because of the circular dependency of locks. This non-termination is caused by permanent
306 Background blocking.That is,when DL-12 tries to acquire L2,it could be blocked if the lock has been acquired by DL-21. The second example is the following client using the lock-free counter in Figure 1.1(a). inc();while (true)inc(); The call of the inc method by the left thread may never terminate. This is because,just before the left thread updates x at line 5,it could be preempted by the right thread,who updates x ahead of the left Then the left thread would fail at the cas command and have to loop at least one more round before termination.This may happen infinitely many times,causing non-termination of the inc method on the left. In this case we say the progress of the left method is delayed by its environment's successful cas. The key difference between blocking and delay is that blocking is caused by the absence of certain environment actions,e.g.,releasing a lock,while delay is caused by the occurrence of certain environment actions,e.g.,a successful cas.In other words,a blocked thread can progress only if its environment progresses first,while a delayed thread can progress if we suspend the execution of its environment. Lock-free algorithms disallow blocking(thus they do not rely on fair scheduling),although delay is common,especially in optimistic algorithms.Starvation-free algorithms allow (limited)blocking,but not delay.As the above example of inc shows,delay from non-terminating clients may cause starvation.Deadlock-free algorithms allow both (but with restrictions).For instance,consider the TAS lock based counter in Figure 2.1(b)and the following client. inc();‖inc(O; Suppose the lock is available,and the left thread tries to acquire the lock and is just before the cas command in the code of L_acq in inc. Then it might be delayed by the right thread who preempts and gets the lock first.After the right thread acquires the lock,the left thread becomes blocked and waits for the lock release by the right thread. In some algorithms(such as the optimistic list),blocking and delay can be intertwined by the combined use of blocking-based synchronization
306 Background blocking. That is, when DL-12 tries to acquire L2, it could be blocked if the lock has been acquired by DL-21. The second example is the following client using the lock-free counter in Figure 1.1(a). inc(); while (true) inc(); The call of the inc method by the left thread may never terminate. This is because, just before the left thread updates x at line 5, it could be preempted by the right thread, who updates x ahead of the left. Then the left thread would fail at the cas command and have to loop at least one more round before termination. This may happen infinitely many times, causing non-termination of the inc method on the left. In this case we say the progress of the left method is delayed by its environment’s successful cas. The key difference between blocking and delay is that blocking is caused by the absence of certain environment actions, e.g., releasing a lock, while delay is caused by the occurrence of certain environment actions, e.g., a successful cas. In other words, a blocked thread can progress only if its environment progresses first, while a delayed thread can progress if we suspend the execution of its environment. Lock-free algorithms disallow blocking (thus they do not rely on fair scheduling), although delay is common, especially in optimistic algorithms. Starvation-free algorithms allow (limited) blocking, but not delay. As the above example of inc shows, delay from non-terminating clients may cause starvation. Deadlock-free algorithms allow both (but with restrictions). For instance, consider the TAS lock based counter in Figure 2.1(b) and the following client. inc(); inc(); Suppose the lock is available, and the left thread tries to acquire the lock and is just before the cas command in the code of L_acq in inc. Then it might be delayed by the right thread who preempts and gets the lock first. After the right thread acquires the lock, the left thread becomes blocked and waits for the lock release by the right thread. In some algorithms (such as the optimistic list), blocking and delay can be intertwined by the combined use of blocking-based synchronization
2.4.Verifying Progress Properties 307 1 local b :=false,p,c; 2 while (!b){ 3 (p,c):=find(e); 4 lock p;lock c; 6 b validate(p,c); 6 if (!b){ 7 unlock c;unlock p;} 6 update(p,c,e); 10 unlock c;unlock p; Figure 2.3:The optimistic list. and optimistic concurrency,which makes the reasoning significantly more challenging than reasoning about lock-free algorithms. Figure 2.3 shows part of the optimistic list implementation.Each node of the list is associated with a TAS lock.A thread first traverses the list without acquiring any locks (line 3).The traversal find returns two adjacent node pointers p and c,the position where the update (adding or removing elements)to the list will take place.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 the update (line 9).Otherwise it releases the two node locks (line 7)and restarts the traversal.We can see that blocking and delay are intertwined in this algorithm-a thread may be blocked when acquiring a lock,and be delayed if the validation fails and the thread has to release the acquired locks and restart the traversal. How do we come up with general principles to allow blocking and/or delay,but on the other hand to guarantee lock-freedom,starvation- freedom or deadlock-freedom? Avoid Circular Reasoning Rely-guarantee style logics provide the power of thread-modular verifi- cation by circular reasoning.When proving the behaviors of a thread t guarantee G,we assume that the behaviors of the environment thread t'satisfy R.Conversely,the proof of thread t'relies on the assumptions on the behaviors of thread t
2.4. Verifying Progress Properties 307 1 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; Figure 2.3: The optimistic list. and optimistic concurrency, which makes the reasoning significantly more challenging than reasoning about lock-free algorithms. Figure 2.3 shows part of the optimistic list implementation. Each node of the list is associated with a TAS lock. A thread first traverses the list without acquiring any locks (line 3). The traversal find returns two adjacent node pointers p and c, the position where the update (adding or removing elements) to the list will take place. 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 the update (line 9). Otherwise it releases the two node locks (line 7) and restarts the traversal. We can see that blocking and delay are intertwined in this algorithm—a thread may be blocked when acquiring a lock, and be delayed if the validation fails and the thread has to release the acquired locks and restart the traversal. How do we come up with general principles to allow blocking and/or delay, but on the other hand to guarantee lock-freedom, starvationfreedom or deadlock-freedom? Avoid Circular Reasoning Rely-guarantee style logics provide the power of thread-modular verifi- cation by circular reasoning. When proving the behaviors of a thread t guarantee G, we assume that the behaviors of the environment thread t 0 satisfy R. Conversely, the proof of thread t 0 relies on the assumptions on the behaviors of thread t
308 Background 1 lock L1; 11 lock L2; 2 local r :L2; 12 local s :L1; 3 whi1e(r！=0){ 13 while (s !=0){ 4 unlock L1; 14 unlock L2; 6 lock L1; 15 lock L2; r:=L2; 16 8:=L1; 7 17 2 8 lock L2; 18 lock L1; 9 unlock L2; 19 unlock L1; 10 unlock L1; 20 unlock L2; Figure 2.4:Rollback with two locks. However,circular reasoning is usually unsound in liveness verifi- cation (Abadi and Lamport,1995).For instance,we could prove ter- mination of each thread in the deadlocking example above,under the assumption that each environment thread eventually releases the lock it owns.How do we avoid the circular reasoning without sacrificing rely-guarantee style thread-modular reasoning? The deadlocking example shows that we should avoid circular rea- soning to rule out circular dependency caused by blocking.Delay may also cause circular dependency too.The left side of Figure 2.4 shows a thread t using two locks.It first acquires L1 (line 1)and then tests whether L2 is available (line 2).If the test fails,the thread rolls back.It releases L1 (line 4),and then repeats the process of acquiring L1 (line 5) and testing L2(line 6).Suppose another thread t'does the opposite (see the right side of Figure 2.4):repeatedly acquiring L2 and testing L1.In this example the acquirement of L2 by t'may cause t to fail its test of the availability of L2.The test could have succeeded if t'did not interfere,so t'delays t.Conversely,the acquirement of L1 by t may delay t'.Then the two threads can cause each other to continually roll back,and neither method progresses. Usually when delay is allowed,we need to make sure that the action delaying other threads is a"good"one in that it makes the executing thread progress (e.g.,a step towards termination).This is the case with the "benign delays"in the examples of the lock-free counter,the TAS
308 Background 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; 11 lock L2; 12 local s := L1; 13 while (s != 0) { 14 unlock L2; 15 lock L2; 16 s := L1; 17 } 18 lock L1; 19 unlock L1; 20 unlock L2; Figure 2.4: Rollback with two locks. However, circular reasoning is usually unsound in liveness verifi- cation (Abadi and Lamport, 1995). For instance, we could prove termination of each thread in the deadlocking example above, under the assumption that each environment thread eventually releases the lock it owns. How do we avoid the circular reasoning without sacrificing rely-guarantee style thread-modular reasoning? The deadlocking example shows that we should avoid circular reasoning to rule out circular dependency caused by blocking. Delay may also cause circular dependency too. The left side of Figure 2.4 shows a thread t using two locks. It first acquires L1 (line 1) and then tests whether L2 is available (line 2). If the test fails, the thread rolls back. It releases L1 (line 4), and then repeats the process of acquiring L1 (line 5) and testing L2 (line 6). Suppose another thread t 0 does the opposite (see the right side of Figure 2.4): repeatedly acquiring L2 and testing L1. In this example the acquirement of L2 by t 0 may cause t to fail its test of the availability of L2. The test could have succeeded if t 0 did not interfere, so t 0 delays t. Conversely, the acquirement of L1 by t may delay t 0 . Then the two threads can cause each other to continually roll back, and neither method progresses. Usually when delay is allowed, we need to make sure that the action delaying other threads is a “good” one in that it makes the executing thread progress (e.g., a step towards termination). This is the case with the “benign delays” in the examples of the lock-free counter, the TAS