20:8 Hongjin Liang and Xinyu Feng Table 2.Wrappers for atomic specifications. PSF PDF Strong Fairness wr(await(B)(C]) wrF(await(B)(C]) Weak Fairness WrPSE(await(B)C)） wrpp(await(B)(C)) often enabled and infinitely often disabled in an execution,making its termination sensitive to the fairness of scheduling. Also note that the two fairness notions coincide when the program does not contain blocking operations.Therefore,regardless of strongly or weakly fair scheduling,the client(2.5)using ticket locks always executes print(1),but it may not do so if using test-and-set locks instead (see Table 1). As a result,for the same object implementation,we may need different abstractions under different scheduling.As shown in Table 1,the specification(2.3)cannot serve as the specification of the test-and-set locks under both strong fairness and weak fairness. Second,even under the same scheduling,different implementations demonstrate different progress, therefore need different abstractions.As shown in Table 1,the different lock implementations have different behaviors,even under the same scheduling. For the above two reasons,we need different abstractions for different combinations of fairness and progress.For PSF and PDF under strong and weak fairness respectively,we may need four different abstractions.Can we systematically generate all of them? Our solution.We define code wrappers over the basic blocking primitive await(B)(C)to generate the abstractions.The code wrappers are syntactic transformations that transform await(B)(C)into possibly non-atomic object specifications which can be refined by the object implementations in the progress-aware contextual refinement.As shown in Table 2,the four wrappers correspond to all combinations of fairness and progress.The definitions are shown in Sec.6.Here we only give some high-level intuitions using the lock objects as examples. First,we observe that the lock specification(2.3)can already serve as an abstraction for ticket locks under strong fairness,or for test-and-set locks under weak fairness.In general,the wrapper wr can be an identity function,i.e.,the atomic partial specifications are already proper abstractions for PSF objects (not only for locks)under strong fairness.But wr is subtle.The atomic partial specifications are insufficient as abstractions for general PDF objects under weak fairness,which we will explain in detail in Sec.6. Second,as we have seen from Table 1,the lock specification(2.3)does not work for PSF locks under weak fairness nor for PDF locks under strong fairness.Then the role of the wrapper wr (or wr)is to generate the same PSF(or PDF)behaviors even though the fairness of scheduling is weaker (or stronger). To guarantee PSF,the idea is to create some kind of"fairness"on termination,ie.,every method call can get the chance to terminate.Given weakly fair scheduling,this requires the enabling condition of the abstraction to continuously remain true.As a result,a possible way to define wr(LACQ)is to keep a queue of threads requesting the lock,and a thread can acquire the lock only when it is at the head of the queue. To support PDF under strongly fair scheduling,we have to allow non-termination even if the enabling condition is infinitely often true.For the client(2.5),the call of L_ACQ'in the specifica- tion(2)under strongly fair scheduling always terminates.Then wrneeds to incorporate with some kind of delaying mechanisms,so that the termination of L_ACQ'of the left thread could be delayed every time when the right thread succeeds in acquiring the lock. Proceedings of the ACM on Programming Languages,Vol.2,No.POPL,Article 20.Publication date:January 2018.20:8 Hongjin Liang and Xinyu Feng Table 2. Wrappers for atomic specifications. PSF PDF Strong Fairness wrsfair PSF (await(B){C}) wrsfair PDF (await(B){C}) Weak Fairness wrwfair PSF (await(B){C}) wrwfair PDF (await(B){C}) often enabled and infinitely often disabled in an execution, making its termination sensitive to the fairness of scheduling. Also note that the two fairness notions coincide when the program does not contain blocking operations. Therefore, regardless of strongly or weakly fair scheduling, the client (2.5) using ticket locks always executes print(1), but it may not do so if using test-and-set locks instead (see Table 1). As a result, for the same object implementation, we may need different abstractions under different scheduling. As shown in Table 1, the specification (2.3) cannot serve as the specification of the test-and-set locks under both strong fairness and weak fairness. Second, even under the same scheduling, different implementations demonstrate different progress, therefore need different abstractions. As shown in Table 1, the different lock implementations have different behaviors, even under the same scheduling. For the above two reasons, we need different abstractions for different combinations of fairness and progress. For PSF and PDF under strong and weak fairness respectively, we may need four different abstractions. Can we systematically generate all of them? Our solution. We define code wrappers over the basic blocking primitive await(B){C} to generate the abstractions. The code wrappers are syntactic transformations that transform await(B){C} into possibly non-atomic object specifications which can be refined by the object implementations in the progress-aware contextual refinement. As shown in Table 2, the four wrappers correspond to all combinations of fairness and progress. The definitions are shown in Sec. 6. Here we only give some high-level intuitions using the lock objects as examples. First, we observe that the lock specification (2.3) can already serve as an abstraction for ticket locks under strong fairness, or for test-and-set locks under weak fairness. In general, the wrapper wrsfair PSF can be an identity function, i.e., the atomic partial specifications are already proper abstractions for PSF objects (not only for locks) under strong fairness. But wrwfair PDF is subtle. The atomic partial specifications are insufficient as abstractions for general PDF objects under weak fairness, which we will explain in detail in Sec. 6. Second, as we have seen from Table 1, the lock specification (2.3) does not work for PSF locks under weak fairness nor for PDF locks under strong fairness. Then the role of the wrapper wrwfair PSF (or wrsfair PDF) is to generate the same PSF (or PDF) behaviors even though the fairness of scheduling is weaker (or stronger). To guarantee PSF, the idea is to create some kind of “fairness” on termination, i.e., every method call can get the chance to terminate. Given weakly fair scheduling, this requires the enabling condition of the abstraction to continuously remain true. As a result, a possible way to define wrwfair PSF (L_ACQ’) is to keep a queue of threads requesting the lock, and a thread can acquire the lock only when it is at the head of the queue. To support PDF under strongly fair scheduling, we have to allow non-termination even if the enabling condition is infinitely often true. For the client (2.5), the call of L_ACQ' in the specifica￾tion (2.3) under strongly fair scheduling always terminates. Then wrsfair PDF needs to incorporate with some kind of delaying mechanisms, so that the termination of L_ACQ' of the left thread could be delayed every time when the right thread succeeds in acquiring the lock. Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 20. Publication date: January 2018