From patchwork Thu Jan 5 01:09:49 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: "Paul E. McKenney" X-Patchwork-Id: 39273 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a5d:4e01:0:0:0:0:0 with SMTP id p1csp56815wrt; Wed, 4 Jan 2023 17:12:43 -0800 (PST) X-Google-Smtp-Source: AMrXdXtA7T8yWfYNzlSSiUjZX9aqzxVQPyglpKYq1d1LJYsqPV6+1OIMJHGLkxxkgP5E22LLasvY X-Received: by 2002:a17:902:7786:b0:192:7d96:570d with SMTP id o6-20020a170902778600b001927d96570dmr17695230pll.19.1672881163391; Wed, 04 Jan 2023 17:12:43 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1672881163; cv=none; d=google.com; s=arc-20160816; b=rIwWiHdeEKbbzY5sl/pWOv5xW1xGMTP+OHu059VdHARcg/8lI6x6846hLsYq2svQj3 +DCSeybZRYLn9kXM7633Cj5HoqdHSFhZFasr6Q56yW72EhjlxCKPQJ/4wTW9fETodN8p 0LUipyzqRg7AGQLaX7k/1W2fz+9YMdLtzsvUp5gpjjD/CZI0sdvBK0MXDsvLivYXKl2E FtuTIKfvw08GW55IEqnZoDfy29G9r3A8eiWGtr1st2z/3SzY8yu9N2o/4XKYyYTptNii dlCtajgv0lBAbDyaprGalUoHmo54ZzFwLl82SXNgVOTZLm/77wB4s8afC8eKPgZ9WP51 Oo4w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:content-transfer-encoding:mime-version :references:in-reply-to:message-id:date:subject:cc:to:from :dkim-signature; bh=Cb7yArdA19gc5Qcd5RPpNxelmNVX/ra3ytBl/iWBTXE=; b=H2XXfxdD7BKl1yqPLQDOEW+VJczlUK6gICQx4Ixf8PhZOye7JrY060kosGgU3CM54e ZDXkjy5cM2SzNEU826WN29QKSCTRC3F9J22eKH4IzZiyxHYVT5RPtrh7TXjtstoQ3GkD ZzZic8QetQfs4KIcidlMWQfpFdBOgNZZ+L2L7H9h0cVnFgh9zWibD5VeVI93CnOtHc6F /1uiTyHkmCdzDojPk6G88f0IHtT07mh3Rscr6m8KgI1eM/+bJRg/vNFVCRC5ZaitN40U nu05/6CStZNVQjHGL2DrKLt+PAIhx8knv5nVy5W0baG9PlT43IyZNlta+hhCztg6pqgY hFaw== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@kernel.org header.s=k20201202 header.b="N/wrTquJ"; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=kernel.org Received: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id b12-20020a170902bd4c00b001894d872b14si1596686plx.66.2023.01.04.17.12.30; Wed, 04 Jan 2023 17:12:43 -0800 (PST) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20; Authentication-Results: mx.google.com; dkim=pass header.i=@kernel.org header.s=k20201202 header.b="N/wrTquJ"; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S230097AbjAEBKW (ORCPT + 99 others); Wed, 4 Jan 2023 20:10:22 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:47770 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229839AbjAEBJ6 (ORCPT ); Wed, 4 Jan 2023 20:09:58 -0500 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 8765A3056A; Wed, 4 Jan 2023 17:09:57 -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 ams.source.kernel.org (Postfix) with ESMTPS id 1971AB81980; Thu, 5 Jan 2023 01:09:56 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id AB55FC433EF; Thu, 5 Jan 2023 01:09:54 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1672880994; bh=BWqPFUcOzk3zqc4HLeT1toRCy9Bsr94f5R2Iqirtebc=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=N/wrTquJO/00KnE4aRJv/uuk255e9SoNQo3kEftNS6bcXNTmMJwU4SLRUtEtsvPdX L+u1oK5mfuEVpwQuQ27KHy/KFEylNCmMI9lAAfA0JuFkZCnWBWZJ1BR9thARpyq5VJ sdThFfSlSalFjgjHb9wJkGQ3orPKgQV91McRyBvwcO2Ji9QQ+7tbwg4nv624yxtXpJ LPAhHa1VTdE6FAXxMXwtmiT209uYQ1KSXgZaGzyS3a0ZAbm3Til+fDuTsATfvWTVYm r/5jcPpIjUacqgzoGUhSdNvGNdImBGruPSwHOAAFN9LM+cTssuUlguazBGKQdMGusK f3/Fm0yLXboVw== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 62CEC5C05CA; Wed, 4 Jan 2023 17:09:54 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, kernel-team@meta.com, mingo@kernel.org Cc: stern@rowland.harvard.edu, 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, akiyks@gmail.com, Parav Pandit , "Paul E . McKenney" Subject: [PATCH memory-model 1/4] locking/memory-barriers.txt: Improve documentation for writel() example Date: Wed, 4 Jan 2023 17:09:49 -0800 Message-Id: <20230105010952.1774272-1-paulmck@kernel.org> X-Mailer: git-send-email 2.31.1.189.g2e36527f23 In-Reply-To: <20230105010944.GA1774169@paulmck-ThinkPad-P17-Gen-1> References: <20230105010944.GA1774169@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 X-Spam-Status: No, score=-7.1 required=5.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,RCVD_IN_DNSWL_HI, SPF_HELO_NONE,SPF_PASS autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on lindbergh.monkeyblade.net Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1754143039079749414?= X-GMAIL-MSGID: =?utf-8?q?1754143039079749414?= From: Parav Pandit The cited commit describes that when using writel(), explicit wmb() is not needed. wmb() is an expensive barrier. writel() uses the needed platform specific barrier instead of wmb(). writeX() section of "KERNEL I/O BARRIER EFFECTS" already describes ordering of I/O accessors with MMIO writes. Hence add the comment for pseudo code of writel() and remove confusing text around writel() and wmb(). commit 5846581e3563 ("locking/memory-barriers.txt: Fix broken DMA vs. MMIO ordering example") Co-developed-by: Will Deacon Signed-off-by: Will Deacon Signed-off-by: Parav Pandit Signed-off-by: Paul E. McKenney --- Documentation/memory-barriers.txt | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt index cc621decd9439..06e14efd8662a 100644 --- a/Documentation/memory-barriers.txt +++ b/Documentation/memory-barriers.txt @@ -1910,7 +1910,8 @@ There are some more advanced barrier functions: These are for use with consistent memory to guarantee the ordering of writes or reads of shared memory accessible to both the CPU and a - DMA capable device. + DMA capable device. See Documentation/core-api/dma-api.rst file for more + information about consistent memory. For example, consider a device driver that shares memory with a device and uses a descriptor status value to indicate if the descriptor belongs @@ -1931,22 +1932,21 @@ There are some more advanced barrier functions: /* assign ownership */ desc->status = DEVICE_OWN; - /* notify device of new descriptors */ + /* Make descriptor status visible to the device followed by + * notify device of new descriptor + */ writel(DESC_NOTIFY, doorbell); } - The dma_rmb() allows us guarantee the device has released ownership + The dma_rmb() allows us to guarantee that the device has released ownership before we read the data from the descriptor, and the dma_wmb() allows us to guarantee the data is written to the descriptor before the device can see it now has ownership. The dma_mb() implies both a dma_rmb() and - a dma_wmb(). Note that, when using writel(), a prior wmb() is not needed - to guarantee that the cache coherent memory writes have completed before - writing to the MMIO region. The cheaper writel_relaxed() does not provide - this guarantee and must not be used here. - - See the subsection "Kernel I/O barrier effects" for more information on - relaxed I/O accessors and the Documentation/core-api/dma-api.rst file for - more information on consistent memory. + a dma_wmb(). + + Note that the dma_*() barriers do not provide any ordering guarantees for + accesses to MMIO regions. See the later "KERNEL I/O BARRIER EFFECTS" + subsection for more information about I/O accessors and MMIO ordering. (*) pmem_wmb(); From patchwork Thu Jan 5 01:09:50 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: "Paul E. McKenney" X-Patchwork-Id: 39277 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a5d:4e01:0:0:0:0:0 with SMTP id p1csp57187wrt; Wed, 4 Jan 2023 17:13:51 -0800 (PST) X-Google-Smtp-Source: AMrXdXs+ErorENrTv/MPCH5SIt38fMDb7bm+LS2lPehURfDv7zIlzs+PjHTIMIFPA0yc1NexsshX X-Received: by 2002:a05:6a21:3944:b0:a3:754c:2769 with SMTP id ac4-20020a056a21394400b000a3754c2769mr60076623pzc.40.1672881231672; Wed, 04 Jan 2023 17:13:51 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1672881231; cv=none; d=google.com; s=arc-20160816; b=ZlwGuP5U82sT9HElb1BtgAwlYwA0hOzHQiYgbYNHDr3rFfkfhmyoXnqQEHT7AkeFoB XRZVD3e8CiRfI2Qko8HxuaN/wLPu1P/f/ptLvlwJzk/bpN1KTkxVNXPGf7Rmrl1XNSnq KHJv3Sk0LZdllcO3WNMdClGLt4OiJxcRwGthHLx2qip09Xfx9cuELBzZ7jsyCPTtLzE3 Pj2NguJnlTf3KhXoO8/cs8vYwKcjdzhv+8qbMTLVST9pbYDHjjMhj0G9oJaVH03R9xEd mv6OG5ggaD52CBVcIJAxaPWGDKy1hSyWqlOeMk4KnbtH8p1XQb/iYOV30TqoVHQdFq1i P19Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:content-transfer-encoding:mime-version :references:in-reply-to:message-id:date:subject:cc:to:from :dkim-signature; bh=wdXxg+dda2/7PU8BR/OgDOUhCPHIC6qt2xD9tOa54Uc=; b=1KOCCMEV001ADuSR6iEJKSI4JykKX4NreHz/yVpu9Zv+epx3cnR/TsT7FMib8xSba1 6b0+jSuBFfCr0yOJEy3xwhaXUkTCOJ9HXrrm8JVhP/XllAlFehCs82dyvw4VY1IRRRoo snTkQUpXCEDlEPDhtwEmuotCllJRajSjVn7cYHo49UQTztrvb2tFu9uzJLqnwEFjhTFb 1FN1KsszODIBOObF0BWY84/zvIw3GoWm4TmkYUxxXBkGj+Bbd0DpqWdgYz33wJVvsgF2 q45v4UsYrPkB5pqLcskZzOMeqioGBgMLFh2u8B53s9ql/WOR4wEOEtDy8/wCdigfllGU RoUA== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@kernel.org header.s=k20201202 header.b=RtAp4j8g; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=kernel.org Received: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id t8-20020a632248000000b00478f1cf941csi35566587pgm.358.2023.01.04.17.13.39; Wed, 04 Jan 2023 17:13:51 -0800 (PST) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20; Authentication-Results: mx.google.com; dkim=pass header.i=@kernel.org header.s=k20201202 header.b=RtAp4j8g; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S230262AbjAEBK0 (ORCPT + 99 others); Wed, 4 Jan 2023 20:10:26 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:44652 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229738AbjAEBJ6 (ORCPT ); Wed, 4 Jan 2023 20:09:58 -0500 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 55E4930571; Wed, 4 Jan 2023 17:09:57 -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 ams.source.kernel.org (Postfix) with ESMTPS id EBEF0B81982; Thu, 5 Jan 2023 01:09:55 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id A915DC433F0; Thu, 5 Jan 2023 01:09:54 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1672880994; bh=Jl/wA3obCQ6eP+HMrthbAFT6/bCzL6xUl5XhR4SNk5c=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=RtAp4j8g5wH01QrSdGedWr8TVWTjosN386/GaatyBP9EPwxuVUa0ZvQHTxXy7uJDn 1RlL4eU5IfHfWduKnd4ULOUmWDO8AekemMFuH4pP59dEbqAopYSxrO9ijrvfVmeq3f OcQVPidUI1LX1xx0oxBuQPTOCP9Awh8cjGXFCNk3gDC2J3ox8IkBddaUzG+MXLQjAA CFYzL/G/ZAqOOnN7E9eVuVcVd2bIoqN3X+ryJz6mg6Qu7R2HMkh7N97MZVwe47pRAd XnSYwNW7EuBG1CZqiiIT+fhJHPzftb9jmOPxFtEBKCLeJt4VqMb2Nvv0UG5hRQvH50 /AXa7YM7iWs4A== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 665A15C086D; Wed, 4 Jan 2023 17:09:54 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, kernel-team@meta.com, mingo@kernel.org Cc: stern@rowland.harvard.edu, 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, akiyks@gmail.com, Viktor Vafeiadis , Jonas Oberhauser , "Paul E . McKenney" Subject: [PATCH memory-model 2/4] tools: memory-model: Add rmw-sequences to the LKMM Date: Wed, 4 Jan 2023 17:09:50 -0800 Message-Id: <20230105010952.1774272-2-paulmck@kernel.org> X-Mailer: git-send-email 2.31.1.189.g2e36527f23 In-Reply-To: <20230105010944.GA1774169@paulmck-ThinkPad-P17-Gen-1> References: <20230105010944.GA1774169@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 X-Spam-Status: No, score=-7.1 required=5.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,RCVD_IN_DNSWL_HI, SPF_HELO_NONE,SPF_PASS autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on lindbergh.monkeyblade.net Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1754143110240248364?= X-GMAIL-MSGID: =?utf-8?q?1754143110240248364?= From: Alan Stern Viktor (as relayed by Jonas) has pointed out a weakness in the Linux Kernel Memory Model. Namely, the memory ordering properties of atomic operations are not monotonic: An atomic op with full-barrier semantics does not always provide ordering as strong as one with release-barrier semantics. The following litmus test illustrates the problem: -------------------------------------------------- C atomics-not-monotonic {} P0(int *x, atomic_t *y) { WRITE_ONCE(*x, 1); smp_wmb(); atomic_set(y, 1); } P1(atomic_t *y) { int r1; r1 = atomic_inc_return(y); } P2(int *x, atomic_t *y) { int r2; int r3; r2 = atomic_read(y); smp_rmb(); r3 = READ_ONCE(*x); } exists (2:r2=2 /\ 2:r3=0) -------------------------------------------------- The litmus test is allowed as shown with atomic_inc_return(), which has full-barrier semantics. But if the operation is changed to atomic_inc_return_release(), which only has release-barrier semantics, the litmus test is forbidden. Clearly this violates monotonicity. The reason is because the LKMM treats full-barrier atomic ops as if they were written: mb(); load(); store(); mb(); (where the load() and store() are the two parts of an atomic RMW op), whereas it treats release-barrier atomic ops as if they were written: load(); release_barrier(); store(); The difference is that here the release barrier orders the load part of the atomic op before the store part with A-cumulativity, whereas the mb()'s above do not. This means that release-barrier atomics can effectively extend the cumul-fence relation but full-barrier atomics cannot. To resolve this problem we introduce the rmw-sequence relation, representing an arbitrarily long sequence of atomic RMW operations in which each operation reads from the previous one, and explicitly allow it to extend cumul-fence. This modification of the memory model is sound; it holds for PPC because of B-cumulativity, it holds for TSO and ARM64 because of other-multicopy atomicity, and we can assume that atomic ops on all other architectures will be implemented so as to make it hold for them. For similar reasons we also allow rmw-sequence to extend the w-post-bounded relation, which is analogous to cumul-fence in some ways. Reported-by: Viktor Vafeiadis Signed-off-by: Alan Stern Reviewed-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney --- .../Documentation/explanation.txt | 30 +++++++++++++++++++ tools/memory-model/linux-kernel.cat | 5 ++-- 2 files changed, 33 insertions(+), 2 deletions(-) diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt index 11a1d2d4f681c..e901b47236c37 100644 --- a/tools/memory-model/Documentation/explanation.txt +++ b/tools/memory-model/Documentation/explanation.txt @@ -1007,6 +1007,36 @@ order. Equivalently, where the rmw relation links the read and write events making up each atomic update. This is what the LKMM's "atomic" axiom says. +Atomic rmw updates play one more role in the LKMM: They can form "rmw +sequences". An rmw sequence is simply a bunch of atomic updates where +each update reads from the previous one. Written using events, it +looks like this: + + Z0 ->rf Y1 ->rmw Z1 ->rf ... ->rf Yn ->rmw Zn, + +where Z0 is some store event and n can be any number (even 0, in the +degenerate case). We write this relation as: Z0 ->rmw-sequence Zn. +Note that this implies Z0 and Zn are stores to the same variable. + +Rmw sequences have a special property in the LKMM: They can extend the +cumul-fence relation. That is, if we have: + + U ->cumul-fence X -> rmw-sequence Y + +then also U ->cumul-fence Y. Thinking about this in terms of the +operational model, U ->cumul-fence X says that the store U propagates +to each CPU before the store X does. Then the fact that X and Y are +linked by an rmw sequence means that U also propagates to each CPU +before Y does. In an analogous way, rmw sequences can also extend +the w-post-bounded relation defined below in the PLAIN ACCESSES AND +DATA RACES section. + +(The notion of rmw sequences in the LKMM is similar to, but not quite +the same as, that of release sequences in the C11 memory model. They +were added to the LKMM to fix an obscure bug; without them, atomic +updates with full-barrier semantics did not always guarantee ordering +at least as strong as atomic updates with release-barrier semantics.) + THE PRESERVED PROGRAM ORDER RELATION: ppo ----------------------------------------- diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index d70315fddef6e..07f884f9b2bff 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -74,8 +74,9 @@ let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = (rfe ; [Marked])? ; r +let rmw-sequence = (rf ; rmw)* let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb | - po-unlock-lock-po) ; [Marked] + po-unlock-lock-po) ; [Marked] ; rmw-sequence let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked] @@ -174,7 +175,7 @@ let vis = cumul-fence* ; rfe? ; [Marked] ; let w-pre-bounded = [Marked] ; (addr | fence)? let r-pre-bounded = [Marked] ; (addr | nonrw-fence | ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))? -let w-post-bounded = fence? ; [Marked] +let w-post-bounded = fence? ; [Marked] ; rmw-sequence let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; [Marked] From patchwork Thu Jan 5 01:09:51 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: "Paul E. McKenney" X-Patchwork-Id: 39275 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a5d:4e01:0:0:0:0:0 with SMTP id p1csp56960wrt; Wed, 4 Jan 2023 17:13:14 -0800 (PST) X-Google-Smtp-Source: AMrXdXsoBU4UOQ8oKEwWNlmo2jfkB5be6xSs4n4N5R4/1e0q+dqoo/vsoF53XQqwFpMarpfqLGrp X-Received: by 2002:a05:6a21:1788:b0:ad:def6:af3 with SMTP id nx8-20020a056a21178800b000addef60af3mr64210284pzb.57.1672881193760; Wed, 04 Jan 2023 17:13:13 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1672881193; cv=none; d=google.com; s=arc-20160816; b=yzRaXQ7YKPCjfeIowWN2QiwljBxwkx8yLQ9wtCGB0mxgOxHEYgBFVyOJxvTNvAxcBy B+AZyeLiK2GVqxJ6G++20wzpRJ02kxx7YjFfPUpv0uCyu4s3YNKa4LXfnvIbtDgBHQmp KHq03bJ4He4Hhb9djGHNDeMrcVVN6aWQIyzKTay8NFwXC6WHdIrTG7XVR6kEZ4Cc0kk6 aK4sAG7skMxG57nGX96yWFYkseWXXeMqy5LvPg+lGtKz5W4ZF8JHO8AlWYBxZ+ZDf8a5 ZxsxPy0FblxvdCXL9JhLjsS9ZDY0NMGc9gDoSWDfX5ZVOzxZfL90EK9fNA8iZ5d4QZxJ aYXQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:content-transfer-encoding:mime-version :references:in-reply-to:message-id:date:subject:cc:to:from :dkim-signature; bh=iHSOwCSV3DQi8CPjYXo0i2mQfFhgvGoSUYSKDDBF5p4=; b=LQ6y1zk+SihjNpVy66Tpqt54R1+1u3zHNx4G7HxCpp18l4KW0lSgTtyMN8oVOLuZnM 82hcendd9YblfopVe8gN93cvHvcNanvp8pHqhq5y6yRDAR70N9o1w+umCqoEB0W+ZhCT 3l+ZKPzcYXeil99pbpqNDCeVTvBW03GkW3OZLlGegx2NdaGNTwiEQqYbQxCtDb/t8T41 hQCaSn03vc0sxiUBrDJv33hbkSF3SkGN+RdcaplJI/+V0EAKMVnwEm88UNGXQf8KeJ+0 SeS4oIwR7xUwUeI+Gyecog7tM+nCNpzOc/43vzpWQSn4D9+/aqKEgXCVn/MpM/BLNhGh 5E8g== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@kernel.org header.s=k20201202 header.b=U9fno5jy; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=kernel.org Received: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id k2-20020a654642000000b00476c8632d24si38878257pgr.686.2023.01.04.17.12.59; Wed, 04 Jan 2023 17:13:13 -0800 (PST) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20; Authentication-Results: mx.google.com; dkim=pass header.i=@kernel.org header.s=k20201202 header.b=U9fno5jy; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S230247AbjAEBKQ (ORCPT + 99 others); Wed, 4 Jan 2023 20:10:16 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:45384 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229508AbjAEBJ6 (ORCPT ); Wed, 4 Jan 2023 20:09:58 -0500 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 4BE0D3056B; Wed, 4 Jan 2023 17:09:57 -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 ams.source.kernel.org (Postfix) with ESMTPS id E5E2FB8167B; Thu, 5 Jan 2023 01:09:55 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id A6E43C433D2; Thu, 5 Jan 2023 01:09:54 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1672880994; bh=3rJgk+HG3HzNQPwHWGNkSihqjzUP/qOuNtY986a0YCo=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=U9fno5jye6FHCf9BozocTVBaOLVQo/x18qjtP3hvOHxWo0EC6ocdc9yS/n5st0t02 //8sZKTyq/IP3xb+IhEtbVLY/U0YrA450JAU+5/03lexxSYPvFP/FUQHvlBKWLitKR 3hpVjkhhOHex3YyP77t088rJ0mQARUhbSwfNHXYM6Bx1j4bE8NraWMMMbQf4xqBnvg P+5w5K7cbVmGhafHR+96gPYE+lDxcXQcLiMNQAntmZvYoJMoK42k2KZEMNdWN37hUl iPxFPPfX4ngmRWTEVkuwH/IvQIRz+h1Y8FrU8Zvi5Tt8nopEyP5u4qFWCk+pJAVi2f W+FEOTJAuAxbg== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 685395C08E5; Wed, 4 Jan 2023 17:09:54 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, kernel-team@meta.com, mingo@kernel.org Cc: stern@rowland.harvard.edu, 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, akiyks@gmail.com, Kushagra Verma , "Paul E . McKenney" Subject: [PATCH memory-model 3/4] Documentation: Fixed a typo in atomic_t.txt Date: Wed, 4 Jan 2023 17:09:51 -0800 Message-Id: <20230105010952.1774272-3-paulmck@kernel.org> X-Mailer: git-send-email 2.31.1.189.g2e36527f23 In-Reply-To: <20230105010944.GA1774169@paulmck-ThinkPad-P17-Gen-1> References: <20230105010944.GA1774169@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 X-Spam-Status: No, score=-7.1 required=5.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,RCVD_IN_DNSWL_HI, SPF_HELO_NONE,SPF_PASS autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on lindbergh.monkeyblade.net Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1754143070684281678?= X-GMAIL-MSGID: =?utf-8?q?1754143070684281678?= From: Kushagra Verma Fixed a typo in the word 'architecture'. Signed-off-by: Kushagra Verma Signed-off-by: Paul E. McKenney --- Documentation/atomic_t.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Documentation/atomic_t.txt b/Documentation/atomic_t.txt index 0f1ffa03db09a..d7adc6d543db4 100644 --- a/Documentation/atomic_t.txt +++ b/Documentation/atomic_t.txt @@ -324,7 +324,7 @@ atomic operations. Specifically 'simple' cmpxchg() loops are expected to not starve one another indefinitely. However, this is not evident on LL/SC architectures, because -while an LL/SC architecure 'can/should/must' provide forward progress +while an LL/SC architecture 'can/should/must' provide forward progress guarantees between competing LL/SC sections, such a guarantee does not transfer to cmpxchg() implemented using LL/SC. Consider: From patchwork Thu Jan 5 01:09:52 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: "Paul E. McKenney" X-Patchwork-Id: 39272 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a5d:4e01:0:0:0:0:0 with SMTP id p1csp56754wrt; Wed, 4 Jan 2023 17:12:34 -0800 (PST) X-Google-Smtp-Source: AMrXdXvvD9I7b7DhHA4wTdrR50NyPjtPN1ICLa9a3PRsz8OehAIOhM8IcqX3Y47f0+Y70GM/OtfK X-Received: by 2002:a17:90b:4c46:b0:226:7e0a:1cc3 with SMTP id np6-20020a17090b4c4600b002267e0a1cc3mr11764330pjb.46.1672881154577; Wed, 04 Jan 2023 17:12:34 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1672881154; cv=none; d=google.com; s=arc-20160816; b=EDBNMza0WP4vdJn9X4CNLBkTJT0oRxeo2CyccCMIiD/FHdkAtF5HasmK6ev8gE87to MCQOEjEmkoM4bPx0DIwR2FoRiSJ9EDdpCjLsXRZvnDFh8PXukv0Q22u8yWu0NR9z2y0N qBNRrn3QU0nXQ8M1WfiLJOw0EehcyjjVfXhMFPqaCvHLz26qfGdEnZU/puWOivFB6jgH 2tNdNKBPmm/dNd4AiX9JPYox6P02GMw4J4URCOjyVyh8c0WoF1OV8TSfDTre7nlHHOT6 6I8rPB3k+77aaaqb1ENE3NMCB6tT//Cij7CPqxWIPqGto4f2v2yBSDQJuKThfi32096U /s7Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:content-transfer-encoding:mime-version :references:in-reply-to:message-id:date:subject:cc:to:from :dkim-signature; bh=Men4kcv7CyPFt7vrH8WuDU4zOvNNE/d7XLFIFpuNvpg=; b=PpAbHETYAAbnBEckhuRONbTEW1mMQoUx3wwAGlbsCVUEeurBygje1hABWxx7o2I30T 0QNnVOH2KNYjnKYS0dq2k3GyAu6OwWfa4sZUi7f7vWRKfKkoVpXns+TMyqckOwhzcues rOdjDOUhuVSj+OF+bxPkgkQqDH1CFkcn6eFfg1cyAy17KKmJmuduSiF8MVxXCv9IUAjj j3pdKEegLmUZMuS2dxibQVa/5SrLl2MbQ9I6Mo7Bl24e4XYdKEaLIGIgL4i9IPLqahR0 Lx5FVxretk7qMj+/QQKoOpmgmxZLnut2veVNloIh7Hy+eSCyLnneR11aMK70u/KxOY3R TaNQ== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@kernel.org header.s=k20201202 header.b=tbbN3Q9O; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=kernel.org Received: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id ls6-20020a17090b350600b002191b3c187csi456621pjb.165.2023.01.04.17.12.16; Wed, 04 Jan 2023 17:12:34 -0800 (PST) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20; Authentication-Results: mx.google.com; dkim=pass header.i=@kernel.org header.s=k20201202 header.b=tbbN3Q9O; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S230180AbjAEBKM (ORCPT + 99 others); Wed, 4 Jan 2023 20:10:12 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:45398 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229479AbjAEBJ4 (ORCPT ); Wed, 4 Jan 2023 20:09:56 -0500 Received: from dfw.source.kernel.org (dfw.source.kernel.org [139.178.84.217]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id BC6DB3055B; Wed, 4 Jan 2023 17:09:55 -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 56EEE618AC; Thu, 5 Jan 2023 01:09:55 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id AD816C433F2; Thu, 5 Jan 2023 01:09:54 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1672880994; bh=DOted7FBYHC/UPK1yKry17PYXPvfX+1xx0FRT1Pw04k=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=tbbN3Q9ODnFr8TGowjXzWOf/gkFS419mGtPPY5Hjt/Vxev8cmZg5PiiDgGXA3I2zj HQCrglp0a9yosw/quelj6HpZb5xQ14DKuB5DAzYU6jO4yfwKqfHYuRB84tt9Xrzd+5 rrA8YWnjqPH1LhygLystDV5zUbjUeDgYSY1prwkcHheNwuGjubzyRDr+wLZipa5rJZ bUw0ZMWNwipfTJY4KSsMbEZVfzz8+bGmIVssiSpnNfc+n0pEBKgONAnZvafIl4I7Z1 FTmZwVQxz8UX3IzzFAFXuC+bfV8ZfeT9QDydmnvqz4dy1r1W5mBHKnTgT+jUAnJgE5 3j/tLBGBOdeTA== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 6A90B5C1456; Wed, 4 Jan 2023 17:09:54 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, kernel-team@meta.com, mingo@kernel.org Cc: stern@rowland.harvard.edu, 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, akiyks@gmail.com, Jonas Oberhauser , Viktor Vafeiadis , "Paul E . McKenney" Subject: [PATCH memory-model 4/4] tools: memory-model: Make plain accesses carry dependencies Date: Wed, 4 Jan 2023 17:09:52 -0800 Message-Id: <20230105010952.1774272-4-paulmck@kernel.org> X-Mailer: git-send-email 2.31.1.189.g2e36527f23 In-Reply-To: <20230105010944.GA1774169@paulmck-ThinkPad-P17-Gen-1> References: <20230105010944.GA1774169@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 X-Spam-Status: No, score=-7.1 required=5.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,RCVD_IN_DNSWL_HI, SPF_HELO_NONE,SPF_PASS autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on lindbergh.monkeyblade.net Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1754143029003650957?= X-GMAIL-MSGID: =?utf-8?q?1754143029003650957?= From: Jonas Oberhauser As reported by Viktor, plain accesses in LKMM are weaker than accesses to registers: the latter carry dependencies but the former do not. This is exemplified in the following snippet: int r = READ_ONCE(*x); WRITE_ONCE(*y, r); Here a data dependency links the READ_ONCE() to the WRITE_ONCE(), preserving their order, because the model treats r as a register. If r is turned into a memory location accessed by plain accesses, however, the link is broken and the order between READ_ONCE() and WRITE_ONCE() is no longer preserved. This is too conservative, since any optimizations on plain accesses that might break dependencies are also possible on registers; it also contradicts the intuitive notion of "dependency" as the data stored by the WRITE_ONCE() does depend on the data read by the READ_ONCE(), independently of whether r is a register or a memory location. This is resolved by redefining all dependencies to include dependencies carried by memory accesses; a dependency is said to be carried by memory accesses (in the model: carry-dep) from one load to another load if the initial load is followed by an arbitrarily long sequence alternating between stores and loads of the same thread, where the data of each store depends on the previous load, and is read by the next load. Any dependency linking the final load in the sequence to another access also links the initial load in the sequence to that access. More deep details can be found in this LKML discussion: https://lore.kernel.org/lkml/d86295788ad14a02874ab030ddb8a6f8@huawei.com/ Reported-by: Viktor Vafeiadis Signed-off-by: Jonas Oberhauser Reviewed-by: Alan Stern Signed-off-by: Paul E. McKenney --- .../Documentation/explanation.txt | 9 +++++- tools/memory-model/linux-kernel.bell | 6 ++++ .../litmus-tests/dep+plain.litmus | 31 +++++++++++++++++++ 3 files changed, 45 insertions(+), 1 deletion(-) create mode 100644 tools/memory-model/litmus-tests/dep+plain.litmus diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt index e901b47236c37..8e70852384709 100644 --- a/tools/memory-model/Documentation/explanation.txt +++ b/tools/memory-model/Documentation/explanation.txt @@ -2575,7 +2575,7 @@ smp_store_release() -- which is basically how the Linux kernel treats them. Although we said that plain accesses are not linked by the ppo -relation, they do contribute to it indirectly. Namely, when there is +relation, they do contribute to it indirectly. Firstly, when there is an address dependency from a marked load R to a plain store W, followed by smp_wmb() and then a marked store W', the LKMM creates a ppo link from R to W'. The reasoning behind this is perhaps a little @@ -2584,6 +2584,13 @@ for this source code in which W' could execute before R. Just as with pre-bounding by address dependencies, it is possible for the compiler to undermine this relation if sufficient care is not taken. +Secondly, plain accesses can carry dependencies: If a data dependency +links a marked load R to a store W, and the store is read by a load R' +from the same thread, then the data loaded by R' depends on the data +loaded originally by R. Thus, if R' is linked to any access X by a +dependency, R is also linked to access X by the same dependency, even +if W' or R' (or both!) are plain. + There are a few oddball fences which need special treatment: smp_mb__before_atomic(), smp_mb__after_atomic(), and smp_mb__after_spinlock(). The LKMM uses fence events with special diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 5be86b1025e8d..70a9073dec3e5 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -82,3 +82,9 @@ flag ~empty different-values(srcu-rscs) as srcu-bad-nesting let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | LKR | LKW | UL | LF | RL | RU let Plain = M \ Marked + +(* Redefine dependencies to include those carried through plain accesses *) +let carry-dep = (data ; rfi)* +let addr = carry-dep ; addr +let ctrl = carry-dep ; ctrl +let data = carry-dep ; data diff --git a/tools/memory-model/litmus-tests/dep+plain.litmus b/tools/memory-model/litmus-tests/dep+plain.litmus new file mode 100644 index 0000000000000..ebf84daa9a590 --- /dev/null +++ b/tools/memory-model/litmus-tests/dep+plain.litmus @@ -0,0 +1,31 @@ +C dep+plain + +(* + * Result: Never + * + * This litmus test demonstrates that in LKMM, plain accesses + * carry dependencies much like accesses to registers: + * The data stored to *z1 and *z2 by P0() originates from P0()'s + * READ_ONCE(), and therefore using that data to compute the + * conditional of P0()'s if-statement creates a control dependency + * from that READ_ONCE() to P0()'s WRITE_ONCE(). + *) + +{} + +P0(int *x, int *y, int *z1, int *z2) +{ + int a = READ_ONCE(*x); + *z1 = a; + *z2 = *z1; + if (*z2 == 1) + WRITE_ONCE(*y, 1); +} + +P1(int *x, int *y) +{ + int r = smp_load_acquire(y); + smp_store_release(x, r); +} + +exists (x=1 /\ y=1)