search

chipsalliance / rocket-chip

Rocket Chip Generator
Other
3.25k stars 1.13k forks source link

sc.w was executed incorrectly in Rocket #3511

Open hanyjie opened 1 year ago

hanyjie commented 1 year ago

Type of issue: bug report

Impact: unknown

Development Phase: proposal

Other information Hello, when using the Rocket core, the sc.w, which should have failed, was executed by Rocket. For example, the following instruction:

l0:    la x15, data
       addi x15, x15, 0
       lr.d x12, (x15)
l1:    la x23, data
       addi x23, x23, 12
       sc.w x14, x8, (x23)
...
data:   .dword 0x25b0b9a021799aeb, 0x24db3c5f591237f4
...

The lr.d instruction was not set at location (x23), so the sc.w operation should have failed. However, when we executed the above instruction using the Spike and Rocket core separately, we observed different results. In Spike, the register x14 (which records whether sc.w executed successfully, with an initial value of a random number other than 0 or 1) was set to a non-zero value, 0x0000000000000001, indicating that sc.w failed in Spike. But in Rocket, it was set to zero, 0x0000000000000000, indicating that sc.w succeeded in Rocket, and the data was successfully stored at the corresponding location.

Can you tell me why Rocket handles such examples this way?

Thanks！

michael-etzkorn commented 1 year ago

From unpriviledged risc-v spec 8.2. (bold, italics is my own):

An implementation can register an arbitrarily large reservation set on each LR, provided the reservation set includes all bytes of the addressed data word or doubleword. An SC can only pair with the most recent LR in program order. An SC may succeed only if no store from another hart to the reservation set can be observed to have occurred between the LR and the SC, and if there is no other SC between the LR and itself in program order. An SC may succeed only if no write from a device other than a hart to the bytes accessed by the LR instruction can be observed to have occurred between the LR and SC. Note this LR might have had a different effective address and data size, but reserved the SC’s address as part of the reservation set.

If I'm not mistaken, I believe Rocket uses larger granularity than Spike for reservation sets.