Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 16:00 - 16:10 at POPL-B - Concurrency (Shared Memory)

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00
Concurrency (Shared Memory)POPL at POPL-B
16:00
10m
Talk
Verifying Observational Robustness Against a C11-style Memory Model
POPL
Roy MargalitTel Aviv University, Israel, Ori LahavTel Aviv University
Link to publication DOI
16:10
10m
Talk
Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper
POPL
Jatin AroraCMU, Sam WestrickCarnegie Mellon University, Umut A. AcarCarnegie Mellon University
Link to publication DOI
16:20
10m
Talk
Modeling and Analyzing Evaluation Cost of CUDA Kernels
POPL
Stefan K. MullerIllinois Institute of Technology, Jan HoffmannCarnegie Mellon University
Link to publication DOI
16:30
10m
Talk
Optimal Prediction of Synchronization-Preserving Races
POPL
Umang MathurUniversity of Illinois at Urbana-Champaign, Andreas PavlogiannisAarhus University, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
16:40
10m
Talk
Taming x86-TSO Persistency
POPL
Artem KhyzhaTel Aviv University, Ori LahavTel Aviv University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL