riscv / riscv-isa-manual

RISC-V Instruction Set Manual
https://riscv.org/
Creative Commons Attribution 4.0 International
3.57k stars 615 forks source link

Clarification on determinism of WLRL and WARL #789

Open martinberger opened 2 years ago

martinberger commented 2 years ago

The file priv-csrs.tex contains the following line twice

deterministically depend on the illegal written value

(in Lines 454 and 471). I suggest to replace them by

deterministically depend on the last illegal written value

Why? Because more than one illegal values might be written, and one might otherwise ask if the determinism depends on the history of all previous illegal values. I think this latter interpretation is not meant, and adding "last" would clarify this. (Otherwise make a corresponding change).

allenjbaum commented 2 years ago

You left out bits that I think make that redundant: "Implementations can return arbitrary bit patterns on the read of a WLRL field when the last write was of an illegal value, but the value returned should deterministically depend on the illegal written value and the value of the field prior to the write." for WLRL So that one should already be covered. Similarly for WARL "Implementations can return any legal value on the read of a WARL field when the last write was of an illegal value, but the legal value returned should deterministically depend on the illegal written value and the architectural state of the hart." for WARL which doesn't make if clear it is architectural state is prior to the write.

This may well be an English thing, in that the context of "the illegally written value" is implied to be the one mentioned in the first part of the sentence ("last write"). If it read "an illegal written value", then it would be more ambiguous, but using "the" (to me, at least) implies a specific write, and that would be the one earlier in the sentence.

Oddly, that full definition could be used to allow an earlier illegal write to be the one that matters, since that earlier write could then be part of the hart architectural state. So an implementation could effectively ignore the write of an illegal value if the state is already illegal, but continue to map that illegal state to a legal read value That (rather twisted, in my opinion) implementation is legal.

On Thu, Dec 2, 2021 at 1:47 AM Martin Berger @.***> wrote:

The file priv-csrs.tex contains the following line twice

deterministically depend on the illegal written value

(in Lines 454 and 471). I suggest to replace this by

deterministically depend on the last illegal written value

Why? Because more than one illegal values might be written, and one might otherwise ask if the determinism depends on the history of all previous illegal values. I think this latter interpretation is not meant, and adding "last" would clarify this. (Otherwise make an corresponding change).

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/riscv/riscv-isa-manual/issues/789, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHPXVJVK34MA37XFDSIZCRDUO46EHANCNFSM5JGU3CDQ . 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.

martinberger commented 2 years ago

Yes. I think this is legal:

write 17  // assuming 17 is illegal
read      // get 3
write 17  // still illegal  
read      // get 4
allenjbaum commented 2 years ago

That's not the case I was thinking of, but I think you're right.

write 17 // assuming 17 is illegal read // get 3 write 16 // still illegal read // get 3

while

write 16 // assuming 17 is illegal read // get 4 write 17 // still illegal read // get 4

and

write 16 // assuming 17 is illegal read // get 4 write 4write 17 // still illegal read // get 3

are also possible. So writing the same or different illegal value might map to the same or different legal value

What is possible depends also on whether the illegal value is mapped to legal when written or when read. The state of the hart is different in those two cases, and my pair of examples above are not possible if the mapping is on the write (so the actual state is always legal, not just the value read)

This makes it difficult to write architectural tests, because if we can't replicate this weird but legal behavior, we can't replicate it in Sail, and then it and DUT will diverge - so we have to avoid testing illegal writes (except to the extent that they map to something legal). And we can't do that because we don't know when we write a test what will be legal or not.

That's OK if the mapping is one of our well behaved cases, (i.e. ignore the write, or sign extend the write, which I encourage everyone to use in their designs) but if they're not they're likely to fail an arch-test.

On Thu, Dec 2, 2021 at 9:32 AM Martin Berger @.***> wrote:

Yes. I think this is legal:

write 17 // assuming 17 is illegal read // get 3 write 17 // still illegal read // get 4

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

martinberger commented 2 years ago

That's not the case I was thinking of, but I think you're right.

I find my example to be pathological and wonder if this is what the specification intends.

difficult to write architectural tests,

Yes. Should we care about this, or is this so remote an edge case that we can ignore it?

aswaterman commented 2 years ago

“Illegal written value” is singular - if it were referring to the history of writes, it would need to be plural.

gfavor commented 2 years ago

On Thu, Dec 2, 2021 at 9:32 AM Martin Berger @.***> wrote:

