Add LDAR/STLR and LDAPR instructions#36
Conversation
febyeji
changed the title
febyeji
changed the title
|
What do you think about inlining decode functions like |
- Add LDAR/STLR and LDAPR decode and execution. - Carry acquire/release/RCpc flags directly through the existing Load and Store AST variants. - Refresh Coq snapshots for the updated acquire/release instruction support. - Use the AccessDescriptor constructors to map those flags into acqsc/acqpc/relsc.
febyeji
changed the title
|
Just to point it out: At this moment, I don't think there is a point to refreshing the snapshots, none of our processes use them |
tperami
left a comment
tperami
left a comment
There was a problem hiding this comment.
Only comment about access descriptor creation and whitespace. The actual instructions are great!
| } | ||
|
|
||
| function create_writeAccessDescriptor() -> AccessDescriptor = { | ||
| function create_gprAccessDescriptor( |
There was a problem hiding this comment.
I don't think this function is useful and any functions with a long list of boolean parameter is generally a bad idea. Calling the function with a long list of true,false,false,true is not helpful to the reader. As I guideline, I think more than 3 boolean in a row is a terrible idea.
| function create_writeAccessDescriptor( | ||
| release : bool, | ||
| exclusive : bool, | ||
| atomicop : bool |
There was a problem hiding this comment.
I don't think you need that one? RMW are going to call another function to make an accessor that is both read and write.
| acquire : bool, | ||
| rcpc : bool, | ||
| exclusive : bool, | ||
| atomicop : bool |
| wMem(2^size, addr, X(t)[(8*2^size-1)..0], accdesc) | ||
| } | ||
|
|
||
|
|
There was a problem hiding this comment.
The goal was to maintain 2-line spacing between different instruction class. Any reason for this change?
2 participants
Uh oh!
There was an error while loading. Please reload this page.