The development of concurrent separation logic has enabled the formal verification of fine-grained concurrent algorithms and data structures such as locks, queues and reference counters. To verify such programs, one needs to come up with an appropriate invariant, which is responsible for tieing the physical state to a logical state and a protocol. For example, in the case of a spin lock, the invariant couples ‘the lock reference holds the value true’ to ‘the lock is in the locked state’, while enforcing that the locked resource is only available after a succesful lock. Note that the spin lock has two valid logical states, which means the invariant contains a disjunction—and this happens for most such data structures.

The next task is to prove that all operations of the program respect the invariant. Besides proving this manually, there are several tools available to automate such proofs. However, all of them struggle with the disjunctive nature of invariants. The main problem is to choose the correct logical state after altering the physical state. The traditional approach is to backtrack: pick one state and continue the proof, but if this fails, pick another. Unfortunately, the correct choice of disjunct may depend on a case analysis. Skipping such a case analysis will cause the proof search to fail.

While disjunctions are no problem for proof automation in classical logic, the challenges with disjunctions are prominent in the study of proof automation for intuitionistic logic. We take inspiration from that area—specifically, based on ideas from connection calculus, we design a simple calculus for separation logic with disjunctions featuring a novel concept of a connection. Although our calculus is not complete, it has the advantage that it can be extended to the state-of-the-art concurrent separation logic Iris, and can be implemented effectively in the Coq proof assistant with little need for backtracking. We evaluate the practicality on 24 challenging benchmarks, 14 of which we can verify fully automatically.