linux-mm.kvack.org archive mirror
 help / color / mirror / Atom feed
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
>



  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