Clarification on determinism of WLRL and WARL #789
Labels
Comments
|
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
<#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>.
|
|
Yes. I think this is legal: |
|
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
<#789 (comment)>,
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>.
|
I find my example to be pathological and wonder if this is what the specification intends.
Yes. Should we care about this, or is this so remote an edge case that we can ignore it? |
|
“Illegal written value” is singular - if it were referring to the history of writes, it would need to be plural. |
|
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
|
|
P.S. My last post was using the WARL definition. But I also agree with
Andrew regarding the WLRL situation.
Greg
|
|
It could be argued that this depends deterministically on the last written illegal value. In contrast, this does not: |
|
See also #520 |
|
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
<#789 (comment)>,
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>.
|
|
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
> <#789 (comment)>,
> 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>.
>
>
|
|
Revisiting this a few years later, we're affirming that the OP's interpretation is correct, but the text doesn't need to be clarified, because "write" being singular implies "most recent write". |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The file
priv-csrs.texcontains the following line twice(in Lines 454 and 471). I suggest to replace them by
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).
The text was updated successfully, but these errors were encountered: