Progress of Concurrent Objects with Partial Methods

Watch a 21-minute conference talk from POPL 2018 exploring new progress properties for concurrent objects with partial methods. Delve into the research by Hongjin Liang and Xinyu Feng from Nanjing University and University of Science and Technology of China as they introduce partial starvation-freedom (PSF) and partial deadlock-freedom (PDF). Learn how these properties specifically address concurrent objects with methods that are not meant to return under certain conditions, like lock_acquire methods. Discover four patterns for writing abstract specifications for PSF/PDF objects under different scheduling conditions, understand the Abstraction Theorem showing equivalence between PSF/PDF and progress-aware contextual refinement, and explore the generalization of the LiLi program logic for verifying these properties and linearizability of concurrent objects.