SAS 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
co-located with SPLASH 2021
Mon 18 Oct 2021 11:20 - 11:35 at Zurich B - Session 2B Chair(s): Cezara Drăgoi
Mon 18 Oct 2021 19:20 - 19:35 at Zurich B - Session 2B Chair(s): Suvam Mukherjee

We present a thread-modular abstract interpretation(TMAI) technique to verify programs under the release-acquire (RA) memory model for safety property violations. The main contributions of our work are: we capture the execution order of program statements as an abstract domain, and propose a sound upper approximation over this domain to efficiently reason over RA concurrency. The proposed domain is general in its application and captures the ordering relations as a first-class feature in the abstract interpretation theory. In particular, the domain represents a set of sequences of modifications of a global variable in concurrent programs as a partially ordered set. Under this approximation, older sequenced-before stores of a global variable are forgotten and only the latest stores per variable are preserved. We establish the soundness of our proposed abstractions and implement them in a prototype abstract interpreter called PRIORI. The evaluations of PRIORI on existing and challenging RA benchmarks demonstrate that the proposed technique is not only competitive in refutation, but also in verification. PRIORI shows significantly fast analysis runtimes with higher precision compared to recent state-of-the-art tools for RA concurrency.

Mon 18 Oct

Displayed time zone: Central Time (US & Canada) change

10:50 - 12:10
Session 2BSAS at Zurich B +8h
Chair(s): Cezara Drăgoi Inria / ENS / Informal Systems
10:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Arie Gurfinkel University of Waterloo, Jorge A. Navas SRI International, Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys
Pre-print
11:05
15m
Talk
Selectively-Amortized Resource BoundingVirtual
SAS
Tianhan Lu University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Ashutosh Trivedi
Pre-print
11:20
15m
Talk
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Divyanjali Sharma IIT Delhi, India, Subodh Sharma IIT Delhi
11:35
35m
Live Q&A
Session 2B Discussion, Questions and Answers
SAS

18:50 - 20:10
Session 2BSAS at Zurich B
Chair(s): Suvam Mukherjee Microsoft Research
18:50
15m
Talk
Compositional Verification of Smart Contracts Through Communication AbstractionVirtual
SAS
Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Arie Gurfinkel University of Waterloo, Jorge A. Navas SRI International, Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys
Pre-print
19:05
15m
Talk
Selectively-Amortized Resource BoundingVirtual
SAS
Tianhan Lu University of Colorado Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Ashutosh Trivedi
Pre-print
19:20
15m
Talk
Thread-modular Analysis of Release-Acquire ConcurrencyVirtual
SAS
Divyanjali Sharma IIT Delhi, India, Subodh Sharma IIT Delhi
19:35
35m
Live Q&A
Session 2B Discussion, Questions and Answers
SAS