Verification of Programs under the Release-Acquire Semantics
We address the verification of concurrent programs running under the release-acquire (RA) semantics.
We show that the reachability problem is undecidable even in the case where the input program is finite-state.
Given this undecidability, we follow the spirit of the work on context-bounded analysis for detecting bugs in
programs under the classical SC model, and propose an under-approximate reachability analysis for the case of RA. To this end, we propose a novel notion, called view-switching, and provide a code-to-code translation from an input program under RA to a program under SC. This leads to a reduction, in polynomial time, of the bounded view-switching reachability problem under RA to the bounded context-switching problem under SC. We have implemented a prototype tool VBMC and tested it on a set of benchmarks, demonstrating that many bugs in programs can be found using a small number of view switches.
Wed 26 Jun Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change
|10:00 - 10:20|
|10:20 - 10:40|
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Daejun ParkUniversity of Illinois at Urbana-Champaign, Theodoros KasampalisUniversity of Illinois at Urbana-Champaign, USA, Vikram S. AdveUniversity of Illinois at Urbana-Champaign, Grigore RosuUniversity of Illinois at Urbana-ChampaignLink to publication DOI Pre-print Media Attached
|10:40 - 11:00|
Li ZhouDepartment of Computer Science and Technology, Tsinghua University, Nengkun YuUniversity of Technology Sydney, Australia, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University.Media Attached