Title:Modular Concurrency Verification
Time:3£º00pm, Monday£¬April 20
Venue:Lecture Room,State Key Lab of Computer Science, Level 3 Building #5, Institute of Software, CAS
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.
The bio of the speaker:
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.