riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
415 stars 156 forks source link

misaligned load/store on page crossing doesn't tablewalk for second page #49

Open scottj97 opened 4 years ago

scottj97 commented 4 years ago

An 8-byte store to address 0xffc, for example, should store 4 bytes to one page and 4 to the next page. When paging is enabled, two separate translations are required.

The Sail model is only translating the first page, then storing 8 bytes to contiguous physical addresses.

I created a repo with a test to recreate the issue. Instruction 128 shows the problem. There is one tablewalk, then 8 bytes loaded from 0x80003FFC.

This should take an exception (with mtval 0x0000003a177df000) because the second page's access bit is 0. The handler will repair the access bit, then re-execute the instruction. The second attempt should succeed, loading the second half of the access from a different physical page.

(Fetches across pages seem to work correctly.)

pmundkur commented 4 years ago

this is a great catch and test case. i'm pondering the cleanest way to fix this.

rmn30 commented 3 years ago

Unfortunately looks like we still need a fix for this. How about adding a width parameter to translateAddr and adding a TR_Straddling case to the TR_Result union? Will need to handle this in quite a lot of places.

PeterSewell commented 3 years ago

It should do two independent accesses, separately translated, no?

On Mon, 28 Jun 2021, 10:54 Robert Norton, @.***> wrote:

Unfortunately looks like we still need a fix for this. How about adding a width parameter to translateAddr and adding a TR_Straddling case to the TR_Result union? Will need to handle this in quite a lot of places.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/rems-project/sail-riscv/issues/49#issuecomment-869545303, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZVQGSATSIK4SJC6EMDTVBBE3ANCNFSM4M4MQK2Q .

rmn30 commented 3 years ago

Yes, I'm proposing that translateAddr would do two translations if necessary and then the caller would have to deal with an additional case for page-straddling by performing multiple accesses and merging the result. Possibly the single-page case would go away and become a degenerate case.

PeterSewell commented 3 years ago

I don't know exactly how the model is structured, but my point is that the decomposition of misaligned accesses into multiple accesses should happen slightly higher up, before one even gets to translateAddr. (Also, when one gets to the concurrency behaviour, they're really independent accesses)

On Mon, 28 Jun 2021 at 12:05, Robert Norton @.***> wrote:

Yes, I'm proposing that translateAddr would do two translations if necessary and then the caller would have to deal with an additional case for page-straddling by performing multiple accesses and merging the result. Possibly the single-page case would go away and become a degenerate case.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/rems-project/sail-riscv/issues/49#issuecomment-869590699, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZR7XYVTQRV3FR5Z6V3TVBJPNANCNFSM4M4MQK2Q .

rmn30 commented 3 years ago

I haven't checked the spec but I imagine you'd want to do both of the translations first to check for faults before doing the accesses otherwise you could end up doing half a write then realising you have to take a fault. The sail model does the translation first then the memory access uses the resulting physical address (unless there is a fault) e.g. https://github.com/rems-project/sail-riscv/blob/master/model/riscv_insts_base.sail#L326 The higher up place you posit doesn't currently exist although it might be useful to introduce a translate-and-handle-misalignment layer.

PeterSewell commented 3 years ago

On Mon, 28 Jun 2021 at 13:30, Robert Norton @.***> wrote:

I haven't checked the spec but I imagine you'd want to do both of the translations first to check for faults before doing the accesses otherwise you could end up doing half a write then realising you have to take a fault.

apparently some real h/w (on other archs) does do the latter

The sail model does the translation first then the memory access uses the resulting physical address (unless there is a fault) e.g. https://github.com/rems-project/sail-riscv/blob/master/model/riscv_insts_base.sail#L326 The higher up place you posit doesn't currently exist although it might be useful to introduce a translate-and-handle-misalignment layer.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/rems-project/sail-riscv/issues/49#issuecomment-869643719, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZU2ZGT52WEKV4QIAVDTVBTNVANCNFSM4M4MQK2Q .

rmn30 commented 3 years ago

