Dr. LIANG Hongjin and Prof. FENG Xinyu from School of Computer Science in University of Science and Technology of China (USTC) have made important breakthrough in the field of concurrent program verification. They have designed the first program logic for verifying starvation-freedom and deadlock-freedom of concurrent objects. This work has been published at the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016
) with the title of “A Program Logic for Concurrent Objects under Fair Scheduling
In a concurrent program, multiple tasks are running in parallel and sharing resources. Bugs like starvation, deadlock or livelock would cause a task to wait for some resource indefinitely and prevent it from making progress. Program testing may not find all those bugs due to the complexity of a concurrent program. LIANG and FENG have proposed a new program logic, which can rigorously prove that a concurrent program never suffers from starvation, deadlock or livelock. The program logic has been applied to verify some classic concurrent algorithms, including the first formal verification of the starvation-freedom of lock-coupling lists and the deadlock-freedom of optimistic lists and lazy lists. This work provides theoretic foundations for real-world concurrent program verification.
POPL is one of the top international conferences on programming languages and systems. It is an annual forum for the discussion of programming language design and implementation, compilers, program analysis and verification, etc. The paper by LIANG and FENG is the only one from mainland China at POPL 2016. Before 2016, there have been only three papers from mainland China published at POPL, the first one of which was published at POPL 2012, also by the team of LIANG, FENG and other colleagues.
POPL 2016 was held in St. Petersburg, FL, USA, from January 20 to January 23. LIANG Hongjin gave a talk about this work.
This work was supported in part by NSFC.
(School of Computer Science and Technology)