Bio

Hongjin Liang is a limited-term associate researcher at University of Science and Technology of China (USTC). She received her Ph.D. in Computer Science from USTC in 2014, under the joint supervision of Prof. Xinyu Feng (USTC) and Prof. Zhong Shao (Yale).

Hongjin is interested in program verification and concurrency theory. Her Ph.D. thesis is about refinement verification of concurrent programs and its applications, in which she designed simulations and Hoare-style program logics for concurrent program refinement, and applied them to verify concurrent garbage collectors and prove linearizability of concurrent objects and algorithms. She is currently trying to extend her refinement verification techniques to also reason about liveness properties of concurrent algorithms.

For more information, please visit http://staff.ustc.edu.cn/~lhj1018.

A Program Logic for Concurrent Objects under Fair Scheduling

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 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.

This is joint work with Xinyu Feng at USTC.