6 Progress-Aware Abstraction 331 6.1 Overview of Our Results..················ 331 6.2 Formalizing Progress-Aware Contextual Refinements.... 334 6.3 Abstraction for Wait-Free and Lock-Free Objects 337 6.4 Abstraction for Starvation-Free and Deadlock-Free Objects 341 6.5 Abstraction for PSF and PDF Objects........... 342 7 Verifying Progress of Concurrent Objects 349 7.1 Challenges and Key ldeas.·.··· 349 7.2 The Program Logic LiLi...... 356 7.3 Soundness 385 7.4 Examples...···· 387 8 Related Work 397 8.1 Progress Properties and Abstraction 397 8.2 Verification.......··············· 398 8.3 Comparison with TaDA-Live ....... 401 9 Conclusion and Future Work 406 Acknowledgements 409 References 4106 Progress-Aware Abstraction 331 6.1 Overview of Our Results . . . . . . . . . . . . . . . . . . . 331 6.2 Formalizing Progress-Aware Contextual Refinements . . . . 334 6.3 Abstraction for Wait-Free and Lock-Free Objects . . . . . 337 6.4 Abstraction for Starvation-Free and Deadlock-Free Objects 341 6.5 Abstraction for PSF and PDF Objects . . . . . . . . . . . 342 7 Verifying Progress of Concurrent Objects 349 7.1 Challenges and Key Ideas . . . . . . . . . . . . . . . . . . 349 7.2 The Program Logic LiLi . . . . . . . . . . . . . . . . . . . 356 7.3 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . 385 7.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . 387 8 Related Work 397 8.1 Progress Properties and Abstraction . . . . . . . . . . . . 397 8.2 Verification . . . . . . . . . . . . . . . . . . . . . . . . . . 398 8.3 Comparison with TaDA-Live . . . . . . . . . . . . . . . . 401 9 Conclusion and Future Work 406 Acknowledgements 409 References 410