VSync：弱内存模型上同步原语的按钮验证和优化（技术报告）
VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)
摘要：
本技术报告包含与我们在ASPLOS'21上发表的相同标题的工作相关的材料。我们从第二节开始。本文详细介绍了本文的核心创新点Await模型检验（AMC）。AMC的正确性证明可以在Sec. 2.接下来，我们将讨论SEC中的三个研究案例。3、介绍在现有代码库中应用VSync时发现的错误和遇到的挑战。最后，在第4我们描述了我们评估的设置细节，并报告了进一步的实验结果。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
