Experimental Patches For Rust-Written Linux Network Drivers

[patrick1946]

Yes, I think we're in agreement.
Not only is the compiler taking a sizable portion of the burden away, it takes arguably the heaviest burden, in the sense that memory safety is the hardest thing for which a developer could build a mental model to try to solve it themselves.

Have you ever written heavily threaded code? There are other algorithms which are much more complex. I would say that ownership is the hardest problem in 90% of glue code(business logic) but there are other much more complex problems. Since I changed to TDD ownership problems vanished as a side effect.

That's I am not so enthusiastic about Rust because it can only solve compile time problems but many problems cannot not be described at compile time. I expect much better testing support. In my view Rust is still to strong in the mind model of a programmer as a poet.

[Nth_man]

Do you know any that works in a multi threading context? And does it work with dynamic memory?

Reading https://nvlpubs.nist.gov/nistpubs/ir...ST.IR.8304.pdf , Astree is able to do that. There are other sound static analyzers mentioned on that PDF.

[bug77]

Have you ever written heavily threaded code? There are other algorithms which are much more complex. I would say that ownership is the hardest problem in 90% of glue code(business logic) but there are other much more complex problems. Since I changed to TDD ownership problems vanished as a side effect.

That's I am not so enthusiastic about Rust because it can only solve compile time problems but many problems cannot not be described at compile time. I expect much better testing support. In my view Rust is still to strong in the mind model of a programmer as a poet.

Yeah, ownership...
My main tool is Java. OOP in general is a nightmare when it comes to ownership. I am currently fighting a few developers to make things private and final and have enabled them the spotbugs plugin, trying to get them to manage state (somewhat) properly. I know all too well how much of a weakness that is for OOP languages

Fwiw, I like how Go solves this: it tells you that once you have sent something over a channel, you are not to modify it anymore. That alone earns much of the memory safety of Rust. But, of course, at the cost of all developers observing that rule all the time.

[bug77]

"we can fix it with tooling" has been the promise for the past 50 years, and yet here we still are

Even if we could do that, I still fail to see how an external tool (that may or may not run) is better than compiler-enforced checks.

[Nth_man]

Even if we could do that, I still fail to see how an external tool (that may or may not run) is better than compiler-enforced checks.

Sound static analysis [...] is far more interesting because the results are as reliable as mathematical proofs.
-- https://sws.cs.ut.ee/Thesis/SoundAnalysis

Reading https://nvlpubs.nist.gov/nistpubs/ir...ST.IR.8304.pdf , some sound static analyzers can check Motor Industry Software Reliability Association (MISRA) guidelines, when human lives are at risk...

[bug77]

Sound static analysis [...] is far more interesting because the results are as reliable as mathematical proofs.
-- https://sws.cs.ut.ee/Thesis/SoundAnalysis

So is Rust's borrow checker.

Reading https://nvlpubs.nist.gov/nistpubs/ir...ST.IR.8304.pdf , some sound static analyzers can check Motor Industry Software Reliability Association (MISRA) guidelines, when human lives are at risk...

And we all know as a result there are no recalls because of software issues in the automotive industry, right? Static analyzers are that good.

[marlock]

I am out of my depth when asking this: can't a compiler do the same checks a static code analyser does? Or are there classes of issues that only a static analyser would be able to catch?

In my very very very non-expert mind anything you can implement in one could also be implemented into the other, at least as a means to generate non-blocking warnings and ideally blocking anything that you're sure is a mistake until overriden to allow it.

Also IMHO industries like automotive and aerospacial are an interesting exception. because of projects like AGL - Automotive Grade Linux, their higher-than-usual standards end up trickling down to general-purpose software codebases like the linux kernel and stack, which is great... but at the same time we all know the rest of the code made around them is prone to being developed in resource-constrained situations where cutting corners and generally not finding time to apply optional best practices (especially add-on instead of built-in practices) is the norm.

