From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail-qv1-f43.google.com (mail-qv1-f43.google.com [209.85.219.43]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 9EF532F4A17 for ; Thu, 19 Jun 2025 18:04:58 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.219.43 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1750356301; cv=none; b=lB7I+nnOg4qMQ8CkZTyqIlGjA/rsZ2ZyW5+rx3mPqPTWn4/zQZ2PVjw2+qK0da3t8LefZp7CtY2WGaCnOXzO7ng6bpQNwClrAoAV/+rMyPYYin/fUJoe/U4MXItuylcFtNCzjiedtFJE6kO3xF+7utV2mwY2ah53YVRBjsOlxKk= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1750356301; c=relaxed/simple; bh=1dJVx9uawlA9hJYDvC4nybtTSvTD1cO2bZ9M1c+EVuk=; h=Date:From:To:Cc:Subject:Message-ID:References:MIME-Version: Content-Type:Content-Disposition:In-Reply-To; b=MvFzTLM670UkX0+A/SF0GGPsjdrukoI/wXIJKBE+lW4zTihzjKk/8DOA/Bbyu2AeBmMtAtAd8BaNY+TOtGsQZ+N/+cfolN1cfox62G/oDwHEIvtbyvxBqEMCdKDfpgLYFdPC8PyuwNNDD7JUMCQ+tzQnGPG4RUdg/8CWpHaO1JE= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=rowland.harvard.edu; spf=fail smtp.mailfrom=g.harvard.edu; dkim=pass (2048-bit key) header.d=rowland.harvard.edu header.i=@rowland.harvard.edu header.b=GYUwGMt+; arc=none smtp.client-ip=209.85.219.43 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=rowland.harvard.edu Authentication-Results: smtp.subspace.kernel.org; spf=fail smtp.mailfrom=g.harvard.edu Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=rowland.harvard.edu header.i=@rowland.harvard.edu header.b="GYUwGMt+" Received: by mail-qv1-f43.google.com with SMTP id 6a1803df08f44-6fadd3ad18eso11236336d6.2 for ; Thu, 19 Jun 2025 11:04:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=rowland.harvard.edu; s=google; t=1750356297; x=1750961097; darn=vger.kernel.org; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:cc:to:from:date:from:to:cc:subject:date:message-id:reply-to; bh=Ju0rK1YrXezG8RMPatgIQGMIY6rdX0cs7akdNztgfu4=; b=GYUwGMt+Me/R2P1+TrGCqwGFsiJmYOM240kgzncIKaBqh85tQJh2KwK4INZBUlLM0v GYf/DgQMZEaSpBRhzk6jUIdvahCLK9PZOfI9xOl4VaAnHMeK7mrmEblsTAwrghk72j0k HP8ZqQM8llTy9iTBykYLa5csHFj/3AJLaIDL+QsXRrWAuRMYdDVGcejlmWryKy3OoRoS x+sbMxdpNrdgxxgwXbbcpbD01xyQfqMYSnV9z2TC+/ZnLkLEmqMMTC2T73wklHCNdKAr 9PlY1bDWrtaJBWum/87pmoK9ivqYCMgXLwfOb7H+jD30LFc7Mw1TVCyhEkdwET9x5bNq RdTA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1750356297; x=1750961097; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:cc:to:from:date:x-gm-message-state:from:to:cc:subject:date :message-id:reply-to; bh=Ju0rK1YrXezG8RMPatgIQGMIY6rdX0cs7akdNztgfu4=; b=GfKS5VQGwH8H49Hpv7O8nBWaNH4PN4UmNLuD6IevvHwlNS1dUQwVw6Dvus8n34HhM1 ZIcXW3prvos67iaMfNvL7vpjgdXUywHZLeFpYRcD2Ceyer/geaewZG+fbJBxWQEdAFXp awvPJVEcFzKb9EuXcye6vq7Jj6M0X21pFQ07mYDOKqxu51qbLbEOJ9D0w0rh3iMGhFkM 7QhlyFbXu9bnarg6zMt9GvGiwBSUISPdpuRVA6oM2VNT9vT5RNOMltBd2wkoLJ9hfc6a ZibNRRt5QQq8I4azeXCBzw6Jh6gE/GiYEExW5d/ZGgUx7vaSJhLxPLpfWatQ9jzIq6q5 oe9w== X-Forwarded-Encrypted: i=1; AJvYcCVODDwt4rSAeTroNd/k0qqNAk2HJSi4yzK4w6yCMKgHCkq5pWKayuO2uR1+8a/bFsBd+itmBMKo+SL3/70=@vger.kernel.org X-Gm-Message-State: AOJu0YyreYWYGjN7zSbmGMCX/x0ZZGAyP3htEovsjdY7+L26rgk7iPGh uoQOtXWAp7O874zvlijIe4Db1p0GQ6m+k4NdPQmsNnu74mVSrm48mVdEroul0rCa1A== X-Gm-Gg: ASbGnctikW0HmDHhWVS7joSmA5hHXeYblIV9LXZlLwmDPpAl/5TQuDH73c2qNSZjRb+ WNnDH2swxpUv15/gAe7a9h9EPy6kAP7VwItJ/TNbgDCh2/OCBzvnDTbCGxPJRRnPy+p/JJn/OC6 WjtZ1FoxIjfwYnHOnyYrIuI7WygrcsXOTUUyiOPpenqkyW/YvsofuFLpx/VV1fLv7Vdmpa9TFvA xWGcv5WB0bgivVYHIul6KYhgWgedSH5u0b5qopiuT07205g7g6JefipQ0SHv3Q0Q90B0Y4rUIO1 X/2aCyCdb5MlqCDRm7KTyfeeEBr0dIYBuStZ6AgDx7MK/Pd0ilSjRM4Wjh97gRI= X-Google-Smtp-Source: AGHT+IHYQPCClOz6CKzGdC08frCU41q/Xam4KfyuktRr18N70eT9mCmlX3M2z1ua5tmNIo2PbaShTw== X-Received: by 2002:a05:6214:4598:b0:6f8:a978:d46 with SMTP id 6a1803df08f44-6fd0a49c0e7mr3871256d6.19.1750356297608; Thu, 19 Jun 2025 11:04:57 -0700 (PDT) Received: from rowland.harvard.edu ([2601:19b:681:fd10::9ca8]) by smtp.gmail.com with ESMTPSA id 6a1803df08f44-6fd09544e75sm2440186d6.70.2025.06.19.11.04.54 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 19 Jun 2025 11:04:57 -0700 (PDT) Date: Thu, 19 Jun 2025 14:04:52 -0400 From: Alan Stern To: Boqun Feng Cc: Peter Zijlstra , linux-kernel@vger.kernel.org, rust-for-linux@vger.kernel.org, lkmm@lists.linux.dev, linux-arch@vger.kernel.org, Miguel Ojeda , Alex Gaynor , Gary Guo , =?iso-8859-1?Q?Bj=F6rn?= Roy Baron , Benno Lossin , Andreas Hindborg , Alice Ryhl , Trevor Gross , Danilo Krummrich , Will Deacon , Mark Rutland , Wedson Almeida Filho , Viresh Kumar , Lyude Paul , Ingo Molnar , Mitchell Levy , "Paul E. McKenney" , Greg Kroah-Hartman , Linus Torvalds , Thomas Gleixner Subject: Re: [PATCH v5 03/10] rust: sync: atomic: Add ordering annotation types Message-ID: References: <20250618164934.19817-1-boqun.feng@gmail.com> <20250618164934.19817-4-boqun.feng@gmail.com> <20250619103155.GD1613376@noisy.programming.kicks-ass.net> <20250619143214.GJ1613376@noisy.programming.kicks-ass.net> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: On Thu, Jun 19, 2025 at 08:00:30AM -0700, Boqun Feng wrote: > Make sense, so something like this in the model should work: > > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat > index d7e7bf13c831..90cb6db6e335 100644 > --- a/tools/memory-model/linux-kernel.cat > +++ b/tools/memory-model/linux-kernel.cat > @@ -27,7 +27,7 @@ include "lock.cat" > (* Release Acquire *) > let acq-po = [Acquire] ; po ; [M] > let po-rel = [M] ; po ; [Release] > -let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po > +let po-unlock-lock-po = po ; (([UL] ; (po|rf) ; [LKR]) | ([Release]; (po;rf); [Acquire & RMW])) ; po > > (* Fences *) > let R4rmb = R \ Noreturn (* Reads for which rmb works *) > > > although I'm not sure whether there will be actual users that use this > ordering. If we do end up making a change like this then we should also start keeping careful track of the parts of the LKMM that are not justified by the operational model (and vice versa), perhaps putting something about them into the documentation. As far as I can remember, po-unlock-lock-po is the only current example, but my memory isn't always the greatest -- just one reason why it would be good to have these things written down in an organized manner. Alan