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 S1753088AbdK0X2G (ORCPT <rfc822;w@1wt.eu>);
        Mon, 27 Nov 2017 18:28:06 -0500
Received: from hqemgate15.nvidia.com ([216.228.121.64]:7450 "EHLO
        hqemgate15.nvidia.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org
        with ESMTP id S1752411AbdK0X2F (ORCPT
        <rfc822;linux-kernel@vger.kernel.org>);
        Mon, 27 Nov 2017 18:28:05 -0500
X-PGP-Universal: processed;
        by hqpgpgate101.nvidia.com on Mon, 27 Nov 2017 15:28:04 -0800
Subject: Re: Unlock-lock questions and the Linux Kernel Memory Model
To: 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>,
        Peter Zijlstra <peterz@infradead.org>,
        Will Deacon <will.deacon@arm.com>, David Howells <dhowells@redhat.com>,
        Palmer Dabbelt <palmer@dabbelt.com>
CC: Kernel development list <linux-kernel@vger.kernel.org>
References: <Pine.LNX.4.44L0.1711271553490.1424-100000@iolanthe.rowland.org>
From: Daniel Lustig <dlustig@nvidia.com>
Message-ID: <b7e2cae8-f752-b40a-bce0-80c8f6b65d3c@nvidia.com>
Date: Mon, 27 Nov 2017 15:28:03 -0800
User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:52.0) Gecko/20100101
 Thunderbird/52.5.0
MIME-Version: 1.0
In-Reply-To: <Pine.LNX.4.44L0.1711271553490.1424-100000@iolanthe.rowland.org>
X-Originating-IP: [10.110.39.27]
X-ClientProxiedBy: HQMAIL108.nvidia.com (172.18.146.13) To
 HQMAIL105.nvidia.com (172.20.187.12)
Content-Type: text/plain; charset="utf-8"
Content-Language: en-US
Content-Transfer-Encoding: 7bit
Sender: linux-kernel-owner@vger.kernel.org
List-ID: <linux-kernel.vger.kernel.org>
X-Mailing-List: linux-kernel@vger.kernel.org

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);
}

P1(int *x, int *y)
{
	WRITE_ONCE(*y, 1);
	smp_store_release(s, 2);
	r3 = smp_load_acquire(s);
	r4 = READ_ONCE(*x);
}

exists (1:r2=0 /\ 1:r4=0)

If smp_store_release() and smp_load_acquire() map to normal TSO loads
and stores on x86, then this test can't be forbidden, can it?

Similar question for the other tests, but this is probably the
easiest one to analyze.

Dan