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 JunDisplayed time zone: Tijuana, Baja California change
Mon 24 Jun
Displayed time zone: Tijuana, Baja California change
10:00 - 11:00 | |||
10:00 20mTalk | 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 20mTalk | 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 20mTalk | Robustness Against Release/Acquire Semantics PLDI Research Papers Pre-print |