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 JunDisplayed time zone: Tijuana, Baja California change
10:00 - 11:00 | |||
10:00 20mTalk | 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 20mTalk | 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 20mTalk | Robustness Against Release/Acquire Semantics PLDI Research Papers Pre-print |