VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models

Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis

Onderzoeksoutput: Conference paperResearch

Samenvatting

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. We use VSync to automatically optimize and verify state-of-the-art synchronization primitives from systems like seL4, CertiKOS, musl libc, DPDK, Concurrency Kit, and Linux, as well as from the literature. In doing so, we found three correctness bugs on deployed systems due to missing barriers and several performance bugs due to overly-constrained barriers. Synchronization primitives optimized by VSync have similar performance to industrial libraries optimized by experts.
Originele taal-2English
TitelProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems
Plaats van productieNew York, NY, USA
UitgeverijAssociation for Computing Machinery
Pagina's530–545
Aantal pagina's16
ISBN van geprinte versie9781450383172
DOI's
StatusPublished - 19 apr 2021
EvenementACM International Conference on Architectural Support for Programming Languages and Operating Systems -
Duur: 12 apr 202123 apr 2021
Congresnummer: 2021
https://asplos-conference.org/asplos2021/index.html

Publicatie series

NaamASPLOS 2021
UitgeverijAssociation for Computing Machinery

Conference

ConferenceACM International Conference on Architectural Support for Programming Languages and Operating Systems
Verkorte titelASPLOS
Periode12/04/2123/04/21
Internet adres

Bibliografische nota

Publisher Copyright:
© 2021 Owner/Author.

Keywords

  • weak memory models
  • model checking

Vingerafdruk

Duik in de onderzoeksthema's van 'VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models'. Samen vormen ze een unieke vingerafdruk.

Citeer dit