VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)

TL;DR

This paper introduces Await Model Checking (AMC), a verification technique for synchronization primitives on weak memory models, demonstrating its effectiveness through bug detection and optimization in real-world code bases.

Contribution

The work presents AMC, a novel verification approach for synchronization primitives under weak memory models, along with case studies and experimental validation.

Findings

Detected bugs in existing code bases using VSync

Validated effectiveness of AMC in verification tasks

Provided insights into synchronization primitive optimizations

Abstract

This technical report contains material accompanying our work with same title published at ASPLOS'21. We start in Sec. 1 with a detailed presentation of the core innovation of this work, Await Model Checking (AMC). The correctness proofs of AMC can be found in Sec. 2. Next, we discuss three study cases in Sec. 3, presenting bugs found and challenges encountered when applying VSync to existing code bases. Finally, in Sec. 4 we describe the setup details of our evaluation and report further experimental results.