I can't see anywhere in the RISC-V specs. that directly addresses this case although it is permitted to emulate unaligned accesses in software implying that partial writes are possible at least in that case.

scottj97 commented 3 years ago

Partial writes are allowed by the spec. Spike does partial writes in this case.

However, some implementations will not, and I'd like Sail to be able to model that implementation choice without requiring extensive rework of this logic.

allenjbaum commented 2 years ago

This is a bug that will interfere with a fair number of tests - has there been any progress? Does that mean that we need to configure not only whether Sail supports unaligned accesses, but that if it does, it checks both halves before writing anything (or reading)? E.g. translate, write, translate, write vs Translate, Translate, Write, Write to ensure we can configure it like a real implementation?

scottj97 commented 2 years ago

Does that mean that we need to configure not only whether Sail supports unaligned accesses, but that if it does, it checks both halves before writing anything (or reading)? E.g. translate, write, translate, write vs Translate, Translate, Write, Write to ensure we can configure it like a real implementation?

I'm not opposed to making source code edits to change this behavior if required, but I hope it can be a small change and not a complete rewrite of the logic.

There are many implementation-dependent things that require source code edits today.

allenjbaum commented 2 years ago

I'm not sure what you mean by source code edits - as opposed to what?

My concern here is that we are comparing the behavior of a Sail model with that of some vendor's legal RISC-V implementation. If more than one result is legally possible, I want to be have the vendor indicate which behavior they implement (and I'm going to make the assumption in this case it is one order or the other), and be able to configure sail to mimic that behavior.

It's a little worse in this case, because we already know that "doesn't support unaligned data access" means an implementation will always trap, while "does support unaligned data access" means that sometimes it will just perform the access, and sometimes it will trap (based on non-architectural state values such as TLB state).

So results can be deterministic (that is, based on known architectural state or architectural options that are communicated via a YAML configuration file), and coild be non-deterministic (non-architectural state dependent). If the number of legal non-deterministic results is small (e.g. 2, possibly 3), we intend to configure Sail to use one behavior, and then rerun with the other behavior, and allow matches on either behavior to be considered a match.

If I understand this case correctly, there are 3 legal results:

It's not the only option that doesn't have a CSR bit or some other means of determining what it does, but this particular example is the most challenging - and one of the more important ones to implement.

scottj97 commented 2 years ago

Editing the source *.sail files, as opposed to editing a config setting in a YAML file. Since no such config system exists today, I've made dozens of source edits to match my team's implementation choices. If you intend to support all legal implementation choices via the YAML then yes you'd need a setting for this.

In this particular test case, we're doing an 8-byte store across two pages, the second of which does not have its PTE's dirty bit set. There are three legal results, depending on implementation choices. There is no nondeterministic behavior here.

Regarding nondeterminism, I'll send you email about that, since it's getting off-topic for this issue report.

allenjbaum commented 2 years ago

Those are basically the 3 cases the ACTs will know about. It either executes without trapping, does a partial execution, and then traps, or does no execution and traps. In your specific case, it may be deterministic, but some implementations might trap if the 2nd half crosses a page boundary but doesn't have a translation in the TLB, but not trap if it doesn't cross a page boundary even if the translation is not in the TLB. For others it might also depend on whether there was a cache miss or not. That is nondeterministic, because it depends on TLB state which is microarchitectural.

regarding source vs YAML: The intent is certainly to support all (well, within limits) legal implementations by configuration using the YAML files. Generally, those implementation choices depend on the value of CSR bits and their writability. That support (with those limits) is what is being added. Every CSR that has optional behavior will describe that behavior (e.g. which bits are read only, and their value). There is documentation on the schema syntax in the riscv-conf repo, and there is a prototype implementation that RIOS labs has developed.

There are a few other optional behaviors that have no CSR controls, and misalign support is at the very top of the list. IF you have a list, I'd love to see it! (beyond: we implement these extensions that don't have MISA bits). There are two other privspec 1.11 features that I'm aware of that aren't implemented: writable BigEndian, and writable XLEN. I'm hoping no one ever tries to support them, because it will be nasty - but they're easily described using the defined syntax and YAML, and if the model can define its behavior based on the value of CSR bits, then the support is almost all there (modulo the changes that have to take effect when you change those CSR bit values....)

