Memory Consistency Verification

Date: May 10, 2011
A widely-adopted methodology for verifying the memory subsystem of a chip multiprocessor (CMP) is to verify the executions of parallel test programs on the processor against the given memory consistency model. To cope with the high time complexity of memory consistency verification, a number of investigations were proposed to speed up memory consistency verification at the cost of availability (e.g., relying on dedicated hardware nonexistent in commodity processors) or completeness (e.g., missing some bugs), while few investigation has been dedicated to the configuration of appropriate test programs which would lead to more efficient verification.

From a novel perspective of test program, we devise a technique called ''program regularization'' to reduce the time complexity of memory consistency verification. The key intuition behind program regularization is that any parallel program, if being reformed appropriately, can enable efficient memory consistency verification. More specifically, for any original program, program regularization introduces some auxiliary memory locations, and periodically insert load/store operations accessing these locations in the original program. With the regularized program, verifying memory consistency only requires a linear time complexity (with respect to the number of memory operations).

The research entitled “Brief Announcement: Program Regularization in Verifying Memory Consistency” has been accepted by 23rd ACM Symposium on Parallelism in Algorithms and Architectures (SPAA).