Recent advances in concurrent separation logic have enabled the formal verification of increasingly sophisticated fine-grained (i.e., lock-free) concurrent programs. For these programs, the golden standard of correctness is linearizability, which expresses that concurrent executions always behave as some valid sequence of sequential executions. Various approaches have been developed to prove linearizability in a compositional manner. One could show that the fine-grained implementation contextually refines a course-grained implementation, or one could prove a logically atomic triple. Both of these approaches have been mechanized in the Iris concurrent separation logic in Coq, enabling one to carry out linearizability proofs in a foundational manner. However, since these proofs are done interactively, proving linearizability remains a laborious task.

This paper develops proof automation for both approaches of proving linearizability. We develop goal-directed versions of the proof rules that can be implemented effectively as strategies, using ideas from logic programming. To enable integration with interactive proofs, we design our rules so that backtracking is only needed to find linearization points. To implement our automation in Coq, we develop Diaframe 2.0—a proof automation extension for Iris. Diaframe 2.0 comes with the existing proof automation for ghost-state and invariant reasoning from Diaframe 1.0, but is extensible w.r.t. various program specification styles. This extensibility is achieved by factoring out separation logic reasoning that is common to all these logics, and the use of novel abduction and transformer hints to capture reasoning rules specific to a program specification style. We evaluate our proof automation on a set of existing benchmarks and novel proofs, showing that it provides significant reduction of proof work for both approaches to linearizability.