286 Introduction If we use the lock-based inc in Figure 1.1(b),whether the call of inc()in the left thread terminates or not depends on the implemen- tation of the lock.If the lock implementation is fair,the inc()on the left always terminates,otherwise it may always fail to acquire the lock and may never terminate.In both cases,if we suspend the right thread when it is executing line 10,the inc()on the left cannot terminate because it can never acquire the lock (which has been taken by the suspended right thread).So we say the lock-based implementation of inc is blocking.The termination of a method call relies on both the lock algorithm and the fairness of scheduling. The goal of this tutorial is to help the reader understand the various progress properties of concurrent objects.We formulate each progress property (together with linearizability as a basic correctness requirement)in terms of contextual refinement.This essentially gives us progress-aware abstraction for concurrent objects.We also introduce a program logic LiLi to formally verify progress properties. 1.1 General Motivation 1.1.1 Progress-Aware Abstraction Progress properties describe conditions under which method calls are guaranteed to successfully complete in an execution.For example,lock- freedom guarantees that "infinitely often some method call finishes in a finite number of steps"(Herlihy and Shavit,2008).They are difficult to use in a modular and layered program verification because they fail to describe how the progress properties affect clients. In a modular verification of client threads,the concrete implemen- tation II of the object methods should be replaced by an abstraction (or specification)II'that consists of equivalent methods.The progress properties should then characterize whether and how the behaviors of a client program will be affected if a client uses II instead of II'.In particular,we are interested in systematically studying whether the termination of a client using the abstract methods II'will be preserved when using an implementation II with some progress guarantee.286 Introduction If we use the lock-based inc in Figure 1.1(b), whether the call of inc() in the left thread terminates or not depends on the implemen￾tation of the lock. If the lock implementation is fair, the inc() on the left always terminates, otherwise it may always fail to acquire the lock and may never terminate. In both cases, if we suspend the right thread when it is executing line 10, the inc() on the left cannot terminate because it can never acquire the lock (which has been taken by the suspended right thread). So we say the lock-based implementation of inc is blocking. The termination of a method call relies on both the lock algorithm and the fairness of scheduling. The goal of this tutorial is to help the reader understand the various progress properties of concurrent objects. We formulate each progress property (together with linearizability as a basic correctness requirement) in terms of contextual refinement. This essentially gives us progress-aware abstraction for concurrent objects. We also introduce a program logic LiLi to formally verify progress properties. 1.1 General Motivation 1.1.1 Progress-Aware Abstraction Progress properties describe conditions under which method calls are guaranteed to successfully complete in an execution. For example, lock￾freedom guarantees that “infinitely often some method call finishes in a finite number of steps” (Herlihy and Shavit, 2008). They are difficult to use in a modular and layered program verification because they fail to describe how the progress properties affect clients. In a modular verification of client threads, the concrete implemen￾tation Π of the object methods should be replaced by an abstraction (or specification) Π0 that consists of equivalent methods. The progress properties should then characterize whether and how the behaviors of a client program will be affected if a client uses Π instead of Π0 . In particular, we are interested in systematically studying whether the termination of a client using the abstract methods Π0 will be preserved when using an implementation Π with some progress guarantee