Re: [RFC] LKMM: Add volatile_if()
From: "Paul E. McKenney" <paulmck@kernel.org>
Date: 2021-08-02 23:32:00
On Fri, Jul 30, 2021 at 06:20:22PM +0100, Jade Alglave wrote: [ . . . ]
Sincere apologies in taking so long to reply. I attach a technical report which describes the status of dependencies in the Arm memory model. I have also released the corresponding cat files and a collection of interesting litmus tests over here: https://github.com/herd/herdtools7/commit/f80bd7c2e49d7d3adad22afc62ff4768d65bf830 I hope this material can help inform this conversation and I would love to hear your thoughts.
It is very good to see this! A few random questions and comments below
based on a couple of passes through this document.
Thanx, Paul
------------------------------------------------------------------------
o Figure 2: The iico_data arc are essentially invisible after
printing, as in the text on the following page is darker
than these arcs. I had similar difficulties with many
of the other diagrams.
o Figure 2: What does the "q" signify in the upper line of the
uppermost event-c box ("R0:X1q=x")? I get that we are reading
register X1 and getting back the address of variable "x". I am
assuming that the "R0" means that process 0 is doing a read,
but I cannot be sure.
I am assuming that the "proc: P0 poi:0" means that this is
the first instruction of process P0. If this is incorrect,
please let me know.
o Figure 6 initializes X0, X1, X2, and X3, while Figure 4
initializes only X0 and X3. Is this difference meaningful?
(My guess is that you have default-zero initialization so
that it does not matter, but I figured that I should ask.)
o Figure 6: The iico_ctrl arcs are easier to see on printed copy
than the iico_data arcs, but it would be nice if they were a
bit darker. The rf-reg arcs are plainly visible.
o Figure 6: Why is there no po arc to the CSEL instruction?
o Section 1.3, "Swap instructions" paragraph. Please supply
a litmus-test figure to go along with Figure 12.
o Figures 10 and 11: Having these on the same page was extremely
helpful, thank you!
o Figure 11: What does the "*" signify in the first line event "a:"
("a: Rx*q=0")? Why is there no "*" in the corresponding event
in Figure 9?
o Figure 11: The ca arcs are nicely visible, but I am coming up
empty on hypotheses for their meaning. Or is ca the new co?
o Figure 11: Why two po arcs into the CAS instruction? Due
to independent register reads taht might proceed concurrently?
If so, why no po arc to event g?
o Figure 11: The connections between events a, f, and h lead me to
believe that the hardware is permitted to rewrite register X3
with the value previously read from X3 as opposed to the value
read from [X1]. Or maybe omit the write entirely.
I don't see anything wrong with taking this approach, but I
figured I should check.
o Section 2 I leave in Alan's capable hands.
o Section 3.1, "Dependency through registers": A "PE" is a
processing element or some such?
o Section 3.1, "Dependency through registers", first bullet:
The exclusion of Store Exclusive is to avoid ordering via
the 0/1 status store, correct?
o Section 3.1, "Address Dependency", second bullet, second
sub-bullet: OK, I will bite. The dependency from the Branching
Effect is due to a load from the program counter or some such?
Or are there some special-purpose ARMv8 branch instructions that
I should look up.
o Figure 27, "MOV W5, W0": It took me a bit to figure out that
this instruction exists strictly for the benefit of the
"exists" clause. Or am I missing something subtle?
o Section 4.1, "Interestingly, this notion of ``pick dependency...":
I suggest using something like "require" instead of "proscribe",
if that is what is meant. The hamming distance between the
antonyms "proscribe" and "prescribe" is quite small, which can
result in errors both when writing and when reading. :-(
o Figure 30: The discarding of register X3 is intentional, correct?
If so, it is indeed hard to imagine wanting ordering from this
code sequence. Though I might once again be suffering from a
failure of imagination...
o Figure 32: The reason for this litmus test being allowed is that
the ordering through CSEL is sort of like a control dependency,
and control dependencies to loads do not force ordering, correct?
Or did I miss a turn in there somewhere?
o Section 4.2, "Pick Basic dependency": Should the second and
third bullets be indented under the first bullet?
It will take at least another pass to get my head around pick
dependencies, so I will stop here for the moment.
Again, good stuff, and great to see the additional definition!
Thanx, Paul