From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from smtp1.osuosl.org (smtp1.osuosl.org [140.211.166.138]) (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 6383D38FA6 for ; Fri, 23 May 2025 08:43:06 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=140.211.166.138 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1747989788; cv=none; b=lJeNsQCWEfrxdx0F38txrvlENy5Ec8qQx4AmiqM0HFJtjr4KOdDk51fP5azwNCK1rd7GZBomR4DuBpTF+ttxAuWuusytYtLgK4MZc+nLAmI8jv+fYxtFpOPPvYUFHlpXmYnFKEWnTymKn7gMq6FuKigT6Y2KquBXJEc7EFk8t/c= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1747989788; c=relaxed/simple; bh=16Fw6yJHs5tHc5W7VB0ZGnOAeG73IaGsWoRy5IXyoeE=; h=Mime-Version:Content-Type:Date:Message-Id:To:Cc:Subject:From: References:In-Reply-To; b=lkGIQAxgxQXA+6zmMl2/OoeFijbp0XYjGJHHDfnVCdWlovj1PZSX4O+xoYC1hNcHZLA/gEFIOjCXtE9iieTndTO2oUseOUqct7D5Ie6uYk/tUSK9ZQqLN7bw4CVb1yaqZkcL5WMhMLGSsGw0KHe2Cw+sE74jq1lmgETswH1pu04= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=fTNGv9Q9; arc=none smtp.client-ip=140.211.166.138 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="fTNGv9Q9" Received: from localhost (localhost [127.0.0.1]) by smtp1.osuosl.org (Postfix) with ESMTP id DA70183C5E for ; Fri, 23 May 2025 08:43:05 +0000 (UTC) X-Virus-Scanned: amavis at osuosl.org X-Spam-Flag: NO X-Spam-Score: -8.092 X-Spam-Level: Received: from smtp1.osuosl.org ([127.0.0.1]) by localhost (smtp1.osuosl.org [127.0.0.1]) (amavis, port 10024) with ESMTP id t-M9bssxeNVO for ; Fri, 23 May 2025 08:43:05 +0000 (UTC) Received-SPF: Pass (mailfrom) identity=mailfrom; client-ip=147.75.193.91; helo=nyc.source.kernel.org; envelope-from=lossin@kernel.org; receiver= DMARC-Filter: OpenDMARC Filter v1.4.2 smtp1.osuosl.org 1595083D5A Authentication-Results: smtp1.osuosl.org; dmarc=pass (p=quarantine dis=none) header.from=kernel.org DKIM-Filter: OpenDKIM Filter v2.11.0 smtp1.osuosl.org 1595083D5A Authentication-Results: smtp1.osuosl.org; dkim=pass (2048-bit key, unprotected) header.d=kernel.org header.i=@kernel.org header.a=rsa-sha256 header.s=k20201202 header.b=fTNGv9Q9 Received: from nyc.source.kernel.org (nyc.source.kernel.org [147.75.193.91]) by smtp1.osuosl.org (Postfix) with ESMTPS id 1595083D5A for ; Fri, 23 May 2025 08:43:04 +0000 (UTC) Received: from smtp.kernel.org (transwarp.subspace.kernel.org [100.75.92.58]) by nyc.source.kernel.org (Postfix) with ESMTP id DD296A4F1D3; Fri, 23 May 2025 08:43:02 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id B392AC4CEE9; Fri, 23 May 2025 08:43:00 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1747989782; bh=16Fw6yJHs5tHc5W7VB0ZGnOAeG73IaGsWoRy5IXyoeE=; h=Date:To:Cc:Subject:From:References:In-Reply-To:From; b=fTNGv9Q9VCTV8TdZMW8wizxI/zSxaEpoXDB2FdmUFwYvj5tpnQ/jme6mEXWHdReBn +b7hlJ9yeqANk1NZQ5106e17ADGdMfA85kFxvCBg/myZW187IY736LtrrnLbnEVnKN bhaApLX+Av0YHRwFhyjKQN5Qf3ivhClI4TYmlG4cHlBuz/ygrkP+uUBqGa8RYSizS8 x4QJrlMio9ZTOSM68Es6qJk5oJV83cy9txMoloqFsP7rAk08GNZG95BsF+uf2J/VRb lkC1lf4R8U7/6kEQKwNmkXmFDS4vdU0aHWAzXc8KeZ+TRAPGNF+TT2xoyDK0eMdxCv pVlCWS9cywgrw== 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: Fri, 23 May 2025 10:42:58 +0200 Message-Id: To: "Marcelo Moreira" , "Boqun Feng" Cc: "Danilo Krummrich" , , , , , , <~lkcamp/patches@lists.sr.ht> Subject: Re: [PATCH v2] rust: doc: Clarify safety invariants for Revocable type From: "Benno Lossin" X-Mailer: aerc 0.20.1 References: <20250503145307.68063-1-marcelomoreira1905@gmail.com> In-Reply-To: On Fri May 23, 2025 at 2:13 AM CEST, Marcelo Moreira wrote: > Thanks a lot for the discussions. I was reading them one by one and > trying to consolidate the ideas. > I am preparing a new patch version focused on improving everything > that was discussed. > > Before submitting the patch, I would like to understand if things are > clear to me. Here is what I am preparing: > > 1. Refined `Revocable` Invariants, suggested by Benno: > Proposed Documentation: > /// # Invariants > /// > /// - `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_available` was `true`. > /// - `data` is valid for writes when `is_available` was atomically > changed from `true` to `false`. A few comments: * your email client seems to wrap this line :( * the "two cases" should be indented, as they logically belong to the bullet point above. * the information for writing `data` needs to be changed according to what I suggested in reply to Danilo > 2. Updated try_access and try_access_with_guard Safety Comments: > Proposed Documentation: > // INVARIANT: `self.data` is valid for reads because > `self.is_available` is true, > // and the RCU read-side lock ensures this condition is maintained > during access. I'm missing the context *where* this invariant comment is placed. Maybe send the patch with the modification or send a link to a branch where you have the commit. > These comments now directly reference the new Revocable read invariant= s. > This addresses the point about justifying the access to data via the > invariants, > especially considering the RCU read-side lock. > > > 3. Clarified revoke_internal for SYNC =3D false and swap correction > Proposed Documentation: > if self.is_available.swap(false, Ordering::Relaxed) { > if SYNC { > // SAFETY: Just an FFI call, there are no further require= ments. > unsafe { bindings::synchronize_rcu() }; @Boqun: is this true? If the answer is yes, then we should add this as a safe function in the rcu module. > } else { > // This branch for `revoke_nosync` requires the caller to prove > that `data` > // can be dropped immediately without waiting for any RCU grace pe= riod. I'm not sure that having a single function that does the revocation, but has this going on is a good idea. The safety requirements will be pretty complex. @Danilo what do you think of inlining this function? > } > // SAFETY: We know `self.data` is valid because only one CPU can succeed = the > // `swap` above that takes `is_available` from `true` to `false`. > unsafe { drop_in_place(self.data.get()) }; > } > } > > I've added a comment for the SYNC =3D false branch (used by revoke_nosyn= c). > This explicit else block, even if semantically empty of executable code, = is for > documenting the unsafe contract for revoke_nosync(). It states that the = caller > must prove data safety since no RCU grace period is awaited, aligning wit= h > Danilo's explanation of revoke_nosync's purpose. Additionally, I've corre= cted > the comment from compare_exchange to swap to accurately reflect the > atomic operation used. > > > 4. Documented RevocableGuard<'_, T> Invariants and PhantomData Adjustment > Proposed Documentation: > /// # Invariants > /// > /// - The RCU read-side lock is held for the lifetime of this guard. > /// - `data_ref` points to valid data for the lifetime of this guard. > pub struct RevocableGuard<'a, T> { > data_ref: *const T, > _rcu_guard: rcu::Guard, > _p: PhantomData<&'a T>, > } I think we can change this type to: pub struct RevocableGuard<'a, T> { data: &'a T, _rcu_guard: rcu::Guard, } And then we don't need any invariants :) > This adds the # Invariants section for RevocableGuard, as we agreed it sh= ould > state its guarantees, including the RCU read-side lock. The adjustment of > _p: PhantomData<&'a ()> to _p: PhantomData<&'a T> is a minor improvement = in > type-level documentation, making the lifetime dependency more explicit to= the > Rust compiler and future readers. > > > 5. Revised RevocableGuard Deref Safety Comment > Proposed Documentation: > fn deref(&self) -> &Self::Target { > // SAFETY: By the invariants of `RevocableGuard`, the RCU > read-side lock is held, > // and `data_ref` points to valid data for the lifetime of this g= uard. > unsafe { &*self.data_ref } With the above change, this body becomes `self.data` :) > } > > The // SAFETY: comment for Deref is updated to refer to the RevocableGuar= d's new > invariants, providing a justification for the unsafe dereference. > > > 6. PinnedDrop for Revocable Safety Documentation & Readability > Proposed Documentation: > let p =3D unsafe { self.get_unchecked_mut() }; > if *p.is_available.get_mut() { > // INVARIANT: `is_available` is true, so `data` is valid for = reads. > // SAFETY: `self.data` is valid for writes because > `is_available` was atomically changed from true to false This is wrong? It still is `true`? > // in `PinnedDrop::drop`, and only one thread can do it > now as we have `&mut self`. > // This ensures `data` is valid for writes in this > context, allowing `drop_in_place`. > unsafe { drop_in_place(p.data.get()) }; > } > > The // INVARIANT: and // SAFETY: comments within the PinnedDrop > implementation are > updated to reflect the new write invariant of Revocable, justifying > the drop_in_place call. > > > Please let me know if something is wrong or unnecessary... I'll try to > rephrase if appropriate. Tks :D It already looks much better than what we have currently. It's fine to send a patch that's still needing review (and it makes it easier to review when I have the full context). So I'd just do that and we go from there. We're only on v2 on this one and I have seen patches go into the double digits, so don't worry about that. --- Cheers, Benno