On Wed Jan 28, 2026 at 1:35 PM JST, Eliot Courtney wrote:
> On Tue Jan 27, 2026 at 3:04 AM JST, Gary Guo wrote:
>>> // - We will only access the driver-owned part of the shared
>>> memory.
>>> // - Per the safety statement of the function, no concurrent
>>> access will be performed.
>>> let gsp_mem = &mut unsafe { self.0.as_slice_mut(0, 1)
>>> }.unwrap()[0];
>>> - // PANIC: per the invariant of `cpu_write_ptr`, `tx` is `<=
>>> MSGQ_NUM_PAGES`.
>>> + // PANIC: per the invariant of `cpu_write_ptr`, `tx` is `<
>>> MSGQ_NUM_PAGES`.
>>
>> Can this just be `tx < MSGQ_NUM_PAGES`?
>
> In previous discussion[1] it's been noted that it's important to
> explain why the preconditions are satisfied, not just what they are,
> so that's the reason I kept this in. Happy to hear arguments either
> way though.
>
> [1]:
> https://lore.kernel.org/all/CAH5fLgg0O=t2T2MQH2hvm4eZnCOa_NffzRw=XZPi9+7+=xs...@mail.gmail.com/
I agree it's a good idea to mention the source of the invariant, lest we
may lose track of why it is indeed true.
>
>>> // # Invariants
>>> //
>>> - // - The returned value is between `0` and `MSGQ_NUM_PAGES`.
>>> + // - The returned value is between `0` and `MSGQ_NUM_PAGES - 1`,
>>> inclusive.
>>
>> I wonder if this can be `is within 0..MSGQ_NUM_PAGES`. What do others think?
>
> I think this is very reasonable, since this is part of the rust
> range syntax so it should be understandable. I also considered the
> mathematical syntax `[0, MSGQ_NUM_PAGES)`, but not sure if this would
> be conventional - it does seem that this notation is used in a bunch
> of places though. Will apply your suggestion in the next version unless
> there is a definitive convention for this.
Since this is Rust code, the Rust syntax to express ranges (within ``
quotes) makes sense IMHO.
