From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from smtp2.osuosl.org (smtp2.osuosl.org [140.211.166.133]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id C60A1243364 for ; Mon, 19 May 2025 12:26:11 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=140.211.166.133 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1747657573; cv=none; b=U+A+TRdM23/yeoJ8ayp8Rtl6NSr9y+2YubUXCcklg90ExovfsBjmGP+mFox8K27x0Au474esVpWT0U8j9SfHtV9Oct5eCe44EDIvbXqtgEcfWuMIAZDTqx2lsMOvZi5OD/WwgM+/bfq5YEQyNrCZGfgosgZfqnLop2qdwwR7x04= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1747657573; c=relaxed/simple; bh=IDm1lnmH8i5Jc0QN2R5yydX3w8LDzL7R8VSGykatnf8=; h=Mime-Version:Content-Type:Date:Message-Id:Cc:Subject:From:To: References:In-Reply-To; b=cgbSC7+YmO4Rdefj64vlfohPxAq9AQiLXK3lkWIW9Oyp0eCE7RA4Qf4Bi11EKv75MLczwGSz9xHIekjdQ9/jSOt4Y+i/mKXityjGCsi5I1bj35TQFP5s2iaw11OIouoEg423z9Z6R9mxjT/9YR2oWc9Hl3lqZp5W988GsHp9jSI= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=Kkh2beBp; arc=none smtp.client-ip=140.211.166.133 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="Kkh2beBp" Received: from localhost (localhost [127.0.0.1]) by smtp2.osuosl.org (Postfix) with ESMTP id 43CC8410DE for ; Mon, 19 May 2025 12:26:11 +0000 (UTC) X-Virus-Scanned: amavis at osuosl.org X-Spam-Flag: NO X-Spam-Score: -10.792 X-Spam-Level: Received: from smtp2.osuosl.org ([127.0.0.1]) by localhost (smtp2.osuosl.org [127.0.0.1]) (amavis, port 10024) with ESMTP id QbOthuz026oh for ; Mon, 19 May 2025 12:26:10 +0000 (UTC) Received-SPF: Pass (mailfrom) identity=mailfrom; client-ip=139.178.84.217; helo=dfw.source.kernel.org; envelope-from=lossin@kernel.org; receiver= DMARC-Filter: OpenDMARC Filter v1.4.2 smtp2.osuosl.org ED9294108D Authentication-Results: smtp2.osuosl.org; dmarc=pass (p=quarantine dis=none) header.from=kernel.org DKIM-Filter: OpenDKIM Filter v2.11.0 smtp2.osuosl.org ED9294108D Authentication-Results: smtp2.osuosl.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.a=rsa-sha256 header.s=k20201202 header.b=Kkh2beBp Received: from dfw.source.kernel.org (dfw.source.kernel.org [139.178.84.217]) by smtp2.osuosl.org (Postfix) with ESMTPS id ED9294108D for ; Mon, 19 May 2025 12:26:09 +0000 (UTC) Received: from smtp.kernel.org (transwarp.subspace.kernel.org [100.75.92.58]) by dfw.source.kernel.org (Postfix) with ESMTP id 912645C059C; Mon, 19 May 2025 12:23:51 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id D9960C4CEE4; Mon, 19 May 2025 12:26:06 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1747657568; bh=IDm1lnmH8i5Jc0QN2R5yydX3w8LDzL7R8VSGykatnf8=; h=Date:Cc:Subject:From:To:References:In-Reply-To:From; b=Kkh2beBpeRsbGlCBVl8e0CULPkNejvQJ4zJKUYGzUejxFwtsFkLHFkidcguhV/2TP ZLP1qFSw7xP9TheeusRNFJpeVDpYPaab0+0k6fQqxV9R6Itm2+buupGUTzjm0AVRfo PRTw5b3EtnkQH1+BCGit9iwe0WK79FUMQmjOAuaeDZaG0H3h2zGVU/xsgNweeQ73v/ n6hHpK3sGEmELblGyxn8uU3mSFK2Z0b7DlETQjZSnVoQL3AlrdxZcTOqxHh9cIZwbw Wft67JZugUPPSGhIcfrJAzrgvgqC1jtK16SWicBcYnjeL+O03YLw3l5tLGuTHWeB6+ B07l/91pwH77g== Precedence: bulk X-Mailing-List: linux-kernel-mentees@lists.linux.dev List-Id: List-Subscribe: List-Unsubscribe: Mime-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=UTF-8 Date: Mon, 19 May 2025 14:26:05 +0200 Message-Id: Cc: "Marcelo Moreira" , , , , , , <~lkcamp/patches@lists.sr.ht> Subject: Re: [PATCH v2] rust: doc: Clarify safety invariants for Revocable type From: "Benno Lossin" To: "Danilo Krummrich" X-Mailer: aerc 0.20.1 References: <20250503145307.68063-1-marcelomoreira1905@gmail.com> In-Reply-To: On Mon May 19, 2025 at 1:37 PM CEST, Danilo Krummrich wrote: > On Mon, May 19, 2025 at 01:10:32PM +0200, Benno Lossin wrote: >> On Mon May 19, 2025 at 11:55 AM CEST, Danilo Krummrich wrote: >> > On Mon, May 19, 2025 at 11:18:42AM +0200, Benno Lossin wrote: >> > Why not? Please show me a case where `is_available` is false, but I ca= n still >> > technically access data (without violating a safety requirement). >>=20 >> let r: Arc> =3D ...; >> let guard =3D r.try_access().unwrap(); // nobody else is holding a r= eference, so this can't fail >>=20 >> let r2 =3D r.clone(); >>=20 >> // I know we don't have threads, but I don't want to have to look up >> // how to use the workqueue or something else... >> thread::spawn(move || { >> r2.revoke(); >> }); >>=20 >> for _ in 0..10_000_000 { >> // do some non-sleeping work that takes a while >> } >>=20 >> // now the thread above has executed `self.is_available.swap(false, = Ordering::Relaxed)` >> // in `revoke_internal` and is waiting for the `synchronize_rcu` cal= l to return. >> // but we can still access `guard`: >>=20 >> pr_info!("{}", &*guard); > > Which is perfectly correct, you're right. I think I was too focused on th= e > optimization case. :-) And I was assuming the example was obvious with just saying "But the `is_available` atomic *can* be altered during the usage of `data`." :-) >> > However, this invariant does not need to be fulfilled for access() and >>=20 >> Where is `access()` defined? > > https://gitlab.freedesktop.org/drm/nova/-/commit/46f91addfabbd4109fb64876= a032ae4a4a924919 "Reviewed-by: Benno Lossin " huh, I already forgot about the patch... But that also shouldn't be difficult to support with the right invariant. >> > revoke_nosync(), because it would circumvent their purpose, i.e. cases= where an >> > abstraction can prove that there can't be a concurrent user of the dat= a or a >> > concurrent user revoking the data respectively. >>=20 >> Yes. How about something like "`data` is valid while `is_available` is >> true. It also is valid if the RCU read-side lock is being held and it >> was taken while `is_available` was true."? >>=20 >> That should also cover the "nobody else is accessing this" case. > > Sounds good to me! I'm not happy with the sentence structure, so how about: * `data` is valid for reads in two cases: * while `is_available` is true, or * while the RCU read-side lock is taken and it was acquired while `is_a= vailable` was `true`. * `data` is valid for writes when `is_available` was atomically changed fro= m `true` to `false`. The last one is needed in order to call `drop_in_place`. --- Cheers, Benno