From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail-qk1-f175.google.com (mail-qk1-f175.google.com [209.85.222.175]) (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 387FA8F6B for ; Tue, 7 Jan 2025 16:10:03 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.222.175 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1736266207; cv=none; b=Mzys1oHirb91Gem9JNsoBYqgZXw+xY/nKHkELYqhN/ApOqmCV56faEgiAUOSeA1BCDKXHF6oPtnD8hXQf+vmek6wUYWIgQPipKXZDTxUFCE0GCe+G6LEt9nI2NTxNOJUoaj2kJULMJi554RULeMx1MltHdSe5ml0RwL8c/GWD6g= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1736266207; c=relaxed/simple; bh=bDJscXv1RXC2286ZEvBuxPoo00Q6pAo7GSGUN3kp5bU=; h=Date:From:To:Cc:Subject:Message-ID:References:MIME-Version: Content-Type:Content-Disposition:In-Reply-To; b=j2NeQNIUtmSRePOuMOIvn/4Gck/12Kne2mCn0qJYPW3YjSck2OlEOk1MdQtiLWt+SatNCPz6N6udnNFG+TgK6FAj0fRQpKxA2AVZCaPKM630SWPlb2bOxQ5cEigSVCdqfqNREVl4lRKSkZ54VrIZbHxLr3iSPN4WLTiDNwNsmo4= 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=O3/vmiF1; arc=none smtp.client-ip=209.85.222.175 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="O3/vmiF1" Received: by mail-qk1-f175.google.com with SMTP id af79cd13be357-7b6eeff1fdfso1175999685a.2 for ; Tue, 07 Jan 2025 08:10:03 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=rowland.harvard.edu; s=google; t=1736266203; x=1736871003; 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=5LvIDWeluTdCgXCnx0predLJUANZH+mX5VnGU6NYk94=; b=O3/vmiF1aiqu8YgKs8o2KjskqrtBkT6DZb0Wq3jVQPOgb1n0vmRf7k3LF6IwPjCJpW WKIB4+tpCEtRZQKKmVG1N8gDbZuhlZt8Y0WJkoX2nxXnbifHrhUe8QdSCfaoKoUV+GkD Mt5FGCXexAhZFImq7iEz+drjp4IrBb168eb3VzEnW+p5kin3BwQGVaqYLRs0V0JgRMGF R9blD/SrxpzjGvqmI/BxIvKgAZqYKPQGrKDnw1uphxn52F0ykG838Uv+tX72MXU1C509 7LczqAZef1CQmEsbp3WxUtSl4xzlTbr9iNTyBgDZv4uYq+Fr0M9351dVrZJSTF1S2D8j g5rw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1736266203; x=1736871003; 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=5LvIDWeluTdCgXCnx0predLJUANZH+mX5VnGU6NYk94=; b=GdgYg+alRLcbiNt9QRzcbuL0080XLph3PJH/J5LsI58BDwl1kwrLk4k31hHCvqAE0J v69PglRR3VgnGDdHIU61rwZ8FbmHm+gVQ57sB4pU9Z/aROGhiskkdsRxH86NMXsXxwNx EQXyxDHze/cOpszaM3WV7T4y2BjACMuS0sRhNO48Io8HDD6Zh4umDnCBQ6aND9I5t+mo bkUPWOOnzZF/wOZ5jHiK4+vHLxlhdhr6jtcJ8gy90BEszIwPYfZ1/IwwxAGf0ChUuZmJ agonMCpMSEpBGorTIfe3L/lB0u6rS93X0vldpgx/JNTba+TKpHaYVHbFgcXwia5qyel3 3MVw== X-Forwarded-Encrypted: i=1; AJvYcCUYFqSup5W5cVvoGc6TcckIvsRToT5bzONqqh1/eHMscWQ49TWE8nFVeew0qwQuKPmpcYZHDMclluUIneM=@vger.kernel.org X-Gm-Message-State: AOJu0YzIF0NjK8/+Hm/Uy87gZYwoUaZwhIX9fNX5jEL1bKHDB9km/+YF 92ZilQAy+KSvn6bEHsA2zQH8QC0gACq5YEtLGqqGEQWuvtBMHsAK432srMr/3Q== X-Gm-Gg: ASbGncvD7kWOMuoxEbFxrrFhbzfYGYxpuXj9crg3UqImIrFwjSaUyNzEjCkR6/MqJyf cfp325dddH3vK3g0lbKinIf8ItT3/I9USdcearB697BCtbrBkoHi+37lhhoJJfoxHf46NnyX8en xUJvtt2XrGG9JKQ7mzpJjb43QSqZ3q0oshlD8pLPb5I0OuzPOSeKkiArGNmMxtlAPISOG7UJXUF QlSqk8Q83UmjPJRt3pu80NfmdWuzefk5kujj/LY5tmm2Om8nv73W3pzTDnXdmWPT90yRTBQzLQ= X-Google-Smtp-Source: AGHT+IG+ycHwyLukwgsBXT6niw1ql2jpnYH+aLV9PPiHxlOrb704y6W2dcgu1wdH7ULWrUqyatgdNw== X-Received: by 2002:a05:620a:4145:b0:7b6:67a6:5adb with SMTP id af79cd13be357-7b9ba784a1dmr12181682885a.21.1736266202963; Tue, 07 Jan 2025 08:10:02 -0800 (PST) Received: from rowland.harvard.edu ([140.247.181.15]) by smtp.gmail.com with ESMTPSA id af79cd13be357-7b9ac4ce6aasm1605198685a.117.2025.01.07.08.10.01 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 07 Jan 2025 08:10:02 -0800 (PST) Date: Tue, 7 Jan 2025 11:09:55 -0500 From: Alan Stern To: Jonas Oberhauser Cc: paulmck@kernel.org, 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, lkmm@lists.linux.dev, hernan.poncedeleon@huaweicloud.com Subject: Re: [RFC] tools/memory-model: Rule out OOTA Message-ID: References: <20250106214003.504664-1-jonas.oberhauser@huaweicloud.com> 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: <20250106214003.504664-1-jonas.oberhauser@huaweicloud.com> On Mon, Jan 06, 2025 at 10:40:03PM +0100, Jonas Oberhauser wrote: > The current LKMM allows out-of-thin-air (OOTA), as evidenced in the following > example shared on this list a few years ago: > > P0(int *a, int *b, int *x, int *y) { > int r1; > > r1 = READ_ONCE(*x); > smp_rmb(); > if (r1 == 1) { > *a = *b; > } > smp_wmb(); > WRITE_ONCE(*y, 1); > } > > P1(int *a, int *b, int *x, int *y) { > int r1; > > r1 = READ_ONCE(*y); > smp_rmb(); > if (r1 == 1) { > *b = *a; > } > smp_wmb(); > WRITE_ONCE(*x, 1); > } > > exists b=42 > > The root cause is an interplay between plain accesses and rw-fences, i.e., > smp_rmb() and smp_wmb(): while smp_rmb() and smp_wmb() provide sufficient > ordering for plain accesses to rule out data races, they do not in the current > formalization generally actually order the plain accesses, allowing, e.g., the > load and stores to *b to proceed in any order even if P1 reads from P0; and in > particular, the marked accesses around those plain accesses are also not > ordered, which causes this OOTA. That's right. The memory model deliberately tries to avoid placing restrictions on plain accesses, whenever it can. In the example above, for instance, I think it's more interesting to ask exists 0:r1=1 /\ 1:r1=1 than to concentrate on a and b. OOTA is a very difficult subject. It can be approached only by making the memory model take all sorts of compiler optimizations into account, and doing this for all possible optimizations is not feasible. (For example, in a presentation to the C++ working group last year, Paul and I didn't try to show how to extend the C++ memory model to exclude OOTA [other than by fiat, as it does now]. Instead we argued that with the existing memory model, no reasonable compiler would ever produce an executable that could exhibit OOTA and so the memory model didn't need to be changed.) > In this patch, we choose the rather conservative approach of forcing only the > order of these marked accesses, specifically, when a marked read r is > separated from a plain read r' by an smp_rmb() (or r' has an address > dependency on r or is r'), on which a write w' depends, and w' is either plain > and seperated by a subsequent write w by an smp_wmb() (or w' is w), then r > precedes w in ppo. Is this really valid? In the example above, if there were no other references to a or b in the rest of the program, the compiler could eliminate them entirely. (Whether the result could count as OOTA is open to question, but that's not the point.) Is it not possible that a compiler might find other ways to defeat your intentions? In any case, my feeling is that memory models for higher languages (i.e., anything above the assembler level) should not try very hard to address the question of OOTA. And for LKMM, OOTA involving _plain_ accesses is doubly out of bounds. Your proposed change seems to add a significant complication to the memory model for a not-very-clear benefit. Alan