VSync：弱内存模型下同步原语的按钮式验证与优化（技术报告）
计算机科学中的逻辑
2021-02-15 v1
摘要
本技术报告包含我们发表于ASPLOS'21的同名工作的配套材料。我们在第1节详细呈现本工作的核心创新——等待模型检测（AMC）。AMC的正确性证明见第2节。接着，我们在第3节讨论三个案例研究，呈现将VSync应用于现有代码库时所发现的缺陷与遇到的挑战。最后，在第4节我们描述评估的设置细节并报告进一步的实验结果。
引用
@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}
}