Yes. I think this is legal:

write 17 // assuming 17 is illegal read // get 3 write 17 // still illegal read // get 4

This example would seem to be illegal given the following definition from the Priv spec: The legal value returned should deterministically depend on the illegal written value and the architectural state of the hart.

In other words, barring some asynchronous event causing an effectively random unpredictable arch state change, the above example shows nothing that would change surrounding arch state that could then cause a different deterministic mapping on/after the second write of the same value.

Greg

gfavor commented 2 years ago

P.S. My last post was using the WARL definition. But I also agree with Andrew regarding the WLRL situation.

Greg

martinberger commented 2 years ago

It could be argued that this

write 17  // assuming 17 is illegal
read       // get 3
read       // get 3
...
read       // get 3
write 17  // still illegal
read       // get 4
read       // get 4
...
read       // get 4

depends deterministically on the last written illegal value. In contrast, this does not:

write 17  // assuming 17 is illegal
read       // get 3
read       // get 17
write 17  // still illegal
read       // get 4
read       // get 99
pdonahue-ventana commented 2 years ago

See also https://github.com/riscv/riscv-isa-manual/issues/520

allenjbaum commented 2 years ago

That this is entirely legal was exactly my point for WARL. Suppose the CSR contains a legal value that is not 3, say it is 2 Writing the illegal 17 does one of two things: a. it writes 2 into the field, or b. it writes 17 into the field that gets output mapped to 2. So f(wtval=17,currstate=2) =3 On the second write, same thing, but this time the output is f(17,3) or f(17,17) =4, and not f(17,5) Now, if you wrote it a third time with 17 , then you'd either get f(17,4) or f(17,17) (assuming no intervening writes) depending on whether approach a) or b) was implemented. If it approach a) then f(wtval=17, currval=currval+1) then continuously writing illegal values would cause the field to increment until it hit a legal write value .

If you take the sane approach, which is to inhibit illegal writes (so f(wrtval,currstate) = currstate), then it is very understandable, consistent, less power hungry, and testable

On Thu, Dec 2, 2021 at 12:11 PM gfavor @.***> wrote:

On Thu, Dec 2, 2021 at 9:32 AM Martin Berger @.***> wrote:

Yes. I think this is legal:

write 17 // assuming 17 is illegal read // get 3 write 17 // still illegal read // get 4

This example would seem to be illegal given the following definition from the Priv spec: The legal value returned should deterministically depend on the illegal written value and the architectural state of the hart.

In other words, barring some asynchronous event causing an effectively random unpredictable arch state change, the above example shows nothing that would change surrounding arch state that could then cause a different deterministic mapping on/after the second write of the same value.

Greg

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

allenjbaum commented 2 years ago

oops, typo; that should have said a) it writes 3 into the field

On Thu, Dec 2, 2021 at 5:30 PM Allen Baum @.***> wrote:

That this is entirely legal was exactly my point for WARL. Suppose the CSR contains a legal value that is not 3, say it is 2 Writing the illegal 17 does one of two things: a. it writes 2 into the field, or b. it writes 17 into the field that gets output mapped to 2. So f(wtval=17,currstate=2) =3 On the second write, same thing, but this time the output is f(17,3) or f(17,17) =4, and not f(17,5) Now, if you wrote it a third time with 17 , then you'd either get f(17,4) or f(17,17) (assuming no intervening writes) depending on whether approach a) or b) was implemented. If it approach a) then f(wtval=17, currval=currval+1) then continuously writing illegal values would cause the field to increment until it hit a legal write value .

If you take the sane approach, which is to inhibit illegal writes (so f(wrtval,currstate) = currstate), then it is very understandable, consistent, less power hungry, and testable - and that's what I'm trying to encourage. (require, even)

On Thu, Dec 2, 2021 at 12:11 PM gfavor @.***> wrote:

On Thu, Dec 2, 2021 at 9:32 AM Martin Berger @.***> wrote:

Yes. I think this is legal:

write 17 // assuming 17 is illegal read // get 3 write 17 // still illegal read // get 4

This example would seem to be illegal given the following definition from the Priv spec: The legal value returned should deterministically depend on the illegal written value and the architectural state of the hart.

In other words, barring some asynchronous event causing an effectively random unpredictable arch state change, the above example shows nothing that would change surrounding arch state that could then cause a different deterministic mapping on/after the second write of the same value.

Greg

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