Implement menvcfg

[Timmmm]

This implements the m/senvcfg(h) CSRs. This CSR is used to enable/disable extensions and behaviours for lower privilege modes. Currently the only implemented bit is FIOM which affects how fences work.

It also affects how atomic memory accesses work in non-cacheable regions, but the model does not currently support PMAs so that can't easily be implemented.

Note there is a partial implementation of menvcfg in #137, so this should simplify that PR a little.

[github-actions]

Unit Test Results

712 tests  ±0   712 ✔️ ±0   0s ⏱️ ±0s
    6 suites ±0       0 💤 ±0 
    1 files   ±0       0 ❌ ±0 

Results for commit da76e06. ± Comparison against base commit 24e3e68.

♻️ This comment has been updated with latest results.

[allenjbaum]

I think you need to define precisely what you mean by "disabling virtual memory" means exactly. By my standards (low as they are), setting SATP.MODE to Bare disables virtual memory. Clearing MISA.S also disables virtual memory...

…

On Thu, Sep 7, 2023 at 10:49 AM Jessica Clarke ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In handwritten_support/riscv_extras_sequential.lem <#303 (comment)>: > @@ -153,6 +153,10 @@ val sys_enable_next : unit -> bool let sys_enable_next () = true declare ocaml target_rep function sys_enable_next = `Platform.enable_next` +val sys_enable_fiom : unit -> bool Depends what privileged spec version you implement. We need to support all versions that people are making implementations for, so can't just go with the requirements of the latest version. — Reply to this email directly, view it on GitHub <#303 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJXVCLI3A5UJ3OKXPD3XZICJNANCNFSM6AAAAAA4NRBPCA> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[Timmmm]

I think you need to define precisely what you mean by "disabling virtual memory" means exactly.

Not sure what you are referring to here, but anyway here's the relevant bit of the spec:

If S-mode is not supported, or if satp.MODE is read-only zero (always Bare), the implementation may make FIOM read-only zero.

Now that I read it again, I think I misread it. The Sail model doesn't let you make satp.MODE be read-only zero but you can disable S-mode so that would be a legitimate way to also have FIOM disabled. I'll add an emulator flag.

[arichardson]

This looks good to me, just one question.

[allenjbaum]

It appears to be allowed but not required : Priv 3.1.18: If S-mode is not supported, or if satp.MODE is read-only zero (always Bare), the implementation *may* make FIOM read-only zero. Otherwise, it looks like it must be RW

…

On Fri, Sep 22, 2023 at 3:38 PM Alexander Richardson < ***@***.***> wrote: ***@***.**** commented on this pull request. This looks good to me, just one question. ------------------------------ In model/riscv_sys_regs.sail <#303 (comment)>: > + // Cache Block Clean and Flush instruction Enable + CBCFE : 6, + // Cache Block Invalidate instruction Enable + CBIE : 5 .. 4, + // Reserved WPRI bits. + wpri_0 : 3 .. 1, + // Fence of I/O implies Memory + FIOM : 0, +} + +register menvcfg : Envcfg +register senvcfg : Envcfg + +function legalize_envcfg(o : Envcfg, v : bits(64)) -> Envcfg = { + let v = Mk_Envcfg(v); + let o = update_FIOM(o, v.FIOM()); Does FIOM need to be hardwired to zero if it's not enabled? — Reply to this email directly, view it on GitHub <#303 (review)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AHPXVJRGTN2NMB3T52HG6ODX3YHPBANCNFSM6AAAAAA4NRBPCA> . You are receiving this because you commented.Message ID: ***@***.***>

[Timmmm]

@arichardson any chance of a final review? Pretty please? :-)

[arichardson]

@arichardson any chance of a final review? Pretty please? :-)

I'm happy with the change, but you'll need it to be approved by one of the maintainers .

[billmcspadden-riscv]

Reconsider the command line argument name.

[jrtc27]

Commits were not squashed before merging

[Timmmm]

Commits were not squashed before merging

Sorry I didn't know the policy for this project, but I agree. Rebase merging like this is probably the worst of both worlds.

Personally I would disable merge commits and rebase merging in the project settings so you have to use squash merge (i.e. squash and rebase).

[jrtc27]

Commits were not squashed before merging

Sorry I didn't know the policy for this project, but I agree. Rebase merging like this is probably the worst of both worlds.

Personally I would disable merge commits and rebase merging in the project settings so you have to use squash merge (i.e. squash and rebase).

We use rebase merging in other projects extensively. It works well if people curate their commits in the PR, and allows you to preserve a patch series as a patch series, rather than squashing it into one. Squashing a PR only works when PRs are logically a single change. Both have their uses, people just need to be disciplined when they come to merge to either squash when appropriate or check that the commit series is sensible.

[Timmmm]

Doesn't it break git bisect though since only the last commit is actually tested by CI? I personally don't see much value in preserving history for changes that were never on master. Anyway I will squash in future!