Write a Blog >>
Thu 21 Jan 2016 11:20 - 11:45 at Grand Bay North - Track 1: Foundations of distributed systems Chair(s): Mooly Sagiv

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

POPL-2016-papers
10:30 - 12:10: Research Papers - Track 1: Foundations of distributed systems at Grand Bay North
Chair(s): Mooly SagivTel Aviv University
POPL-2016-papers10:30 - 10:55
Talk
Media Attached
POPL-2016-papers10:55 - 11:20
Talk
Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6
Media Attached
POPL-2016-papers11:20 - 11:45
Talk
Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China
Media Attached
POPL-2016-papers11:45 - 12:10
Talk
Cezara DrăgoiINRIA, ENS, CNRS, Thomas A. HenzingerIST Austria, Damien ZuffereyMIT
Link to publication DOI Pre-print Media Attached File Attached