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 X-Spam-Level: X-Spam-Status: No, score=-6.9 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI, SIGNED_OFF_BY,SPF_HELO_NONE,SPF_PASS,URIBL_BLOCKED autolearn=no autolearn_force=no version=3.4.0 Received: from mail.kernel.org (mail.kernel.org [198.145.29.99]) by smtp.lore.kernel.org (Postfix) with ESMTP id 14AD7C4727D for ; Sun, 4 Oct 2020 21:07:53 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id CB0242078D for ; Sun, 4 Oct 2020 21:07:52 +0000 (UTC) Authentication-Results: mail.kernel.org; dkim=pass (1024-bit key) header.d=joelfernandes.org header.i=@joelfernandes.org header.b="s67vt7a3" Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1726583AbgJDVHw (ORCPT ); Sun, 4 Oct 2020 17:07:52 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:48460 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1726313AbgJDVHv (ORCPT ); Sun, 4 Oct 2020 17:07:51 -0400 Received: from mail-qk1-x741.google.com (mail-qk1-x741.google.com [IPv6:2607:f8b0:4864:20::741]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 384B2C0613CE for ; Sun, 4 Oct 2020 14:07:50 -0700 (PDT) Received: by mail-qk1-x741.google.com with SMTP id v123so9624592qkd.9 for ; Sun, 04 Oct 2020 14:07:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=joelfernandes.org; s=google; h=date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to; bh=AmeqHM8IDXYitzI0EgnxUl/gsEaL+uyJCislVPlifDE=; b=s67vt7a3tmBSv1ugGD6TFAB2dlUtTioftfBWuRfSttQFSfgkoH0YxA2QMINdkGwgBD ZB/m2NmL9E1Vmsq5y5sG9p0onnyzbu2dehbTkR08mFQ0+UNukbrRpl7aIWmk8LiNlp1T YCzXBwUnXDmfVh5t+5GQlD0Kq/fFEFf7T/dmY= 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=AmeqHM8IDXYitzI0EgnxUl/gsEaL+uyJCislVPlifDE=; b=ZX4rKfja00gtb5B/B/9haJsSr+UooKjMjvFVuSsgqseKl5rfby6VgnoOE+Xia+Sg8x TEyvi2ezVKPQKJlTwaR5dQ34De1Kp3/m5wREr4Nzogrs6m6YWF+mi54hmTNZKNrWsCkp c+rWGYwKYSaLk95DgNR1iWKXdbnMRj0h+OqW4bKgenC4t4pkqRc9UJeaRp0MCWoyi+Q2 5VqGzM1P++b2Ur9CccS6HsDCK9Cs3HhXP0TtpqYAZoDBVb/1ZUI6VawU2FojFVSqe70C Xb7zjNn4SSlm8yXxhvhWKtBwibEdJRuL5zXCszuCgBLmFPsY4ORnHfZYrsghaVN3IYe9 8gow== X-Gm-Message-State: AOAM532giDgZFv9bA8fhyKXlBdrv7m8cVBNObPiyUpszoXXfCXVGvO9b wRvXSwZAVeLRNtikX5HF42UJzQ== X-Google-Smtp-Source: ABdhPJzJGyxbqmB3t1IJ2AjZ1Lmr3ha2xRe6WYWMIDN3x1lfvpV07MJX/c0dksabjyquHYbmTL7AjQ== X-Received: by 2002:a05:620a:13e8:: with SMTP id h8mr11508033qkl.322.1601845669322; Sun, 04 Oct 2020 14:07:49 -0700 (PDT) Received: from localhost ([2620:15c:6:12:cad3:ffff:feb3:bd59]) by smtp.gmail.com with ESMTPSA id l25sm6410651qtf.18.2020.10.04.14.07.48 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 04 Oct 2020 14:07:48 -0700 (PDT) Date: Sun, 4 Oct 2020 17:07:47 -0400 From: joel@joelfernandes.org To: Alan Stern Cc: "Paul E. McKenney" , Akira Yokosawa , parri.andrea@gmail.com, will@kernel.org, peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, dlustig@nvidia.com, viro@zeniv.linux.org.uk, linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org Subject: Re: [PATCH] tools: memory-model: Document that the LKMM can easily miss control dependencies Message-ID: <20201004210747.GA4078883@google.com> References: <20201001045116.GA5014@paulmck-ThinkPad-P72> <20201001161529.GA251468@rowland.harvard.edu> <20201001213048.GF29330@paulmck-ThinkPad-P72> <20201003132212.GB318272@rowland.harvard.edu> <045c643f-6a70-dfdf-2b1e-f369a667f709@gmail.com> <20201003171338.GA323226@rowland.harvard.edu> <20201004014022.GA332600@rowland.harvard.edu> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20201004014022.GA332600@rowland.harvard.edu> Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Sat, Oct 03, 2020 at 09:40:22PM -0400, Alan Stern wrote: > Add a small section to the litmus-tests.txt documentation file for > the Linux Kernel Memory Model explaining that the memory model often > fails to recognize certain control dependencies. > > Suggested-by: Akira Yokosawa > Signed-off-by: Alan Stern Reviewed-by: Joel Fernandes (Google) thanks, - Joel > > --- > > tools/memory-model/Documentation/litmus-tests.txt | 17 +++++++++++++++++ > 1 file changed, 17 insertions(+) > > Index: usb-devel/tools/memory-model/Documentation/litmus-tests.txt > =================================================================== > --- usb-devel.orig/tools/memory-model/Documentation/litmus-tests.txt > +++ usb-devel/tools/memory-model/Documentation/litmus-tests.txt > @@ -946,6 +946,23 @@ Limitations of the Linux-kernel memory m > carrying a dependency, then the compiler can break that dependency > by substituting a constant of that value. > > + Conversely, LKMM sometimes doesn't recognize that a particular > + optimization is not allowed, and as a result, thinks that a > + dependency is not present (because the optimization would break it). > + The memory model misses some pretty obvious control dependencies > + because of this limitation. A simple example is: > + > + r1 = READ_ONCE(x); > + if (r1 == 0) > + smp_mb(); > + WRITE_ONCE(y, 1); > + > + There is a control dependency from the READ_ONCE to the WRITE_ONCE, > + even when r1 is nonzero, but LKMM doesn't realize this and thinks > + that the write may execute before the read if r1 != 0. (Yes, that > + doesn't make sense if you think about it, but the memory model's > + intelligence is limited.) > + > 2. Multiple access sizes for a single variable are not supported, > and neither are misaligned or partially overlapping accesses. >