What every C Programmer should know about undefined behavior #2/3 [LWN.net]

What every C Programmer should know about undefined behavior #2/3

Posted May 17, 2011 22:38 UTC (Tue) by cmccabe (guest, #60281)
In reply to: What every C Programmer should know about undefined behavior #2/3 by marcH
Parent article: What every C Programmer should know about undefined behavior #2/3

I'm not against the use of little proof checkers when writing code. Arguably, static type systems are just examples of little proof checkers. Another example is the lexing and parsing step where the compiler decides whether your program is syntactically correct. You can argue that while parsing the program, it proves that the program is parsable.

Polyspace looks like another such tool. It can prove that certain programs clearly violate C semantics, like dereferencing a NULL pointer. But it can't prove the program as a whole correct because it doesn't have enough information about the requirements and the environment.

There are other examples of little model checkers. Sparse allows kernel hackers to annotate functions with interesting properties like what locks it takes, etc. cpplint finds potential errors in C++ programs. And -Wall and -Wextra add even more checks. Those things are great and we should have more of them.

But if you did a survey of most academic programming language departments, you would find that most of them focus on developing completely new programming languages and rewriting things from scratch. Nothing is more common than a grad student inventing a new functional programming language for his thesis. Nothing is more uncommon than an actual useful tool coming out of it. Even your own example confirms this: Polyspace is commercial and not developed in academia.

to post comments

What every C Programmer should know about undefined behavior #2/3

Posted May 18, 2011 0:34 UTC (Wed) by price (guest, #59790) [Link] (5 responses)

> Polyspace is commercial and not developed in academia.

Wrong. It is commercial, but it came from academia.

Quick history of Polyspace, unfortunately quoting an obituary (http://christele.faure.pagesperso-orange.fr/AlainDeutsch.html - see original for many links):

1992-1993: Alain obtained his PhD on static analysis by abstract interpretation for dynamic data structures with pointers. He made a post-doc at the University of Carnegie-Mellon on the static analysis of communication protocols.
1993-1996: Alain joined PARA/INRIA Rocquencourt. He focussed on the static analysis of programs and developed the IABC analyser based on abstract interpretation.
1996-1999: He specialized his IABC analyzer to runtime error detection in Ada source code and proved the effectiveness of static analysis by exhibiting code errors in the flight programme of Ariane 5 incriminated in the flight 501 crash. Alain was a member of the qualification board of flight 502, which gave the green light for the second (successful) launch of Ariane 5. ...
1999-2006: He founded PolySpace Technologies together with Daniel Pilaud and became the Technical Director (Chief Technical Officer). PolySpace Technologies industrialized his IABC analyzer for Ada source code, extended it to C C++ Ada95 and commercialized PolySpace Verifier for Ada83, C, C++, Ada95.

So the tool was developed by a PhD researcher working at a research lab (and well-known hotbed of static type systems), refined for several years, and finally commercialized by him and others.

Another static analysis tool widely used in practice is Coverity -- that one came from a bunch of academics at Stanford. That's the usual story for this kind of tool.

What every C Programmer should know about undefined behavior #2/3

Posted May 18, 2011 4:08 UTC (Wed) by cmccabe (guest, #60281) [Link] (4 responses)

I stand corrected. It looks like Polyspace came mostly from academia.

It's also interesting that it was associated with the launch of a European rocket, Ariane 5. Everyone knows that the space race in the 1960s helped to push technology ahead in the United States; I guess that still happens, at least to a certain extent.

I think this kind of research is really interesting. It seems like it could help create more efficient compilers and perhaps better tools.

For what it's worth, I like static type systems. I really hope that in the future, we'll be able to have more and more information about programs even before running them. Programmers ought to be free from the drudgery of spotting typos or passing the wrong arguments to functions. Or even accidentally dereferencing a pointer before assigning it. As I said before, though, there are always things in the design that are impossible to "prove" (in the mathematical sense), like user interface, the performance of heuristic algorithms, and artistic design.

What every C Programmer should know about undefined behavior #2/3

Posted May 18, 2011 5:02 UTC (Wed) by price (guest, #59790) [Link] (3 responses)

Huh, nice observation re: this technology being connected to the space race. I hadn't made that connection.

Definitely beats Tang, if you ask me.

What every C Programmer should know about undefined behavior #2/3

Posted May 19, 2011 3:53 UTC (Thu) by raven667 (subscriber, #5198) [Link] (2 responses)

If Feynman is to be believed then a significant part of modern technological living was developed at least in part as part of the space race and this is evidence that this continues to be true at a smaller scale.

What every C Programmer should know about undefined behavior #2/3

Posted May 19, 2011 13:11 UTC (Thu) by marcH (subscriber, #57642) [Link] (1 responses)

Do not forget World War II just before that. In some cases the same people involved http://en.wikipedia.org/wiki/Wernher_von_Braun

What every C Programmer should know about undefined behavior #2/3

Posted May 19, 2011 18:01 UTC (Thu) by raven667 (subscriber, #5198) [Link]

well that part of the space race was about who captured the better germans at the end.