Re: [SystemSafety] Scalability of Formal Methods [was: Logic]

From: Rod Chapman < >
Date: Thu, 27 Feb 2014 13:15:47 +0000

Patrick Wrote:
>I'll point out that neither SPARK proofs nor any other formal verification
>are deductive proof that the software will operate as specified when
deployed on real
>target hardware.

I've followed this thread with some interest. Patrick raises ligitimate concerns regarding the trustworthiness of compilers, and the assumptions that underpin static verification systems such as SPARK.

As the current technical authority of SPARK team, I feel I can (and probably should) offer some response.

Over the years, I have worked on and with many projects using SPARK with commerical Ada compilers for a vareity of "real world" targets. I have observed that real "compiler silently generates the wrong object code" bugs are actually very rare. Why should this be?

Well..having thought about it for a few days, I can offer the following observations:

  1. Ease and correctness of compilation really were design goals of SPARK from the very beginning. In 1987, reliable compilation of Ada83 was still seen as something of a challenge, so the language was very conservative indeed at steering clear of hard-to-verify constructs, such as derived types, generics and tasking. It turns out there seems to be some correlation between "hard to verify" and "hard to compile correctly". In short: if you want correct compilation, then make your language (subset) small!
  2. Over the years, SPARK has grown substantially in expressive power, but that's been matched by the growing maturity of commerical-grade compilers. I am personally familiar with AdaCore's internaly quality control system, and it's as good as anything I've ever seen for any software product.
  3. With compilers, you get what you pay for. Don't confuse the quality of the "free" GCC builds from FSF, for example, with the quality of compilers from commercial vendors.
  4. A great many problems reported as "compiler bugs" are not actually bugs at all, but are instance of the user unintentionally writing code that exhibits unspecified or undefined behaviour. Modern compilers can do some very surprising things with propagating undefinedness, for example.
  5. SPARK's single most important design goal is the provision of an unambiguous dynamic semantics, which basically means getting rid of all the undefined and unspecified behaviours. This means the verification tools can stand a chance of being sound, but it also means SPARK seems to be immune from many compiler-related problems - even in the face of aggressive optimization, SPARK programs "just work"...see our work in the SPARKSkein reference implementation, for example.
  6. This also makes SPARK program really portable, since the semantics are independent of compiler and target machine. We once (some time ago) had a customer do a "mid life upgrade" on an application, switching from Transputer (yes..that long ago) to PowerPC, from Ada83 to Ada95, and changing compiler vendor en-passant. It worked with apparently very little pain, and I recall "one line of code had to change, but that was a timing constant."
  7. The SPARK tools do indeed assume that memory is reliable, so that program variables will behave as expected, although the language draws a strict distinction between "normal" program variables and "external" variables, which are never trusted to be "in type" when read. Ada95 introduced the special 'Valid attribute to deal with this, and the SPARK tools are smart enough to know what it means, so that proofs can be discharged but only after an externally read value has been properly validated.
  8. Patrick is right to point that all SPARK programs include some fragments written in Ada, C, assembler, or something else. I don't think I've ever seen a 100% SPARK program deployed. At these boundaries, we are very careful to firstly minimize the amount of non-SPARK code, then to verify the contracts, interface, and bodies of the non-SPARK stuff using whatever means necessary.

I think that's all I can come up with for now.

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Thu Feb 27 2014 - 14:18:24 CET

This archive was generated by hypermail 2.3.0 : Wed Feb 20 2019 - 21:17:07 CET