Message-ID: <CA+wEVJajSGzb85YTiv98yAY3bcJFS0Qp_xjLc++wnU8t=wDAOg@mail.gmail.com>
Date: Wed, 22 Oct 2025 16:06:10 +0200
From: Gabriele Paoloni <gpaoloni@...hat.com>
To: Greg KH <gregkh@...uxfoundation.org>
Cc: shuah@...nel.org, linux-kselftest@...r.kernel.org, 
	linux-kernel@...r.kernel.org, corbet@....net, linux-doc@...r.kernel.org, 
	linux-mm@...ck.org, safety-architecture@...ts.elisa.tech, acarmina@...hat.com, 
	kstewart@...uxfoundation.org, chuckwolber@...il.com
Subject: Re: [RFC PATCH v2 0/3] Add testable code specifications

Hi Greg

On Tue, Oct 21, 2025 at 6:46 PM Greg KH <gregkh@...uxfoundation.org> wrote:
>
> On Tue, Oct 21, 2025 at 11:42:24AM +0200, Gabriele Paoloni wrote:
> > Hi Greg
> >
> > On Tue, Oct 21, 2025 at 9:35 AM Greg KH <gregkh@...uxfoundation.org> wrote:
> > >
> > > On Wed, Sep 10, 2025 at 06:59:57PM +0200, Gabriele Paoloni wrote:
> > > > [1] was an initial proposal defining testable code specifications for
> > > > some functions in /drivers/char/mem.c.
> > > > However a Guideline to write such specifications was missing and test
> > > > cases tracing to such specifications were missing.
> > > > This patchset represents a next step and is organised as follows:
> > > > - patch 1/3 contains the Guideline for writing code specifications
> > > > - patch 2/3 contains examples of code specfications defined for some
> > > >   functions of drivers/char/mem.c
> > > > - patch 3/3 contains examples of selftests that map to some code
> > > >   specifications of patch 2/3
> > > >
> > > > [1] https://lore.kernel.org/all/20250821170419.70668-1-gpaoloni@redhat.com/
> > >
> > > "RFC" implies there is a request.  I don't see that here, am I missing
> > > that?  Or is this "good to go" and want us to seriously consider
> > > accepting this?
> >
> > I assumed that an RFC (as in request for comments) that comes with proposed
> > changes to upstream files would be interpreted as a request for feedbacks
> > associated with the proposed changes (what is wrong or what is missing);
> > next time I will communicate the request explicitly.
> >
> > WRT this specific patchset, the intent is to introduce formalism in specifying
> > code behavior (so that the same formalism can also be used to write and
> > review test cases), so my high level asks would be:
> >
> > 1) In the first part of patch 1/3 we explain why we are doing this and the high
> > level goals. Do you agree with these? Are these clear?
>
> No, and no.
>
> I think this type of thing is, sadly, folly.  You are entering into a
> path that never ends with no clear goal that you are conveying here to
> us.
>
> I might be totally wrong, but I fail to see what you want to have happen
> in the end.
>
> Every in-kernel api documented in a "formal" way like this?  Or a
> subset?  If a subset, which ones specifically?  How many?  And who is
> going to do that?  And who is going to maintain it?  And most
> importantly, why is it needed at all?
>
> For some reason Linux has succeeded in pretty much every place an
> operating system is needed for cpus that it can run on (zephyr for those
> others that it can not.)  So why are we suddenly now, after many
> decades, requiring basic user/kernel stuff to be formally documented
> like this?

Let me try to answer starting from the "why".
IMO There are 2 aspects to consider.
The first one is that requirements/specification and associated tests
are valuable in claiming that Linux can be used in safety critical industries
(like automotive or aerospace).
The second one (that goes beyond the business need) is that the duality
of specifications and tests VS code increases the dependability of the
code itself so that its expected behaviour and associated constraints
are clear to the user and there is evidence of the code behaving as specified
(I already tried to address this point in [1]).
Some evidence of improvements can be found in the experiments we did.
E.g.:
- this [2] is a bug found in __ftrace_event_enable_disable()
- this [3] is a code optimization that came as we looked at the
specifications of
  __ftrace_event_enable_disable()
