A reinforcement learning agent requires proper state approximation when handling partially observable environments. Bounded sequences of action-observation pairs are generally employed to approximate the notion of state, but the choice of representations for actions and observations depends on the specific environment. When targeting the verification environment of a multicore design, observations should capture coherent shared-memory behavior, which can be modeled with order relations capturing properties of the execution of concurrent programs, such as the reads-from (RF) and the coherence (CO) relations. A recent work proposed the use of RF-signatures as observations. However, that relation only provides value observation from loads (all having effect limited to the local core consuming its value), but not from stores (each potentially having effect on all cores sharing the same block, due to the coherence protocol). That is why this paper proposes an agent-directed approach that relies on CO-signatures and combined CO/RF-signatures to improve verification. We evaluated variants of a directed test generator based on the DQN agent under distinct signatures choices for different verification tasks involving 16 and 32-core ARMv8 2-level MOESI designs. Experimental results show that CO/RF-signatures lead to faster median coverage evolution.

A crucial step in the design of multicore systems is to validate the interaction between cores. This involves test program generation and runtime analysis. We propose a novel reinforcement learning approach to directed test generation, where an agent induces a suite of programs, which are executed in a simulation environment for a multicore. It focuses on how to recover state information from raw observations of the environment such that the agent can learn from interaction how to improve coverage for any verification task. We evaluated our state representation for different verification tasks involving 16 and 32-core ARMv8 2-level MOESI designs.