A program logic for concurrent objects under fair scheduling

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 threadmodular reasoning about both starvation-freedom and deadlockfreedom in one framework. It also establishes progress-aware ion 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 d...

• Type: Journal
• Year: 2016
• Where: POPL
• Authors: Hongjin Liang, Xinyu Feng
• Keywords: POPL 2016, Programming Languages