1. 11

The abstract reads:

In our Formalin project to formalize C11 (the ANSI/ISO standard of the C programming language) we discovered many subtleties that make formalization of this standard difficult. We discuss some of these subtleties and indicate how they may be addressed in a formal C semantics.

Furthermore, we argue that the C standard does not allow Turing complete implementations, and that its evaluation semantics does not preserve typing. Finally, we claim that no strictly conforming programs exist. That is, there is no C program for which the standard can guarantee that it will not crash.

Ouch. :)

  1. 3

    I skipped ahead to where “int main() {}” isn’t conforming. Because the stack may be so small that it crashes. Meh. Maybe I also removed the x bit from file system permissions. Would that count too?

    Or maybe I turn the computer off in the nanosecond between main starting and returning. Should the standard also be amended to specify that C programs are not guaranteed to return correct results when the computer is shut down?

    1. 1

      Nothing to see here. Just a couple of academics over-hyping their work. Move along: http://shape-of-code.coding-guidelines.com/2015/09/14/recent-formal-methods-and-c-papers-sep-2015/

      1. 2

        That blog post is dismissive, and perhaps justly, but it really doesn’t address the paper in much detail.

        All it really takes issue with is the paper’s authors' assertion that “The ISO C standard famously does not give semantics to a significant subset of syntactically valid C programs.” - which is true. As the blogger says, C is not even remotely unique in this respect; however, it was a very conscious choice by the ANSI committee, and the standard contains a great deal of language about why they chose to under-specify it and what the bounds of that under-specification are. To the best of my knowledge, previous languages, though similarly under-specified, were not nearly so formal or deliberate about it.

        I have at least looked through the paper in enough detail to see that it indeed enumerates specific real issues which any formal semantics of C must address. The headline-grabbing claim that “no strictly conforming programs exist” is based on the existence of stack overflows, which is perhaps a fair enough thing for the language to break its own rules on, but from my understanding the claim is true, nonetheless.

        Whether the paper is actually useful as a basis for anyone else’s work, I have no idea. :) That would be a fair category of complaint, which I’m not qualified to evaluate.

        1. 2

          I think stack overflow point is wrong. As the author points out, the standard does not mention stack overflow at all. From this, the author concludes an implementation that always overflows stack is conforming, therefore no strictly conforming programs exist, therefore all implementations are conforming. More reasonable conclusion is that under the current standard, implementations are not allowed to overflow stack, therefore no bounded storage conforming implementation is possible, and all current implementations are buggy. Is anyone surprised that all current implementations are buggy?

          It would have been more interesting if the author discussed Microsoft’s solution to this problem, namely __try/__except and EXCEPTION_STACK_OVERFLOW, which is actually used by programmers to recover from stack overflow.

          1. 1

            I read more carefully. You’re right - and that’s a really obnoxious bit of fast-talk in the paper. (Or maybe I just find it obnoxious because I fell for it.) Of course the reasonable interpretation is that no extant implementation is correct, and of course that says nothing at all about the interesting theoretical properties that are supposedly the point here.