Brief Announcement: Program Regularization in Verifying Memory Consistency

摘要

Verifying memory consistency, which is to verify the executions of parallel test programs on a multiprocessor system against the given memory consistency model, is NP-hard. To accelerate verifying memory consistency in practice, we devise a technique called "program regularization". The key intuition behind program regularization is that a parallel program with some specific patterns can enable efficient verification. More specifically, for any original program, program regularization introduces some auxiliary memory locations, and periodically inserts store/load operations accessing these locations to the original program. With the regularized program, verifying memory consistency only requires a linear time complexity (with respect to the number of memory operations).