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.
Thu 21 Jan
|10:30 - 10:55|
|10:55 - 11:20|
Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6Media Attached
|11:20 - 11:45|
Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of ChinaMedia Attached
|11:45 - 12:10|
|Link to publication DOI Pre-print Media Attached File Attached|