And that's even assuming no corners get cut in those higher-standards industries, which is slightly harder after seeing news about certains manufacturers being caught in the act cheating vehicular emissions testing and whatnot... I'm sure the checks and balances help, but they're not quite absolute like "impossible to skip", right?

[piotrj3]

Reading https://nvlpubs.nist.gov/nistpubs/ir...ST.IR.8304.pdf , Astree is able to do that. There are other sound static analyzers mentioned on that PDF.

You confuse few stuff....

First static sound analyzers require heavy adnotations in your code to proof safety of some stuff. There is very giant gap between adnotated code made from start to comply with something like Astree and hey let's take linux kernel through Astree. I doubt even such tool could proof mathematically safety (or unsafety) of such giant code base, but without adnotations on entire large code base you would generate milions of potential warnings and errors where 99% of them will be false positive. So when people say why use Rust, well because it will take you a ton more effort to write memory safe C with Astree (that will generate no warnings) then safe Rust without warnings.

Second what Richard Yao said is completly wrong that you quote on your website. All mathematically proven safety languages does have similar or greater runtime checks as Rust because they are impossible to avoid. Eg. simplest example : user provides index of array you read it from. Obviously you have to add runtime check. Rust does it for you and if you add own runtime check to have diffrent error handling Rust will remove own runtime checks because it will recognize you cover it. Astree and SPARK (and any mathematical proof of safety will force you to add it on your own. The diffrence is you have 3 classes of languages:
- ones where verification will force you (Astree analyzer),
- ones where runtime check added is minimal/only when necessery (Rust, SPARK and few more)
- ones with full runtime checking (most garbage collected langs),

Third. Most people instead of trying to prove safety of C will jump to language designed for their needs. You will not fight much with Rust (if you only aim memory safety), and you will fight a lot less with SPARK, comparing to trying to plug C through Astree.

Forth. Most people don't want absolute safety. Rust offers you memory safety (without unsafe) but allows you to go unsafe if needed. The same goes for most garbage collected languages - they are much easier to work with, although yea you can do some wrong stuff in them. Why people do that - because mathematically proving your entire work is entirly memory safe and entirly logical safe is damn hard. You can't eat your cake and have it.

People kinda forget aim of Rust is not true safety, but easier to write big programs with multithreading and without garbage collector and decent enough safety - in nutshell same niche as Go. Rust doesn't force you to write tons of adnotations like SPARK, FRAMA-C, MISRA-C, all sound static analyzers do. Rust simply proves you memory safety to reasonable limit, and it is commonly often making people it is too much for them. And you propose something like Astree for them? Good luck!

Astree aims as competition to something like SPARK - a widely used language in aviation/medical aplications. And best proof to SPARK is that Lockheed martin, general electic, Rolls-royce trent, Eurofighter, Nvidia firmware etc.. And actually Astree does provide lower safety comparing to SPARK - Astree fails to meet one criteria from DO-178C where SPARK meets all.

Just so you know DO-178C requirements say you need to prove absence of errors including even architecture of end system. For example, if compiler would transform code, you need to prove safety after transformation as well.

[darkonix]

"If a sound static analyzer were deployed, we could make C code with zero memory safety issues and do it without the hack of compiler added runtime checks [...] to claim memory safety. The aviation and nuclear power industries have been doing this for years". There is more information available.

What is preventing them to be deployed and save the world? On the other hand every single Rust program is already benefing of Rust assurances.

[bug77]

I am out of my depth when asking this: can't a compiler do the same checks a static code analyser does? Or are there classes of issues that only a static analyser would be able to catch?

In my very very very non-expert mind anything you can implement in one could also be implemented into the other, at least as a means to generate non-blocking warnings and ideally blocking anything that you're sure is a mistake until overriden to allow it.

Technically you can. But static analyzers are not meant to be real-time tools, so they can implement checks that take more time to perform that what's acceptable in a compiler. The catch is static analyzers are not guaranteed to run on every build. To make matters worse, the more the analysis takes, the less likely developers are to run it.