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 bombadil.infradead.org (bombadil.infradead.org [198.137.202.133]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.lore.kernel.org (Postfix) with ESMTPS id 88A83C6FD1F for ; Sat, 23 Mar 2024 14:41:55 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=lists.infradead.org; s=bombadil.20210309; h=Sender: Content-Transfer-Encoding:Content-Type:List-Subscribe:List-Help:List-Post: List-Archive:List-Unsubscribe:List-Id:In-Reply-To:MIME-Version:References: Message-ID:Subject:Cc:To:From:Date:Reply-To:Content-ID:Content-Description: Resent-Date:Resent-From:Resent-Sender:Resent-To:Resent-Cc:Resent-Message-ID: List-Owner; bh=stXyKLeVFi2iA000WMFXRn4cDnGqewmeDMGy0jUuzpg=; b=1+jffgEmdsKUM4 evNt0dSRxqZjaFDtkZcab8L/TcVbtWyXapZL71CX6CAeBBYQqLzhBNOifSZWWBiClhH1ItZvYiY1f 0Y65DKhwVAjZhmPzrgwpmMFLLIGAeXnMPlMdmMtC4X9o7BCF4gEEJNntuaR0IgaGuK4bI5LOamYf8 zijtcSVkvI8X3i2jGxiB6A7wH0ISju1syNzTiZR0r2Y5qytEKjhIDkP0XC23yBpZzvDeGuf39s4SD r5JW57DLhA/ANSUOh4PROgasLHop9OTbgpPk6Ye1FgYzmTWq2NysAOZRUYxioScWP2rL84VlI3dtD YbFffaYoG1D3XMzYpmQQ==; Received: from localhost ([::1] helo=bombadil.infradead.org) by bombadil.infradead.org with esmtp (Exim 4.97.1 #2 (Red Hat Linux)) id 1ro2Z2-0000000AZT7-1cyd; Sat, 23 Mar 2024 14:41:40 +0000 Received: from mail-qk1-x734.google.com ([2607:f8b0:4864:20::734]) by bombadil.infradead.org with esmtps (Exim 4.97.1 #2 (Red Hat Linux)) id 1ro2Yy-0000000AZRz-475m for linux-arm-kernel@lists.infradead.org; Sat, 23 Mar 2024 14:41:38 +0000 Received: by mail-qk1-x734.google.com with SMTP id af79cd13be357-78a4708a557so36995585a.0 for ; Sat, 23 Mar 2024 07:41:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1711204893; x=1711809693; darn=lists.infradead.org; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:cc:to:from:date:feedback-id:from:to:cc:subject:date :message-id:reply-to; bh=JBoHlroea6/GTbzQ3nCArEwBGcVlF3t6u5u31TFOQ5c=; b=mr45Kd9kAws2jlkPdPMTUnSQjqULkxPIwf4nGhMllXITXPMFprm2ywEkhPPedZyOs+ hUpTMyCn6m7OVmYwakJy9N32kgB3Gc2nwSgnOWnz8/mYjSE+scbD522s+GzpsaV9TFMq aR7vf9VJd/NeBmgMuvfrrlXvUYmPtAahz6vOY+RVmb5il6Q/O+rqYwi9AOXqgeB7xZEF xsYpgSApN6sN0E2thOGWn9Enwl8VqoCK5ATZ87Tk3Xt5HK2cbIeSgoQ4T/dNK6bEtTgk K8iyWrrdZkWr7EleAHZ5KxNntEFhvzANV00PgmGWyUv2IFa0qRbs/KGpteE4vGM6y8Es XX4A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1711204893; x=1711809693; 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 :subject:date:message-id:reply-to; bh=JBoHlroea6/GTbzQ3nCArEwBGcVlF3t6u5u31TFOQ5c=; b=H+EOtVAWJJvBqYDkgfc+zMOblmB0vF9uDuzMf4CAr88fYPBMpa+8z+U2iTDPRtEpgg e/Yqg2bu1hl/w4JlpSftGnCbqi9Xcfrz913/Q+x0zrOm3lZ4uH7BhdqiUy+IG60d+HVf TxSNNU/S6Jq8LaTOKgdxFh/sUMXJoplhXGywr36mtWgluT7E2vdrpBXcC8KFY6KcWDLL 2iYBUC7YMFRRLHS8xe7uwUehPDoLTrgcXXWHob41+zjCGw8YxEFm7S3BS+xKoAJdDBNY r6MxK892BFFsfM7qIjG4xzYqaXW/ut0TdrHgMvKxTMPFfpyKkbQusfnE8xIDW5UVgaYe i//A== X-Forwarded-Encrypted: i=1; AJvYcCUtXPxeRZIa1J2zcqq/BJfAFlHQlCbwF0AfbXbKb2uMkYq8QD31w2bKGN6CI1jjhkuJE4raOD1CNzY42n2KXkIniox5ROnRU1bdkEr8sJINjxiqvck= X-Gm-Message-State: AOJu0Yy2f15ppfPAxvTa66htnh4UyVrWC6VGfLzVo+zK5xZP/0S/UmEK RecmqSTZ23kfbSJpKNM7yiAISdLVl+38O1VMB/lhi74forzkUomJ X-Google-Smtp-Source: AGHT+IHlE4DNx4doL/DAGkVKI+43x0e7x4Fv3FAQsZNSiGDB9AFauE0kQDFVKk0ctSx+uT+Q0ETTzg== X-Received: by 2002:a05:620a:a53:b0:789:e5e3:f0f6 with SMTP id j19-20020a05620a0a5300b00789e5e3f0f6mr3057320qka.14.1711204893267; Sat, 23 Mar 2024 07:41:33 -0700 (PDT) Received: from fauth2-smtp.messagingengine.com (fauth2-smtp.messagingengine.com. [103.168.172.201]) by smtp.gmail.com with ESMTPSA id k26-20020a05620a0b9a00b00789e2961225sm714626qkh.61.2024.03.23.07.41.32 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 23 Mar 2024 07:41:32 -0700 (PDT) Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailfauth.nyi.internal (Postfix) with ESMTP id B26BB1200066; Sat, 23 Mar 2024 10:41:31 -0400 (EDT) Received: from mailfrontend2 ([10.202.2.163]) by compute3.internal (MEProxy); Sat, 23 Mar 2024 10:41:31 -0400 X-ME-Sender: X-ME-Received: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedvledruddtgedgieekucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucesvcftvggtihhpihgvnhhtshculddquddttddmne cujfgurhepfffhvfevuffkfhggtggujgesthdtredttddtvdenucfhrhhomhepuehoqhhu nhcuhfgvnhhguceosghoqhhunhdrfhgvnhhgsehgmhgrihhlrdgtohhmqeenucggtffrrg htthgvrhhnpeehudfgudffffetuedtvdehueevledvhfelleeivedtgeeuhfegueeviedu ffeivdenucevlhhushhtvghrufhiiigvpedtnecurfgrrhgrmhepmhgrihhlfhhrohhmpe gsohhquhhnodhmvghsmhhtphgruhhthhhpvghrshhonhgrlhhithihqdeiledvgeehtdei gedqudejjeekheehhedvqdgsohhquhhnrdhfvghngheppehgmhgrihhlrdgtohhmsehfih igmhgvrdhnrghmvg X-ME-Proxy: Feedback-ID: iad51458e:Fastmail Received: by mail.messagingengine.com (Postfix) with ESMTPA; Sat, 23 Mar 2024 10:41:29 -0400 (EDT) Date: Sat, 23 Mar 2024 07:41:28 -0700 From: Boqun Feng To: Andrew Lunn Cc: Kent Overstreet , rust-for-linux@vger.kernel.org, linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, llvm@lists.linux.dev, Miguel Ojeda , Alex Gaynor , Wedson Almeida Filho , Gary Guo , =?iso-8859-1?Q?Bj=F6rn?= Roy Baron , Benno Lossin , Andreas Hindborg , Alice Ryhl , Alan Stern , Andrea Parri , Will Deacon , Peter Zijlstra , Nicholas Piggin , David Howells , Jade Alglave , Luc Maranget , "Paul E. McKenney" , Akira Yokosawa , Daniel Lustig , Joel Fernandes , Nathan Chancellor , Nick Desaulniers , kent.overstreet@gmail.com, Greg Kroah-Hartman , elver@google.com, Mark Rutland , Thomas Gleixner , Ingo Molnar , Borislav Petkov , Dave Hansen , x86@kernel.org, "H. Peter Anvin" , Catalin Marinas , torvalds@linux-foundation.org, linux-arm-kernel@lists.infradead.org, linux-fsdevel@vger.kernel.org Subject: Re: [WIP 0/3] Memory model and atomic API in Rust Message-ID: References: <20240322233838.868874-1-boqun.feng@gmail.com> <03f629b6-1e4e-4689-9b69-db0b75577822@lunn.ch> MIME-Version: 1.0 Content-Disposition: inline In-Reply-To: <03f629b6-1e4e-4689-9b69-db0b75577822@lunn.ch> X-CRM114-Version: 20100106-BlameMichelson ( TRE 0.8.0 (BSD) ) MR-646709E3 X-CRM114-CacheID: sfid-20240323_074137_067802_772A5CEE X-CRM114-Status: GOOD ( 16.11 ) X-BeenThere: linux-arm-kernel@lists.infradead.org X-Mailman-Version: 2.1.34 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Sender: "linux-arm-kernel" Errors-To: linux-arm-kernel-bounces+linux-arm-kernel=archiver.kernel.org@lists.infradead.org On Sat, Mar 23, 2024 at 03:29:11PM +0100, Andrew Lunn wrote: > > There are also issues like where one Rust thread does a store(.., > > RELEASE), and a C thread does a rcu_deference(), in practice, it > > probably works but no one works out (and no one would work out) a model > > to describe such an interaction. > > Isn't that what Paul E. McKenney litmus tests are all about? > Litmus tests (or herd, or any other memory model tools) works for either LKMM or C++ memory model. But there is no model I'm aware of works for the communication between two memory models. So for example: Rust thread: let mut foo: Box = ...; foo.a = 1; let global_ptr: &AtomicPtr = ...; global_ptr.store(foo.leak() as _, RELEASE); C thread: rcu_read_lock(); foo = rcu_dereference(global_ptr); if (foo) { r1 = foo->a; } rcu_read_unlock(); no tool or model yet to guarantee "r1" is 1, but yeah, in practice for the case we care, it's probably guaranteed. But no tool or model means challenging for code reasoning. Regards, Boqun > tools/memory-model/litmus-test > > Andrew _______________________________________________ linux-arm-kernel mailing list linux-arm-kernel@lists.infradead.org http://lists.infradead.org/mailman/listinfo/linux-arm-kernel