Existing work on verifying concurrent objects is mostly concerned with safety only, e.g., partial correctness or linearizability. Although there has been recent work verifying lock-freedom of non-blocking objects, much less efforts are focused on deadlock-freedom and starvation-freedom, progress properties of blocking objects. These properties are more challenging to verify than lock-freedom because they allow the progress of one thread to depend on the progress of another, assuming fair scheduling.
We propose LiLi, a new rely-guarantee style program logic for verifying linearizability and progress together for concurrent objects under fair scheduling. The rely-guarantee style logic unifies thread-modular reasoning about both starvation-freedom and deadlock-freedom in one framework. It also establishes progress-aware abstraction for concurrent objects, which can be applied when verifying safety and liveness of client code. We have successfully applied the logic to verify starvation-freedom or deadlock-freedom of representative algorithms such as ticket locks, queue locks, lock-coupling lists, optimistic lists and lazy lists.
Conference DayThu 21 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
10:30 - 12:10
|Certified Causally Consistent Distributed Key-Value Stores|
Research PapersMedia Attached
|'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems|
Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6Media Attached
|A Program Logic for Concurrent Objects under Fair Scheduling|
Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of ChinaMedia Attached
|PSync: a partially synchronous language for fault-tolerant distributed algorithms|
Research PapersLink to publication DOI Pre-print Media Attached File Attached