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
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

10:30 - 12:10
Track 1: Foundations of distributed systemsResearch Papers at Grand Bay North
Chair(s): Mooly SagivTel Aviv University
10:30
25m
Talk
Certified Causally Consistent Distributed Key-Value Stores
Research Papers
Media Attached
10:55
25m
Talk
'Cause I'm Strong Enough: Reasoning about Consistency Choices in Distributed Systems
Research Papers
Alexey GotsmanIMDEA, Hongseok YangUniversity of Oxford, UK, Carla FerreiraUniversidade Nova Lisboa, Mahsa NajafzadehUPMC & INRIA, Marc ShapiroInria & LIP6
Media Attached
11:20
25m
Talk
A Program Logic for Concurrent Objects under Fair Scheduling
Research Papers
Hongjin LiangUniversity of Science and Technology of China, Xinyu FengUniversity of Science and Technology of China
Media Attached
11:45
25m
Talk
PSync: a partially synchronous language for fault-tolerant distributed algorithms
Research Papers
Cezara DrăgoiINRIA, ENS, CNRS, Thomas A. HenzingerIST Austria, Damien ZuffereyMIT
Link to publication DOI Pre-print Media Attached File Attached