Validation of compiler and IDE - Why, when and how to? - Part 2: compilers
By Mitch on Friday, 28 March 2014, 12:50 - Processes - Permalink
We saw in the last post how to validate a software development tool. But we saw also that validating a compiler this way is not a satisfactory task.
Then: Why, when, and how to validate a compiler?
Why?
A compiler is an assembly of finite state machines, which transform programming language into assembly code or P-code. Given their complexity, there are good chances that some bugs remain in compilers.
Want to se a list of opened bugs on a compiler? Have a look at gcc bugs in C++ or bugs in C!
Looking at these lists, are you convinced that bugs remain in compilers? And why a compiler should be validated?
Fortunately, most of these bugs arise when advanced language features are used! And fortunately, the effect of most of these bugs is that the code won't compile.
This is why coding rules are important for critical software. Using simplified coding rules (eg: no use of advanced language features) is the best way to avoid compiler bugs.
When?
Now that we understand that a compiler should be validated, when should we do it?
When compiler bug may generate an unacceptable risk for the patient or the operator using the compiled software.
Examples (dummy, as usual): There's a bug in the rounding of floating point variables under certain circumstances, and at runtime output values are randomly inconsistent. In which context is it unacceptable:
- The compiled software is a PACS viewer: displayed images are very rarely affected by the bug, with a few pixels in wrong color. The practician will see that occasionally some pixels are inconsistent. Negligible risk for the patient (the manufacturer didn't even bother to fix the bug!).
- The compiled software is in a perfusion pump: the computed volumes are inconsistent from time to time. The manufacturer will discover the bug in software tests (the software is class C, it has hundreds of unit tests). And in the very unlikely case that the bug is not found during tests, if it arises in real conditions, there is still a watchdog protection which rips off too high volume values.
- The compiled software is in a pacemaker! The computed energy quantity in an electric shock is inconsistent from time to time. Accuracy in the energy quantity is absolutely vital. Oops! I think I'm going to validate my compiler!
How?
Validating a compiler is not an easy task.
Given its complexity, only formal validation is possible, namely by mathematical demonstration.
There's a team at INRIA who works on this infinite task and they created a compiler named CompCert. CompCert is the result of their research in formal validation.
Xavier Leroy, researcher at INRIA, presented the results of his team about C compiler validation at a symposium dedicated to code generation in 2011. Here is his presentation: http://www.cgo.org/cgo2011/Xavier_Leroy.pdf
His presentation looks quite readable at the beginning but it becomes quickly very difficult to follow. Just have a look at this presentation to see the complexity of formal compiler validation!
There are also commercial compiler validation suites which contain thousands of tests cases to verify compilers compliance to C language standards. These products don't provide a formal validation, like CompCert. But they reduce the probability of error in a compiler to an extremely low probability.
But they are extremely expensive. Because they contain a huge history of tests added day by day by their manufacturers.
That's why unless working on very critical medical device, it's better to spend time testing the software than the chain of development tools. If there is a bug in the compiler then the generated code will be buggey as well.
By the way: why shouldn't we validate processors as well?
Remember the fdiv error in Intel pentium 4 instruction set. :-)
See also the next article, with additional comments on this topic.
