RISC-V Memory Consistency Model Update

[Daniel Lustig]

Hi all,

The RISC-V memory consistency model task group is releasing the latest
version of our specification for public review. This update has been
merged into the public upstream riscv-isa-manual repo, and it is also
attached here as a PDF.

https://github.com/riscv/riscv-isa-manual

The memory model is specified in what is now Chapter 6 plus two
appendices, but we did make minor changes to the base ISA and the "A"
extension as well. We also defined two new extensions: "Zam" for
misaligned AMOs in Chapter 20, and "Ztso" for Total Store Ordering in
Chapter 21, to separate out and standardize some optional features
that were previously defined inline as parts of other modules.

This public release also starts the Foundation's 45-day ratification
clock. The ratification process is described at the following link:
https://workspace.riscv.org/higherlogic/ws/public/workgroup?wg_abbrev=tech

We welcome any feedback you might have, from small typo corrections to
major issues. Feedback or questions can be sent as a reply to this
message on isa-dev, to me directly, or as a pull request or issue on
the riscv-isa-manual GitHub repo.

We will also have a tutorial, a presentation, and the normal members-
only meeting at the RISC-V Workshop in Barcelona next week. We would
be happy to take any questions or any in-person feedback there as
well.

Thanks,
Dan

-----------------------------------------------------------------------------------
This email message is for the sole use of the intended recipient(s) and may contain
confidential information. Any unauthorized review, use, disclosure or distribution
is prohibited. If you are not the intended recipient, please contact the sender by
reply email and destroy all copies of the original message.
-----------------------------------------------------------------------------------

[Luke Kenneth Casson Leighton]

On Thu, May 3, 2018 at 2:58 AM, Daniel Lustig <dlu...@nvidia.com> wrote:
> Hi all,
>
> The RISC-V memory consistency model task group is releasing the latest
> version of our specification for public review. This update has been
> merged into the public upstream riscv-isa-manual repo, and it is also
> attached here as a PDF.
>
> https://github.com/riscv/riscv-isa-manual

thank you daniel, much appreciated, particularly the clarification on
misaligned atomics.

do you have the git commit reference handily available so that people
may easily identify precisely what was added (or taken away)? the two
chapters themselves are easily identified, however locations where the
wording was changed (if it was changed) within the rest of the 237
page manual are much harder to track down. the git commit
reference(s) will help people to help you, with minimal effort
expended.

l.

[Andrew Waterman]

https://github.com/riscv/riscv-isa-manual/commit/b875fe417948635ed68b9644ffdf718cb343a81a

 

l.

--
You received this message because you are subscribed to the Google Groups "RISC-V ISA Dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to isa-dev+unsubscribe@groups.riscv.org.
To post to this group, send email to isa...@groups.riscv.org.
Visit this group at https://groups.google.com/a/groups.riscv.org/group/isa-dev/.
To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/isa-dev/CAPweEDwo5vvtWERmEG%3DVGXHJk%3D%3DSV1GRDyiNdfXiAQ1CuVN6bw%40mail.gmail.com.

[Luke Kenneth Casson Leighton]

On Sun, May 6, 2018 at 11:30 AM, Andrew Waterman
<wate...@eecs.berkeley.edu> wrote:

> https://github.com/riscv/riscv-isa-manual/commit/b875fe417948635ed68b9644ffdf718cb343a81a

fantastic, thank you andrew

-The execution environment may require that the address held in {\em rs1} be
+For AMOs, the A extension requires that the address held in {\em rs1} be

clear language! no either/or. whew. either/or is a pain for proofs.

+64-bit words and four-byte aligned for 32-bit words). If the address is
+not naturally aligned, a misaligned address exception will be generated.
+The ``Zam'' extension, described in Chapter~\ref{sec:zam}, relaxes this
+requirement and specifies the semantics of misaligned AMOs.

how about:

+64-bit words and four-byte aligned for 32-bit words). If the address is
+not naturally aligned, and the ``Zam'' extension is not enabled,
+ a misaligned address exception will be generated.
+ The requirements and semantics of misaligned AMOs when the ``Zam''
+ extension is enabled are specifically covered by Chapter~\ref{sec:zam}.

here:

-preceding the AMO in this RISC-V hart.
+preceding the AMO in this RISC-V hart. Setting both the {\em aq} and the {\em
+rl} bit on an AMO makes the it sequence sequentially consistent, meaning that
+it cannot be reordered with earlier or later memory operations from the same
+hart.

"makes the it sequence"? that should probably be "makes the sequence"?

src/machine.tex

+Support for misaligned LR/SC sequences is not currently standardized.
+

