[cpp-threads] Sequential Consistency redux

Alan Stern stern at rowland.harvard.edu
Tue Nov 22 19:31:33 GMT 2011


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




More information about the cpp-threads mailing list