QED - Quod erat demonstrandum

Concurrency-related bugs are notoriously difficult to discover by code review and testing. By doing a formal proof on the program text, one can statically verify that no execution of the program leads to an error. The effectiveness of the proof depends on the proper choice of the manual inputs such as code annotations. Deriving these annotations for a concurrent program requires complicated reasoning. The main reason behind this is the interaction between threads over the shared memory. While writing the proof, at every point, one has to consider the possible interleavings of conflicting operations. Existing proof methods including Owicki-Gries, rely/guarantee and concurrent separation logic are applied at the finest level of concurrency. Analyzing the program at this level requires complex annotations and invariants, along with many auxiliary variables. QED is a new proof method that simplifies verifying assertions in concurrent programs. The key feature of our method is the use of atomicity as the main proof tool. A proof is done by rewriting the program with larger atomic blocks in a number of steps. In order to reach the desired level of atomicity, we alternate proof steps that apply abstraction and reduction, each of which improves the outcome of the other in a following step. Then, we check assertions sequentially within the atomic blocks of the resulting program. We declare the original program correct when we discharge all the assertions. Our proof style provides separation of concerns: At each step, we either use facts about a concurrency protocol to enlarge atomic blocks, or check data properties sequentially.