A model-based approach to design test oracles for memory subsystems of multicore microprocessors

The paper describes a method for constructing test oracles for memory subsystems of multicore microprocessors. The method is based on using nondeterministic reference models of systems under test. The key idea of the approach is on-the-fly determinization of the model behavior by using reactions from the system. Every time a nondeterministic choice appears in the reference model, additional model instances are created and launched (each simulating a possible variant of the memory subsystem behavior). When the testbench receives a reaction from the subsystem under test, it terminates all model instances whose behavior is inconsistent with that reaction. An error is detected if there is no active instance of the reference model. A reference model and the test oracle are divided into three levels: (1) the operation level, (2) the cache line level, and (3) the memory subsystem level. An operation oracle checks whether processing of a single request of the corresponding type is correct. A cache line oracle is comprised of the operation oracles and responsible for checking requests to the given cache line. The memory subsystem oracle combines cache line oracles and performs overall evaluation of the device behavior. To be implemented efficiently, the method implies the following two restrictions on the memory subsystem under test: (1) requests to different cache lines are executed independently; (2) requests to the same cache line are serialized (at most one request to a cache line is executed at each moment of time). The suggested method with slight modifications was used for verifying the L3 cache of the Elbrus-8C microprocessor; as a result, three bugs were found.