VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)
Logic in Computer Science
2021-02-15 v1
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.
Cite
@article{arxiv.2102.06590,
title = {VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)},
author = {Jonas Oberhauser and Rafael Lourenco de Lima Chehab and Diogo Behrens and Ming Fu and Antonio Paolillo and Lilith Oberhauser and Koustubha Bhat and Yuzhong Wen and Haibo Chen and Jaeho Kim and Viktor Vafeiadis},
journal= {arXiv preprint arXiv:2102.06590},
year = {2021}
}