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.

Wed 26 Jun

Displayed time zone: Tijuana, Baja California change

10:00 - 11:00
Verification IIPLDI Research Papers at 229AB
Chair(s): Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia
Verification of Programs under the Release-Acquire Semantics
PLDI Research Papers
Parosh Aziz Abdulla Uppsala University, Sweden, Jatin Arora IIT Bombay, India, Mohamed Faouzi Atig Uppsala University, Shankaranarayanan Krishna IIT Bombay, India
A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
PLDI Research Papers
Sandeep Dasgupta University of Illinois at Urbana-Champaign, USA, Daejun Park University of Illinois at Urbana-Champaign, Theodoros Kasampalis University of Illinois at Urbana-Champaign, USA, Vikram S. Adve University of Illinois at Urbana-Champaign, Grigore Ro┼ču University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached
An Applied Quantum Hoare Logic
PLDI Research Papers
Li Zhou Department of Computer Science and Technology, Tsinghua University, Nengkun Yu University of Technology Sydney, Australia, Mingsheng Ying University of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University.
Media Attached