A Canonical Test Representation for Verification of Shared-Memory Behavior in Multiprocessor Systems

The scope of this article is the design verification of a multicore chip or multichip multiprocessor by running concurrent test programs until coverage goals are reached. Interactions between multiple processors through shared memory must obey a memory consistency model, which specifies valid behaviors. We propose a canonical test-program representation that encodes primal shared-memory behaviors to be induced at runtime. It is intended as one of the main keys to the design of new test generators. We prove that our representation does not limit the search space, because it induces equivalence classes that can be completely and uniquely encoded. In particular, we show experimental evidence that our representation is also suitable to learning-based test generators, because it enables the design of effective actions. We have built a generator directed by a Reinforcement Learning agent, designed its actions based on our encoding, and compared it with three generators when targeting 32-core designs. For a given time limit, our generator reached the largest coverage and led to the fastest error diagnosis in 3/4 of the verification scenarios, despite our choice of a minimalist agent. The theoretical guarantees and the experimental evidence indicate that our representation provides proper grounds for defining effective actions, and it prevents them from either inducing redundant tests or limiting the test suite.