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)
