Pipeline not being flushed on PMP register clears #2193
Assignees
Labels
Type:Bug
Bugs
Comments
|
Thanks for finding this @mndstrmr I'll be putting a fix together shortly. In the scenario you describe any instruction that's in the IF stage when the clear is executed has already has its PMP check done under the old pre-clear state. Ultimately whilst clearly an issue that must be fixed I think the practical impact of this is limited. First it is only the instruction in the IF stage that immediately follows the clear that 'sees' the old PMP state (before clear) and hence could execute when it shouldn't. It's also notable that only the execute part of the PMP permissions is effected as the read/write is checked when we attempt to being the relevant memory transaction and will always see the latest version of the PMP state. Second there are limited scenarios under which an csrrc can cause a PMP state change that is immediately relevant. You must alter the configuration of a region that you are about to execute (i.e. a region that covers the instruction after your clear) and any change to the PMP CSRs must be done in M mode so you need to alter M mode relevant state. This means either the region is locked (so cannot be altered unless msseccfg.RLB is set) or is one of the epmp shared data regions (which don't provide execute permissions so don't matter for this issue). This means you have to have msseccfg.RLB set to produce a code sequence that can be effected by this issue. The MMWP and MML bits in msseccfg cannot be cleared once set so cannot be affected by this issue (which only relates to CSR bit clears). For any software running on a version of Ibex effected by this issue it's recommended the CSR clears are never used to alter PMP state to avoid this scenario entirely. |
GregAC
added a commit
to GregAC/ibex
that referenced
this issue
Sep 17, 2024
This fixes lowRISC#2193, an issue that meant bit clears in PMP related CSRs didn't immediately apply to an instruction already in the fetch stage due to a lack of a pipeline flush. With this change the pipeline will flush in that scenario, fixing the issue. It now flushes the pipeline on all CSR modifications as this makes the pipeline more resliant against similar issues in the future (where the list of CSRs to flush on should have been updated but wasn't).
marnovandermaas
added a commit
to marnovandermaas/ibex
that referenced
this issue
Jan 13, 2025
Here's a high-level overview of what this commit does: - Compiles Sail into SystemVerilog including patchin compiler bugs - Create a TCL file that tells JasperGold what to prove and assume - Check memory operations modelling the LSU Most of these properties now prove without time-bound on the response from memory due to alternative LSUs - Check memory even with Smepmp errors: Continues on top of riscv/sail-riscv#196 - CSR verification - Checks for instruction types such as B-Type, I-Type, R-Type - Check illegal instructions and WFI instructions - Using psgen language for proof generation - Documentation on how to use the setup - Wrap around proof that proves instructions executed in a row still match the specification. - Liveness proof to guarantee instructions will retire within a upper bound of cycles. All of these proofs make heavy use of the concept of k-induction. All the different properties and steps are necessary to help the tool get the useful properties it needs to prove the next step. The instruction correctness, wrap-around and liveness all give us increased confidence that Ibex is trace-equivalent to Sail. Throughout this process an issue was found in Ibex where the pipeline was not flushing properly on changing PMP registers using clear: lowRISC#2193 Alternative LSUs: This makes all top level memory properties prove quickly and at a low proof effort (1 or 2-induction). Three 'alternative LSUs' representing three stages of memory instructions: 1. Before the first response is received, in the EX stage 2. After the first response is received, but not the second grant, also in the EX stage 3. Before the last response is received in the WB stage. In each case we ask 'if the response came now, would the result be correct?'. Similar is applied for CSRs/PC though less directly. This is particularly interesting (read: ugly) in the case of a PMP error wbexc_exists makes Wrap properties fast to prove. The bottleneck becomes SpecPastNoWbexcPC, which fails only due to a bug. See the comment in riscv.proof. Co-authored-by: Marno van der Maas <[email protected]>
marnovandermaas
pushed a commit
to GregAC/ibex
that referenced
this issue
Jan 24, 2025
This fixes lowRISC#2193, an issue that meant bit clears in PMP related CSRs didn't immediately apply to an instruction already in the fetch stage due to a lack of a pipeline flush. With this change the pipeline will flush in that scenario, fixing the issue. It now flushes the pipeline on all CSR modifications as this makes the pipeline more resliant against similar issues in the future (where the list of CSRs to flush on should have been updated but wasn't).
marnovandermaas
added a commit
to marnovandermaas/ibex
that referenced
this issue
Jan 27, 2025
Here's a high-level overview of what this commit does: - Compiles Sail into SystemVerilog including patchin compiler bugs - Create a TCL file that tells JasperGold what to prove and assume - Check memory operations modelling the LSU Most of these properties now prove without time-bound on the response from memory due to alternative LSUs - Check memory even with Smepmp errors: Continues on top of riscv/sail-riscv#196 - CSR verification - Checks for instruction types such as B-Type, I-Type, R-Type - Check illegal instructions and WFI instructions - Using psgen language for proof generation - Documentation on how to use the setup - Wrap around proof that proves instructions executed in a row still match the specification. - Liveness proof to guarantee instructions will retire within a upper bound of cycles. All of these proofs make heavy use of the concept of k-induction. All the different properties and steps are necessary to help the tool get the useful properties it needs to prove the next step. The instruction correctness, wrap-around and liveness all give us increased confidence that Ibex is trace-equivalent to Sail. Throughout this process an issue was found in Ibex where the pipeline was not flushing properly on changing PMP registers using clear: lowRISC#2193 Alternative LSUs: This makes all top level memory properties prove quickly and at a low proof effort (1 or 2-induction). Three 'alternative LSUs' representing three stages of memory instructions: 1. Before the first response is received, in the EX stage 2. After the first response is received, but not the second grant, also in the EX stage 3. Before the last response is received in the WB stage. In each case we ask 'if the response came now, would the result be correct?'. Similar is applied for CSRs/PC though less directly. This is particularly interesting (read: ugly) in the case of a PMP error wbexc_exists makes Wrap properties fast to prove. The bottleneck becomes SpecPastNoWbexcPC, which fails only due to a bug. See the comment in riscv.proof. Co-authored-by: Marno van der Maas <[email protected]>
marnovandermaas
added a commit
to marnovandermaas/ibex
that referenced
this issue
Jan 27, 2025
Here's a high-level overview of what this commit does: - Compiles Sail into SystemVerilog including patchin compiler bugs - Create a TCL file that tells JasperGold what to prove and assume - Check memory operations modelling the LSU Most of these properties now prove without time-bound on the response from memory due to alternative LSUs - Check memory even with Smepmp errors: Continues on top of riscv/sail-riscv#196 - CSR verification - Checks for instruction types such as B-Type, I-Type, R-Type - Check illegal instructions and WFI instructions - Using psgen language for proof generation - Documentation on how to use the setup - Wrap around proof that proves instructions executed in a row still match the specification. - Liveness proof to guarantee instructions will retire within a upper bound of cycles. All of these proofs make heavy use of the concept of k-induction. All the different properties and steps are necessary to help the tool get the useful properties it needs to prove the next step. The instruction correctness, wrap-around and liveness all give us increased confidence that Ibex is trace-equivalent to Sail. Throughout this process an issue was found in Ibex where the pipeline was not flushing properly on changing PMP registers using clear: lowRISC#2193 Alternative LSUs: This makes all top level memory properties prove quickly and at a low proof effort (1 or 2-induction). Three 'alternative LSUs' representing three stages of memory instructions: 1. Before the first response is received, in the EX stage 2. After the first response is received, but not the second grant, also in the EX stage 3. Before the last response is received in the WB stage. In each case we ask 'if the response came now, would the result be correct?'. Similar is applied for CSRs/PC though less directly. This is particularly interesting (read: ugly) in the case of a PMP error wbexc_exists makes Wrap properties fast to prove. The bottleneck becomes SpecPastNoWbexcPC, which fails only due to a bug. See the comment in riscv.proof. Co-authored-by: Marno van der Maas <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In this commit the pipeline was made to flush on changes to PMP registers, changes made via
CSR_OP_CLEARhowever are missed.This is likely because prior to this commit only mstatus and mie were listed, and clearing is safe for those.
This meant that instructions being fetched were passing PMP checks which they should not have been.
The text was updated successfully, but these errors were encountered: