Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

sc.w was executed incorrectly in Rocket #3511

Open
HanyJie opened this issue Oct 18, 2023 · 1 comment
Open

sc.w was executed incorrectly in Rocket #3511

HanyJie opened this issue Oct 18, 2023 · 1 comment

Comments

@HanyJie
Copy link

HanyJie commented Oct 18, 2023

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
Copy link
Contributor

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants