fix(arm): Propagate load-exclusive post-view through STXR forwarding - #175
Open
febyeji wants to merge 1 commit into
Open
fix(arm): Propagate load-exclusive post-view through STXR forwarding#175febyeji wants to merge 1 commit into
febyeji wants to merge 1 commit into
Conversation
febyeji
marked this pull request as ready for review
July 1, 2026 14:15
febyeji
force-pushed
the
fix/arm-exclusive-forwarding
branch
from
July 1, 2026 18:04
7f593e8 to
e0713aa
Compare
febyeji
marked this pull request as draft
July 1, 2026 19:56
febyeji
marked this pull request as ready for review
July 2, 2026 15:41
febyeji
force-pushed
the
fix/arm-exclusive-forwarding
branch
5 times, most recently
from
July 6, 2026 11:02
edd6a5d to
a23e2e0
Compare
febyeji
force-pushed
the
fix/arm-exclusive-forwarding
branch
2 times, most recently
from
July 17, 2026 21:28
39ebfae to
ca35228
Compare
tperami
reviewed
Jul 22, 2026
tperami
left a comment
tperami
left a comment
Collaborator
There was a problem hiding this comment.
The commit message must mention that this is a weakening from original promising model and Armed cats paper to current Arm model
| Module XclItem. | ||
| Record t := | ||
| make { | ||
| time : nat; |
Collaborator
There was a problem hiding this comment.
Need to say this is the data of the load exclusive (time is the external read time, and view is the vpost of the load exclusive
Comment on lines
+223
to
+224
| (* The latest load-exclusive, if its matching store-exclusive has not | ||
| run yet. *) |
Collaborator
There was a problem hiding this comment.
Suggested change
| (* The latest load-exclusive, if its matching store-exclusive has not | |
| run yet. *) | |
| (* The latest unmatched load-exclusive. *) |
| time : nat; | ||
| view : view; | ||
| xcl : bool | ||
| xcl_view : option nat |
Collaborator
There was a problem hiding this comment.
Suggested change
| xcl_view : option nat | |
| xcl_view : option nat (** Implement the new [[R];rmw;rfi;[A|Q]] rule in [aob]*) |
Carry the paired load-exclusive post-view separately from the forwarded write view, and join it back only for acquire reads from successful store-exclusive forwarding. This implementation is a weakening from the original Promising model and the Armed Cats paper to the current Arm model.
febyeji
force-pushed
the
fix/arm-exclusive-forwarding
branch
from
July 23, 2026 04:13
ca35228 to
77bc071
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This fix follows the original Promising-ARM model’s treatment of exclusive state: its
Exbankrecords both the load timestamp and the resulting view (tsandview), and an exclusive read savesview_postthere.However, the current ArchSem code keeps only the LDXR timestamp in the exclusive buffer. As a result, later reads that forward from the successful STXR may miss ordering information that came from the paired LDXR.