On Wed, Dec 13, 2023 at 11:40:26PM +0000, Benno Lossin wrote:

On 12/13/23 22:48, Andrew Lunn wrote:

quoted

quoted

Well, a safety comment is a basic part of Rust, which identifies the
safe/unsafe boundary (i.e. where the code could go wrong in memory
safety) and without that, the code will be just using Rust syntax and
grammar. Honestly, if one doesn't try hard to identify the safe/unsafe
boundaries, why do they try to use Rust? Unsafe Rust is harder to write
than C, and safe Rust is pointless without a clear safe/unsafe boundary.
Plus the syntax is not liked by anyone last time I heard ;-)

Maybe comments are the wrong format for this? Maybe it should be a
formal language? It could then be compiled into an executable form and
tested? It won't show it is complete, but it would at least show it is
correct/incorrect description of the assumptions. For normal builds it
would not be included in the final binary, but maybe debug or formal
verification builds it would be included?

That is an interesting suggestion, do you have any specific tools in
mind?

Sorry, no. I've no experience in this field at all. But given the
discussions this patch has caused, simply a list of C or Rust
expressions which evaluate to True when an assumption is correct would
be a good start.

We have said that we assume the phydev->lock is held. That is easy to
express in code. We have said that phydev->mdio must be set, which is
again easy to express. phydev->mdio.addr must be in the range
0..PHY_MAX_ADDR, etc.

You probably cannot express all the safety requirements this way, but
the set you can describe should be easy to understand and also
unambiguous, since it is code. The rest still can be as comments.  It
would be easy to compile this code and insert it before the function
on a verification build. Its only runtime checking, but its more
functional than comments which the compiler just throws away. And
maybe subsystems like this which are pretty much always slow path
might even leave them enabled all the time, to act as a set of
assert()s, which you sometimes see in code bases.

	Andrew