Title: Reasoning about Optimistic Concurrency using a Program Logic for History
Speaker: Professor SHAO Zhong　  (Yale University)
Time:　  3pm, Thursday May 27
Venue:　 Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

ABSTRACT:

In this talk, we propose a novel program logic that uses invariants on historical traces to reason about highly-concurrent optimistic algorithms. We use past tense temporal operators in our assertions to specify execution histories. Following previous work on separation logic, our logic supports separation over both space (program states) and time so that the specification with history information would not break modularity. We prove some classic optimistic algorithms, and show that the intuition behind these algorithms can be naturally captured using trace invariants. Specifications and proofs in our logic are simple and intuitive and they do not need to use any auxiliary variables.

This is joint work with Ming Fu (USTC & Yale), Yong Yi (USTC & Yale), Xinyu Feng (TTI Chicago), and Yu Zhang (USTC).