[cpp-threads] Fwd: Sequential Consistency redux

[Mark Batty]

As Alan points out, the mutex specification is rather vague.

The version of the standard I have is slightly different in 30.4.1.2
(it's newer too, n3291). It says:

" The implementation shall provide lock and unlock operations, as
described below. For purposes of determining the existence of a data
race, these behave as atomic operations (1.10). The lock and unlock
operations on a single mutex shall appear to occur in a single total
order. [ Note: this can be viewed as the modification order (1.10) of
the mutex. — end note ] [ Note: Construction and destruction of an
object of a mutex type need not be thread-safe; other synchronization
should be used to ensure that mutex objects are initialized and
visible to other threads. — end note ] "

There is still no requirement that the order over locks agrees with
happens-before, which there should be.

Discussing Nick's example, Alan says: "And yet, contrary to what the
note in 1.10p12 says, the example does not involve consume
operations." -- I agree with your logic, and it seems that that note
should be removed. It was added before I had thought sufficiently
about the mutex rules.

- Mark




---------- Forwarded message ----------
From: Alan Stern <stern at rowland.harvard.edu>
Date: Tue, Nov 22, 2011 at 7:31 PM
Subject: Re: [cpp-threads] Sequential Consistency redux
To: C++ threads standardisation <cpp-threads at decadent.org.uk>


On Tue, 22 Nov 2011, Boehm, Hans wrote:

> > It's worth mentioning that even before the "litmus test" was devised
> > and 1.10p12 was added, it was felt that the text would rule out the
> > sort of non-sequentially-consistent behavior of mutexes you asked
> > about.
> Yes.  Other cycles are arguably impossible because they prevent a
> read access from seeing any write.  If an atomic release write R is
> seen by a corresponding acquire operation A, and they occur in a
> happens-before cycle, we immediately get a contradiction, because R
> is not in the visible sequence of side-effects with respect to A.
> Thus such executions aren't allowed.  30.4.1.2p5 arguably applies
> this to locks as well.  That aside, it could be argued that the note
> actually doesn't add much insight for the typical reader.  Thus I no
> longer feel strongly about this one way or another.

I don't see how 30.4.1.2p5 is relevant.  It merely says "The
implementation shall serialize those operations".  (Is that not the
same as what the second Note in 1.10p8 says?  The term "serialize"
isn't explained here.)  There's nothing about side-effects, visible or
otherwise.

Compare this situation to 1.10p15: "If an operation A that modifies an
atomic object M happens before an operation B that modifies M, then
A shall be earlier than B in the modification order of M".  There's no
corresponding requirement for mutexes.  That is, nothing says: If
operations A and B lock the same mutex and A happens before B, then A
shall be earlier than B in the mutex's order.

No doubt this omission is related to the fact that the mutex order
concept is relegated to a Note in 1.10p8 rather than being part of the
main text.  This is odd, since it seems comparable in importance to the
modification order concept.

> > (On the other hand, even now I think the text could stand a little more
> > clarification.  1.10p8 says "All operations on a given mutex occur in a
> > single total order", but it doesn't say explicitly that this order must
> > be consistent with "happens before".  Contrast this with the way 1.10p6
> > talks about the relation between an atomic object's modification order
> > and "happens before".)
> Again, I don't see how this could fail to be satisfied.  I don't
> believe there is a way to get a cycle in happens-before union
> mutex-order without violating the other constraints.  The other
> constraints on mutexes are such that mutex-order is a subset of
> happens-before.  (Outermost acquires and releases must alternate.
> The acquire -> release edges contribute to sequenced before, and
> release -> acquire contribute to synchronizes-with.)

As far as I can tell, currently the only way to rule out Nick's example
is by 1.10p12.  In the example, each mutex is accessed according to a
total order, the mutex orders are subsets of "happens before", the
variable assignments are all visible to the "cout" expressions, and
"happens before" is cyclic.  And yet, contrary to what the note in
1.10p12 says, the example does not involve consume operations.

Alan Stern


--
cpp-threads mailing list
cpp-threads at decadent.org.uk
http://www.decadent.org.uk/cgi-bin/mailman/listinfo/cpp-threads