Hi Gabriel, It doesn't surprise me at all that there are unreachable states in the protocol. Specifically MESI_Three_Level was kind of quickly thrown together a few years ago to try to have an example three level protocol that looked something like Intel systems. The L0 cache was bolted on the MESI_Two_Level.
You have some very good questions that I don't know the answers to! Having a tool to check for dead transitions in SLICC would be very cool! I'm not sure how much effort this would take, TBH. At one point, there was some effort to make it possible to convert SLICC into a model checking language, but I don't think it was ever finished. To answer your question about how to know the total number of transitions... all I can say is that you can't assume all possible transitions will be exercised through testing. Many protocols have transitions that happen very rarely with unlikely race conditions. One example I can think of was this paper from ASPLOS ( http://research.cs.wisc.edu/multifacet/papers/asplos17_crossing_guard.pdf) which counted the number of transitions possible and that were visited by the tester. You may be able to reach out the the first author, Lena, to get more information. Sorry I can't help more. It sounds like your work has interesting research potential! Cheers, Jason On Wed, Oct 31, 2018 at 9:50 AM Gabriel Arthur Gerber Andrade < [email protected]> wrote: > 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 _______________________________________________ gem5-dev mailing list [email protected] http://m5sim.org/mailman/listinfo/gem5-dev
