Proving the Correctness of GNAT Light Runtime | Hacker News Reader

Proving the Correctness of GNAT Light Runtime

blog.adacore.com

75 pointsrbanffy8 comments

I'm a little disappointed in the lack of substantive discussion here! There are many interesting technical issues raised by this post ripe for discussion. For instance:

> As you can see from the source files, that required adding many specifications (around 400 preconditions and 500 postconditions) and ghost code (around 150 loop invariants, 400 assertions, 300 ghost entities), and the daily proof takes 1.5 hours on a Linux server with 36 cores.

So 40 units with only a few hundred pre/post conditions and invariants seems to take an enormous amount of compute time to verify.

I expect that the verifier has already been fairly well optimized since Spark has been around awhile. Is this the case?

For verification in general, is the expense of verification in this case because of the model needed to verify Ada? For instance, perhaps a language that makes different choices might have a model checker that could scale better.

This has important implications for scaling formal methods to more software.

> For verification in general, is the expense of verification in this case because of the model needed to verify Ada? For instance, perhaps a language that makes different choices might have a model checker that could scale better.

I don't think so. The SPARK subset has been chosen to aid verification. The problem of proof is inherently computationally hard, and the most gains you can expect will come from advances in solver technology, both algorithmic and in terms of scaling to multiple cores or GPU eventually.

Just my opinion :) But I work at AdaCore (not on SPARK) so have some familiarity with the subject.

Here, we are targeting full functional specification, which is hard. So there is a lot of ghost code to support the proof (the loop invariants, assertions and ghost entities). That's what's driving the verification time up. I don't find this enormous at all, given the guarantees provided.

Most code in SPARK is proved to a much more modest level, where the proof is much easier, and that's where you get scaling.

And yes, we're using the best available provers for the task under the hood (currently Alt-Ergo, CVC4, Z3 and COLIBRI), and on some of the checks in that proof of the light runtime, a call to a single prover on a single check may take minutes.

I sometimes wonder if we would be better off using a lot more formal methods and specifications. It would be a lot more effort, but is it really less than all the "maintenance" we do to fix bugs and wrangle huge amounts of technical debt?

I mean, if it's proven code, it's probably a lot simpler, also.

AdaCore rocks. Such professionals. Serious about their work and the success of their customers. I was proud to have helped an employer form a relationship with them.

Glad to see AdaCore reaching for the limits of their tech to improve the trust base. I hope there are some lessons learned there on the direction the proof tech needs to go in, for further solidification of our base. I also like where they're going with network stacks https://blog.adacore.com/enhancing-the-security-of-a-tcp-sta... , can't wait to get some time off to try and plug all that in something like dpdk :-)

This is awesome. Proofs about runtimes increase confidence for all their users - or tell us what needs fixing. I hope to see more of this kind of thing.

This is really amazing work from AdaCore, as usual!

Reply on news.ycombinator.com