[cpp-threads] Sequential Consistency redux

[Alan Stern]

On Fri, 18 Nov 2011, Mark Batty wrote:

> Hello Nick,
> 
> > Are the facilities in 30 [Thread] required to be sequentially consistent
> > or not as far as ordinary code goes?
> 
> We have proved this is true (in the absence of forging pointers to
> atomic locations) for our formal version of the memory model, which is
> faithful to the intent of the standard. The standard makes the claim
> of SC behavior for programs that don't use weaker-than-seq_cst atomics
> in  n2391-1.10p21.
> 
> > Orthogonally to that, does the same apply to relaxed atomics in the code
> > sections protected by mutexes?
> 
> If you protect relaxed atomic reads and writes as if they were
> non-atomics, so that there would be no data races, then you should get
> back sequential consistency. This is not simply stated in the
> standard, and is a theorem requiring argument over the model. I do
> think it's true though.
> 
> > Can both threads 3 and 4 print 1 and 0, thus indicating that
> > mutex-locked code is not sequentially consistent?  If not, where is that
> > stated?
> 
> 10-10 should not be visible. This hinges on the total order of mutex
> actions at a single location described in n2391-30.4.1.2p5.

My earlier response was wrong; Mark is correct.  Perhaps the easiest 
way to explain this is in terms of the "happens before" relation.

> Consider the following example:
> 
>   In serial code:
>       static mutex A, B;
>       int a = 0, b = 0;
>   The program then creates 4 threads.
>   In thread 1:
>       A.lock(); a = 1; A.unlock();
>   In thread 2:
>       B.lock(); b = 1; B.unlock();
>   In thread 3:
>       A.lock(); cout << a << endl; A.unlock();
>       B.lock(); cout << b << endl; B.unlock();
>   In thread 4:
>       B.lock(); cout << b << endl; B.unlock();
>       A.lock(); cout << a << endl; A.unlock();
> 
> Can both threads 3 and 4 print 1 and 0, thus indicating that
> mutex-locked code is not sequentially consistent?  If not, where is that
> stated?

If threads 3 and 4 both print 1 and 0, then we must have:

	(thread 4) cout << a	(prints 0) is sequenced before
	(thread 4) A.unlock	synchronizes with
	(thread 1) A.lock	is sequenced before
	(thread 1) a = 1	is sequenced before
	(thread 1) A.unlock	synchronizes with
	(thread 3) A.lock	is sequenced before
	(thread 3) cout << a	(prints 1) is sequenced before
	(thread 3) cout << b	(prints 0) is sequenced before
	(thread 3) B.unlock	synchronizes with
	(thread 2) B.lock	is sequenced before
	(thread 2) b = 1	is sequenced before
	(thread 2) B.unlock	synchronizes with
	(thread 4) B.lock	is sequenced before
	(thread 4) cout << b	(prints 1) is sequenced before
	(thread 4) cout << a

Therefore thread 4's "cout << a" "happens before" itself, which
violates the requirement in 1.10p12 that the "happens before" relation
must not exhibit any cycles.

Alan Stern