From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id D33DCC433EF for ; Tue, 1 Feb 2022 19:09:04 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S241933AbiBATJE (ORCPT ); Tue, 1 Feb 2022 14:09:04 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:34550 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S242319AbiBATJD (ORCPT ); Tue, 1 Feb 2022 14:09:03 -0500 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 7AB29C06173D; Tue, 1 Feb 2022 11:09:03 -0800 (PST) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 23FAD61620; Tue, 1 Feb 2022 19:09:03 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 4CBB3C340EB; Tue, 1 Feb 2022 19:09:02 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1643742542; bh=d3pFi42Uh3ZoFdVzy1yM36RhreXXwmQdUKKQ7KPWFzI=; h=Date:From:To:Cc:Subject:Reply-To:References:In-Reply-To:From; b=hPfZ+4Xa94+rgXV8WBlS0c28n+M3gWGwXNG1puqnSpIBaqnmBAYov/WNlHu3H2wlb i1df88jP5keXlqidDeSC5p82TICIw7/sagr/2FGivjZVf2SoZp5Xyy5PR3nu+3mYrL KXGlQUgMEq6iVICxDTdW4n8eSRNYXdZsXH4ablUb/PSqQsUTdEit/JlA/fJfNnmB7z dG5rRinunXHEFhKtGr+NHFEMbydTOSU9UWtxrwFIdvBJPrStmrgqa9aIaZqEj5Y6KU jMgdQoNfQ0um4uEhkmhaDyAxcfqh+WNVWpS3X4pP3XSeeT1bvKwdNTuL/IdSjD6rpZ PqqIVpJkFZtbA== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 180BA5C0326; Tue, 1 Feb 2022 11:09:02 -0800 (PST) Date: Tue, 1 Feb 2022 11:09:02 -0800 From: "Paul E. McKenney" To: Alan Stern Cc: Paul =?iso-8859-1?Q?Heidekr=FCger?= , Andrea Parri , Will Deacon , Peter Zijlstra , Boqun Feng , Nicholas Piggin , David Howells , Jade Alglave , Luc Maranget , Akira Yokosawa , Daniel Lustig , Joel Fernandes , =?iso-8859-1?Q?Bj=F6rn_T=F6pel?= , linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, Marco Elver , Charalampos Mainas , Pramod Bhatotia Subject: Re: [PATCH v2] tools/memory-model: Explain syntactic and semantic dependencies Message-ID: <20220201190902.GC4285@paulmck-ThinkPad-P17-Gen-1> Reply-To: paulmck@kernel.org References: MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: Precedence: bulk List-ID: X-Mailing-List: linux-arch@vger.kernel.org On Tue, Feb 01, 2022 at 02:00:08PM -0500, Alan Stern wrote: > Paul Heidekrüger pointed out that the Linux Kernel Memory Model > documentation doesn't mention the distinction between syntactic and > semantic dependencies. This is an important difference, because the > compiler can easily break dependencies that are only syntactic, not > semantic. > > This patch adds a few paragraphs to the LKMM documentation explaining > these issues and illustrating how they can matter. > > Suggested-by: Paul Heidekrüger > Signed-off-by: Alan Stern Very good, queued and pushed with Akira's Reviewed-by. Thank you all! Thanx, Paul > --- > > v2: Incorporate changes suggested by Paul McKenney, along with a few > other minor edits. > > > [as1970b] > > > tools/memory-model/Documentation/explanation.txt | 51 +++++++++++++++++++++++ > 1 file changed, 51 insertions(+) > > Index: usb-devel/tools/memory-model/Documentation/explanation.txt > =================================================================== > --- usb-devel.orig/tools/memory-model/Documentation/explanation.txt > +++ usb-devel/tools/memory-model/Documentation/explanation.txt > @@ -485,6 +485,57 @@ have R ->po X. It wouldn't make sense f > somehow on a value that doesn't get loaded from shared memory until > later in the code! > > +Here's a trick question: When is a dependency not a dependency? Answer: > +When it is purely syntactic rather than semantic. We say a dependency > +between two accesses is purely syntactic if the second access doesn't > +actually depend on the result of the first. Here is a trivial example: > + > + r1 = READ_ONCE(x); > + WRITE_ONCE(y, r1 * 0); > + > +There appears to be a data dependency from the load of x to the store > +of y, since the value to be stored is computed from the value that was > +loaded. But in fact, the value stored does not really depend on > +anything since it will always be 0. Thus the data dependency is only > +syntactic (it appears to exist in the code) but not semantic (the > +second access will always be the same, regardless of the value of the > +first access). Given code like this, a compiler could simply discard > +the value returned by the load from x, which would certainly destroy > +any dependency. (The compiler is not permitted to eliminate entirely > +the load generated for a READ_ONCE() -- that's one of the nice > +properties of READ_ONCE() -- but it is allowed to ignore the load's > +value.) > + > +It's natural to object that no one in their right mind would write > +code like the above. However, macro expansions can easily give rise > +to this sort of thing, in ways that often are not apparent to the > +programmer. > + > +Another mechanism that can lead to purely syntactic dependencies is > +related to the notion of "undefined behavior". Certain program > +behaviors are called "undefined" in the C language specification, > +which means that when they occur there are no guarantees at all about > +the outcome. Consider the following example: > + > + int a[1]; > + int i; > + > + r1 = READ_ONCE(i); > + r2 = READ_ONCE(a[r1]); > + > +Access beyond the end or before the beginning of an array is one kind > +of undefined behavior. Therefore the compiler doesn't have to worry > +about what will happen if r1 is nonzero, and it can assume that r1 > +will always be zero regardless of the value actually loaded from i. > +(If the assumption turns out to be wrong the resulting behavior will > +be undefined anyway, so the compiler doesn't care!) Thus the value > +from the load can be discarded, breaking the address dependency. > + > +The LKMM is unaware that purely syntactic dependencies are different > +from semantic dependencies and therefore mistakenly predicts that the > +accesses in the two examples above will be ordered. This is another > +example of how the compiler can undermine the memory model. Be warned. > + > > THE READS-FROM RELATION: rf, rfi, and rfe > -----------------------------------------