Wed 26 Jun 2019 10:00 - 10:20 at 229AB - Verification II Chair(s): Michael Norrish

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.

Conference Day
Wed 26 Jun

Displayed time zone: Tijuana, Baja California change

10:00 - 11:00
Verification IIPLDI Research Papers at 229AB
Chair(s): Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia
Verification of Programs under the Release-Acquire Semantics
PLDI Research Papers
Parosh Aziz AbdullaUppsala University, Sweden, Jatin AroraIIT Bombay, India, Mohamed Faouzi AtigUppsala University, Shankaranarayanan KrishnaIIT Bombay, India
A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
PLDI Research Papers
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 Ro┼čuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached
An Applied Quantum Hoare Logic
PLDI Research Papers
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