On Fri, Oct 1, 2021 at 11:49 PM Scott Johnson @.***> wrote:

Editing the source *.sail files, as opposed to editing a config setting in a YAML file. Since no such config system exists today, I've made dozens of source edits to match my team's implementation choices. If you intend to support all legal implementation choices via the YAML then yes you'd need a setting for this.

In this particular test case, we're doing an 8-byte store across two pages, the second of which does not have its PTE's dirty bit set. There are three legal results, depending on implementation choices. There is no nondeterministic behavior here.

  • write the second PTE's dirty bit to 1, write 4 bytes to the first page, write 4 bytes to the second page (not necessarily in that order)
  • write 4 bytes to the first page, then trap because the second page's dirty bit is 0
  • write nothing; trap because the second page's dirty bit is 0

Regarding nondeterminism, I'll send you email about that, since it's getting off-topic for this issue report.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-932695440, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJVRIBZ2GNX2V4HDMSDUE2TO5ANCNFSM4M4MQK2Q . 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.

Timmmm commented 5 months ago

I am going to fix this.

For memory reads I think it isn't too bad to solve. I will just change the code to a single mem_read() that takes a virtual address, and does virtual address translation and the memory read. For reads I can't see any reason to split up address translation and physical memory access.

Putting everything in one function means it is very easy to handle split accesses, and also means the virtual address is readily accessible for logging which is something we require for our verif system.

For writes, that doesn't quite work because of the requirement for the write value to be calculated after mem_write_ea() but before mem_write_value(). In most languages you could pass a get_value() callback that would calculate the write value, but Sail doesn't support first class functions so that isn't an option.

My proposal is to do the same as read - have a single mem_write() that takes a virtual address. However split it into two functions with an opaque type passed between them:

let opaque_data = mem_write_prepare(vaddr, width, etc.);
let write_value = X(rs1);
mem_write_commit(opaque_data, write_value);

I think this will work and be fairly elegant. It also allows you to fairly easily modify the code that it does partial writes. I will implement the case that does both translations up front though, since that's what the chip I'm working on does and I think it is the simplest & most likely case in most implementations.

If anyone thinks this is a bad idea let me know!

allenjbaum commented 5 months ago

Note that the spec doesn't require that the write to the 2 halves appear in a particular order, nor that an exception caused by one or the other, prevents the write of the other half (likely order dependent, but could be always prevent the write). nor if both halves take exceptions, which one is taken (also likely order dependent, but could be report the one with higher priority and write noter).

