Hello, I'm part of a research team that works with memory-model verification. We use the gem5 to evaluate our techniques. From the results of our most recent experiments, a concern arose about the protocol we adopted: the *MESI Three Level* protocol.
We measured the number of distinct transitions stimulated in the finite state machine of each cache controller when running a suite of constrained random tests. The results indicated an unexpected saturation around 70% of stimulated transitions. We applied two different types of test generator, and both were unable to attain a higher percentage. In order to explain such result, we analyzed each transition not stimulated. In doing so, we identified transitions in the SLICC implementation of the protocol that seem to be unreachable. Therefore, we would like to know if someone in the development team can confirm that some transitions are unreachable (or if we are missing something). As an example, let's take one transition of the first-level cache controller (file `src/mem/protocol/MESI_Three_Level-L0cache.sm`). According to the finite state machine, the controller should change the state of a *Modified *cache block to *Shared *when it receives a forward of a load request from the second-level cache (`transition(M, Fwd_GetS, S)` in the SLICC code). However, the second-level cache never forwards such request. Instead, when the latter receives a `CoherenceRequestType:GETS` from the third-level cache (which acts as the Directory), it triggers a `L0_Invalidate_Else` event and sends an *invalidation* request to the first-level cache. Hence, the previously mentioned transition is unreachable and, naturally, was never covered in our experiments. If we are correct in our analysis, how can we correctly define the total amount of transitions in each controller? Is there any kind of automated tool to verify unreachable SLICC code? source code for reference: 1. src/mem/protocol/MESI_Three_Level-L0cache.sm 2. src/mem/protocol/MESI_Three_Level-L1cache.sm 3. src/mem/protocol/MESI_Two_Level-L2cache.sm Best regards, Gabriel Arthur _______________________________________________ gem5-dev mailing list [email protected] http://m5sim.org/mailman/listinfo/gem5-dev
