Change *_reservation to take physaddr #676
Conversation
| @@ -68,3 +67,13 @@ struct zMcause { | |||
| extern struct zMcause zmcause, zscause; | |||
|
|
|||
| extern mach_bits zminstret; | |||
|
|
|||
| enum kind_zphysaddr { Kind_zphysaddr }; | |||
There was a problem hiding this comment.
Having to duplicate this sail-internal representation does not sound like a good idea to me. IMO the C callback should just use the underlying bits.
There was a problem hiding this comment.
If/when we switch to the struct Model { #include "model.c" } trick then we won't have to do this. But I agree, it's too error-prone until it's actually checked by the compiler.
There was a problem hiding this comment.
I think this just makes it more difficult to read for no real gain. If we want to ensure that load_reservation takes a physaddr we should make it a sail function that calls the C function with the raw bits. Not sure this adds much value over the current physaddrbits though.
|
Emmm, @arichardson in fact, if follow your requirements, it is indeed simpler to convert it directly to physaddrbits. However, another question is why functions like *_reservation are C functions; would it be more consistent to define them as sail functions? |
That is a good question - I am not familiar with this part of the model and why they are not written in sail. Maybe to allow swapping them out for something else in the concurrency model? But I would imagine we could do the same by moving them into a separate .sail file. |
So @Timmmm what do you think ? |
I presume it is because reservation is a memory thing and that is also handled outside Sail. I think a practical reason is that if you are simulating a multicore chip then you would have a single memory in C, and you'd also need to handle reservations there. If you had reservation state in Sail then it would be duplicated for each core and that wouldn't work, e.g. multiple cores could reserve different addresses at the same time. (I didn't write it though so that's just a guess.) |
Fix #670, edit Sail's C language code so that the load_reservation and match_reservation functions can accept physaddr type parameters