From patchwork Thu Jan 26 13:46:03 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Jonas Oberhauser X-Patchwork-Id: 48660 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:adf:eb09:0:0:0:0:0 with SMTP id s9csp278327wrn; Thu, 26 Jan 2023 05:49:26 -0800 (PST) X-Google-Smtp-Source: AMrXdXv0FOI7PK2ErkjMH7Dxug2bY6dk9zTijvqkpTdwFFSJH7rGI7B8IdbS7ygvnOXhQdVPXUgB X-Received: by 2002:a17:907:2b01:b0:877:6e09:468d with SMTP id gc1-20020a1709072b0100b008776e09468dmr24614229ejc.7.1674740966808; Thu, 26 Jan 2023 05:49:26 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1674740966; cv=none; d=google.com; s=arc-20160816; b=AkzfKq7N6SohzMgD5yzYagCJvjZLeOLtHu2hfUK4LIna1LzMmxmuqST01Dk9XcpH8W 51rInLfZkRPFUmgSuDnpJo40xkKy9oIbVX5RaHKQGRLhArzwdJilwLjLDATEW/uJW0UF 8/zjQccbEhFRHRBAQ+0q/ljDl+bResLdJpFshSUxduRwRuetJYW31CZMvgYTq1Af15Nk FoDbI7feDhkcolj9qiSP8bHbai9OfOUuwfPn2+TlddjvZUJ6OrStjdQDfh/YETOWMKek eCjBPTrkaTFJkQ2ctU67MVbBeDLL+UN9VTy08fiPn0uKTFxUnHGMErLBjZU1miOJNnZT uzlw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:references:in-reply-to:message-id:date:subject :cc:to:from; bh=b0Y4sz9ibn8pk+u8gCubAcrENbu66W4TmJCWNoE8/Og=; b=oINaJAnE2OsGDyAF+l6eC+IK3cWYlV7H0tyNmurAD6JkkbMrTyv9fgMaWP3X+WYMBX sABQVvkHK+5h00XNVxicItp4DgkayQ5HzS+/a2Idkovrvv4isMepzOyohas6fb+J5UM0 6uEq/sWo07AOgO9tDRh83J27nXU8xOKlVEml5EQQ7uOwqU2q2FrN0YfssYKpxMvoUcpY 8IXApAD1iNHDHVCNqWhmPOi7EQakf0qp98F+uAzkke2S8sZ5BWZEalzvHqn70EsOazTo XQi6CpLJm4LE6yT2ZgQqImk3MBBWzv+iArLhja00/4I1syx9WaK42OuZcOr8WHuN5Fkh xQZg== ARC-Authentication-Results: i=1; mx.google.com; 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 Received: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id hw19-20020a170907a0d300b007b8b7da6480si1153569ejc.659.2023.01.26.05.49.03; Thu, 26 Jan 2023 05:49:26 -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; 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 Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S231923AbjAZNml (ORCPT + 99 others); Thu, 26 Jan 2023 08:42:41 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:54464 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S231641AbjAZNme (ORCPT ); Thu, 26 Jan 2023 08:42:34 -0500 Received: from frasgout12.his.huawei.com (frasgout12.his.huawei.com [14.137.139.154]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 0C4FE6DFC3 for ; Thu, 26 Jan 2023 05:42:17 -0800 (PST) Received: from mail02.huawei.com (unknown [172.18.147.229]) by frasgout12.his.huawei.com (SkyGuard) with ESMTP id 4P2hWN2TYMz9v7cJ for ; Thu, 26 Jan 2023 21:34:08 +0800 (CST) Received: from huaweicloud.com (unknown [10.206.133.88]) by APP2 (Coremail) with SMTP id GxC2BwBnOWAOg9JjSrPJAA--.522S3; Thu, 26 Jan 2023 14:41:53 +0100 (CET) From: Jonas Oberhauser To: paulmck@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, dlustig@nvidia.com, joel@joelfernandes.org, urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org, linux-kernel@vger.kernel.org, Jonas Oberhauser Subject: [PATCH v2 1/2] tools/memory-model: Unify UNLOCK+LOCK pairings to po-unlock-lock-po Date: Thu, 26 Jan 2023 14:46:03 +0100 Message-Id: <20230126134604.2160-2-jonas.oberhauser@huaweicloud.com> X-Mailer: git-send-email 2.17.1 In-Reply-To: <20230126134604.2160-1-jonas.oberhauser@huaweicloud.com> References: <20230126134604.2160-1-jonas.oberhauser@huaweicloud.com> X-CM-TRANSID: GxC2BwBnOWAOg9JjSrPJAA--.522S3 X-Coremail-Antispam: 1UD129KBjvJXoWxAr47ZrW7Xw4DWr1rtryDAwb_yoWrZrW8pr Wqgw45Kr4qyr1ku3Z7Ww45ZF4fCa1fGryrArsrZwn8Aa45Xr4xur1UKrWYq3srGrn7uFWq vF4jvas8Cr1kAaDanT9S1TB71UUUUU7qnTZGkaVYY2UrUUUUjbIjqfuFe4nvWSU5nxnvy2 9KBjDU0xBIdaVrnRJUUUBE14x267AKxVWrJVCq3wAFc2x0x2IEx4CE42xK8VAvwI8IcIk0 rVWrJVCq3wAFIxvE14AKwVWUJVWUGwA2048vs2IY020E87I2jVAFwI0_Jr4l82xGYIkIc2 x26xkF7I0E14v26r4j6ryUM28lY4IEw2IIxxk0rwA2F7IY1VAKz4vEj48ve4kI8wA2z4x0 Y4vE2Ix0cI8IcVAFwI0_Jr0_JF4l84ACjcxK6xIIjxv20xvEc7CjxVAFwI0_Gr0_Cr1l84 ACjcxK6I8E87Iv67AKxVW8JVWxJwA2z4x0Y4vEx4A2jsIEc7CjxVAFwI0_Gr1j6F4UJwAS 0I0E0xvYzxvE52x082IY62kv0487Mc02F40EFcxC0VAKzVAqx4xG6I80ewAv7VC0I7IYx2 IY67AKxVWUGVWUXwAv7VC2z280aVAFwI0_Jr0_Gr1lOx8S6xCaFVCjc4AY6r1j6r4UM4x0 Y48IcxkI7VAKI48JM4x0x7Aq67IIx4CEVc8vx2IErcIFxwACI402YVCY1x02628vn2kIc2 xKxwCF04k20xvY0x0EwIxGrwCFx2IqxVCFs4IE7xkEbVWUJVW8JwC20s026c02F40E14v2 6r1j6r18MI8I3I0E7480Y4vE14v26r106r1rMI8E67AF67kF1VAFwI0_GFv_WrylIxkGc2 Ij64vIr41lIxAIcVC0I7IYx2IY67AKxVWUJVWUCwCI42IY6xIIjxv20xvEc7CjxVAFwI0_ Gr0_Cr1lIxAIcVCF04k26cxKx2IYs7xG6r1j6r1xMIIF0xvEx4A2jsIE14v26r1j6r4UMI IF0xvEx4A2jsIEc7CjxVAFwI0_Gr0_Gr1UYxBIdaVFxhVjvjDU0xZFpf9x0JUSYLPUUUUU = X-CM-SenderInfo: 5mrqt2oorev25kdx2v3u6k3tpzhluzxrxghudrp/ X-CFilter-Loop: Reflected X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,SPF_HELO_NONE, SPF_NONE 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?1756093184055378194?= X-GMAIL-MSGID: =?utf-8?q?1756093184055378194?= LKMM uses two relations for talking about UNLOCK+LOCK pairings: 1) po-unlock-lock-po, which handles UNLOCK+LOCK pairings on the same CPU or immediate lock handovers on the same lock variable 2) po;[UL];(co|po);[LKW];po, which handles UNLOCK+LOCK pairs literally as described in rcupdate.h#L1002, i.e., even after a sequence of handovers on the same lock variable. The latter relation is used only once, to provide the guarantee defined in rcupdate.h#L1002 by smp_mb__after_unlock_lock(), which makes any UNLOCK+LOCK pair followed by the fence behave like a full barrier. This patch drops this use in favor of using po-unlock-lock-po everywhere, which unifies the way the model talks about UNLOCK+LOCK pairings. At first glance this seems to weaken the guarantee given by LKMM: When considering a long sequence of lock handovers such as below, where P0 hands the lock to P1, which hands it to P2, which finally executes such an after_unlock_lock fence, the mb relation currently links any stores in the critical section of P0 to instructions P2 executes after its fence, but not so after the patch. P0(int *x, int *y, spinlock_t *mylock) { spin_lock(mylock); WRITE_ONCE(*x, 2); spin_unlock(mylock); WRITE_ONCE(*y, 1); } P1(int *y, int *z, spinlock_t *mylock) { int r0 = READ_ONCE(*y); // reads 1 spin_lock(mylock); spin_unlock(mylock); WRITE_ONCE(*z,1); } P2(int *z, int *d, spinlock_t *mylock) { int r1 = READ_ONCE(*z); // reads 1 spin_lock(mylock); spin_unlock(mylock); smp_mb__after_unlock_lock(); WRITE_ONCE(*d,1); } P3(int *x, int *d) { WRITE_ONCE(*d,2); smp_mb(); WRITE_ONCE(*x,1); } exists (1:r0=1 /\ 2:r1=1 /\ x=2 /\ d=2) Nevertheless, the ordering guarantee given in rcupdate.h is actually not weakened. This is because the unlock operations along the sequence of handovers are A-cumulative fences. They ensure that any stores that propagate to the CPU performing the first unlock operation in the sequence must also propagate to every CPU that performs a subsequent lock operation in the sequence. Therefore any such stores will also be ordered correctly by the fence even if only the final handover is considered a full barrier. Indeed this patch does not affect the behaviors allowed by LKMM at all. The mb relation is used to define ordering through: 1) mb/.../ppo/hb, where the ordering is subsumed by hb+ where the lock-release, rfe, and unlock-acquire orderings each provide hb 2) mb/strong-fence/cumul-fence/prop, where the rfe and A-cumulative lock-release orderings simply add more fine-grained cumul-fence edges to substitute a single strong-fence edge provided by a long lock handover sequence 3) mb/strong-fence/pb and various similar uses in the definition of data races, where as discussed above any long handover sequence can be turned into a sequence of cumul-fence edges that provide the same ordering. Signed-off-by: Jonas Oberhauser Reviewed-by: Alan Stern --- tools/memory-model/linux-kernel.cat | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 07f884f9b2bf..6e531457bb73 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -37,8 +37,19 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) +(* + * Note: The po-unlock-lock-po relation only passes the lock to the direct + * successor, perhaps giving the impression that the ordering of the + * smp_mb__after_unlock_lock() fence only affects a single lock handover. + * However, in a longer sequence of lock handovers, the implicit + * A-cumulative release fences of lock-release ensure that any stores that + * propagate to one of the involved CPUs before it hands over the lock to + * the next CPU will also propagate to the final CPU handing over the lock + * to the CPU that executes the fence. Therefore, all those stores are + * also affected by the fence. + *) + ([M] ; po-unlock-lock-po ; + [After-unlock-lock] ; po ; [M]) let gp = po ; [Sync-rcu | Sync-srcu] ; po? let strong-fence = mb | gp From patchwork Thu Jan 26 13:46:04 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Jonas Oberhauser X-Patchwork-Id: 48661 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:adf:eb09:0:0:0:0:0 with SMTP id s9csp278397wrn; Thu, 26 Jan 2023 05:49:36 -0800 (PST) X-Google-Smtp-Source: AMrXdXuZuU02TsDiae1BAb70bPs5BBvjqfu/+c+SkPD6wavo6UQsQaRHQeum3k919p+gfi0ou+S5 X-Received: by 2002:a05:6402:44:b0:497:233d:3ef6 with SMTP id f4-20020a056402004400b00497233d3ef6mr36120904edu.17.1674740976339; Thu, 26 Jan 2023 05:49:36 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1674740976; cv=none; d=google.com; s=arc-20160816; b=Lfj+JTN33Xpuew78lrp3dtoffdnqDIqDbn+fUhWPNfa4ZXqiKmgN4YY7rOue753oD9 MlKRJ7o/jgubswJ4avuOTszSP/TZftyNPgQFn66l3aJte4392fTQ8s2wDtJdV/dUA+Bf HsyGSWMVZXd9gqG0fOvxULXhwZOClxl+aem0ZGDkIps6dRpOjRVcdxJh674jFlyhoL1b xlC/TObCGgrNzfK4mwkpLxUR5TOVGne5vtlo4DOX2M8HoMhEXxI7jdESf8pEcEJKqf5S ivHlUj5Wn237Flrca8mLtuPSwXVK1V1mrtH/d4/GsNgoQKaBdhgP3+IIjWqU4m7gLHH8 s2uA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:references:in-reply-to:message-id:date:subject :cc:to:from; bh=KL4oPQ3Zd1CCKdQBWgvmrYOhqL5VnPtk6M0OuLdqQl0=; b=l2ijvrRAEuh17kCrbHzXU2BSeeY7sgkLmCCm3TsbCZytSpu0UnIqzqQL5o4pwCe980 4EKNN553gBC3pg2RzG7WLySXJkWdDWSt/OF9e5/3Liq9nIQi8we0XOdGaqMRV2yf7Nh4 Mw+B1FEQlQryGEeesass6zIW9NtqVk2vXUATz6hTO/su9JIIvItPcxAV/rwWJOYoczLo kJlXljyPXT4u20Ryf+2In7akuI28OL9mEea2K+0jIiqJ6lSSSrKGiS/7Ncwi0XlJh63Q Al6/G1CXAus/Ag/UfJuFQAVbAxILXhnGgYpXohBJiu8nAp0Zt+lyI3JSUgdbtynaHV6m 6Hyg== ARC-Authentication-Results: i=1; mx.google.com; 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 Received: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id o15-20020aa7d3cf000000b004a0901f70f0si1654523edr.581.2023.01.26.05.49.06; Thu, 26 Jan 2023 05:49:36 -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; 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 Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S232123AbjAZNmu (ORCPT + 99 others); Thu, 26 Jan 2023 08:42:50 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:54570 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S231590AbjAZNmk (ORCPT ); Thu, 26 Jan 2023 08:42:40 -0500 Received: from frasgout11.his.huawei.com (frasgout11.his.huawei.com [14.137.139.23]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id E07506DFF0 for ; Thu, 26 Jan 2023 05:42:26 -0800 (PST) Received: from mail02.huawei.com (unknown [172.18.147.229]) by frasgout11.his.huawei.com (SkyGuard) with ESMTP id 4P2hWf2L9wz9v7gZ for ; Thu, 26 Jan 2023 21:34:22 +0800 (CST) Received: from huaweicloud.com (unknown [10.206.133.88]) by APP2 (Coremail) with SMTP id GxC2BwBnOWAOg9JjSrPJAA--.522S4; Thu, 26 Jan 2023 14:42:02 +0100 (CET) From: Jonas Oberhauser To: paulmck@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, dlustig@nvidia.com, joel@joelfernandes.org, urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org, linux-kernel@vger.kernel.org, Jonas Oberhauser Subject: [PATCH v2 2/2] tools/memory-model: Make ppo a subrelation of po Date: Thu, 26 Jan 2023 14:46:04 +0100 Message-Id: <20230126134604.2160-3-jonas.oberhauser@huaweicloud.com> X-Mailer: git-send-email 2.17.1 In-Reply-To: <20230126134604.2160-1-jonas.oberhauser@huaweicloud.com> References: <20230126134604.2160-1-jonas.oberhauser@huaweicloud.com> X-CM-TRANSID: GxC2BwBnOWAOg9JjSrPJAA--.522S4 X-Coremail-Antispam: 1UD129KBjvJXoW7ZF48GrWDJryktw1UKr4kJFb_yoW5JrW3pr y0k343KF4UtrsY93ZrW3ZxuF1UCa1xKw18GF4DAw1rAw13WFZFvF18trs8Wa4aqrZ7GFWD Zr1Yvrn2yayDAFJanT9S1TB71UUUUU7qnTZGkaVYY2UrUUUUjbIjqfuFe4nvWSU5nxnvy2 9KBjDU0xBIdaVrnRJUUUP014x267AKxVWrJVCq3wAFc2x0x2IEx4CE42xK8VAvwI8IcIk0 rVWrJVCq3wAFIxvE14AKwVWUJVWUGwA2048vs2IY020E87I2jVAFwI0_Jryl82xGYIkIc2 x26xkF7I0E14v26ryj6s0DM28lY4IEw2IIxxk0rwA2F7IY1VAKz4vEj48ve4kI8wA2z4x0 Y4vE2Ix0cI8IcVAFwI0_JFI_Gr1l84ACjcxK6xIIjxv20xvEc7CjxVAFwI0_Cr0_Gr1UM2 8EF7xvwVC2z280aVAFwI0_Gr0_Cr1l84ACjcxK6I8E87Iv6xkF7I0E14v26r4UJVWxJr1l e2I262IYc4CY6c8Ij28IcVAaY2xG8wAqx4xG64xvF2IEw4CE5I8CrVC2j2WlYx0E2Ix0cI 8IcVAFwI0_JrI_JrylYx0Ex4A2jsIE14v26r1j6r4UMcvjeVCFs4IE7xkEbVWUJVW8JwAC jcxG0xvY0x0EwIxGrwACjI8F5VA0II8E6IAqYI8I648v4I1lFIxGxcIEc7CjxVA2Y2ka0x kIwI1l42xK82IYc2Ij64vIr41l4I8I3I0E4IkC6x0Yz7v_Jr0_Gr1lx2IqxVAqx4xG67AK xVWUJVWUGwC20s026x8GjcxK67AKxVWUGVWUWwC2zVAF1VAY17CE14v26r4a6rW5MIIYrx kI7VAKI48JMIIF0xvE2Ix0cI8IcVAFwI0_JFI_Gr1lIxAIcVC0I7IYx2IY6xkF7I0E14v2 6F4j6r4UJwCI42IY6xAIw20EY4v20xvaj40_Jr0_JF4lIxAIcVC2z280aVAFwI0_Jr0_Gr 1lIxAIcVC2z280aVCY1x0267AKxVW8JVW8JrUvcSsGvfC2KfnxnUUI43ZEXa7VU1489tUU UUU== X-CM-SenderInfo: 5mrqt2oorev25kdx2v3u6k3tpzhluzxrxghudrp/ X-CFilter-Loop: Reflected X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,SPF_HELO_NONE, SPF_NONE 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?1756093194067723106?= X-GMAIL-MSGID: =?utf-8?q?1756093194067723106?= As stated in the documentation and implied by its name, the ppo (preserved program order) relation is intended to link po-earlier to po-later instructions under certain conditions. However, a corner case currently allows instructions to be linked by ppo that are not executed by the same thread, i.e., instructions are being linked that have no po relation. This happens due to the mb/strong-fence relations, which (as one case) provide order when locks are passed between threads followed by an smp_mb__after_unlock_lock() fence. This is illustrated in the following litmus test (as can be seen when using herd7 with `doshow ppo`): P0(int *x, int *y) { spin_lock(x); spin_unlock(x); } P1(int *x, int *y) { spin_lock(x); smp_mb__after_unlock_lock(); *y = 1; } The ppo relation will link P0's spin_lock(x) and P1's *y=1, because P0 passes a lock to P1 which then uses this fence. The patch makes ppo a subrelation of po by eliminating this possibility from mb (but not strong-fence) and relying explicitly on mb|gp instead of strong-fence when defining ppo. Signed-off-by: Jonas Oberhauser --- tools/memory-model/linux-kernel.cat | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 6e531457bb73..815fdafacaef 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -36,7 +36,9 @@ let wmb = [W] ; fencerel(Wmb) ; [W] let mb = ([M] ; fencerel(Mb) ; [M]) | ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | + ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) +let gp = po ; [Sync-rcu | Sync-srcu] ; po? +let strong-fence = mb | gp | (* * Note: The po-unlock-lock-po relation only passes the lock to the direct * successor, perhaps giving the impression that the ordering of the @@ -50,10 +52,9 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | *) ([M] ; po-unlock-lock-po ; [After-unlock-lock] ; po ; [M]) -let gp = po ; [Sync-rcu | Sync-srcu] ; po? -let strong-fence = mb | gp -let nonrw-fence = strong-fence | po-rel | acq-po + +let nonrw-fence = mb | gp | po-rel | acq-po let fence = nonrw-fence | wmb | rmb let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu | Before-atomic | After-atomic | Acquire | Release |