[concurrency-interest] What can an incorrectly synchronized read see?

Aleksey Shipilev shade at redhat.com
Thu Sep 29 04:05:10 EDT 2016

On 09/29/2016 09:13 AM, Alex Otenko wrote:
> You need to be careful about using a “proof by example” as a proof. It
> is ok to use it to demonstrate what happens to two reads of two writes,
> but it is not a proof about *all* reads and *all* writes.
> It is not as formal as it looks. How do you conclude it is sufficient to
> consider just two diagrams? How do you conclude it is sufficient to
> consider just four outcomes?

If you look closely, my proof basically shows the same properties you
picked: actions that happened-before lock acquisition in one thread
cannot see the updates happening in after lock acquisition in another
thread. For the same reason your interpretation uses -- the total
ordering of locks/unlocks, plus transitivity -- we are free to only look
for two cases of relative sequencing of Reader and Writer, either R->W,
or W->R, and everything else is the extension of these two basic patterns.

But I would be very, very careful with interpretations that talk about
statements, and not the program actions with the actual values observed.
Because this is subtly broken: "All statements in program order before a
lock release happen-before any statements that are in program order
after the lock acquires following that lock release"

Statements do not form a program order. Program order is total, and
statements are not forming total order (easy example: control flow split
at conditionals). As stated, in this example:

Thread 1:
  if (false) // more complicated predicate in real-life case, of course
    y = 1
  sync(this) {
    w = 1

Thread 2:
  sync(this) {
    r1 = w;
    r2 = y;

...your interpretation says the "statement" y=1 happens-before r2=y,
which mandates seeing (r1, r2) = (1, 1), which is obviously incorrect.
This is an easy mistake that everyone makes when talking about JMM [1],
and it does not help that we keep perpetuating it with inaccurate claims
on public lists.



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20160929/7609305d/attachment.sig>

More information about the Concurrency-interest mailing list