Received: by 2002:a25:1506:0:0:0:0:0 with SMTP id 6csp3353495ybv; Mon, 24 Feb 2020 23:37:54 -0800 (PST) X-Google-Smtp-Source: APXvYqyscBOp26SkOVvPE4zBtuPFwG3OMnHjtgrWAxw6kvwcD3syi9OSZ0c70ghA+TZ6wM5pkGgN X-Received: by 2002:aca:f587:: with SMTP id t129mr2325833oih.143.1582616274514; Mon, 24 Feb 2020 23:37:54 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1582616274; cv=none; d=google.com; s=arc-20160816; b=InJgfBQyU4IMXyjGTPpjuVbuNCsbSJ1gd94vbt/XBa+UI6Apqw5DUDobwhY9mc1vlk e6oTEK3AfQvDOX0Vimm32g/QeDxJBqqF0sA0NTIxdb2+FFLgabzhVyCboSHKjgSuHQG6 YMeGnqk+rNnP2UPVuRgB6XZrSHHksowbAev8orlwgjIxVUIqPCy4rA5JUgZxEu7uVz/j AxdSkH1tlLuglswEuAjj3gQk2AQRICJqKjIQQGYATcJnecUUiyZ/jmKWVGh02MkMX+UG Z8qpRHG6gQPpx/AZiwbHSzZaq4cgCHg3d6zKU30O/8zrrLSRQZ5Z5kj5TYJVXh0el+yL wU8A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:sender:in-reply-to:content-disposition :mime-version:references:message-id:subject:cc:to:from:date :dkim-signature; bh=2BaVUFSv/to+L4aW8kB/7KAen05ZTlbgy3P8SSzYyyg=; b=dchIrSFZc6VQJcZeSBhQLV858cZuPun108oi8Qhb0m9Gt99dAjUQvbpQEUTKl6snP8 dmPT/snN30mN0mbXRDFE3awKqly4CQp6xJIldm4OIaiwBoIn41ywMqjgXOzX5Do/mDvs KjlVXd/On5krG/KqQ7I30bB73j5OP42woL1XCqYLhzH0eosQQT3vBnvL1vGNvwRTRdPs tUDEavDBPbtvcMp+mhhg+wAasrMkJZ2bhpFOsKQTVglKqhudFI+lJLJFBwsqQTDqBWX3 Gwnhu5ilYLDrp0hWrba7j8iKo4E8TsRJ0PwsiCxjNBl8+XSi0C6/uEUAP7yGTkHLmBJC uFFg== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=FZJEEX8l; 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; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from vger.kernel.org (vger.kernel.org. [209.132.180.67]) by mx.google.com with ESMTP id s9si5940831oij.78.2020.02.24.23.37.41; Mon, 24 Feb 2020 23:37:54 -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; dkim=pass header.i=@gmail.com header.s=20161025 header.b=FZJEEX8l; 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; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1729273AbgBYHfA (ORCPT + 99 others); Tue, 25 Feb 2020 02:35:00 -0500 Received: from mail-qt1-f194.google.com ([209.85.160.194]:41917 "EHLO mail-qt1-f194.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1729268AbgBYHe7 (ORCPT ); Tue, 25 Feb 2020 02:34:59 -0500 Received: by mail-qt1-f194.google.com with SMTP id l21so8417500qtr.8; Mon, 24 Feb 2020 23:34:58 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to; bh=2BaVUFSv/to+L4aW8kB/7KAen05ZTlbgy3P8SSzYyyg=; b=FZJEEX8lRPAawuOMkBShF4iPQyGKh1OhCpM41mbm1RM+6Im0p5s413VaTMkhsXDuLn FGOyjdv4/Y8XioBGmeRFV+SRiwSfz1+U6SpmjeRYhfyXBeM0MPbgv/Yacbiklvn7iiu3 3/NYPR6qkj67TguKnT7EOIF3Va0ySN14Y7kM3h8bpnTz/IQJjd9MiChu3M7ifeWr8wSZ uM0Par3HzzzUxhuqKWdFmz0/x+M4vTJc8CHcJoheIHyBJtvvLDCKeJmxbSlSDRxdL+MU Zg/Cf1fELu/miLUUNE9VNKoMzW8DBe+Y84Uoo/iftwaslyResSljjFCt7qH4A42honES +KeQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:date:from:to:cc:subject:message-id:references :mime-version:content-disposition:in-reply-to; bh=2BaVUFSv/to+L4aW8kB/7KAen05ZTlbgy3P8SSzYyyg=; b=ni9SOkDCrB7eCmt+UrZ/p2xCZIyhJLksjoTzayKjeZvRZYK3hrRDVsesNsgiLVmyWx zzGLEJ4pxf62Qwsh075rv6mAtLrBTKyzrZtShWcNiTGpeooIEaYA1Wd6an4s4+gYXxn0 XRFEhxJaYtkHLY5aIzcg750cbywRuA/emSAZfeOtJemGHA90BxZtbhUoQRDBq0ckd7JT mmYa//RX2beo4kd2OzW673T5MUlHxJvgJGRenaELq+FE4aIrXLSA5kusXTeVfp8swayj 41lrdL9nRvBg/zI5nRHqXa08iAEzIKkAsUe8U5lixi3o0tISwFIkMdKiDtj8/KQDWcLJ nfhg== X-Gm-Message-State: APjAAAXeyeF3lQD5UjmFDk7Q5XWmLjvBwU5BHptBUAl5KIgUvfKTwEbm hdQDfWc3MkZ5rI6Engdl7mg= X-Received: by 2002:aed:2862:: with SMTP id r89mr3014031qtd.289.1582616097470; Mon, 24 Feb 2020 23:34:57 -0800 (PST) Received: from auth2-smtp.messagingengine.com (auth2-smtp.messagingengine.com. [66.111.4.228]) by smtp.gmail.com with ESMTPSA id s19sm5768916qkj.88.2020.02.24.23.34.56 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 24 Feb 2020 23:34:56 -0800 (PST) Received: from compute6.internal (compute6.nyi.internal [10.202.2.46]) by mailauth.nyi.internal (Postfix) with ESMTP id 5118122007; Tue, 25 Feb 2020 02:34:55 -0500 (EST) Received: from mailfrontend1 ([10.202.2.162]) by compute6.internal (MEProxy); Tue, 25 Feb 2020 02:34:55 -0500 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedugedrledugdduudduucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne cujfgurhepfffhvffukfhfgggtuggjsehttdertddttddvnecuhfhrohhmpeeuohhquhhn ucfhvghnghcuoegsohhquhhnrdhfvghnghesghhmrghilhdrtghomheqnecuffhomhgrih hnpehkvghrnhgvlhdrohhrghenucfkphephedvrdduheehrdduuddurdejudenucevlhhu shhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhrohhmpegsohhquhhnodhmvg hsmhhtphgruhhthhhpvghrshhonhgrlhhithihqdeiledvgeehtdeigedqudejjeekheeh hedvqdgsohhquhhnrdhfvghngheppehgmhgrihhlrdgtohhmsehfihigmhgvrdhnrghmvg X-ME-Proxy: Received: from localhost (unknown [52.155.111.71]) by mail.messagingengine.com (Postfix) with ESMTPA id A2B75328005D; Tue, 25 Feb 2020 02:34:52 -0500 (EST) Date: Tue, 25 Feb 2020 15:34:51 +0800 From: Boqun Feng To: Andrea Parri , Luc Maranget Cc: linux-kernel@vger.kernel.org, Alan Stern , Will Deacon , Peter Zijlstra , Nicholas Piggin , David Howells , Jade Alglave , Luc Maranget , "Paul E. McKenney" , Akira Yokosawa , Daniel Lustig , Jonathan Corbet , linux-arch@vger.kernel.org, linux-doc@vger.kernel.org Subject: Re: [RFC 2/3] tools/memory-model: Add a litmus test for atomic_set() Message-ID: <20200225073451.GP69864@debian-boqun.qqnc3lrjykvubdpftowmye0fmh.lx.internal.cloudapp.net> References: <20200214040132.91934-1-boqun.feng@gmail.com> <20200214040132.91934-3-boqun.feng@gmail.com> <20200214081213.GA17708@andrea> <20200214104003.GC20408@debian-boqun.qqnc3lrjykvubdpftowmye0fmh.lx.internal.cloudapp.net> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20200214104003.GC20408@debian-boqun.qqnc3lrjykvubdpftowmye0fmh.lx.internal.cloudapp.net> Sender: linux-kernel-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Luc, Could you have a look at the problem Andrea and I discuss here? It seems that you have done a few things in herd for atomic_add_unless() in particular, and based on the experiments of Andrea and me, seems atomic_add_unless() works correctly. So can you confirm that herd now can handle atomic_add_unless() or there is still something missing? Thanks! Regards, Boqun On Fri, Feb 14, 2020 at 06:40:03PM +0800, Boqun Feng wrote: > On Fri, Feb 14, 2020 at 09:12:13AM +0100, Andrea Parri wrote: > > > @@ -0,0 +1,24 @@ > > > +C Atomic-set-observable-to-RMW > > > + > > > +(* > > > + * Result: Never > > > + * > > > + * Test of the result of atomic_set() must be observable to atomic RMWs. > > > + *) > > > + > > > +{ > > > + atomic_t v = ATOMIC_INIT(1); > > > +} > > > + > > > +P0(atomic_t *v) > > > +{ > > > + (void)atomic_add_unless(v,1,0); > > > > We blacklisted this primitive some time ago, cf. section "LIMITATIONS", > > entry (6b) in tools/memory-model/README; the discussion was here: > > > > https://lkml.kernel.org/r/20180829211053.20531-3-paulmck@linux.vnet.ibm.com > > > > And in an email replying to that email, you just tried and seemed > atomic_add_unless() works ;-) > > > but unfortunately I can't remember other details at the moment: maybe > > it is just a matter of or the proper time to update that section. > > > > I spend a few time looking into the changes in herd, the dependency > problem seems to be as follow: > > For atomic_add_unless(ptr, a, u), the return value (true or false) > depends on both *ptr and u, this is different than other atomic RMW, > whose return value only depends on *ptr. Considering the following > litmus test: > > C atomic_add_unless-dependency > > { > int y = 1; > } > > P0(int *x, int *y, int *z) > { > int r0; > int r1; > int r2; > > r0 = READ_ONCE(*x); > if (atomic_add_unless(y, 2, r0)) > WRITE_ONCE(*z, 42); > else > WRITE_ONCE(*z, 1); > } > > P1(int *x, int *y, int *z) > { > int r0; > > r0 = smp_load_acquire(z); > > WRITE_ONCE(*x, 1); > } > > exists > (1:r0 = 1 /\ 0:r0 = 1) > > , the exist-clause will never trigger, however if we replace > "atomic_add_unless(y, 2, r0)" with "atomic_add_unless(y, 2, 1)", the > write on *z and the read from *x on CPU 0 are not ordered, so we could > observe the exist-clause triggered. > > I just tried with the latest herd, and herd can work out this > dependency. So I think we are good now and can change the limitation > section in the document. But I will wait for Luc's input for this. Luc, > did I get this correct? Is there any other limitation on > atomic_add_unless() now? > > Regards, > Boqun > > > Thanks, > > Andrea