The Anchor Verifier for Blocking and Non-blocking Concurrent Software
summary
Anchor is an automatic SMT-based verifier plus compiler that checks reduction-style concurrency using concise moves_as synchronization specs and weakest-precondition reasoning, and it can emit executable code. It handles locks and CAS (including ABA reasoning), provides yield-based decomposition and counterexample traces for debugging, and verifies a LibLFDS single-producer single-consumer queue. Comparison: Armada required 760 lines and 36 minutes to verify the queue; Anchor implements it in 62 lines and 13 seconds after about a person-day of work.
AI-written summary · about
chapters (4)
related talks
28mAutomated Correctness Analysis for core.async
01h 08mSimplifying Concurrent Programming via Synchronization Synthesis
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)
47mThread Safety with Phaser, StampedLock, and VarHandle
01h 00mConcurrency in C++20: A Deep Dive
52mNonblocking algorithms/ CAS/Atomics
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
16mFast Atomicity Monitoring