Mon 24 Jun 2019 10:40 - 11:00 at 229AB - Concurrency II Chair(s): Dan Grossman

We present an algorithm for automatically checking robustness of concurrent programs against C/C++11 release/acquire semantics, namely verifying that all program behaviors under release/acquire are allowed by sequential consistency. Our approach reduces robustness verification to a reachability problem under (instrumented) sequential consistency. We have implemented our algorithm in a prototype tool called Rocker and applied it to several challenging concurrent algorithms. To the best of our knowledge, this is the first precise method for verifying robustness against a high-level programming language weak memory semantics.

Mon 24 Jun

Displayed time zone: Tijuana, Baja California change

10:00 - 11:00
Concurrency IIPLDI Research Papers at 229AB
Chair(s): Dan Grossman University of Washington
10:00
20m
Talk
Model Checking for Weakly Consistent Libraries
PLDI Research Papers
Michalis Kokologiannakis Max Planck Institute for Software Systems (MPI-SWS), Azalea Raad MPI-SWS, Germany, Viktor Vafeiadis MPI-SWS, Germany
Pre-print Media Attached
10:20
20m
Talk
Towards Certified Separate Compilation for Concurrent Programs
PLDI Research Papers
Hanru Jiang University of Science and Technology of China, Hongjin Liang Nanjing University, China, Siyang Xiao University of Science and Technology of China, China, Junpeng Zha University of Science and Technology of China, China, Xinyu Feng Nanjing University
Pre-print Media Attached
10:40
20m
Talk
Robustness Against Release/Acquire Semantics
PLDI Research Papers
Ori Lahav Tel Aviv University, Roy Margalit Tel Aviv University, Israel
Pre-print