一句话：提出 VSync 框架，自动检测弱内存模型同步原语中缺失与过度约束的内存屏障，并验证其安全与活性。
现代弱内存模型架构（如 ARM 和 RISC-V）上，即使专家也难实现高效且正确的同步原语；缺失或过度约束的 barrier 会威胁正确性或性能。VSync 是一个辅助优化与验证此类同步原语的框架，可自动检测缺失和过度约束的 barrier，并确保必要的安全与活性属性。它引入两项新技术：自适应线性松弛（ALR）利用 barrier 单调性和推测，快速寻找正确且最大程度松弛的 barrier 组合；Await 模型检测（AMC）则首次使在弱内存模型上检查 await 循环终止性成为可能。该工作为 WMM 同步原语的一键式验证与优化提供了新途径。
Implementing highly efficient and correct synchronization primitives on modern Weak Memory Model (WMM) architectures, such as ARM and RISC-V, is very difficult even for human experts. We introduce VSync, a framework to assist in optimizing and verifying synchronization primitives on WMM architectures. VSync automatically detects missing and overly-constrained barriers, while ensuring essential safety and liveness properties. VSync relies on two novel techniques: 1) Adaptive Linear Relaxation (ALR), which utilizes barrier monotonicity and speculation to quickly find a correct maximally-relaxed barrier combination; and 2) Await Model Checking (AMC), which for the first time makes it possible to check termination of await loops on WMMs.
@inproceedings{paperbot6083,
title = {VSync: push-button verification and optimization for synchronization primitives on weak memory models},
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},
booktitle = {ASPLOS},
year = {2021},
doi = {10.1145/3445814.3446748}
}