Formal specs and optimizations in general

Yes, I know that UB is the candidate for compiler extensions, and if you know you have a particular compiler extension, you may exploit that, but absent that, my statement applies. And categorizing undefined behaviour in this way is liable to make reasoning about it general more common, even when you don't know for a fact you are doing something the compiler lets you do.

The as-if rule agrees with you, unless and until UB is involved. At which point, the as-if rule frees the implementation from any and all requirements. This is the basis for a number of optimizations, the ability to assume a program does not contain undefined behaviour, because the negation of that case permits any results.

I fall to see how "programs may be nonportable" and "implementations may define language extensions" seems to imply "the existence of UB as an optimization tool is bad," as you seem to be arguing.

Rather than try to design a language specification that fully describes all of the constructs that programmers may need to accomplish everything they need to do, the authors of the Standard wanted to encourage variety among implementations, by allowing implementations to process many actions in whatever way would best serve their individual customers' needs. When the Standard says some construct invokes UB, that means nothing more nor less than that the Standard waives jurisdiction. Because the Standard makes no effort to mandate everything necessary to make an implementation suitable for any particular purpose, failure to mandate something does not imply any judgment as to whether or not implementations claiming to be suitable for various purposes should, as a consequence of that claimed suitability, be expected to process it meaningfully.

The as-if rule agrees with you, unless and until UB is involved. At which point, the as-if rule frees the implementation from any and all requirements. This is the basis for a number of optimizations, the ability to assume a program does not contain undefined behaviour, because the negation of that case permits any results.

An optimization predicated on the assumption that a program won't do X may be useful when a compiler is used for tasks that don't involve doing X, but worse than useless for tasks that do. If some tasks require doing X and some don't then those that don't involve doing X may be usefully processed by an optimizer that assumes the program won't do X, but those which would involve doing X should not be "optimized" in that fashion. The only way a set of optimization rules could be appropriate for all tasks would be if it provided an easy way for programmers to indicate when a compiler must allow for the possibility of their code doing any of the things it might need to do, and when no such allowance is necessary. When the Standard was written, however, it was expected that programmers would select and configure implementations in whatever ways would be suitable for whatever tasks they needed to perform, rather than trying to indicate particular requirements within the source code itself. If the Standard were to specify constructs that programmers could use to indicate their requirements, then reliance upon such extensions without the use of such constructs could be deprecated. Responsibly deprecating something, however, requires that one first acknowledge it and provide a replacement--something the Standard has yet to do.

Yes, I know that UB is the candidate for compiler extensions, and if you know you have a particular compiler extension, you may exploit that, but absent that, my statement applies

One problem is that many compiler vendors never viewed the fact that their compiler would process something the same way as every other C compiler that had existed before it as an "extension", and thus saw no need to explicitly document it as such, even if the Standard neglected to define the behavior of the action in question but couldn't imagine any reason why a quality compiler wouldn't process the construct meaningfully anyhow. For example, given a structure like:

struct S { int x[4]; } s;

Although the Standard would allow an object of type struct S to be used to access the stored value of an int, the way N1570 6.5p7 is written does not allow the use of a dereferenced int* to access the stored value of a struct S.Of course, the ability to include arrays within structures would be rather useless on a compiler which would use N1570 6.5p7 as an excuse not to recognize that s.x[2]=4; which is a dereferenced int* equivalent to *(x+2) might access the stored value of a struct S, so compilers pretty much unanimously extend the language to support constructs of that form, but I don't think I've seen any that document that "extension".

Also, it may be worth noting that if Q is a conforming compiler, and L is a program that is processed by Q in conforming fashion, and that exercises the translation limits given in N1570 5.2.4.1, the following would also be a conforming implementation:

  If input I matches L
    Process program L using Q
  Otherwise
    Behave in arbitrary fashion

Judging from the Rationale, I don't think the authors of the Standard would have intended that such an implementation be considered non-conforming: "While a deficient implementation could probably contrive a program that meets this requirement, yet still succeed in being useless, the C89 Committee felt that such ingenuity would probably require more work than making something useful." I think the Committee overestimated the difficulty of contriving an a conforming-but-useless implementation, but I think it's abundantly clear that the Standard makes no real effort to mandate everything necessary to make an implementation be suitable for any particular purpose, or even any useful purpose whatsoever.

