Re: [PATCH v1] driver core: unbind only the driver whose unbind file was written

[Nickolai Zeldovich]

On Sat, Oct 17, 2026 at 5:49 AM Greg Kroah-Hartman
<gregkh@xxxxxxxxxxxxxxxxxxx> wrote:
> > The pattern is as old as the unbind file: the check was never under the
> > lock and the release never named the driver.  The locked variant has
> > existed since commit 4bdb35506b89 ("driver core: Add a wrapper around
> > __device_release_driver()") added the drv argument to
> > device_release_driver_internal() for driver_detach(), which has the
> > same requirement.
>
> Because this has always been present, and no one has actually reported
> this, perhaps it is not really a problem at all?  In other words, what
> real-life-use requires this?  Again, bind/unbind is for developers only.

The goal was to pin down a precise spec of what should happen when
writing a device name A to /sys/bus/B/drivers/D/unbind.  I think the
intended effect is that it should unbind driver D from device A.  The
code already has a check that tries to ensure this.  However, the
check isn't technically enough to achieve this precise effect, in the
presence of concurrent operations on other cores (like
binding/unbinding other drivers to the same device).

It sounds like this level of precise specification under weird
concurrent operations isn't useful for developer-facing interfaces.
I'll stick to more clear-cut bugs.

> ...
> > Found by formal verification of drivers/base/bus.c.
>
> Where is the formal verification proof?  Please don't have your LLM
> claim this without that as it's pointless.

The intended point was to give some indication of where this patch is
coming from: it aims to formally prove something about the behavior of
the kernel, rather than fix any specific issue encountered by a Linux
user.  There isn't a formal spec for the Linux user-kernel boundary,
though (as in the above example: what exactly should happen in this
weird concurrent scenario?), so for many cases I'm trying to infer
what the expected spec is.

Happy to describe it in more detail once I have a coherent checkpoint.
The current proofs aren't complete for Linux yet; we'll see if it's
possible to get there.  We verified a smaller OS kernel
(https://arxiv.org/abs/2609.04043) and now I'm trying to do the same
for Linux, roughly speaking.

Nickolai.