Fast and Generalized Polynomial Time Memory Consistency Verification

TL;DR

This paper introduces a fast, parallelized algorithm for verifying multi-threaded execution against various memory consistency models, significantly improving efficiency in processor verification.

Contribution

It presents a low-complexity, fully parallelized algorithm that supports multiple memory consistency models without performance loss.

Findings

Algorithm is efficient and parallelized.

Supports multiple memory models.

Used in practical processor verification.

Abstract

The problem of verifying multi-threaded execution against the memory consistency model of a processor is known to be an NP hard problem. However polynomial time algorithms exist that detect almost all failures in such execution. These are often used in practice for microprocessor verification. We present a low complexity and fully parallelized algorithm to check program execution against the processor consistency model. In addition our algorithm is general enough to support a number of consistency models without any degradation in performance. An implementation of this algorithm is currently used in practice to verify processors in the post silicon stage for multiple architectures.