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 43DB6ECAAD1 for ; Sat, 27 Aug 2022 16:45:13 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S233354AbiH0QpM (ORCPT ); Sat, 27 Aug 2022 12:45:12 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35270 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229905AbiH0QpL (ORCPT ); Sat, 27 Aug 2022 12:45:11 -0400 Received: from mail-qv1-xf2a.google.com (mail-qv1-xf2a.google.com [IPv6:2607:f8b0:4864:20::f2a]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 151FA37FAE; Sat, 27 Aug 2022 09:45:08 -0700 (PDT) Received: by mail-qv1-xf2a.google.com with SMTP id s1so3359026qvn.11; Sat, 27 Aug 2022 09:45:08 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:cc:to:from:date:feedback-id:from:to:cc; bh=ZhfbAHlPQFx8IPZok5WapkkflkTEU7J+fDiYrhhmxIA=; b=M0b5ENI57ijrrSBOdqsI4nNWdePJhQB34ojLnGx1NLyBtuxthw5HlWP80AiqIjk3lU P+4RUXrRoTcBjhATVcFtXruNMuUNuq5BfeWxNcVYkhW7BRJb77nwQFSn/SSa9GWuBftT X/XfiA7vA+5aXegoOnnIsISEdiPbJI81WGEtV9CC0VVX3MWrFOhfjuMfH2x99/uOOubr aeb78qeaalSJoe7g7YFhlYJlRMff+XiTQRvKZ+Hv07z2YlMmENAYl3wG/9JIT+utk58T ti0+hXqvLSktqm0iREGzUKghPcnhEvABZEDtSQc7UuFUhwfAC0O6CQVogaiJZecAMOD4 03vw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:cc:to:from:date:feedback-id:x-gm-message-state:from:to:cc; bh=ZhfbAHlPQFx8IPZok5WapkkflkTEU7J+fDiYrhhmxIA=; b=zTh8Bi0RRA0wLbb8980hj52yZK5enVQrq9wXmx13yoeYRdQu14J8aS8rhOcoXVVhe7 jNJIP71/74A7ROQgBLq/M0ceaer/key3URlycg7X5hDd3oV5yKNYajlxQ7PvaROF3HFK bRUzp3RJunqBLs9645mnpBinOW2ZzcL4izx3WPZN4nnUaPkUREQer+v5L/ubR3UrT3Gk swb6ryRJuYz/J2CNltNCx9yohKas57nqUhKoP4Lzh8jSJ74daMuiAlac7eQWSJt/GRcr FFnii6N5er2yccqj5MND6z12qpXIR9KWFyoiy7DfnF7Fh8RwEI8ZVm8ChZcDY6+OkfxC Dd4A== X-Gm-Message-State: ACgBeo0WelIyAKEzUwN0sZWMeVxw6CL9XACqZax+ivmhNmc+NfxUm+KS KSMLW2cqqwackZFNWN/whJBF2/rk3QE= X-Google-Smtp-Source: AA6agR4EA7lK9MqSZtDKKlmHSyAAvzyqsEy9HxXgmoadwDV/yIFxuEYAmu1UBax8Q8IbbfSdHwJjxw== X-Received: by 2002:a05:6214:5005:b0:472:e6b0:1fb2 with SMTP id jo5-20020a056214500500b00472e6b01fb2mr4073953qvb.124.1661618707237; Sat, 27 Aug 2022 09:45:07 -0700 (PDT) Received: from auth2-smtp.messagingengine.com (auth2-smtp.messagingengine.com. [66.111.4.228]) by smtp.gmail.com with ESMTPSA id j10-20020ac874ca000000b003434e47515csm1886500qtr.7.2022.08.27.09.45.06 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 27 Aug 2022 09:45:06 -0700 (PDT) Received: from compute2.internal (compute2.nyi.internal [10.202.2.46]) by mailauth.nyi.internal (Postfix) with ESMTP id 0935527C0054; Sat, 27 Aug 2022 12:45:05 -0400 (EDT) Received: from mailfrontend2 ([10.202.2.163]) by compute2.internal (MEProxy); Sat, 27 Aug 2022 12:45:06 -0400 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvfedrvdejjedguddtkecutefuodetggdotefrod ftvfcurfhrohhfihhlvgemucfhrghsthforghilhdpqfgfvfdpuffrtefokffrpgfnqfgh necuuegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmd enucfjughrpeffhffvvefukfhfgggtuggjsehttdertddttddvnecuhfhrohhmpeeuohhq uhhnucfhvghnghcuoegsohhquhhnrdhfvghnghesghhmrghilhdrtghomheqnecuggftrf grthhtvghrnheptdegffdugfefhfdugfeiheefheekudehfeeiieegleegheejleefieek veeuhfdunecuffhomhgrihhnpegvvghlrdhishdpiihulhhiphgthhgrthdrtghomhenuc evlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhrohhmpegsohhquhhn odhmvghsmhhtphgruhhthhhpvghrshhonhgrlhhithihqdeiledvgeehtdeigedqudejje ekheehhedvqdgsohhquhhnrdhfvghngheppehgmhgrihhlrdgtohhmsehfihigmhgvrdhn rghmvg X-ME-Proxy: Feedback-ID: iad51458e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Sat, 27 Aug 2022 12:45:04 -0400 (EDT) Date: Sat, 27 Aug 2022 09:44:17 -0700 From: Boqun Feng To: Alan Stern Cc: Peter Zijlstra , "Paul E. McKenney" , parri.andrea@gmail.com, will@kernel.org, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org, linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org Subject: Re: "Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models" Message-ID: References: <20220826124812.GA3007435@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: Precedence: bulk List-ID: X-Mailing-List: linux-arch@vger.kernel.org On Sat, Aug 27, 2022 at 12:05:33PM -0400, Alan Stern wrote: > On Sat, Aug 27, 2022 at 01:47:48AM +0200, Peter Zijlstra wrote: > > On Fri, Aug 26, 2022 at 01:10:39PM -0400, Alan Stern wrote: > > > > > > - some babbling about a missing propagation -- ISTR Linux if stuffed > > > > full of them, specifically we require stores to auto propagate > > > > without help from barriers > > > > > > Not a missing propagation; a late one. > > > > > > Don't understand what you mean by "auto propagate without help from > > > barriers". > > > > Linux hard relies on: > > > > CPU0 CPU1 > > > > WRITE_ONCE(foo, 1); while (!READ_ONCE(foo)); > > > > making forward progress. > > Indeed yes. As far as I can tell, this requirement is not explicitly > mentioned in the LKMM, although it certainly is implicit. I can't even > think of a way to express it in a form Herd could verify. > FWIW, C++ defines this as (in https://eel.is/c++draft/atomics#order-11): Implementations should make atomic stores visible to atomic loads within a reasonable amount of time. in other words: if one thread does an atomic store, then all other threads must see that store eventually. (from: https://rust-lang.zulipchat.com/#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Rust.20forward.20progress.20guarantees/near/294702950) Should we add something somewhere in our model, maybe in the explanation.txt? Plus, I think we cannot express this in Herd because Herd uses graph-based model (axiomatic model) instead of an operational model to describe the model: axiomatic model cannot describe "something will eventually happen". There was also some discussion in the zulip steam of Rust unsafe-code-guidelines. Regards, Boqun > > There were a few 'funny' uarchs that were broken, see for example commit > > a30718868915f. > > Ha! That commit should be a lesson in something, although I'm not sure > what. :-) > > Alan