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

pldi-2019-papers
10:00 - 11:00: PLDI Research Papers - Concurrency II at 229AB
Chair(s): Dan GrossmanUniversity of Washington
pldi-2019-papers10:00 - 10:20
Talk
Michalis KokologiannakisMax Planck Institute for Software Systems (MPI-SWS), Azalea RaadMPI-SWS, Germany, Viktor VafeiadisMPI-SWS, Germany
Pre-print Media Attached
pldi-2019-papers10:20 - 10:40
Talk
Hanru JiangUniversity of Science and Technology of China, Hongjin LiangNanjing University, China, Siyang XiaoUniversity of Science and Technology of China, China, Junpeng ZhaUniversity of Science and Technology of China, China, Xinyu FengNanjing University
Pre-print Media Attached
pldi-2019-papers10:40 - 11:00
Talk
Ori LahavTel Aviv University, Roy MargalitTel Aviv University, Israel
Pre-print