4 ms·

See this sibling thread https://news.ycombinator.com/item?id=17189666 https://news.ycombinator.com/item?id=17189666 - typically anything touching memory needs i

by eddyb 8y ago

See this sibling thread https://news.ycombinator.com/item?id=17189666 https://news.ycombinator.com/item?id=17189666 - typically anything touching memory needs invariants to be optimized, which in languages that can directly manipulate memory means there's also UB (code that can't be statically proven not to break those invariants).

vyodaiken 8y ago
you don't need UB for invariant optimization. What UB permits the compiler to do is INCORRECTLY assume invariance. This permits the compiler to "optimize" badly written C code in a way that silently changes its function - which I don't call an optimization.
- xenadu02 8y ago
  I’m not sure you’ve though this through. Any C function that manipulates pointers (or arrays) can alias those pointers, type pun, and otherwise touch the same block of memory through different paths and/or treating the bits as different types. Vast areas of optimization are completely closed to you if you want code to be resilient in the face of aliasing. You should sit down with pen and paper to figure out how to optimize a simple function while preserving invariants but without UB. It would be very illuminating.
  - vyodaiken 8y ago
    It's really irritating that people take this condescending approach. C is harder to optimize than language that e.g. do not have pointers. That is a tradeoff the language designers chose because they wanted C programmers to be able to type pun, for example. This is why C89's only limit on type punning was memory alignment. The intent of "restrict" was to enable some aliasing optimizations via opt-in. So, sure, things that are not invariant in C are not available for invariant optimization. C permits aliasing. So it calls for smarter compiler techniques. If you want a language that forbids aliasing, use one that does and then call out to C libraries. But breaking C to allow CS220 "clever optimizing tricks" to be easily used is bad engineering. Essentially, what you are saying is, "elimination of invariants is a good optimization, so pretending C has more invariants than it does is a good thing. " So maybe come up with a real example and stop hand waving.
- eddyb 8y ago
  The UB is the result of operations which assume invariants, when they are not met. Invariants are useless if you can't assume them. Having no UB in C would require having no way to break those assumptions but C is memory/type-unsafe so that's outright impossible. Recently I've been trying to imagine what Rust's safe abstractions that use `unsafe` code internally would look like on top of some advanced mix of dependent type theory and proofs about state-manipulating imperative programs. At that point, the optimizer would have proofs of the invariants it can rely on and it could even potentially emit proofs that every single transformation it performed preserves the (safe) semantics of the code being optimized. But we're not there yet. Today, we need at least a small subset of the libraries of a systems language to prevent UB "by hand". And in C (or C++, although not necessarily for the same reasons), that's even harder, as there is no notion of a "safe abstraction" (one which you cannot misuse to produce UB).
  - vyodaiken 8y ago
    >Invariants are useless if you can't assume them. I would think that what we want is invariants that have been validated, not assumed - especially not assumed incorrectly.
    - eddyb 8y ago
      You won't be able to entirely validate yourself most memory-related invariants in a language which can allow breaking memory safety, that's why I mentioned the hypothetical language which can encode proofs for invariants. What you want is effectively automated proof-search (a hard problem) for an entirely-safe systems language (which doesn't even exist yet, AFAIK. at least not what I described).
      - vyodaiken 8y ago
        Right. C is not designed to be memory safe. So certain invariants are harder to prove (or just not true). One problem with UB is that it allows compilers to assume false things.

by eddyb 8y ago

vyodaiken 8y ago

you don't need UB for invariant optimization. What UB permits the compiler to do is INCORRECTLY assume invariance. This permits the compiler to "optimize" badly written C code in a way that silently changes its function - which I don't call an optimization.

xenadu02 8y ago
I’m not sure you’ve though this through. Any C function that manipulates pointers (or arrays) can alias those pointers, type pun, and otherwise touch the same block of memory through different paths and/or treating the bits as different types. Vast areas of optimization are completely closed to you if you want code to be resilient in the face of aliasing. You should sit down with pen and paper to figure out how to optimize a simple function while preserving invariants but without UB. It would be very illuminating.
- vyodaiken 8y ago
  It's really irritating that people take this condescending approach. C is harder to optimize than language that e.g. do not have pointers. That is a tradeoff the language designers chose because they wanted C programmers to be able to type pun, for example. This is why C89's only limit on type punning was memory alignment. The intent of "restrict" was to enable some aliasing optimizations via opt-in. So, sure, things that are not invariant in C are not available for invariant optimization. C permits aliasing. So it calls for smarter compiler techniques. If you want a language that forbids aliasing, use one that does and then call out to C libraries. But breaking C to allow CS220 "clever optimizing tricks" to be easily used is bad engineering. Essentially, what you are saying is, "elimination of invariants is a good optimization, so pretending C has more invariants than it does is a good thing. " So maybe come up with a real example and stop hand waving.
eddyb 8y ago
The UB is the result of operations which assume invariants, when they are not met. Invariants are useless if you can't assume them. Having no UB in C would require having no way to break those assumptions but C is memory/type-unsafe so that's outright impossible. Recently I've been trying to imagine what Rust's safe abstractions that use `unsafe` code internally would look like on top of some advanced mix of dependent type theory and proofs about state-manipulating imperative programs. At that point, the optimizer would have proofs of the invariants it can rely on and it could even potentially emit proofs that every single transformation it performed preserves the (safe) semantics of the code being optimized. But we're not there yet. Today, we need at least a small subset of the libraries of a systems language to prevent UB "by hand". And in C (or C++, although not necessarily for the same reasons), that's even harder, as there is no notion of a "safe abstraction" (one which you cannot misuse to produce UB).
- vyodaiken 8y ago
  >Invariants are useless if you can't assume them. I would think that what we want is invariants that have been validated, not assumed - especially not assumed incorrectly.
  - eddyb 8y ago
    You won't be able to entirely validate yourself most memory-related invariants in a language which can allow breaking memory safety, that's why I mentioned the hypothetical language which can encode proofs for invariants. What you want is effectively automated proof-search (a hard problem) for an entirely-safe systems language (which doesn't even exist yet, AFAIK. at least not what I described).
    - vyodaiken 8y ago
      Right. C is not designed to be memory safe. So certain invariants are harder to prove (or just not true). One problem with UB is that it allows compilers to assume false things.