Verifying Observational Robustness Against a C11-style Memory Model
We study the problem of verifying the robustness of concurrent programs against a C11-style memory model that includes relaxed accesses and release/acquire accesses and fences, and show that this verification problem can be reduced to a standard reachability problem under sequential consistency. We further observe that existing robustness notions do not allow the verification of programs that use speculative reads as in the sequence lock mechanism, and introduce a novel “observational robustness” property that fills this gap. In turn, we show how to soundly check for observational robustness. We have implemented our method and applied it to several challenging concurrent algorithms, demonstrating the applicability of our approach. To the best of our knowledge, this is the first method for verifying robustness against a programming language concurrency model that includes relaxed accesses and release/acquire fences.
Thu 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
| 16:00 - 17:00 | |||
| 16:0010m Talk | Verifying Observational Robustness Against a C11-style Memory Model POPLLink to publication DOI | ||
| 16:1010m Talk | Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper POPLLink to publication DOI | ||
| 16:2010m Talk | Modeling and Analyzing Evaluation Cost of CUDA Kernels POPLLink to publication DOI | ||
| 16:3010m Talk | Optimal Prediction of Synchronization-Preserving Races POPL Umang Mathur University of Illinois at Urbana-Champaign, Andreas Pavlogiannis Aarhus University, Mahesh Viswanathan University of Illinois at Urbana-ChampaignLink to publication DOI Pre-print | ||
| 16:4010m Talk | Taming x86-TSO Persistency POPLLink to publication DOI Pre-print | ||
| 16:5010m Break | Break POPL | ||
