Better handling of misaligned accesses (take 2) #861

pmundkur · 2025-04-15T20:03:18Z

This is a rebased version of #467.

The first commit is essentially the same as #467, except rebased and made to work with the config system.

The second commit uses the new vmem_{read,write} helpers in the floating point and vector extensions.

The AMO instructions are intact, since they don't fit nicely into the assumptions of the helpers. So are the zicboz and zicbom; they are low-level anyway so should not use a high-level helper. Fetch is untouched, left for future.

I tested variations of the new config parameters to ensure the upstream riscv-tests and vector tests still pass (or have no regressions, in the case of vector).

github-actions · 2025-04-15T20:15:46Z

Test Results

400 tests ±0 400 ✅ ±0 1m 54s ⏱️ ±0s
1 suites ±0 0 💤 ±0
1 files ±0 0 ❌ ±0

Results for commit 677dab9. ± Comparison against base commit da6f449.

♻️ This comment has been updated with latest results.

nadime15

Looks awesome! Just a few comments

nadime15 · 2025-04-16T16:58:46Z

model/riscv_insts_base.sail

+      match vmem_write(vaddr, width_bytes, data, aq, rl, false) {
+        Ok(_) => RETIRE_SUCCESS,
+        Err(vaddr, e) => {
+          handle_mem_exception(vaddr, e);
+          return RETIRE_FAIL
        }


Suggested change

match vmem_write(vaddr, width_bytes, data, aq, rl, false) {

Ok(_) => RETIRE_SUCCESS,

Err(vaddr, e) => {

handle_mem_exception(vaddr, e);

return RETIRE_FAIL

}

match vmem_write(vaddr, width_bytes, data, aq, rl, false) {

Ok(_) => RETIRE_SUCCESS,

Err(vaddr, e) => { handle_mem_exception(vaddr, e); return RETIRE_FAIL }

To match model/riscv_insts_fext.sail and the rest.

This will change anyway once I rebase on top of #755.

nadime15 · 2025-04-16T16:59:20Z

model/riscv_insts_fext.sail

+        Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+        Ok(result)    => { F(rd) = nan_box(result); RETIRE_SUCCESS }


Suggested change

Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },

Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }

Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }

Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },

Thanks, done.

nadime15 · 2025-04-16T17:11:34Z

model/riscv_vmem_utils.sail

