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 75F7BC25B4E for ; Tue, 24 Jan 2023 15:12:04 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234924AbjAXPMD (ORCPT ); Tue, 24 Jan 2023 10:12:03 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:55928 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S233135AbjAXPMA (ORCPT ); Tue, 24 Jan 2023 10:12:00 -0500 Received: from frasgout13.his.huawei.com (frasgout13.his.huawei.com [14.137.139.46]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 4BC334A21A for ; Tue, 24 Jan 2023 07:11:53 -0800 (PST) Received: from mail02.huawei.com (unknown [172.18.147.229]) by frasgout13.his.huawei.com (SkyGuard) with ESMTP id 4P1Vbr3Vr0z9xFg7 for ; Tue, 24 Jan 2023 23:03:52 +0800 (CST) Received: from [10.48.129.122] (unknown [10.48.129.122]) by APP1 (Coremail) with SMTP id LxC2BwBX3gkU9c9jpyTDAA--.13249S2; Tue, 24 Jan 2023 16:11:28 +0100 (CET) Message-ID: <8cc799ab-ffa1-47f7-6e1d-97488a210f14@huaweicloud.com> Date: Tue, 24 Jan 2023 16:11:14 +0100 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101 Thunderbird/102.6.1 Subject: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) To: paulmck@kernel.org, Andrea Parri Cc: Alan Stern , Jonas Oberhauser , Peter Zijlstra , will , "boqun.feng" , npiggin , dhowells , "j.alglave" , "luc.maranget" , akiyks , dlustig , joel , urezki , quic_neeraju , frederic , Kernel development list References: <20230120175804.GN2948950@paulmck-ThinkPad-P17-Gen-1> <20230120192032.GR2948950@paulmck-ThinkPad-P17-Gen-1> <20230120212037.GW2948950@paulmck-ThinkPad-P17-Gen-1> <20230123201659.GA3754540@paulmck-ThinkPad-P17-Gen-1> <20230124040611.GD2948950@paulmck-ThinkPad-P17-Gen-1> <20230124145423.GI2948950@paulmck-ThinkPad-P17-Gen-1> From: Jonas Oberhauser In-Reply-To: <20230124145423.GI2948950@paulmck-ThinkPad-P17-Gen-1> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit X-CM-TRANSID: LxC2BwBX3gkU9c9jpyTDAA--.13249S2 X-Coremail-Antispam: 1UD129KBjvdXoW7Xw4UJF4Uur1Uur4rWw4xXrb_yoWDKrX_uw naya1kAw4DWws3tFWUtF1Yv3srKFyUAFy8X3y3Ka17Kw18JayxJF97G34IvryjqFs2grsx CrZ0qa43uw43KjkaLaAFLSUrUUUUUb8apTn2vfkv8UJUUUU8Yxn0WfASr-VFAUDa7-sFnT 9fnUUIcSsGvfJTRUUUbIkYFVCjjxCrM7AC8VAFwI0_Xr0_Wr1l1xkIjI8I6I8E6xAIw20E Y4v20xvaj40_Wr0E3s1l1IIY67AEw4v_Jr0_Jr4l8cAvFVAK0II2c7xJM28CjxkF64kEwV A0rcxSw2x7M28EF7xvwVC0I7IYx2IY67AKxVWUJVWUCwA2z4x0Y4vE2Ix0cI8IcVCY1x02 67AKxVW8JVWxJwA2z4x0Y4vEx4A2jsIE14v26r4j6F4UM28EF7xvwVC2z280aVCY1x0267 AKxVW8Jr0_Cr1UM2AIxVAIcxkEcVAq07x20xvEncxIr21l5I8CrVACY4xI64kE6c02F40E x7xfMcIj6xIIjxv20xvE14v26r1j6r18McIj6I8E87Iv67AKxVWUJVW8JwAm72CE4IkC6x 0Yz7v_Jr0_Gr1lF7xvr2IY64vIr41lFIxGxcIEc7CjxVA2Y2ka0xkIwI1lc7I2V7IY0VAS 07AlzVAYIcxG8wCF04k20xvY0x0EwIxGrwCFx2IqxVCFs4IE7xkEbVWUJVW8JwC20s026c 02F40E14v26r1j6r18MI8I3I0E7480Y4vE14v26r106r1rMI8E67AF67kF1VAFwI0_GFv_ WrylIxkGc2Ij64vIr41lIxAIcVC0I7IYx2IY67AKxVWUJVWUCwCI42IY6xIIjxv20xvEc7 CjxVAFwI0_Gr0_Cr1lIxAIcVCF04k26cxKx2IYs7xG6rWUJVWrZr1UMIIF0xvEx4A2jsIE 14v26r1j6r4UMIIF0xvEx4A2jsIEc7CjxVAFwI0_Gr0_Gr1UYxBIdaVFxhVjvjDU0xZFpf 9x07UZ18PUUUUU= X-CM-SenderInfo: 5mrqt2oorev25kdx2v3u6k3tpzhluzxrxghudrp/ X-CFilter-Loop: Reflected Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On 1/24/2023 3:54 PM, Paul E. McKenney wrote: > On Tue, Jan 24, 2023 at 12:09:48PM +0100, Andrea Parri wrote: >>> There is the one below, but I am (1) not sure that I have it right, >>> (2) not immediately certain that the Linux-kernel implementation would >>> forbid it, (3) not immediately sure that it should be forbidden. >>> >>> In the meantime, thoughts? >> As it stands, P0 to completion, then P1 to completion, then P2 to >> completion should meet the "exists" clause; I guess we want "x=1" >> in the clause (or the values of the stores to "x" exchanged). > OK, so I still don't have it right. ;-) > > Make that x=1. I think. > If it is x=1, why doesn't LKMM forbid it? Because T1:y=1 is read by T1 before the GP, the whole CS is before the GP, i.e., srcu_read_unlock(s, r1); ->rcu-order synchronize_srcu(s); The GP is furthermore po;prop;strong-fence;prop;po ordered before the unlock, which you can shuffle around to get    Wx=2  ->prop;po;rcu-order;po ;  prop;strong-fence  Wx=2 or    Wx=2  ->rb  Wx=2 which is forbidden because rb is irreflexive. Right? jonas