Hi Jonathan

On Tue, Sep 16, 2025 at 12:39 AM Jonathan Corbet [off-list ref] wrote:

Gabriele Paoloni [off-list ref] writes:

quoted

This patch proposes initial kernel-doc documentation for memory_open()
and most of the functions in the mem_fops structure.
The format used for the specifications follows the guidelines
defined in Documentation/doc-guide/code-specifications.rst

I'll repeat my obnoxious question from the first patch: what does that
buy for us?

I tried to explain my reply on patch 1

quoted

Signed-off-by: Gabriele Paoloni <redacted>
---
 drivers/char/mem.c | 231 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 225 insertions(+), 6 deletions(-)

diff --git a/drivers/char/mem.c b/drivers/char/mem.c
index 48839958b0b1..e69c164e9465 100644
--- a/drivers/char/mem.c
+++ b/drivers/char/mem.c

@@ -75,9 +75,54 @@ static inline bool should_stop_iteration(void)
      return signal_pending(current);
 }

-/*
- * This funcion reads the *physical* memory. The f_pos points directly to the
- * memory location.
+/**
+ * read_mem - read from physical memory (/dev/mem).
+ * @file: struct file associated with /dev/mem.
+ * @buf: user-space buffer to copy data to.
+ * @count: number of bytes to read.
+ * @ppos: pointer to the current file position, representing the physical
+ *        address to read from.
+ *
+ * This function checks if the requested physical memory range is valid
+ * and accessible by the user, then it copies data to the input
+ * user-space buffer up to the requested number of bytes.
+ *
+ * Function's expectations:
+ *
+ * 1. This function shall check if the value pointed by ppos exceeds the
+ *    maximum addressable physical address;
+ *
+ * 2. This function shall check if the physical address range to be read
+ *    is valid (i.e. it falls within a memory block and if it can be mapped
+ *    to the kernel address space);
+ *
+ * 3. For each memory page falling in the requested physical range
+ *    [ppos, ppos + count - 1]:
+ *   3.1. this function shall check if user space access is allowed (if
+ *        config STRICT_DEVMEM is not set, access is always granted);
+ *
+ *   3.2. if access is allowed, the memory content from the page range falling
+ *        within the requested physical range shall be copied to the user space
+ *        buffer;
+ *
+ *   3.3. zeros shall be copied to the user space buffer (for the page range
+ *        falling within the requested physical range):
+ *     3.3.1. if access to the memory page is restricted or,
+ *     3.2.2. if the current page is page 0 on HW architectures where page 0 is
+ *            not mapped.
+ *
+ * 4. The file position '*ppos' shall be advanced by the number of bytes
+ *    successfully copied to user space (including zeros).

My kneejerk first reaction is: you are repeating the code of the
function in a different language.  If we are not convinced that the code
is correct, how can we be more confident that this set of specifications
is correct?  And again, what will consume this text?  How does going
through this effort get us to a better kernel?

In summary specifications provide the criteria to be used in verifying the
code (both when reviewing and testing).
Otherwise:
1) Developers and reviewers have no criteria to evaluate the code, other
than their expertise and judgement when they read it;
2) Testers would write test cases based on the code itself (so it is more
likely that a wrong code is not detected due to wrong test cases).

WRT your first point, if specifications are wrong, a reviewer or a test
would detect a gap between code and associated specs, hence leading
to process of scrutiny of both code and specs where such a gap must
be resolved. This is the reason why the duality of specification and tests
VS the code being verified lead to confidence in code becoming more
dependable (also from a user point of view that can now clearly see
the assumptions to be met when invoking the code)

Thanks
Gab

Despite having been to a couple of your talks, I'm not fully
understanding how this comes together; people who haven't been to the
talks are not going to have an easier time getting the full picture.

Thanks,

jon