From: Gabriele Paoloni <gpaoloni@redhat.com>
To: Jonathan Corbet <corbet@lwn.net>
Cc: shuah@kernel.org, linux-kselftest@vger.kernel.org,
linux-kernel@vger.kernel.org, linux-doc@vger.kernel.org,
gregkh@linuxfoundation.org, linux-mm@kvack.org,
safety-architecture@lists.elisa.tech, acarmina@redhat.com,
kstewart@linuxfoundation.org, chuckwolber@gmail.com
Subject: Re: [RFC v2 PATCH 2/3] /dev/mem: Add initial documentation of memory_open() and mem_fops
Date: Wed, 17 Sep 2025 17:38:25 +0200 [thread overview]
Message-ID: <CA+wEVJatTLKt-3HxyExtXf4M+fmD6pXcmmCuhd+3-n2J_2Tw8A@mail.gmail.com> (raw)
In-Reply-To: <874it3gx2q.fsf@trenco.lwn.net>
Hi Jonathan
On Tue, Sep 16, 2025 at 12:39 AM Jonathan Corbet <corbet@lwn.net> wrote:
>
> Gabriele Paoloni <gpaoloni@redhat.com> writes:
>
> > 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
>
> > Signed-off-by: Gabriele Paoloni <gpaoloni@redhat.com>
> > ---
> > 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
>
next prev parent reply other threads:[~2025-09-17 15:38 UTC|newest]
Thread overview: 25+ messages / expand[flat|nested] mbox.gz Atom feed top
2025-09-10 16:59 [RFC PATCH v2 0/3] Add testable code specifications Gabriele Paoloni
2025-09-10 16:59 ` [RFC v2 PATCH 1/3] Documentation: add guidelines for writing " Gabriele Paoloni
2025-09-15 22:33 ` Jonathan Corbet
2025-09-17 15:24 ` Gabriele Paoloni
2025-10-20 19:35 ` David Hildenbrand
2025-10-20 20:54 ` Chuck Wolber
2025-10-20 21:02 ` Chuck Wolber
2025-10-21 15:37 ` David Hildenbrand
2025-10-21 16:27 ` Gabriele Paoloni
2025-10-21 16:34 ` David Hildenbrand
2025-10-21 16:43 ` Gabriele Paoloni
2025-09-10 16:59 ` [RFC v2 PATCH 2/3] /dev/mem: Add initial documentation of memory_open() and mem_fops Gabriele Paoloni
2025-09-15 22:39 ` Jonathan Corbet
2025-09-16 7:29 ` Chuck Wolber
2025-09-17 15:38 ` Gabriele Paoloni [this message]
2025-09-10 17:00 ` [RFC v2 PATCH 3/3] selftests/devmem: initial testset Gabriele Paoloni
2025-10-21 7:35 ` Greg KH
2025-10-21 17:40 ` Alessandro Carminati
2025-10-21 7:35 ` [RFC PATCH v2 0/3] Add testable code specifications Greg KH
2025-10-21 9:42 ` Gabriele Paoloni
2025-10-21 16:46 ` Greg KH
2025-10-22 14:06 ` Gabriele Paoloni
2025-10-22 17:13 ` Greg KH
2025-11-07 16:29 ` Chuck Wolber
2025-11-26 13:55 ` Greg KH
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=CA+wEVJatTLKt-3HxyExtXf4M+fmD6pXcmmCuhd+3-n2J_2Tw8A@mail.gmail.com \
--to=gpaoloni@redhat.com \
--cc=acarmina@redhat.com \
--cc=chuckwolber@gmail.com \
--cc=corbet@lwn.net \
--cc=gregkh@linuxfoundation.org \
--cc=kstewart@linuxfoundation.org \
--cc=linux-doc@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=linux-kselftest@vger.kernel.org \
--cc=linux-mm@kvack.org \
--cc=safety-architecture@lists.elisa.tech \
--cc=shuah@kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox