Received: by 2002:ac0:a5b6:0:0:0:0:0 with SMTP id m51-v6csp672384imm; Thu, 31 May 2018 07:28:45 -0700 (PDT) X-Google-Smtp-Source: ADUXVKK8kZoviTJLGynPRu6f/+XvpkmwbTDARFBhn70iOIkLENn5O2lmJQPiO9qQ+eVAURFjrGVP X-Received: by 2002:a65:43c9:: with SMTP id n9-v6mr5608742pgp.399.1527776925569; Thu, 31 May 2018 07:28:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527776925; cv=none; d=google.com; s=arc-20160816; b=CughhpNMxvE2mnmbdhomUaBZugH7qkpZlfiAx5BHvaaTbzE95WJjOTDUZoMQhedzIr oay6JR6YYLIq1D1FYQY+7Cu3jtDpMS61+6CpqyLZTN/8xn6Z1u+804UpxrD4nfxCnhLq PC9x+WBxyx6L7fP+ZTJdivDZ45ZLQIISpz//mfdYxPZ8pmN7LaS+3Yih1OtDavDr14Xa TWjnSFvkmh6WAGujYg5QHZgcqBYsH+dLkWvK4y0GTVoI+I/zVINLYFwh+appO3GvLQHG S8PA3Pourn80wXBfyC1JozsT87BS9lIkEPmCFlt9rrkXt/me00CdqQ+wsKJuNbu+/k+w MELQ== 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:arc-authentication-results; bh=4oo51UwLItSlvrAAdIdv06/X6dZChh7sNY/eMgY7oBQ=; b=PvrCm0aDRZpDQqHR3GE+ahaTIF36ml0QvKxLA2Bo/DWCl3X0OXIaGYU64g4Bqlrh8m NDCh1Xhbt2QFumi29dt1BynpYN1NnAM2QRjt2qt8XrCjogzzdeyztJ/DrMl+b7xcyMT+ 9j9I1NlVg0do20x6UOYzXMTkCqvpa6QiXCECq+8UsnsHTQqE2xmXgIIlObXkGYi+rNdJ gdoqA4XM3Nbe67OECsXcFf7cEps83qj/WlTEPpyr+lqUZEGLqaDzqBVLqSauIJOnwwQt JuqNN679ateQooZKDkbfR178DgAevQYH8iH3YVj0Xu16/AHz8tlc64hzi/30iW/Kw4/g 0QrA== 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 q4-v6si26977521pgc.43.2018.05.31.07.28.31; Thu, 31 May 2018 07:28:45 -0700 (PDT) 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 S1755468AbeEaO1i (ORCPT + 99 others); Thu, 31 May 2018 10:27:38 -0400 Received: from iolanthe.rowland.org ([192.131.102.54]:51418 "HELO iolanthe.rowland.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with SMTP id S1755459AbeEaO1e (ORCPT ); Thu, 31 May 2018 10:27:34 -0400 Received: (qmail 2339 invoked by uid 2102); 31 May 2018 10:27:33 -0400 Received: from localhost (sendmail-bs@127.0.0.1) by localhost with SMTP; 31 May 2018 10:27:33 -0400 Date: Thu, 31 May 2018 10:27:33 -0400 (EDT) From: Alan Stern X-X-Sender: stern@iolanthe.rowland.org To: "Paul E. McKenney" cc: Linus Torvalds , Linux Kernel Mailing List , linux-arch , , Will Deacon , Peter Zijlstra , Boqun Feng , Nick Piggin , David Howells , Jade Alglave , Luc Maranget , Akira Yokosawa , Ingo Molnar , Roman Pen Subject: Re: LKMM litmus test for Roman Penyaev's rcu-rr In-Reply-To: <20180530231441.GO7063@linux.vnet.ibm.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 Wed, 30 May 2018, Paul E. McKenney wrote: > On Wed, May 30, 2018 at 05:01:01PM -0500, Linus Torvalds wrote: > > On Wed, May 30, 2018 at 2:08 PM Alan Stern wrote: > > > > > > Indeed. The very first line Linus quoted in his first reply to me > > > (elided above) was: > > > > > > Putting this into herd would be extremely difficult, if not impossible, > > > because it involves analyzing code that was not executed. > > > > > > It should be clear from this that I was talking about herd. Not gcc or > > > real hardware. > > > > So what does herd actually work on? The source code or the executable, > > or a trace? > > The source code, that is, the source code of the litmus test. > There are definitions for the various Linux operations, partly within > the herd tool and partly in the linux.def file in tools/memory-model. > The problem we are having is nailing down control dependencies and > compiler optimizations. The bit about limiting control dependencies > through the end of "if" statement itself works well in a great many cases, > but this clearly is not one of them. > > > I found the herd paper, but I'm on the road helping my daughter in > > college move, and I don't have the background to skim the paper > > quickly and come up with the obvious answer, so I'l just ask. > > It is not a short learning curve. > > > Because I really think that from our memory model standpoint, we > > really do have the rule that > > > > load -> cond -> store > > > > is ordered - even if the store address and store data is in no way > > dependent on the load. The only thing that matters is that there's a > > conditional that is dependent on the load in between the load and the > > store. This is true for all the architectures supported by the Linux kernel. However, in the future it might not always hold. I can imagine that CPU designers would want to include an optimization that checks a conditional branch to see if it skips over only the following instruction (and the following instruction can't affect the flow of control); in that situation, they might decide there doesn't need to be a control dependency to future stores. Such an optimization would not violate the C11 memory model. Of course, this is purely theoretical. And if anybody does decide to try doing that, the memory-model people might scream at them so hard they change their minds. :-) ... > > But I don't know what level 'herd' works on. If it doesn't see > > compiler barriers (eg our own "barrier()" macro that literally is just > > that), only sees the generated code, then it really has no other > > information than what he compiler _happened_ to do - it doesn't know > > if the compiler did the store after the conditional because it *had* > > to do so, or whether it was just a random instruction scheduling > > decision. > > The 'herd' tool works on litmus-test source, and has almost no idea of > what compilers get up to. In this particular case, it would be better > off being even more ignorant of what compilers get up to. ;-) In more detail, herd analyzes the source code and constructs a set of all possible candidate executions. herd then checks each execution to see if it violates the rules of the memory model as expressed in the .bell and .cat files. If any of the non-violating executions satisfies the litmus test's final "exists" condition, herd reports that the test is allowed. The point here is that when herd checks any one particular execution, it pays attention _only_ to the statements which are part of that execution. Statements belonging to an untaken "if" branch are ignored completely. That's why I think it would be difficult to make herd do exactly what we want in this case. Alan