[4-20]Modular Concurrency Verification

Date:2009-04-19

Title: Modular Concurrency Verification
Speaker: Feng Xinyu, Toyota Technological Institute at Chicago
Time: 3pm, Monday April 20, 2009
Venue: Lecture room, State Key Lab of Computer Science, Level 3 Building #5

Abstract:

Concurrent Separation Logic (CSL) and Rely-Guarantee (R-G) reasoning are widely used to reason about shared-state concurrent programs. However, neither of them supports modular verification of fine-grained concurrency. In this talk, I will propose a new program logic, LRG, for Local Rely-Guarantee reasoning. LRG combines the support of local reasoning and information hiding in CSL with the expressiveness for fine-grained concurrency in traditional R-G reasoning. The logic, for the first time, supports a frame rule over rely/guarantee conditions so that specifications of program modules only need to talk about the resources used locally, and the verified modules can be reused in different threads without redoing the proof. Moreover, we introduce a new hiding rule to hide the resources shared by a subset of threads from the rest in the system. The support of information hiding not only improves the modularity of Rely-Guarantee reasoning, but also enables the sharing of dynamically allocated resources, which requires adjustment of rely/guarantee conditions.

Bio:
Xinyu Feng is a research assistant professor at Toyota Technological Institute at Chicago (TTI-C). He got his Bachelor’s and Master’s degree from Nanjing University in 1999 and 2002, and Ph.D. degree from Yale University in 2007, all in Computer Science. His research interests are in the area of programming languages and formal methods. In particular, he is interested in developing theories, programming languages and tools to build formally certified system software, with rigorous guarantees of safety and correctness properties.