Pith. sign in

REVIEW

VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report)

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2102.06590 v1 pith:IGE3WBZP submitted 2021-02-12 cs.LO

Jonas Oberhauser , Rafael Lourenco de Lima Chehab , Diogo Behrens , Ming Fu , Antonio Paolillo , Lilith Oberhauser , Koustubha Bhat , Yuzhong Wen
show 3 more authors
Haibo Chen Jaeho Kim Viktor Vafeiadis
This is my paper · ORCID
classification cs.LO
keywords reportfoundtechnicalvsyncworkaccompanyingapplyingasplos
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Pith tools