We need to have programmable controls for those cases (and we'll figure out how to set them later when the configuration support comes up)

On Mon, Mar 11, 2024 at 3:34 PM Tim Hutt @.***> wrote:

I am going to fix this.

For memory reads I think it isn't too bad to solve. I will just change the code to a single mem_read() that takes a virtual address, and does virtual address translation and the memory read. For reads I can't see any reason to split up address translation and physical memory access.

Putting everything in one function means it is very easy to handle split accesses, and also means the virtual address is readily accessible for logging which is something we require for our verif system.

For writes, that doesn't quite work because of the requirement for the write value to be calculated after mem_write_ea() but before mem_write_value(). In most languages you could pass a get_value() callback that would calculate the write value, but Sail doesn't support first class functions so that isn't an option.

My proposal is to do the same as read - have a single mem_write() that takes a virtual address. However split it into two functions with an opaque type passed between them:

let opaque_data = mem_write_prepare(vaddr, width, etc.); let write_value = X(rs1); mem_write_commit(opaque_data, write_value);

I think this will work and be fairly elegant. It also allows you to fairly easily modify the code that it does partial writes. I will implement the case that does both translations up front though, since that's what the chip I'm working on does and I think it is the simplest & most likely case in most implementations.

If anyone thinks this is a bad idea let me know!

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1989561127, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJQDHT4P47JS4WYEU7TYXYWOHAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJYHE2TMMJRGI3Q . You are receiving this because you commented.Message ID: @.***>

PeterSewell commented 5 months ago

On Tue, 12 Mar 2024 at 06:15, Allen Baum @.***> wrote:

Note that the spec doesn't require that the write to the 2 halves appear in a particular order, nor that an exception caused by one or the other, prevents the write of the other half (likely order dependent, but could be always prevent the write). nor if both halves take exceptions, which one is taken (also likely order dependent, but could be report the one with higher priority and write noter).

We plan to handle this with a local PAR construct in Sail (at some point...)

We need to have programmable controls for those cases (and we'll figure out how to set them later when the configuration support comes up)

On Mon, Mar 11, 2024 at 3:34 PM Tim Hutt @.***> wrote:

I am going to fix this.

For memory reads I think it isn't too bad to solve. I will just change the code to a single mem_read() that takes a virtual address, and does virtual address translation and the memory read. For reads I can't see any reason to split up address translation and physical memory access.

Putting everything in one function means it is very easy to handle split accesses, and also means the virtual address is readily accessible for logging which is something we require for our verif system.

For writes, that doesn't quite work because of the requirement for the write value to be calculated after mem_write_ea() but before mem_write_value(). In most languages you could pass a get_value() callback that would calculate the write value, but Sail doesn't support first class functions so that isn't an option.

My proposal is to do the same as read - have a single mem_write() that takes a virtual address. However split it into two functions with an opaque type passed between them:

let opaque_data = mem_write_prepare(vaddr, width, etc.); let write_value = X(rs1); mem_write_commit(opaque_data, write_value);

I think this will work and be fairly elegant. It also allows you to fairly easily modify the code that it does partial writes. I will implement the case that does both translations up front though, since that's what the chip I'm working on does and I think it is the simplest & most likely case in most implementations.

If anyone thinks this is a bad idea let me know!

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1989561127,

or unsubscribe < https://github.com/notifications/unsubscribe-auth/AHPXVJQDHT4P47JS4WYEU7TYXYWOHAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJYHE2TMMJRGI3Q>

. You are receiving this because you commented.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1990782018, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZSHLMFYDZ67O7BQBWTYX2MO3AVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJZGA3TQMRQGE4A . You are receiving this because you commented.Message ID: @.***>

allenjbaum commented 5 months ago

I'm not familiar with the PAR acronym, or its use in this context (I'm guessing it has something to do with parallelism?)

On Mon, Mar 11, 2024 at 11:33 PM Peter Sewell @.***> wrote:

On Tue, 12 Mar 2024 at 06:15, Allen Baum @.***> wrote:

Note that the spec doesn't require that the write to the 2 halves appear in a particular order, nor that an exception caused by one or the other, prevents the write of the other half (likely order dependent, but could be always prevent the write). nor if both halves take exceptions, which one is taken (also likely order dependent, but could be report the one with higher priority and write noter).

We plan to handle this with a local PAR construct in Sail (at some point...)

We need to have programmable controls for those cases (and we'll figure out how to set them later when the configuration support comes up)

On Mon, Mar 11, 2024 at 3:34 PM Tim Hutt @.***> wrote:

I am going to fix this.

For memory reads I think it isn't too bad to solve. I will just change the code to a single mem_read() that takes a virtual address, and does virtual address translation and the memory read. For reads I can't see any reason to split up address translation and physical memory access.

Putting everything in one function means it is very easy to handle split accesses, and also means the virtual address is readily accessible for logging which is something we require for our verif system.

For writes, that doesn't quite work because of the requirement for the write value to be calculated after mem_write_ea() but before mem_write_value(). In most languages you could pass a get_value() callback that would calculate the write value, but Sail doesn't support first class functions so that isn't an option.

My proposal is to do the same as read - have a single mem_write() that takes a virtual address. However split it into two functions with an opaque type passed between them:

let opaque_data = mem_write_prepare(vaddr, width, etc.); let write_value = X(rs1); mem_write_commit(opaque_data, write_value);

I think this will work and be fairly elegant. It also allows you to fairly easily modify the code that it does partial writes. I will implement the case that does both translations up front though, since that's what the chip I'm working on does and I think it is the simplest & most likely case in most implementations.

If anyone thinks this is a bad idea let me know!

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1989561127,

or unsubscribe <

https://github.com/notifications/unsubscribe-auth/AHPXVJQDHT4P47JS4WYEU7TYXYWOHAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJYHE2TMMJRGI3Q>

. You are receiving this because you commented.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1990782018,

or unsubscribe < https://github.com/notifications/unsubscribe-auth/ABFMZZSHLMFYDZ67O7BQBWTYX2MO3AVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJZGA3TQMRQGE4A>

. You are receiving this because you commented.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1990848345, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJQ2PSNPAL44Y6YFBUDYX2OTHAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJZGA4DIOBTGQ2Q . You are receiving this because you commented.Message ID: @.***>

PeterSewell commented 5 months ago

y

On Tue, 12 Mar 2024 at 06:36, Allen Baum @.***> wrote:

I'm not familiar with the PAR acronym, or its use in this context (I'm guessing it has something to do with parallelism?)

On Mon, Mar 11, 2024 at 11:33 PM Peter Sewell @.***> wrote:

On Tue, 12 Mar 2024 at 06:15, Allen Baum @.***> wrote:

Note that the spec doesn't require that the write to the 2 halves appear in a particular order, nor that an exception caused by one or the other, prevents the write of the other half (likely order dependent, but could be always prevent the write). nor if both halves take exceptions, which one is taken (also likely order dependent, but could be report the one with higher priority and write noter).

We plan to handle this with a local PAR construct in Sail (at some point...)

We need to have programmable controls for those cases (and we'll figure out how to set them later when the configuration support comes up)

On Mon, Mar 11, 2024 at 3:34 PM Tim Hutt @.***> wrote:

I am going to fix this.

For memory reads I think it isn't too bad to solve. I will just change the code to a single mem_read() that takes a virtual address, and does virtual address translation and the memory read. For reads I can't see any reason to split up address translation and physical memory access.

Putting everything in one function means it is very easy to handle split accesses, and also means the virtual address is readily accessible for logging which is something we require for our verif system.

For writes, that doesn't quite work because of the requirement for the write value to be calculated after mem_write_ea() but before mem_write_value(). In most languages you could pass a get_value() callback that would calculate the write value, but Sail doesn't support first class functions so that isn't an option.

My proposal is to do the same as read - have a single mem_write() that takes a virtual address. However split it into two functions with an opaque type passed between them:

let opaque_data = mem_write_prepare(vaddr, width, etc.); let write_value = X(rs1); mem_write_commit(opaque_data, write_value);

I think this will work and be fairly elegant. It also allows you to fairly easily modify the code that it does partial writes. I will implement the case that does both translations up front though, since that's what the chip I'm working on does and I think it is the simplest & most likely case in most implementations.

If anyone thinks this is a bad idea let me know!

— Reply to this email directly, view it on GitHub < https://github.com/riscv/sail-riscv/issues/49#issuecomment-1989561127>,

or unsubscribe <

https://github.com/notifications/unsubscribe-auth/AHPXVJQDHT4P47JS4WYEU7TYXYWOHAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJYHE2TMMJRGI3Q>

. You are receiving this because you commented.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1990782018,

or unsubscribe <

https://github.com/notifications/unsubscribe-auth/ABFMZZSHLMFYDZ67O7BQBWTYX2MO3AVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJZGA3TQMRQGE4A>

. You are receiving this because you commented.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1990848345,

or unsubscribe < https://github.com/notifications/unsubscribe-auth/AHPXVJQ2PSNPAL44Y6YFBUDYX2OTHAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJZGA4DIOBTGQ2Q>

. You are receiving this because you commented.Message ID: @.***>

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1990859057, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZWM5PWNQHWFKPFVHL3YX2PALAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJZGA4DKOJQGU3Q . You are receiving this because you commented.Message ID: @.***>

Timmmm commented 5 months ago

Note that the spec doesn't require that the write to the 2 halves appear in a particular order, nor that an exception caused by one or the other, prevents the write of the other half...

Yep, and consolidating all of this behaviour into one read and two write functions will make it much easier to support all of those behaviours, and make them configurable eventually (though I don't plan to do that at this point).

a local PAR construct in Sail

Interesting, so you'll do something like:

let paddr0, paddr1 = par(
   translateAddr(...),
   translateAddr(...),
);

and it will do them sequentially in the C/OCaml versions, but in "any order" in the formal version?

PeterSewell commented 5 months ago

On Tue, 12 Mar 2024 at 10:35, Tim Hutt @.***> wrote:

Note that the spec doesn't require that the write to the 2 halves appear in a particular order, nor that an exception caused by one or the other, prevents the write of the other half...

Yep, and consolidating all of this behaviour into one read and two write functions will make it much easier to support all of those behaviours, and make them configurable eventually (though I don't plan to do that at this point).

a local PAR construct in Sail

Interesting, so you'll do something like:

let paddr0, paddr1 = par( translateAddr(...), translateAddr(...), );

and it will do them sequentially in the C/OCaml versions, but in "any order" in the formal version?

y. One needs the two translate-and-write's to be unordered, and to take care with fault handling and any register write-backs, but that all seems doable.

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-1991320614, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABFMZZW7N4OJW2EFGKIU5IDYX3K6HAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TCOJZGEZTEMBWGE2A . You are receiving this because you commented.Message ID: @.***>

Timmmm commented 5 months ago

One other question @PeterSewell - why does mem_write_ea() do an alignment check? I still don't really understand the exact conditions under which it is expected to be called.

Btw - an extra complication with this that we discovered - if your two physical memory accesses happen to be in two different PMP regions then it must cause an access fault. It unfortunately means you can't treat the split access as two independent normal accesses.

allenjbaum commented 5 months ago

Why can't you treat it as two independent accesses? I have looked at this extensively, and as far as I can tell an implementation can

If it is a misaligned store, it can store the first half that executes, and trap with an exception on the second half. A misaligned store where both halves fail can report either one, regardless of the priorities of the cause in each Sail will need to be handle of of these legal configurations by being passed the order of operations, whether it should be treated as one operation or two, and exception priority order.

On Mon, Mar 25, 2024 at 10:01 AM Tim Hutt @.***> wrote:

One other question @PeterSewell https://github.com/PeterSewell - why does mem_write_ea() do an alignment check? I still don't really understand the exact conditions under which it is expected to be called.

Btw - an extra complication with this that we discovered - if your two physical memory accesses happen to be in two different PMP regions then it must cause an access fault. It unfortunately means you can't treat the split access as two independent normal accesses.

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-2018479864, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJVJN4STUWJ23JOW3FTY2BJ77AVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TEMBRHA2DOOJYGY2A . You are receiving this because you commented.Message ID: @.***>

rsnikhil commented 5 months ago

For writes, that doesn't quite work because of the requirement for the write value to be calculated after mem_write_ea() but before mem_write_value().

Why? Can’t the write-value calculation (just a register read) be done concurrently, or even before ea calculation?

Timmmm commented 5 months ago

Why can't you treat it as two independent accesses?

Probably isn't clear without seeing my code but the PMP checks were being done within the functions that do the access. It's effectively like this (pseudocode):

function vmem_read(vaddr : xlenbits, ...) = {
   ...
   let (paddr0, paddr1) = translate(vaddr);
   let part0 = mem_read(paddr0, width0);
   let part1 = mem_read(paddr1, width1);
   part0 @ part1
}

function mem_read(paddr : xlenbits, width : ...) = {
   let pmp_exc = pmp_check(paddr, width);
   ...
}

That's wrong because the PMP check can pass for each part separately, but if they happen to be accesses to different PMP regions then the vmem_read() should fail with an access fault. Even if the PMP checks for each part are ok.

Why? Can’t the write-value calculation (just a register read) be done concurrently, or even before ea calculation?

For the sequential model it makes no difference at all since mem_write_ea() doesn't actually do anything. It's some requirement for the concurrency model which I don't fully understand (see this discussion). I think it would be really worthwhile to get some detailed documentation around that because otherwise it's going to be constantly broken by people editing the code who are only using the emulator, which I think is most of us.

allenjbaum commented 5 months ago

I interpret that to mean that [a misaligned load or store] could be treated as 2 different accesses, but your code isn't doing that, which is a separate issue From a spec point of view, it is allowed to be completely separate - or not

On Mon, Mar 25, 2024 at 12:36 PM Tim Hutt @.***> wrote:

Why can't you treat it as two independent accesses?

Probably isn't clear without seeing my code but the PMP checks were being done within the functions that do the access. It's effectively like this (pseudocode):

function vmem_read(vaddr : xlenbits, ...) = { ... let (paddr0, paddr1) = translate(vaddr); let part0 = mem_read(paddr0, width0); let part1 = mem_read(paddr1, width1); part0 @ part1 }

function mem_read(paddr : xlenbits, width : ...) = { let pmp_exc = pmp_check(paddr, width); ... }

That's wrong because the PMP check can pass for each part separately, but if they happen to be accesses to different PMP regions then the vmem_read() should fail with an access fault. Even if the PMP checks for each part are ok.

Why? Can’t the write-value calculation (just a register read) be done concurrently, or even before ea calculation?

For the sequential model it makes no difference at all since mem_write_ea() doesn't actually do anything. It's some requirement for the concurrency model which I don't fully understand (see this discussion https://github.com/riscv/sail-riscv/discussions/392). I think it would be really worthwhile to get some detailed documentation around that because otherwise it's going to be constantly broken by people editing the code who are only using the emulator, which I think is most of us.

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-2018766159, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJXQCDFCQF2ZPVJRNXTY2B4ETAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TEMBRHA3TMNRRGU4Q . You are receiving this because you commented.Message ID: @.***>

Timmmm commented 5 months ago

I think we're talking about different things. Implementations are allowed to do the actual memory writes (after PMP checks) separately, but they can't do independent PMP checks for each part as if they were two separate store instructions.

Here's the relevant bit of the spec:

The lowest-numbered PMP entry that matches any byte of an access determines whether that access succeeds or fails. The matching PMP entry must match all bytes of an access, or the access fails, irrespective of the L, R, W, and X bits.

Not unsolvable but I'm going to have to do even more refactoring... :-/

scottj97 commented 5 months ago

I think we're talking about different things. Implementations are allowed to do the actual memory writes (after PMP checks) separately, but they can't do independent PMP checks for each part as if they were two separate store instructions.

Here's the relevant bit of the spec:

The lowest-numbered PMP entry that matches any byte of an access determines whether that access succeeds or fails. The matching PMP entry must match all bytes of an access, or the access fails, irrespective of the L, R, W, and X bits.

Not unsolvable but I'm going to have to do even more refactoring... :-/

Allen is correct. I forget where I learned this but it’s acceptable in RISC-V for an implementation to split up a single load/store into multiple accesses.

allenjbaum commented 5 months ago

The critical wording is: The lowest-numbered PMP entry that matches any byte of an access

If an op splits a misaligned load or store into separate accesses, they are (as I understand it) treated separately - and "separateness" is an implementation defined parameter (that has to be passed to Sail

That means even if one half of a request matches a PMP entry, and the other a different PMP entry, if both requests don't otherwise cause exceptions, each is allowed to proceed.

I think this turns out to be necessary for emulation, which might execute with byte-by-byte loads and stores (with MPRV set appropriately) I will be getting confirmation of this...

On Mon, Mar 25, 2024 at 3:55 PM Scott Johnson @.***> wrote:

I think we're talking about different things. Implementations are allowed to do the actual memory writes (after PMP checks) separately, but they can't do independent PMP checks for each part as if they were two separate store instructions.

Here's the relevant bit of the spec:

The lowest-numbered PMP entry that matches any byte of an access determines whether that access succeeds or fails. The matching PMP entry must match all bytes of an access, or the access fails, irrespective of the L, R, W, and X bits.

Not unsolvable but I'm going to have to do even more refactoring... :-/

Allen is correct. I forget where I learned this but it’s acceptable in RISC-V for an implementation to split up a single load/store into multiple accesses.

— Reply to this email directly, view it on GitHub https://github.com/riscv/sail-riscv/issues/49#issuecomment-2019059757, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJUWGNSREOXJ2TUAEV3Y2CTNBAVCNFSM4M4MQK22U5DIOJSWCZC7NNSXTN2JONZXKZKDN5WW2ZLOOQ5TEMBRHEYDKOJXGU3Q . You are receiving this because you commented.Message ID: @.***>

Timmmm commented 5 months ago

Oh yeah you're right... I should have read slightly further!

Note that a single instruction may generate multiple accesses, which may not be mutually atomic. An access-fault exception is generated if at least one access generated by an instruction fails, though other accesses generated by that instruction may succeed with visible side effects. Notably, instructions that reference virtual memory are decomposed into multiple accesses

That's a relief!

Alasdair commented 3 months ago

I had a go at refactoring the LOAD instruction:

function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
  let offset : xlenbits = sign_extend(imm);
  /* Get the address, X(rs1) + offset.
     Some extensions perform additional checks on address validity. */
  match ext_data_get_addr(rs1, offset, Read(Data), width) {
    Ext_DataAddr_Error(e)  => {
      ext_handle_data_check_error(e);
      RETIRE_FAIL
    },

    Ext_DataAddr_OK(vaddr) => {
      if check_misaligned(vaddr, width) then {
         handle_mem_exception(vaddr, E_Load_Addr_Align());
         return RETIRE_FAIL
      };

      let bytes = width_bytes(width);
      if bytes > sizeof(xlen_bytes) then {
         report_invalid_width(__FILE__, __LINE__, width, "load")
      } else {
         let (n, bytes) = misalignment(vaddr, bytes);
         var data = zeros(8 * n * bytes);

         foreach (i from 0 to (n - 1)) {
           let vaddr = vaddr + (i * bytes);
           match translateAddr(vaddr, Read(Data)) {
             TR_Failure(e, _) => {
               handle_mem_exception(vaddr, e);
               return RETIRE_FAIL
             },

             TR_Address(paddr, _) => match mem_read(Read(Data), paddr, bytes, aq, rl, false) {
               MemValue(v) => {
                 data[(8 * (i + 1) * bytes) - 1 .. 8 * i * bytes] = v
               },
               MemException(e) => {
                 handle_mem_exception(vaddr, e);
                 return RETIRE_FAIL
               }
             }
           }
         };

         X(rd) = if is_unsigned then zero_extend(data) else sign_extend(data);

         RETIRE_SUCCESS
      }
    }
  }
}

the line:

let (n, X) = misalignment(vaddr, Y);

splits a X bytes load into n times Y bytes load (if vaddr is aligned, n is always 1). This behaviour could be configurable for implementations that always want to split misaligned accesses into byte accesses, but I just made it split into the largest aligned width.

For the linked test the offending instruction now gives:

[128] [S]: 0x0000000080002096 (0x0002B303) ld t1, 0x0(t0)
mem[R,0x0000000081000740] -> 0x0000000020400C01
mem[R,0x00000000810035D8] -> 0x0000000020401001
mem[R,0x0000000081004EF0] -> 0x0000000020000CCF
mem[R,0x0000000080003FFC] -> 0x80670052
mem[R,0x0000000081000740] -> 0x0000000020400C01
mem[R,0x00000000810035D8] -> 0x0000000020401001
mem[R,0x0000000081004EF8] -> 0x000000002000140F
trapping from S to M to handle load-page-fault
handling exc#0x0D at priv M with tval 0x0000003A177DF000
CSR mstatus <- 0x0000000A00000800
mem[X,0x0000000080002104] -> 0x1173
mem[X,0x0000000080002106] -> 0x3401