[Gems-users] Protocol bugs found in MESI

[Rakesh Komuravelli <komurav1@xxxxxxxxxxxx>]

Hi,

We are trying to submit a paper and in this regard, we are working on formally verifying the MESI protocol that is shipped with GEMS(MESI_SCMP_bankdirectory). I think we found some bugs in the MESI protocol implementation and most of them are caused by races related to write backs. We would appreciate your feedback on this before we discuss it in our paper. Let me describe one of the bugs here. It is caused by a race between L1/L2 replacement. The trace that leads to an error is as follows:

(Prefix L1_ and L2_ indicate events happening or states at L1 and L2 respectively. For this discussion, we have only one processor with private L1, one address and an L2. Each entry in the trace is written as <old_state, event, new_state> [Actions performed])

1. <L1_I, Load, L1_IS> [Issue GETS to L2]

2. <L2_NP, GETS, L2_ISS> [Issue GETS to Memory]

3. Mem_Fetch [Send DATA to L2]

4. <L2_ISS, DATA, L2_MT_MB> [Send DATA_Exclusive to L1]

5. <L1_IS, DATA_Exclusive, L1_E> [Issue Exclusive_UNBLOCK to L2]

6. <L2_MT_MB, Exclusive_UNBLOCK, L2_MT>

7. <L2_MT, L2_Replacement, L2_MCT_I> [Issue INV to L1]

8. <L1_E, L1_Replacement, L1_M_I> [Issue PUTX to L2]

9. <L1_M_I, PUTX, L1_I> [Issue DATA to L2]

10. <L2_MCT_I, WB_DATA_clean, L2_NP>

11. <L1_I, Store, L1_IM> [Issue GETX to L2]

12. <L2_NP, GETX, L2_IM> [Issue GETS to Memory]

13. Mem_Fetch [Send DATA to L2]

14. <L2_IM, DATA, L2_MT_MB> [Send DATA to L1]

15. <L1_IM, DATA, L1_M> [Send Exclusive_UNBLOCK to L2]

16. <L2_MT_MB, Exclusive_UNBLOCK, L2_MT]

(Now, PUTX that was issued by L1 in 8 reaches L2)

17. <L2_MT, PUTX, L2_M> [Issue WB_ACK to L1]

18. <L1_M, WB_ACK, !!!!ERROR!!!!

WB_ACK reaches L1 while it is in 'M' state. But L1 wasn't expecting WB_ACK in this state.

Thanks,

Rakesh