chipsalliance / dromajo

RISC-V RV64GC emulator designed for RTL co-simulation
Apache License 2.0
210 stars 63 forks source link

Fix #64 track memory sequence numbers #69

Closed et-tommythorn closed 1 year ago

et-tommythorn commented 1 year ago

Stores may invalidate reservations held by other harts. I tried to find the cheapest possible implementation of this and settled on store sequence numbers. Stores increment the global and the local reservation sequence numbers so they will stay in sync as long as no other hart stores before the store conditional.

Using the test case provided by Laurentiu-Cristian Duca, and changing Dromajo to execute only a single instruction per hart per iteration, we can observe that reservations are broken as expected:

0: lr.w: addr=80001000, S#0
1: lr.w: addr=80001000, S#0
2: lr.w: addr=80001000, S#0
3: lr.w: addr=80001000, S#0
0: sc.w success memval=1 S#0
1: sc.w failed memval=1 S#0 != S#1
2: sc.w failed memval=1 S#0 != S#1
3: sc.w failed memval=1 S#0 != S#1

It's still slightly more expensive than I like. Two possible variations:

et-tommythorn commented 1 year ago

Timed out on @renau