- here [4] we have documented assumptions of use that must be met when
  invoking event_enable_read(), otherwise there could be a wrong event status
  being reported to the user.

Finally the need for having specifications/requirements associated with Kernel
code has been already discussed at LPC'24 last year ([5]) and we got a thumb
up from some key maintainers with initial directions (hence we started
this activity).

[1] https://lore.kernel.org/all/CA+wEVJatTLKt-3HxyExtXf4M+fmD6pXcmmCuhd+3-n2J_2Tw8A@mail.gmail.com/
[2] https://lore.kernel.org/all/20250321170821.101403-1-gpaoloni@redhat.com/
[3] https://lore.kernel.org/all/20250723144928.341184323@kernel.org/
[4] https://lore.kernel.org/all/20250814122206.109096-1-gpaoloni@redhat.com/
[5] https://lpc.events/event/18/contributions/1894/

Now I'll try to answer about the goals.
I do not expect to have all Kernel APIs to be specified according
to the format that we are proposing; my initial goal is to have such
a formalism to be available in the Kernel so that developers that
need to write such specifications have a guideline available.
For example today we have a guideline to write kernel-doc comments,
however (AFAIK) patch acceptance is not gated by these being
present or not.
I think that developers having a direct interest can write such
specifications and associated tests and these could be reviewed and
eventually accepted by maintainers.

>
> In the past, when we have had "validating bodies" ask for stuff like
> this, the solution is to provide it in a big thick book, outside of the
> kernel, by the company that wishes to sell such a product to that
> organization to justify the cost of doing that labor.  In every instance
> that I know of, that book sits on a shelf and gathers dust, while Linux
> is just updated over the years in those sites to new versions and the
> book goes quickly out of date as no one really cares about it, except
> it having been a check-box for a purchase order requirement.

I agree and in fact a key ask from maintainers, as we discussed at
LPC'24 in [5], was to have the code specifications sitting next to the
code so that they could be maintainable as the code evolves (and they
would be even more maintainable if specs come with tests that can flag
regressions as the code evolves).

>
> That's business craziness, no need to get us involved in all of that.
> Heck, look at the stuff around FIPS certification for more insanity.
> That's a check-box that is required by organizations and then totally
> ignored and never actually run at all by the user.  I feel this is much
> the same.
>
> So step back, and tell us exactly what files and functions and apis are
> needed to be documented in this stilted and formal way, who exactly is
> going to be doing all of that work, and why we should even consider
> reviewing and accepting and most importantly, maintaining such a thing
> for the next 40+ years.

Putting business needs aside, I would expect maintainers, today, to
happily accept kernel-doc compliant code documentation as well as kunit
or selftests associated with the code; simply because they add technical
value.
If my assumption here is correct, having these kernel-doc specifications
clearly formalised should be an improvement for the maintainers (since
it would be easier to verify incoming patches when specs and tests are
in place and also it would be easier for a developer to write such
patches).

WRT the scope of code to be documented, I expect that to depend on
the vested interest of companies contributing to it.
The directions from the LPC24 session were to start with some pilot
drivers/subsystems first to define 'how' to specify the code and later
focus on what and scale...

>
> > 2) In the rest of the patchset we introduce the formalism, we propose some
> > specs (in patch 2) and associated selftests (in patch 3). Please let us know
> > if there is something wrong, missing or to be improved.
>
> I made many comments on patch 3, the most important one being that the
> tests created do not seem to follow any of the standards we have for
> Linux kernel tests for no documented reason.
>
> The irony of submitting tests for formal specifications that do not
> follow documented policies is rich :)

Thanks for your comments and sorry for the mistakes, I see that Alessandro
replied so we'll pay more attention in writing tests in the next revision.

Kind Regards
Gab

>
> thanks,
>
> greg k-h
>

Powered by blists - more mailing lists