Date: Wed, 13 Dec 2023 23:40:26 +0000
From: Benno Lossin <benno.lossin@...ton.me>
To: Andrew Lunn <andrew@...n.ch>, Boqun Feng <boqun.feng@...il.com>
Cc: FUJITA Tomonori <fujita.tomonori@...il.com>, alice@...l.io, netdev@...r.kernel.org, rust-for-linux@...r.kernel.org, tmgross@...ch.edu, miguel.ojeda.sandonis@...il.com, wedsonaf@...il.com, aliceryhl@...gle.com
Subject: Re: [PATCH net-next v10 1/4] rust: core abstractions for network PHY drivers

On 12/13/23 22:48, Andrew Lunn wrote:
>> 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?
There are some Rust tools for formal verification, see
https://rust-formal-methods.github.io/tools.html
but I don't know if they can be used in the kernel, especially since we
would need a tool that also supports C (I have no experience/knowledge
of verification tools for C, so maybe you have something).
Also my experience tells me that there are several issues with formal
verification in practice:

1. When you want to use some formal system to prove something it is
   often an "all or nothing" game. So you will have to first verify
   everything that lies beneath you, or assume that it is correctly
   implemented. But assuming that everything is correctly implemented is
   rather dangerous, because if you base your formal system on classical
   logic [1], then a single contradiction allows you to prove
   everything. So in order for you to be _sure_ that it is correct, you
   need to work from the ground up.

2. There is no formal Rust memory model. So proving anything for
   interoperability between Rust and C is going to be challenging.

3. The burden of fully verifying a program is great. I know this, as I
   have some experience in this field. Now the programmer not only needs
   to know how to write a piece of code, but also how to write the
   required statements in the formal system and most importantly how to
   prove said statements from the axioms and theorems.


When using safety comments, we avoid the problems of having to prove the
statements formally (which is _very_ difficult). Of course people still
need to know how to write safety comments, which is why I am working on
a standard for safety comments. I hope to post an RFC in a couple weeks.
It will also make the safety comments more formal by having a fixed
set of phrases with exact interpretations, so there can be less room for
misunderstandings.


[2]: You might try to work around this by using a paraconsistent logic,
     but I have little to no experience with that field, so I cannot
     really say more than "it exists".


>> Having a correct safety comment is really the bottom line. Without that,
>> it's just bad Rust code, which I don't think netdev doesn't want either?
>> Am I missing something here?
> 
> It seems much easier to agree actual code is correct, maybe because it
> is a formal language, with a compiler, and a method to test it. Is

I disagree. You always have to consider the entire kernel when you want
to determine if some piece of code is correct. This is by the nature of
the formal language, anything can affect anything.
For example you consider this:

    foo(void **ptr) {
        *ptr = NULL;
        synchronize_rcu()
        print(**x)
    }

How do you know that this is correct? Well you have to look at all
locations where `foo` is invoked and see if after a `synchronize_rcu`
the supplied pointer is valid.

If we do the safety comment stuff correctly, then we have a _local_
property, so something where you do not have to consider the entire
kernel. Instead you assume that all other safety comments are correct
and then only verify the boundary. If all boundaries agree, we have a
reasonably correct program.

> that code really bad without the comments? It would be interesting to
> look back and see how much the actual code has changed because of
> these comments? I _think_ most of the review comments have resulted in
> changes to the comments, not the executable code itself. Does that
> mean it is much harder to write correct comments than correct code?

The code not having changed does not mean that it is correct. There are
no obvious issues present, but can we really know that it is correct?
Only time will tell (or a formal verification).

The issue that we currently have with this patch series is that the
people who know how the stuff works and the people who know how to
write good safety comments are not the same. I hope that my safety
standard will help close this gap.

For example we do not know how the synchronization mechanism for
`phy_suspend` and `phy_resume` work, but you mentioned in some previous
thread that the knowledge is actually somewhere out there. It would help
us a lot if you could give us a link or an explanation. Then we can work
on a suitable safety comment.

-- 
Cheers,
Benno

Powered by blists - more mailing lists