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
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

10:00 - 11:00: PLDI Research Papers - Concurrency II at 229AB
Chair(s): Dan GrossmanUniversity of Washington
pldi-2019-papers10:00 - 10:20
Michalis KokologiannakisMax Planck Institute for Software Systems (MPI-SWS), Azalea RaadMPI-SWS, Germany, Viktor VafeiadisMPI-SWS, Germany
Pre-print Media Attached
pldi-2019-papers10:20 - 10:40
Hanru JiangUniversity of Science and Technology of China, Hongjin LiangNanjing University, China, Siyang XiaoUniversity of Science and Technology of China, China, Junpeng ZhaUniversity of Science and Technology of China, China, Xinyu FengNanjing University
Pre-print Media Attached
pldi-2019-papers10:40 - 11:00
Ori LahavTel Aviv University, Roy MargalitTel Aviv University, Israel