Verifying the correctness of concurrent software with subtle
synchronization is notoriously challenging. We present the
Anchor verifier, which is based on a new formalism for
specifying synchronization disciplines that describes both (1)
what memory accesses are permitted, and (2) how each permitted
access commutes with concurrent operations of other threads (to
facilitate reduction proofs). Anchor supports the verification
of both lock-based blocking and cas-based non-blocking
algorithms. Experiments on a variety concurrent data structures
and algorithms show that Anchor significantly reduces the burden
of concurrent verification.