+val split_misaligned : forall 'width, 'width > 0.
+  (virtaddr, int('width)) -> {'n 'bytes, 'width == 'n * 'bytes & 'bytes > 0. (int('n), int('bytes))}


I am not sure if I overlooked that Sail feature, but I have not encountered it so far (is this new?). So essentially, it allows validating that the return values satisfy certain conditions?

Yes, I think it's an existential type; it's mentioned in passing in the Sail manual (see the val div1 example). It's been around for a while I think.

It's not new. Not sure exactly what it's called (refinement type, liquid type, existential type, etc. take a guess!) but yeah it lets you add conditions to a type. I think we use them in some type aliases too; it doesn't have to be in the return position.

You can use them in argument positions too but we generally use the forall syntax instead.

nadime15 · 2025-04-16T17:35:54Z

model/riscv_vmem_utils.sail

+function prop_access_within_is_aligned(addr : bits(32), bytes : bits(4)) -> bool = {
+  let bytes = unsigned(zero_extend(32, 0b1) << unsigned(bytes));
+  if bytes > 0 then {
+    access_within(addr, bytes, bytes) == (fmod_int(unsigned(addr), bytes) == 0)


What is fmod_int() doing?

Good question. It's integer modulus. I now notice there are two of these: emod_int and fmod_int. The first always returns a positive value, the second ('f' stands for 'floor' according to GMP docs) retains the sign of the divisor. Not sure the difference matters here. @Alasdair?

fdiv and fmod are flooring, so they round down always. tdiv and tmod are truncating so they round towards zero. emod and ediv are euclidian division. Wikipedia has good summary of the differences here https://en.wikipedia.org/wiki/Modulo#Variants_of_the_definition

The only reason we really have euclidian division is it's the definition used in the SMT integer theory

Seems like since these are both positive, they’d all be the same? In which case we might as well use %, which is already defined in the prelude to mean emod.

The SMT properties check out in both cases, so I'll switch it to % when I rebase.

pmundkur · 2025-04-18T19:53:37Z

The last push rebased on master and refactored #467 to pull the ext_data_get_addr calls into the vmem_utils helpers. This cleans up the calling code significantly, and (hopefully) isolates almost all the RVWMO-relevant pieces for usual loads/stores into vmem_utils.

As before, AMOs, fetch, and CBOs are untouched.

There is a slight difference in alignment checks for LOADRES/STORECON in the read/write helpers. I'll try to clean it up before final merge.

@Alasdair could you check if this breaks RVWMO modelling in any way? There's a comment in vmem_utils that I retained from your #467 that may need adjusting?

pmundkur · 2025-04-18T20:08:36Z

Hmm, the CI failure is odd. It's building locally (and passing tests) with Sail 0.19.

pmundkur · 2025-04-18T20:18:52Z

Hmm, the CI failure is odd. It's building locally (and passing tests) with Sail 0.19.

Drat, I think this is triggering a bug in the smt backend of Sail, both 0.19 and the latest master.

pmundkur · 2025-04-22T00:22:58Z

@bacam Could you take a look at this Rocq failure? Perhaps it's being triggered by the match being inside a repeat? Adding a let _ : unit = match { ... }; annotation did not help.

jordancarlin

Overall looking like an amazing simplification!

Makefile.old

model/riscv_vmem_utils.sail

jordancarlin · 2025-04-21T03:40:51Z

model/riscv_vmem_utils.sail

+
+  // If the Zama16b extension is enabled, the region_width must be at least 16
+  let region_width = if currentlyEnabled(Ext_Zama16b) then {
+    max_int(16, region_width)


Suggested change

max_int(16, region_width)

max(16, region_width)

model/riscv_vmem_utils.sail

jordancarlin · 2025-04-22T05:58:33Z

doc/ReadingGuide.md

+  See the [Virtual Memory Notes](./notes_Virtual_Memory.adoc) for
+  details.
+
+- The `riscv_vmem_utils.sail` file provides a higher level interface


Might be worth adding a more detailed description to the notes_Virtual_Memory.adoc file.

I'm not sure what can go in there in addition to what's already described in comments in riscv_vmem_utils.sail.

model/riscv_vmem_utils.sail

bacam · 2025-04-25T17:09:24Z

model/riscv_vmem_utils.sail

+  /* If the load is misaligned or an allowed misaligned access, split into `n`
+     (single-copy-atomic) memory operations, each of `bytes` width. If the load is
+     aligned, then `n` = 1 and bytes will remain unchanged. */
+  let ('n, bytes) = split_misaligned(vaddr, width);


We can work around the Rocq problem by changing bytes to 'bytes - this gives data a printable type that can be used in rewrites. (Rocq also needs a couple of termination measures, but I'll give those separately.)

bacam · 2025-04-25T17:11:00Z

For Rocq output we also need to add two termination measures to riscv_termination.sail:

termination_measure vmem_write_addr repeat n
termination_measure vmem_read repeat n

Although it would be helpful if someone could check that n is the correct limit in both cases.

pmundkur · 2025-04-25T17:55:22Z

For Rocq output we also need to add two termination measures to riscv_termination.sail:
termination_measure vmem_write_addr repeat n
termination_measure vmem_read repeat n
Although it would be helpful if someone could check that n is the correct limit in both cases.

Yeah, I think n is the correct limit since the loop should repeat at most n times in both cases.

Your suggestions fixed the build. Thanks!

jordancarlin · 2025-04-28T23:39:42Z

model/riscv_vmem_utils.sail

+  let region_width = min(2 ^ pagesize_bits, sys_misaligned_allowed_within());
+
+  // If the Zama16b extension is enabled, the region_width must be at least 16
+  let region_width = if currentlyEnabled(Ext_Zama16b) then {


The interaction between Zama16b and allowed_within still needs to be resolved: #860 (comment). As discussed in that issue, I think Zama16b should not directly impact this function. Once we have configuration validation set up, we can have an assertion that if Zama16b is supported then allowed_within >= 16. For this PR, I think I would be in favor of just dropping the Zama16b configuration option altogether.

Ok, makes sense to add Zama16b on top of this later. Removed.

nadime15

Looks good!

It would be great to prioritize and get this merged so work on the other PRs can move forward!

Refactor the LOAD and STORE instruction so they split misaligned accesses into multiple sub-accesses and perform address translation separately. This means we should handle the case where a misaligned access straddles a page boundary in a sensible way, even if we don't yet cover the full range of possibilities allowed for any RISC-V implementation. There are options for the order in which misaligned happen, i.e. from high-to-low or from low-to-high as well as the granularity of the splitting, either all the way to bytes or to the largest aligned size. The splitting can also be disabled if an implementation supports misaligned accesses in hardware. In addition tidy up the implementation in a few ways: - Very long lines on the LOAD encdec were fixed by adding a helper - Add some linebreaks in the code so it reads as less claustrophobic - Ensure we use the same names for arguments in encdec/execute/assembly. Previously we used 'size' and 'width'. I opted for 'width' consistently. Primary author: Alasdair Armstrong <[email protected]> Co-authored-by: Alasdair Armstrong <[email protected]>

Add some comments on the API available from `vmem_utils`. Update Makefile.old for SMT properties. Update the ReadingGuide.

jordancarlin

LGTM now that the configuration issue has been resolved. This will be great to get in!

pmundkur requested a review from Alasdair April 15, 2025 20:04

nadime15 reviewed Apr 16, 2025

View reviewed changes

pmundkur force-pushed the ldst_misaligned_take2 branch from 9323a72 to a23d5fc Compare April 18, 2025 19:45

pmundkur force-pushed the ldst_misaligned_take2 branch from a23d5fc to d5ffd8c Compare April 18, 2025 21:16

pmundkur added the tgmm-agenda Tagged for the next Golden Model meeting agenda. label Apr 18, 2025

jordancarlin mentioned this pull request Apr 21, 2025

Configuration validation #860

Open

pmundkur force-pushed the ldst_misaligned_take2 branch 2 times, most recently from 066874c to fec2fa5 Compare April 21, 2025 23:56

jordancarlin reviewed Apr 22, 2025

View reviewed changes

pmundkur force-pushed the ldst_misaligned_take2 branch from fec2fa5 to 597d678 Compare April 22, 2025 14:09

pmundkur mentioned this pull request Apr 22, 2025

Use result type for TR_Result instead of union #875

Open

pmundkur force-pushed the ldst_misaligned_take2 branch 2 times, most recently from 4fd40f9 to 50034c4 Compare April 24, 2025 15:01

pmundkur mentioned this pull request Apr 25, 2025

Test Lean/Coq output when it's all working #744

Closed

bacam reviewed Apr 25, 2025

View reviewed changes

bacam mentioned this pull request Apr 25, 2025

Unprintable types cause type-checking problems during rewrites rems-project/sail#1261

Open

pmundkur force-pushed the ldst_misaligned_take2 branch from 50034c4 to 132308b Compare April 25, 2025 17:40

pmundkur force-pushed the ldst_misaligned_take2 branch from 132308b to 3c0a61a Compare April 28, 2025 23:21

jordancarlin requested changes Apr 28, 2025

View reviewed changes

nadime15 approved these changes Apr 29, 2025

View reviewed changes

pmundkur and others added 2 commits April 29, 2025 15:19

Update the F/D and vector loads/stores to use the vmem_utils helpers.

677dab9

Add some comments on the API available from `vmem_utils`. Update Makefile.old for SMT properties. Update the ReadingGuide.

pmundkur force-pushed the ldst_misaligned_take2 branch from 3c0a61a to 677dab9 Compare April 29, 2025 20:23

jordancarlin approved these changes Apr 29, 2025

View reviewed changes

pmundkur mentioned this pull request Apr 29, 2025

Generating SMT files #903

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Better handling of misaligned accesses (take 2) #861

Better handling of misaligned accesses (take 2) #861

pmundkur commented Apr 15, 2025

github-actions bot commented Apr 15, 2025 •

edited

Loading

nadime15 left a comment

nadime15 Apr 16, 2025

pmundkur Apr 16, 2025

nadime15 Apr 16, 2025

pmundkur Apr 16, 2025

nadime15 Apr 16, 2025

pmundkur Apr 16, 2025

Timmmm Apr 16, 2025

nadime15 Apr 16, 2025

pmundkur Apr 16, 2025

Alasdair Apr 16, 2025

Alasdair Apr 16, 2025

jordancarlin Apr 17, 2025

pmundkur Apr 17, 2025 •

edited

Loading

pmundkur commented Apr 18, 2025

pmundkur commented Apr 18, 2025

pmundkur commented Apr 18, 2025

pmundkur commented Apr 22, 2025

jordancarlin left a comment

jordancarlin Apr 21, 2025

pmundkur Apr 22, 2025

jordancarlin Apr 22, 2025

pmundkur Apr 22, 2025

bacam Apr 25, 2025

bacam commented Apr 25, 2025

pmundkur commented Apr 25, 2025

jordancarlin Apr 28, 2025

pmundkur Apr 29, 2025

nadime15 left a comment

jordancarlin left a comment

		Err(vaddr, e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
		Ok(result) => { F(rd) = nan_box(result); RETIRE_SUCCESS }

		val split_misaligned : forall 'width, 'width > 0.
		(virtaddr, int('width)) -> {'n 'bytes, 'width == 'n * 'bytes & 'bytes > 0. (int('n), int('bytes))}

Better handling of misaligned accesses (take 2) #861

Are you sure you want to change the base?

Better handling of misaligned accesses (take 2) #861

Conversation

pmundkur commented Apr 15, 2025

github-actions bot commented Apr 15, 2025 • edited Loading

Test Results

nadime15 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

pmundkur Apr 17, 2025 • edited Loading

Choose a reason for hiding this comment

pmundkur commented Apr 18, 2025

pmundkur commented Apr 18, 2025

pmundkur commented Apr 18, 2025

pmundkur commented Apr 22, 2025

jordancarlin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bacam commented Apr 25, 2025

pmundkur commented Apr 25, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nadime15 left a comment

Choose a reason for hiding this comment

jordancarlin left a comment

Choose a reason for hiding this comment

github-actions bot commented Apr 15, 2025 •

edited

Loading

pmundkur Apr 17, 2025 •

edited

Loading