is that to _be_ standardised (ever)? are implementors prevented and
prohibited *from* supporting (non-standardised) misligned LR/SC
sequences? if not, that would result in.. non-standard *differing*
implementations, and they could end up getting it "wrong" (not
technically, but wrong as in "they implemented something different
from a future standard covering this specific area"). my feeling is:
it should be made absolutely clear that it's prohibited, and that
anyone wishing to do so should approach the RISC-V Foundation to start
the standardisation process.

standards really really must not let anyone have *any* wiggle-room
unless it has no impact i.e. there is only forward-interaction within
the "uncontrolled" (out-of-scope) state diagram. if there *is* any
interaction of state it *must* be covered by the standard i.e. must
*not* link or combine with another "uncontrolled" piece of state
(hardware or software) that is also out-of-scope for the standard. i
was beginning to formulate this clearly in another thread.

l.

[Andrew Waterman]

On Sun, May 6, 2018 at 6:26 PM, Luke Kenneth Casson Leighton <lk...@lkcl.net> wrote:

On Sun, May 6, 2018 at 11:30 AM, Andrew Waterman
<wate...@eecs.berkeley.edu> wrote:

> https://github.com/riscv/riscv-isa-manual/commit/b875fe417948635ed68b9644ffdf718cb343a81a

 fantastic, thank you andrew

-The execution environment may require that the address held in {\em rs1} be
+For AMOs, the A extension requires that the address held in {\em rs1} be

clear language!  no either/or.  whew.  either/or is a pain for proofs.

+64-bit words and four-byte aligned for 32-bit words). If the address is
+not naturally aligned, a misaligned address exception will be generated.
+The ``Zam'' extension, described in Chapter~\ref{sec:zam}, relaxes this
+requirement and specifies the semantics of misaligned AMOs.

how about:

+64-bit words and four-byte aligned for 32-bit words). If the address is
+not naturally aligned, and the ``Zam'' extension is not enabled,
+ a misaligned address exception will be generated.
+ The requirements and semantics of misaligned AMOs when the ``Zam''
+ extension is enabled are specifically covered by Chapter~\ref{sec:zam}.

I actually prefer the way it's currently expressed.

 

here:

-preceding the AMO in this RISC-V hart.
+preceding the AMO in this RISC-V hart. Setting both the {\em aq} and the {\em
+rl} bit on an AMO makes the it sequence sequentially consistent, meaning that
+it cannot be reordered with earlier or later memory operations from the same
+hart.

"makes the it sequence"?  that should probably be "makes the sequence"?

Yes, thanks.

src/machine.tex

+Support for misaligned LR/SC sequences is not currently standardized.
+

is that to _be_ standardised (ever)?  are implementors prevented and
prohibited *from* supporting (non-standardised) misligned LR/SC
sequences?  if not, that would result in.. non-standard *differing*
implementations, and they could end up getting it "wrong" (not
technically, but wrong as in "they implemented something different
from a future standard covering this specific area").  my feeling is:
it should be made absolutely clear that it's prohibited, and that
anyone wishing to do so should approach the RISC-V Foundation to start
the standardisation process.

standards really really must not let anyone have *any* wiggle-room
unless it has no impact i.e. there is only forward-interaction within
the "uncontrolled" (out-of-scope) state diagram.  if there *is* any
interaction of state it *must* be covered by the standard i.e. must
*not* link or combine with another "uncontrolled" piece of state
(hardware or software) that is also out-of-scope for the standard.  i
was beginning to formulate this clearly in another thread.

The A extension chapter clearly says that misaligned LR/SC raises an exception. Nevertheless, it seems helpful to use more explicit language here, so I'll amend it.

l.

--
You received this message because you are subscribed to the Google Groups "RISC-V ISA Dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to isa-dev+unsubscribe@groups.riscv.org.
To post to this group, send email to isa...@groups.riscv.org.
Visit this group at https://groups.google.com/a/groups.riscv.org/group/isa-dev/.

To view this discussion on the web visit https://groups.google.com/a/groups.riscv.org/d/msgid/isa-dev/CAPweEDwfg70b47N84BmH%2BkyokKtzCyBQ-kWve8QuigFELuCCpA%40mail.gmail.com.

[Luke Kenneth Casson Leighton]

On Sun, May 6, 2018 at 6:37 PM, Andrew Waterman
<wate...@eecs.berkeley.edu> wrote:
>> how about:
>>
>> +64-bit words and four-byte aligned for 32-bit words). If the address is
>> +not naturally aligned, and the ``Zam'' extension is not enabled,
>> + a misaligned address exception will be generated.
>> + The requirements and semantics of misaligned AMOs when the ``Zam''
>> + extension is enabled are specifically covered by Chapter~\ref{sec:zam}.
>
>
> I actually prefer the way it's currently expressed.

it was just a suggestion for wording, you can see where i was going
with it? thinking in "programmer" terms: in a linear fasion AND the
conditions together first then allow fall-through to cover the Zam
case. the way it's worded presently, the conditions are clearly
set... but then there's a follow-up statement *after* that which
retrospectively modify / contradict the previous sentence. as a
programmer that makes me... nervous. plus, the LALR parser state
diagram that peoples' minds have to create is larger :)

>> +Support for misaligned LR/SC sequences is not currently standardized.
>> +
>>
>> is that to _be_ standardised (ever)? are implementors prevented and
>> prohibited *from* supporting (non-standardised) misligned LR/SC
>> sequences?

