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/
>> // # 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.
