The TAU Programming Languages and Systems Seminar - Robustness Against Release/Acquire Semantics
Ori Lahav
28 באפריל 2019, 12:30
בניין שרייבר, חדר 309
Abstract:
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.