Consistency of atomic memory operations and store operations

[Samuel Riedel]

I have a question regarding the consistency of atomic memory operations

(AMOs) and regular write operations. Imagine the following example:

The memory at location a0 is initially 0. Two harts execute the following
sequence of instructions simultaneously:

Hart 0:

li              t0,  10
amo.add   t1,   t0,  (a0)

Hart 1:

li      t2,  2

sw    t2,  (a0)

After both harts have executed these instructions, I see the following
possible outcomes:

• t1=0, (a0)=2
  (The AMO was executed before the store operation.)
• t1=2, (a0)=12
  (The AMO was executed after the store operation.)
• t1=0, (a0)=10
  (The AMO was translated into a read operation (reading 0) and a
  write operation (a0 <-- 10). The store of hart 1 (a0 <-- 2) was
  executed between the AMO's read and write operation and therefore
  overwritten by it.)
  

In the third scenario, one might argue that the AMO was not executed
atomically due to the store in between the AMO's read and write. But the
question is: Must AMOs be consistent with regular store operations or only
with other AMOs?

The question is closely linked to the programming model. Is there any
guarantee on the value of a shared memory location that is written using
regular stores? An 'AMO-consistent' write can easily be achieved by using
an amo.swap operation and discarding the return value. Therefore, the
programming model could require writing to shared memory locations only
using AMOs to guarantee consistency. Regular stores might be lost.

A special case of this question concerns the store-conditional. Is it
possible that the result of a successful store-conditional is 'overseen' by
an AMO and therefore lost?

The reason for this question is that some memory controllers and buses do
not offer any ordering guarantee of reads with respect to writes. In such
cases it is very expensive to ensure that no write in flight to the memory
gets overtaken by the read operation of an AMO.

[Andrew Waterman]

Yes, they must.  The memory model states, "memory operations [...] can never be observed in a partially-complete state" and "an aligned AMO gives rise to a single memory operation" -- taken together, this means AMOs are indivisible with respect to non-AMO memory accesses.

The question is closely linked to the programming model. Is there any
guarantee on the value of a shared memory location that is written using
regular stores? An 'AMO-consistent' write can easily be achieved by using
an amo.swap operation and discarding the return value. Therefore, the
programming model could require writing to shared memory locations only
using AMOs to guarantee consistency. Regular stores might be lost.

A special case of this question concerns the store-conditional. Is it
possible that the result of a successful store-conditional is 'overseen' by
an AMO and therefore lost?

The reason for this question is that some memory controllers and buses do
not offer any ordering guarantee of reads with respect to writes. In such
cases it is very expensive to ensure that no write in flight to the memory
gets overtaken by the read operation of an AMO.

I believe this is a red herring.  Even for uniprocessor memory ordering, you need to guarantee that reading a given memory location returns the most recently written value.  Therefore, you already have some agent (probably a data cache) that can enforce this ordering.  The same agent can perform AMOs in accordance with the ISA spec.

--
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+u...@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/990d299c-e807-4f7b-bef7-d78b1ac3bbce%40groups.riscv.org.

[Shaked Flur]

For questions like this, one can explore what the RISC-V architecture allows

using our RMEM web-interface tool, which incorporates the RVWMO

operational model.  This link,  https://is.gd/Bv4s5c , has the test you mention

already loaded (and with the "all eager" option selected).  To compute

the set of all architecture-allowed executions, one just needs to click

Search->Exhaustive, or one can explore what's allowed interactively by

clicking the blue enabled transitions.   One can also run the same test

exhaustively w.r.t. the axiomatic-model version of RVWMO in the herd

tool, downloadable from http://diy.inria.fr/.

Best,

Shaked Flur and Peter Sewell

--

[Samuel Riedel]

Thank you both for your answers. The RMEM tool was really helpful to us.

Best,

Samuel Riedel