[Moderator note: This isn't the right place to litigate the wording or use of the C Standard. Please drop this sidebar, or focus it back on what it means for specific Rust formalization/specification projects.]

7 Likes

FWIW, Rust uses no form of TBAA, so discussion of TBAA is completely irrelevant to Rust.

You can argue all you want about what K&R "intended" C to be, or what the original authors of the ISO C specification "intended" C to be, but that doesn't mean much when what matters is what current spec authors intend and what current mainstream compilers implement.

For a potential Rust specification, it's clear that the most promising way forward is to define Rust as a series of operations on an Abstract Machine, where certain kinds of operations are not allowed (on pain of arbitrary UB). These illegal operations are then disallowed in safe Rust, and defined to be (fairly) easily tracked both by authors of unsafe code and tools such as Miri.

So how do you handle special system knowledge, like with linker shenanigans or special addresses, etc.? By telling the compiler/abstract machine about them, rather than trying to dance around its back, hiding from it.

You might be interested in Jai instead, as one of its key philosophies is explicit control over optimization and performance.

9 Likes

You can argue all you want about what K&R "intended" C to be, or what the original authors of the ISO C specification "intended" C to be, but that doesn't mean much when what matters is what current spec authors intend and what current mainstream compilers implement.

What do the current spec authors intend? I would think that a good standard should focus on specifying a dialect which is designed to facilitate proofs of correctness, such as the CompCert C dialect (if LLVM were to include all the instructions necessary to represent code in that dialect, and a Rust compiler were to target such instructions, then optimizations of Rust programs could be likely validated just as optimizations of CompCert C programs can). To be sure, CompCert C doesn't allow all of the optimizations that the present C Standard does, but having a small set of optimizations which can all be proven correct is better than having a larger set of potential optimizations whose interactions make it essentially impossible to prove that all corner cases are handled correctly.

Also, by "mainstream compilers", are you ignoring everything other than the dialects that clang and gcc process with all optimizations enabled? If every single remotely-conforming remotely-general-purpose C compiler made in the last 30 years for any remotely-commonplace platform can be configured to process a construct in the same predictable fashion, I would hardly regard such a construct as obscure.

For many language constructs, there are multiple sensible interpretations, some of which would facilitate more optimizations, and others of which would facilitate a wider range of tasks. If a program performs a pointer-to-integer conversion operations, for example, there are a few useful meanings such a construct could have:

  1. Produce a pointer whose accessing and aliasing sets are limited to objects that were converted to integers within the source code of the current function [assuming that even if those integers were passed to opaque functions, those functions would neither persist them nor do anything with them except pass them back verbatim].

  2. Produce a pointer whose aliasing set is limited to objects that were converted to integers within the source code of the current function, but whose access sets are not [allowing for the possibility that if the outside function might take an int-cast pointer to an array, it may return an int-cast pointer to another part of the same array].

  3. Produce a pointer whose access and aliasing sets include all objects reachable from objects whose address may have been exposed to the outside world [i.e. all objects other than those whose address can be proven not to have been exposed].

The first form of conversion would allow the widest range of optimization, and would be useful in cases where outside code never does anything with int-cast pointers other than pass them back verbatim, but would be unsuitable for cases where an outside functions would do anything else with the pointers. The second form would allow somewhat fewer optimizations, but would be suitable for a somewhat wider range of situations; it would still not be suitable, however, for situations where code may need to do weird kinds of pointer trickery a compiler should not be expected to be capable of analyzing fully. The third form would allow the fewest optimizations, but would allow programs to do many things that would be impossible given the first two, such as take a region of address space supplied by the environment and carve out objects from it.

If a language can distinguish those operations syntactically or with the aid of directives in the source text, then it would make sense for a compiler to process each operation with the meaning implied by the syntax or directives. If. however, a language represents all three operations using the same syntax, and lacks such directives, it will be impossible for language rules to reliably select among those operations in a way that is suitable for all tasks unless it frequently foregoes what would otherwise be useful optimizations. If the language doesn't allow direct specification of the required semantics, the only way for a compiler to avoid needlessly foregoing optimizations or breaking what should be working programs will be for it to offer different compilation modes for different tasks.

If an intermediate language like LLVM is designed to be generated and processed by machines, I don't think there's any reason why it shouldn't be designed to allow the required semantics to be specified fully within its source text, but if it's necessary to work with an intermediate language whose design failed to make such distinctions, the best remedy would probably be to specify command-line options, recognizing that it's possible for an optimization and a program to be incompatible without either being defective. Essentially, the command-line options would select among different dialects, one of which would support the widest range of programs (so a correct implementation of that dialect would be a correct implementation of any other), and one of which would allow compilers to assume the most constricted program behavior (so a correct program in that dialect would be a correct program in all).

For most tasks, the most useful dialects would allow more optimizations than the first, but support a wider range of useful constructs than the last, but if all implementations support the first (as gcc and clang would with -O0), they would be able to correctly process programs that are designed for any of them. If a compiler lacks particular support for a dialect, it could simply substitute any dialect whose range of usable programs is a superset of the dialect specified.

I consider the default optimizations (with -O or the equivalent), for gcc, clang, and MSVC as the minimum for mainstream compilers. All of these compilers say that turning up optimizations does not change the behavior of correct programs (with exceptions, such as -ffast-math).

Any default compiler for a reasonably mass produced embedded platform should probably also count. I have no experience with those (and most that aren't just GCC are probably under NDA).

That a program works under no optimization is not indication that it is "correct but for optimizations." At best it's (highly) unportable.

I am done here and you are not baiting me back.

There's nothing fundamental that makes "full C" impossible to verify where "CompCert C" can be verified. It's just very hard to define the right semantics for this. But the complexity of these semantics is only loosely correlated with the complexity of the reasoning principles that arise once that semantics is defined; I think you are conflating these two aspects here.

Also not that CompCert in most cases has strictly more UB than real C. The reason it optimizes less is because proving optimizations correct is hard, not because those optimizations would be incorrect in CompCert C. (The one exception here is strict aliasing / TBAA.)

It is very easy to define a version of C that permits more optimizations than C does. The hard job is permitting as many optimizations as possible while also permitting as many programs as possible.

Furthermore, there already is work on validating LLVM semantics (Alive/Alive2, to name just one research effort). There are people working on improving the precision C standard to the level required to perform formal analyses. So, there's no reason to "give up" and leave full C in the unsatisfying limbo state that it currently is in.

To summarize: everything indicates that it is very possible to move all of C to the same level of precision as CompCert C, using the "Abstract Machine" approach. It's just a lot of work. That work is happening, and it is already improving the world by pointing out compiler bugs and fixing them -- many of these bugs will certainly affect real programs, but debugging such miscompilations in complex C/C++ codebases can be near impossible, so these efforts are doing invaluable work and making real software more reliable.

This is notwithstanding the possibility of writing a simple C compiler that defines way more behavior than the standard does, possibly even all the way to making C "portable assembly". But those compilers are effectively implementing a different programming language, one with way less UB than C. That is certainly useful, but it is not the direction that "mainstream C" has been moving in -- or should we say, has been pushed in by stakeholders with huge C/C++ codebases that need them to "go fast" or else they have to provision 5% more servers, which for them means another datacenter or two. Maybe you wish for C to be a different language than what it is; that's fair, but that does not mean that there's anything fundamentally wrong with C. (Though C does have some fundamental flaws, I won't defend that here; the one you are complaining about is not one of them though IMO.) If you want portable assembler, then by all means -- go find some likeminded people and define "C--" and implement a compiler for it. There have been such approaches in the past (djb's "boringcc" comes to my mind) that haven't caught on, but I do think that such a language could be useful for certain areas. (Indeed, through standards like MISRA C, there are significant parts of the C ecosystem that are effectively written in such a dialect.)

Rust, however, is not "portable assembly" and does not want to be like that. I believe that there is a way to define the Abstract Machine that will permit writing low-level pointer manipulation software and bootloaders and also perform strong optimizations in high-level code. I think Rust, with the benefit of hindsight and learning from C/C++ (among many other languages), is on the right track to hit this sweet spot. You seem to fundamentally disagree with this design decision. I respect that, but if you hoped that Rust would become a language like that, I have to disappoint you.

11 Likes

There's nothing fundamental that makes "full C" impossible to verify where "CompCert C" can be verified. It's just very hard to define the right semantics for this.

From what I understand, there is something fundamental. CompCertC allows objects of pointer type to have their storage accessed using lvalues of other pointer types, but only pointer types. Other languages and frameworks that are designed to support static verification, such as Java and .NET, impose similar restrictions. Provided there is a way to place lvalues of various types at static hardware addresses (e.g. through special linker controls), the only situations where integer-to-pointer conversions would be needed for low-level programming would be on certain kinds of segmented-memory platforms, or in situations where e.g. a DMA controller might require that a program use two 16-bit writes to set the upper and lower halves of a DMA address.

Also not that CompCert in most cases has strictly more UB than real C. The reason it optimizes less is because proving optimizations correct is hard, not because those optimizations would be incorrect in CompCert C. (The one exception here is strict aliasing / TBAA.)

The only things I can think of that are allowed in "real" C but not CompCert C are operations which would access the backing storage of pointers without using lvalues of pointer types to do so. On the flip side, IIRC, CompCert C specifies the use of precise wrapping signed integer semantics, and doesn't allow compilers as much license to make aliasing assumptions which might be appropriate for some tasks but not all.

But those compilers are effectively implementing a different programming language , one with way less UB than C.

I.e. they are implementing the language that became popular in the 1980s, and that the C Standard was chartered to describe. Perhaps it would be good to use a retronym when referring to that language, much as the phrase "acoustic guitar" is used to describe an instrument that 100 years ago would have been simply called a "guitar". Good any good suggestions for a concise retronym that would be easily recognizable?

On the other hand, given that the Committee has expressly said "Although it strove to give programmers the opportunity to write truly portable programs, the C89 Committee did not want to force programmers into writing portably, to preclude the use of C as a “high-level assembler”: the ability to write machine specific code is one of the strengths of C." Unless the Committee was lying, those who would try to use the Standard to claim that people writing in the popular "high-level assembler" aren't really writing in C are grossly misrepresenting the Committee's publicly stated intention.

In the days before the Standard, C was not so much as a single language, but as a meta-language--a mapping which, given a target platforms (and to some extent, application field), would produce a language that could be used to program that platform. When targeting commonplace platforms, many constructs would behave identically on all implementations, even thought they might behave differently on more obscure platforms. So far as I can tell, the intention of the Committee was that people needing compilers for different platforms and purposes would use compilers that would best serve their platforms and purposes, not that programmers would be compelled to cater to the lowest-common denominator.

Moderator note: This discussion is going in circles, and still isn't the right place to litigate the original purpose behind the C standard. I'm locking it.

10 Likes