From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <linux-kernel-owner@vger.kernel.org>
Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand
        id S1752347AbdK1Jo6 (ORCPT <rfc822;w@1wt.eu>);
        Tue, 28 Nov 2017 04:44:58 -0500
Received: from bombadil.infradead.org ([65.50.211.133]:52736 "EHLO
        bombadil.infradead.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org
        with ESMTP id S1752303AbdK1Joy (ORCPT
        <rfc822;linux-kernel@vger.kernel.org>);
        Tue, 28 Nov 2017 04:44:54 -0500
Date: Tue, 28 Nov 2017 10:44:40 +0100
From: Peter Zijlstra <peterz@infradead.org>
To: Daniel Lustig <dlustig@nvidia.com>
Cc: Alan Stern <stern@rowland.harvard.edu>,
        "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>,
        Andrea Parri <parri.andrea@gmail.com>,
        Luc Maranget <luc.maranget@inria.fr>,
        Jade Alglave <j.alglave@ucl.ac.uk>, Boqun Feng <boqun.feng@gmail.com>,
        Nicholas Piggin <npiggin@gmail.com>, Will Deacon <will.deacon@arm.com>,
        David Howells <dhowells@redhat.com>,
        Palmer Dabbelt <palmer@dabbelt.com>,
        Kernel development list <linux-kernel@vger.kernel.org>
Subject: Re: Unlock-lock questions and the Linux Kernel Memory Model
Message-ID: <20171128094440.z32ieyh72xt64jhw@hirez.programming.kicks-ass.net>
References: <Pine.LNX.4.44L0.1711271553490.1424-100000@iolanthe.rowland.org>
 <b7e2cae8-f752-b40a-bce0-80c8f6b65d3c@nvidia.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <b7e2cae8-f752-b40a-bce0-80c8f6b65d3c@nvidia.com>
User-Agent: NeoMutt/20170609 (1.8.3)
Sender: linux-kernel-owner@vger.kernel.org
List-ID: <linux-kernel.vger.kernel.org>
X-Mailing-List: linux-kernel@vger.kernel.org

On Mon, Nov 27, 2017 at 03:28:03PM -0800, Daniel Lustig wrote:
> On 11/27/2017 1:16 PM, Alan Stern wrote:> C rel-acq-write-ordering-3
> > 
> > {}
> > 
> > P0(int *x, int *s, int *y)
> > {
> > 	WRITE_ONCE(*x, 1);
> > 	smp_store_release(s, 1);
> > 	r1 = smp_load_acquire(s);
> > 	WRITE_ONCE(*y, 1);
> > }
> > 
> > P1(int *x, int *y)
> > {
> > 	r2 = READ_ONCE(*y);
> > 	smp_rmb();
> > 	r3 = READ_ONCE(*x);
> > }
> > 
> > exists (1:r2=1 /\ 1:r3=0)
> > 
> <snip>
> > 
> > And going to extremes...
> 
> Sorry if I'm missing something obvious, but before going to extremes...
> what about this one?
> 
> "SB+rel-acq" (or please rename if you have a different scheme)
> 
> {}
> 
> P0(int *x, int *s, int *y)
> {
> 	WRITE_ONCE(*x, 1);
> 	smp_store_release(s, 1);
> 	r1 = smp_load_acquire(s);
> 	r2 = READ_ONCE(*y);
> }

Yes, this one doesn't work on TSO and Power.

Ideally it would work for locks though, but that would mean mandating
RCsc lock implementations and currently Power is holding out on that.