Reasoning about Optimistic Concurrency Using a Program Logic for History

Optimistic concurrency algorithms provide good performance for parallel programs but they are extremely hard to reason about. Program logics such as concurrent separation logic and rely-guarantee reasoning can be used to verify these algorithms, but they make heavy uses of history variables which may obscure the high-level intuition underlying the design of these algorithms. In this paper, we propose a novel program logic that uses invariants on history traces to reason about optimistic concurrency algorithms. We use past tense temporal operators in our assertions to specify execution histories. Our logic supports modular program specifications with history information by providing separation over both space (program states) and time. We verify Michael's non-blocking stack algorithm and show that the intuition behind such algorithm can be naturally captured using trace invariants.

• Type: Conference
• Year: 2010
• Where: CONCUR
• Authors: Ming Fu, Yong Li, Xinyu Feng, Zhong Shao, Yu Zhang
• Keywords: CONCUR 2010, Concurrent Separation Logic, Distributed And Parallel Computing, Optimistic Concurrency Algorithms, Program Logic