> The A extension chapter clearly says that misaligned LR/SC raises an
> exception. Nevertheless, it seems helpful to use more explicit language
> here, so I'll amend it.

a cross-reference to the chapter would be great (if needed?)

"Support for misaligned LR/SC sequences is not currently standardized

and, as outlined in the A-extension chapter an exception must be raised"

i'll do diffs/patches next time, Andrew, makes things easier.

l.

[Jacob Bachmeyer]

Luke Kenneth Casson Leighton wrote:
> On Sun, May 6, 2018 at 6:37 PM, Andrew Waterman
> <wate...@eecs.berkeley.edu> wrote:
>
>>> how about:
>>>
>>> +64-bit words and four-byte aligned for 32-bit words). If the address is
>>> +not naturally aligned, and the ``Zam'' extension is not enabled,
>>> + a misaligned address exception will be generated.
>>> + The requirements and semantics of misaligned AMOs when the ``Zam''
>>> + extension is enabled are specifically covered by Chapter~\ref{sec:zam}.
>>>
>> I actually prefer the way it's currently expressed.
>>
>
> it was just a suggestion for wording, you can see where i was going
> with it? thinking in "programmer" terms: in a linear fasion AND the
> conditions together first then allow fall-through to cover the Zam
> case. the way it's worded presently, the conditions are clearly
> set... but then there's a follow-up statement *after* that which
> retrospectively modify / contradict the previous sentence. as a
> programmer that makes me... nervous. plus, the LALR parser state
> diagram that peoples' minds have to create is larger :)
>

Dr. Waterman's preferred wording makes more sense to me, since I view
RISC-V base with extensions as analogous to a tarball and a patch set
rather than an integrated whole.

>>> +Support for misaligned LR/SC sequences is not currently standardized.
>>> +
>>>
>>> is that to _be_ standardised (ever)? are implementors prevented and
>>> prohibited *from* supporting (non-standardised) misligned LR/SC
>>> sequences?
>>>
>> The A extension chapter clearly says that misaligned LR/SC raises an
>> exception. Nevertheless, it seems helpful to use more explicit language
>> here, so I'll amend it.
>>
>
> a cross-reference to the chapter would be great (if needed?)
>
> "Support for misaligned LR/SC sequences is not currently standardized
> and, as outlined in the A-extension chapter an exception must be raised"

I would suggest rewording that as:

"The current standard does not support misaligned LR/SC sequences and
requires that a misaligned AMO exception be raised on such an access."



-- Jacob

[Luke Kenneth Casson Leighton]

On Mon, May 7, 2018 at 2:00 AM, Jacob Bachmeyer <jcb6...@gmail.com> wrote:
>> it was just a suggestion for wording, you can see where i was going
>> with it? thinking in "programmer" terms: in a linear fasion AND the
>> conditions together first then allow fall-through to cover the Zam
>> case. the way it's worded presently, the conditions are clearly
>> set... but then there's a follow-up statement *after* that which
>> retrospectively modify / contradict the previous sentence. as a
>> programmer that makes me... nervous. plus, the LALR parser state
>> diagram that peoples' minds have to create is larger :)
>>
>
>
> Dr. Waterman's preferred wording makes more sense to me, since I view RISC-V
> base with extensions as analogous to a tarball and a patch set rather than
> an integrated whole.

my understanding was that he (you) weren't happy with the
sentence-reordering. a simpler way to cause peoples' minds not to
need to maintain a large (and consequently unclear) LALR mental parser
stack is:

+64-bit words and four-byte aligned for 32-bit words).

+ If the ``Zam'' extension is not enabled, and the address is
+not naturally aligned, a misaligned address exception will be generated.

the addition "If the Zam extension is not enabled" makes it clear and
unambiguous *at the point of reading* exactly what the conditions are.

the wording for the remaining sentence i do not feel comfortable
making suggestions for fear of contradicting you or andrew.

>>>> +Support for misaligned LR/SC sequences is not currently standardized.
>>>> +
>>>>
>>>> is that to _be_ standardised (ever)? are implementors prevented and
>>>> prohibited *from* supporting (non-standardised) misligned LR/SC
>>>> sequences?
>>>>
>>>
>>> The A extension chapter clearly says that misaligned LR/SC raises an
>>> exception. Nevertheless, it seems helpful to use more explicit language
>>> here, so I'll amend it.
>>>
>>
>>
>> a cross-reference to the chapter would be great (if needed?)
>>
>> "Support for misaligned LR/SC sequences is not currently standardized
>> and, as outlined in the A-extension chapter an exception must be raised"
>
>
> I would suggest rewording that as:
>
> "The current standard does not support misaligned LR/SC sequences and
> requires that a misaligned AMO exception be raised on such an access."

i like "current standard" better than "currently standardised". my
feeling is that the addition "as outlined in the A-extension chapter"
is important as a cross-reference.

l.