Mon 24 Jun 2019 10:00 - 10:20 at 229AB - Concurrency II Chair(s): Dan Grossman

We present GenMC, a model checking algorithm for concurrent programs that is parametric in the choice of memory model and can be used for verifying clients of concurrent libraries. Subject to a few basic conditions about the memory model, our algorithm is sound, complete and optimal, in that it explores each consistent execution of the program according to the model exactly once, and does not explore inconsistent executions or embark on futile exploration paths. We implement GenMC as a tool for verifying C programs. Despite the generality of the algorithm, its performance is comparable to the state-of-art specialized model checkers for specific memory models, and in certain cases exponentially faster thanks to its coarse partitioning of executions.

Mon 24 Jun

Displayed time zone: Tijuana, Baja California change

10:00 - 11:00
Concurrency IIPLDI Research Papers at 229AB
Chair(s): Dan Grossman University of Washington
10:00
20m
Talk
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
20m
Talk
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
20m
Talk
Robustness Against Release/Acquire Semantics
PLDI Research Papers
Ori Lahav Tel Aviv University, Roy Margalit Tel Aviv University, Israel
Pre-print