Received: by 2002:a25:1506:0:0:0:0:0 with SMTP id 6csp2015021ybv; Fri, 14 Feb 2020 09:51:21 -0800 (PST) X-Google-Smtp-Source: APXvYqyVrrIxc4t3zoJ0uPqJAlxOAYA4XLkp+VtTDO/Ku2kNYXNvqPH9O13axRM8pMhCE/YmZsLh X-Received: by 2002:a05:6830:124b:: with SMTP id s11mr3154664otp.333.1581702681830; Fri, 14 Feb 2020 09:51:21 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1581702681; cv=none; d=google.com; s=arc-20160816; b=ygHcuQckfF8H7ZMb934Vr7xZwJXJcj8o2WlM10hwqb2YyM4nLKPeBfnkPGO+w/InVk Vgg1X42vB3s/1Gta9AaA2N/7N9R7Ec+3o/IzKR1abflQunV7gHvpB0bmhCiCXCrBTwxT M1f2+c2mLJ6ZBKcfi6b1JgjRw77KoNoeWCEAaQkBfOihUYndZVT9scdhQ5+VNkXq3fTw IIx1FgfmjpdAcszgYNJ9F1Sdg03S4B79DX+JCH0zOs+qQ6n2pazeGeWS75ZX6jp+UxOZ U7VyELDKvVtWIlAatGlOXiXbu5R1ONxYMHX4GxQzjcBzF3aFy/DtkIRvPxvzQPw9QVih sqMQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:sender:mime-version:message-id:in-reply-to :subject:cc:to:from:date; bh=+JOqHPQLecbTC/QtlRvUrHYGzpefdka2MOXA6H5pmGc=; b=m8jgzgtNpseLluoVKtwjUlMsgXhsfxQK/6l8iIgKu0tgaOSVbKlS89PAIUHiJUEZgY JjujshgDG1SnFtgRy/WygVD6n4rMV/u1h7JwMNmkms9oh+CJ+banTur31Mpf/UqHalmW 3bCvpr9GWZxPmTg2r6vFU4ggMm/Z1DP70VKx0izqnHbAtaFW9EwpB6PKH3psdxxBxGQx UUOpixmbyEAuZepTDhv6G1PHyngWsro57rAiC7Zs3EVKlOACHhgN4boGKY/OL15Undom k3raL3CuvVHO+o409brpyUIbFBBBKVx6CBFfFSKAzSxRT0oCVENIycgXGKfOqLdo3+NN rFrg== ARC-Authentication-Results: i=1; mx.google.com; spf=pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Return-Path: Received: from vger.kernel.org (vger.kernel.org. [209.132.180.67]) by mx.google.com with ESMTP id s7si3170787otd.280.2020.02.14.09.51.10; Fri, 14 Feb 2020 09:51:21 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67; Authentication-Results: mx.google.com; spf=pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S2388762AbgBNRvF (ORCPT + 99 others); Fri, 14 Feb 2020 12:51:05 -0500 Received: from iolanthe.rowland.org ([192.131.102.54]:39840 "HELO iolanthe.rowland.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with SMTP id S2388139AbgBNP66 (ORCPT ); Fri, 14 Feb 2020 10:58:58 -0500 Received: (qmail 3236 invoked by uid 2102); 14 Feb 2020 10:58:57 -0500 Received: from localhost (sendmail-bs@127.0.0.1) by localhost with SMTP; 14 Feb 2020 10:58:57 -0500 Date: Fri, 14 Feb 2020 10:58:57 -0500 (EST) From: Alan Stern X-X-Sender: stern@iolanthe.rowland.org To: Boqun Feng cc: linux-kernel@vger.kernel.org, Andrea Parri , Will Deacon , Peter Zijlstra , Nicholas Piggin , David Howells , Jade Alglave , Luc Maranget , "Paul E. McKenney" , Akira Yokosawa , Daniel Lustig , Jonathan Corbet , , Subject: Re: [RFC 3/3] tools/memory-model: Add litmus test for RMW + smp_mb__after_atomic() In-Reply-To: <20200214040132.91934-4-boqun.feng@gmail.com> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: linux-kernel-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Fri, 14 Feb 2020, Boqun Feng wrote: > We already use a litmus test in atomic_t.txt to describe atomic RMW + > smp_mb__after_atomic() is "strong acquire" (both the read and the write > part is ordered). "strong acquire" is not an appropriate description -- there is no such thing as a strong acquire in the LKMM -- nor is it a good name for the litmus test. A better description would be "stronger than acquire", as in the sentence preceding the litmus test in atomic_t.txt. > So make it a litmus test in memory-model litmus-tests > directory, so that people can access the litmus easily. > > Additionally, change the processor numbers "P1, P2" to "P0, P1" in > atomic_t.txt for the consistency with the processor numbers in the > litmus test, which herd can handle. > > Signed-off-by: Boqun Feng > --- > Documentation/atomic_t.txt | 6 ++-- > ...+mb__after_atomic-is-strong-acquire.litmus | 29 +++++++++++++++++++ > tools/memory-model/litmus-tests/README | 5 ++++ > 3 files changed, 37 insertions(+), 3 deletions(-) > create mode 100644 tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus > > diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt > index ceb85ada378e..e3ad4e4cd9ed 100644 > --- a/Documentation/atomic_t.txt > +++ b/Documentation/atomic_t.txt > @@ -238,14 +238,14 @@ strictly stronger than ACQUIRE. As illustrated: > { > } > > - P1(int *x, atomic_t *y) > + P0(int *x, atomic_t *y) > { > r0 = READ_ONCE(*x); > smp_rmb(); > r1 = atomic_read(y); > } > > - P2(int *x, atomic_t *y) > + P1(int *x, atomic_t *y) > { > atomic_inc(y); > smp_mb__after_atomic(); > @@ -260,7 +260,7 @@ This should not happen; but a hypothetical atomic_inc_acquire() -- > because it would not order the W part of the RMW against the following > WRITE_ONCE. Thus: > > - P1 P2 > + P0 P1 > > t = LL.acq *y (0) > t++; > diff --git a/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus > new file mode 100644 > index 000000000000..e7216cf9d92a > --- /dev/null > +++ b/tools/memory-model/litmus-tests/Atomic-RMW+mb__after_atomic-is-strong-acquire.litmus > @@ -0,0 +1,29 @@ > +C Atomic-RMW+mb__after_atomic-is-strong-acquire > + > +(* > + * Result: Never > + * > + * Test of an atomic RMW followed by a smp_mb__after_atomic() is s/Test of/Test that/ > + * "strong-acquire": both the read and write part of the RMW is ordered before This should say "stronger than a normal acquire". And "part" should be "parts", and "is ordered" should be "are ordered". Also, please try to arrange the line breaks so that the comment lines don't have vastly different lengths. Similar changes should be made for the text added to README. Alan Stern