Add preliminary support for Zsn extension #79
Conversation
| @@ -29,6 +29,11 @@ bitfield PTE_Bits : pteAttribs = { | |||
| V : 0 | |||
| } | |||
|
|
|||
| bitfield PTE_Ext : extPte = { | |||
There was a problem hiding this comment.
If you're making this defined by the standard then this should be a separate type (logically, part of pteAttribs, but it may be easier to have pteAttribsHi and pteAttribsLo), not extPte. extPte is for non-standard extensions to the model to use (i.e. just sail-cheri-riscv, currently), but this also needs to be done in a way that those extensions continue to be able to work (code changes are fine and may well be necessary, but there must be a way for them to hook into sail-riscv as needed without modifying sail-riscv).
There was a problem hiding this comment.
Thanks for the feedback @jrtc27. Is renaming to pteAttribsHi and pteAttribsLo enough to avoid that conflict, or are you suggesting something else also needs to be done?
There was a problem hiding this comment.
Yes and no. It means extPte is free to be defined by extensions again, but there's still the issue of changing what you can do with it; either it overlaps with some/all of pteAttribsHi and things get really weird, or you reduce it to the bits not defined by the standard and then extensions using them break. Either way there are issues for CHERI-RISC-V; the former means composing Zsn and Xcheri doesn't work (but if done correctly you should still be able to support them as mutually exclusive extensions in the model), the latter just breaks it entirely and forces us to change CheriBSD, our four/five different hardware implementations, QEMU, spike and, of course, sail-cheri-riscv, to pick different bits for the 5 bits (and researchers at Microsoft are reserving a 6th bit) we need (and then rinse and repeat as RISC-V gobbles more up in the coming years), which is manageable for a research group but extremely painful when we have downstreams at other universities and companies across the world building things on CHERI-RISC-V. There was no reserved space for non-standard extensions so we picked what we thought was most likely to remain unused (yeah, picking reserved bits not marked for that is a risk, but we had no other option), but here we are. So I don't know what the right answer is beyond being able to convince the virtual memory task group to leave those bits reserved for non-standard extensions.
There was a problem hiding this comment.
Also, this was done based on the fact that riscv-privileged says "These reserved bits may also be used to facilitate research experimentation.", which is exactly what we're doing.
| } else if (v & mask) == pattern then { | ||
| n + 1 | ||
| } else { | ||
| napot_bits39(v, n + 1) |
There was a problem hiding this comment.
The recursion seems unnecessarily complex. What are you actually trying to compute? Would a loop suit you better or can you do away with even that?
There was a problem hiding this comment.
Please forgive my Sail naivety. This is really just "find last one" aka "count trailing zeros + 1". If there's a simpler way to write that, great.
There was a problem hiding this comment.
There's a count_leading_zeros in the standard library (in fact it's a builtin) but seemingly no trailing ones. There's also the following commented-out version (for if it weren't a builtin):
function count_leading_zeros x = {
foreach (i from ('N - 1) to 0 by 1 in dec)
if [x[i]] == [bitone] then return 'N - i - 1;
return 'N;
}
so I imagine something like the following would work:
val count_trailing_zeros : forall 'N , 'N >= 1. bits('N) -> {'n, 0 <= 'n <= 'N . atom('n)}
function count_trailing_zeros x = {
foreach (i from 0 to ('N - 1) by 1)
if [x[i]] == [bitone] then return i;
return 'N;
}
Not sure what the square brackets around x[i] and bitone are for, mind, I'd expect it to work without.
There was a problem hiding this comment.
what about count_trailing_zeroes = 'N - count_leading_zeroes(~(X^-X)). (with the correct syntax)
| } else if (v & mask) == pattern then { | ||
| n + 1 | ||
| } else { | ||
| napot_bits39(v, n + 1) |
There was a problem hiding this comment.
Wrong function? And how is the implementation of this meant to differ from the Sv48 version? Can they share a common implementation?
There was a problem hiding this comment.
Oops, yes, this should be napot_bits48. Good catch.
In general almost all of the code in Sv32, Sv39, and Sv48 is redundant already. I agree it would make sense to factor out not just this new napot_bits function but also all of the rest of that common code, but I didn't want to tie that into this Zsn PR or take all of that on at one in my first attempt to write Sail, so I kept it separate for now.
There was a problem hiding this comment.
Yeah, it's just slightly more awkward with the extra level of translation (but easy enough to do), and Sv32 is rather different due to not having the upper bits in the PTEs. Merging Sv39 and Sv48 together is easy enough to do, but for Sv32 it'd probably be a case of pulling out common functionality but still having separate files, one for Sv32 and one for Sv39+48(+57).
There was a problem hiding this comment.
I'm willing to give this refactoring a shot (on a separate standalone commit). We're also planning to add Sv57 soon, so it would make sense to refactor this now before duplicating the code yet again.
I do have one question though @jrtc27. Within the walkN functions, while the code is mostly the same, there are function calls like Mk_SV48_PTE(v) which are specific to the PTE type, and the Sv32, Sv39, Sv48, and Sv57 (assuming I follow the pattern) PTEs are defined as different types in riscv_vmem_common.sail, even though all but Sv32 are actually the same. If I make the function generic, I don't see an easy way to call the right Mk_SVN_PTE function for the given PTE type. I can't just factor it out from the top either because the function is called recursively.
Is there an easy way in Sail to write a function like walk in a generic way while still being able to specialize for the right Mk_SVN_PTE(v) function internally? Similar question elsewhere, e.g., for translate48 and add_to_TLB48. I couldn't figure out how to pass a function pointer as an argument, if that's even possible in Sail. Are there other ways around this? If not, perhaps that's why the code was just duplicated in the first place?
Alternatively, would it be a bad thing to at least simply merge the Sv39, Sv48, and Sv57 PTE types into common "64b PTE" types, so at least we'd get this down to 2x duplication (32b vs. 64b) instead of 4x or more?
There was a problem hiding this comment.
Hello Daniel, what's the state of the refactoring you mentioned?
There was a problem hiding this comment.
@daniellustig I have no strong preference. It would be good to speed up merging important PRs in. I'm not sure anyone will rewrite Sail for you. There is a shortage of Sail programmers.
There was a problem hiding this comment.
@daniellustig I've had some undergraduate summer interns who did a lot of Sail. They are back at university, I can ask them if they wanted to do (paid) Sail work, if you like.
There was a problem hiding this comment.
Hi @martinberger, sorry for the delayed response (it was the Thanksgiving holiday here in the US). If they are interested and funding is available, then it would be great to have their help.
There was a problem hiding this comment.
@daniellustig I don't know about funding, I doubt that the RISCV organisation pays this. But he is interested, I'll connect you in a PM.
There was a problem hiding this comment.
Mark Himelstein is the person to talk to about that. I know there is money floating around for some things like this, but don't recall exactly what.
|
just an observation: does Sail allow comments in code? If so, could we
start using them?
…On Mon, Oct 18, 2021 at 6:44 AM Daniel Lustig ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In model/riscv_vmem_sv48.sail
<#79 (comment)>:
> @@ -1,5 +1,18 @@
/* Sv48 address translation for RV64. */
+val napot_bits48 : (bits(44), nat) -> nat
+function napot_bits48 (v, n) = {
+ let mask = shiftl(v ^ v ^ EXTZ(0b1), n + 1) - 1;
+ let pattern = shiftl(v ^ v ^ EXTZ(0b1), n);
+ if n > 8 then {
+ 0
+ } else if (v & mask) == pattern then {
+ n + 1
+ } else {
+ napot_bits39(v, n + 1)
@martinberger <https://github.com/martinberger> I'm still at the same
place I was in my earlier comments: I don't have enough Sail expertise at
this point to properly clean all this up myself, and unfortunately I won't
have a chance to dive back into it within the next few weeks at least...
I'm happy to help review PRs if someone else is willing to try it though.
Also, I can't tell if your preference now is to do Sv57 first, or to do
Svnapot first, or to somehow do both simultaneously (without conflicting)?
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#79 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHPXVJTRUO3HYQQL4AFSG5DUHQQCNANCNFSM4UL7RJTQ>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.
|
|
Yes, and we already do. There are 326 instances of |
|
Yes, that was a rhetorical question, and the point was that I haven't seen
many comments in the code that is being added, e.g. this specific snippet
which, in isolation, is pretty hard to interpret.
…On Mon, Oct 18, 2021 at 7:58 AM Jessica Clarke ***@***.***> wrote:
Yes, and we already do. There are 326 instances of // and 6157 instances
of /* (a lot of which, but not all, are copyright headers) in model/.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#79 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHPXVJUXVYI7E6I3DM7BMD3UHQYYFANCNFSM4UL7RJTQ>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.
|
|
adding Mark who may have duget for this
…On Mon, Nov 22, 2021 at 3:22 AM Martin Berger ***@***.***> wrote:
***@***.**** commented on this pull request.
------------------------------
In model/riscv_vmem_sv48.sail
<#79 (comment)>:
> @@ -1,5 +1,18 @@
/* Sv48 address translation for RV64. */
+val napot_bits48 : (bits(44), nat) -> nat
+function napot_bits48 (v, n) = {
+ let mask = shiftl(v ^ v ^ EXTZ(0b1), n + 1) - 1;
+ let pattern = shiftl(v ^ v ^ EXTZ(0b1), n);
+ if n > 8 then {
+ 0
+ } else if (v & mask) == pattern then {
+ n + 1
+ } else {
+ napot_bits39(v, n + 1)
@daniellustig <https://github.com/daniellustig> I've had some
undergraduate summer interns who did a lot of Sail. They are back at
university, I can ask them if they wanted to do (paid) Sail work, if you
like.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#79 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AHPXVJXVG6H57UA6TC7BEDTUNIRVTANCNFSM4UL7RJTQ>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.
|
@daniellustig @cetola @allenjbaum Did anything come out of this? |
|
@martinberger @allenjbaum We’re looking into internship possibilities, and also have a job req out for a full time Sail developer. |
|
Closing this PR for now. If we can find someone who can properly implement Svnapot in the Sail model, they can either reopen this PR and continue working on it, or they can redo it from scratch, as they prefer. |
|
Thanks @daniellustig I hope we'll the see new version soon. |
Zsn is a new supervisor mode extension being developed by the virtual memory task group. The goal of Zsn is to support contiguous address translation ranges of naturally-aligned power-of-two (NAPOT) sizes between the existing page sizes (4KiB, 2MiB). The specific region size we're aiming to support for now is 64KiB, but we may extend support to other power-of-two sizes in the future. Zsn is currently in draft state, with a plan to go to public review hopefully by the end of the year.
See https://github.com/riscv/virtual-memory for more info on Zsn. See https://github.com/riscv/virtual-memory/blob/main/presentations/2020-12-03-Zsn-Sail.adoc for some commentary on these Sail changes.
The Zsn part itself has not yet been tested. The virtual memory group is working on creating a suite of tests, but we don't have them ready yet. There's no urgency to merge this before we're sure it's ready, but I figured I'd still open a PR to allow for feedback on the code in the meantime. This is my first attempt to write Sail, so feedback is welcome.