Date: Sat, 20 Sep 2025 22:43:14 +0100
On 20 September 2025 20:20:35 BST, Nate Eldredge <nate_at_[hidden]> wrote:
>
>
>> On Sep 19, 2025, at 10:08, Lénárd Szolnoki via Std-Discussion <std-discussion_at_[hidden]> wrote:
>>
>>
>> I agree with this sentiment, and I think there might be room to allow the useful optimizations without the full-on UB.
>>
>> It feels that the useful optimizations can be exhausted by allowing the abstract machine to do infinite unobservable operations in finite time, which would equate with eliding the loop, but keeping the semantics of the program intact before and after the loop.
>
>That seems problematic.
>
>Given code like
>
>while (cond) {
> // no break or goto statements in the loop body
>}
>another_statement;
>
>it's a pretty fundamental principle of program flow that if `another_statement` is executed, it means that the loop terminated when `cond` evaluated to false, and the compiler can assume that fact in optimizing `another_statement` and subsequent code.
You are right. This looks like a useful optization to make, which wouldn't be available with my model. I missed this, and this mght be undesirable.
>
>Right now, that principle holds for all valid C++ programs whose behavior is defined. If the loop did not in fact terminate, then the compiler believes something that is false, and it's very hard to limit the negative consequences of that ("ex falso quodlibet"); but that's okay because the program's behavior is undefined anyway. But if you want the behavior to be defined, you're asking to derive some sort of consistent logical conclusion from contradictory hypotheses.
>
>I don't think eliding a loop can actually be described in terms of "infinite operations in finite time". If the loop does not terminate, it means that `cond` *never* evaluates to false. It doesn't matter how many times you iterate the loop, be it finite or infinite; that won't change.
There is an alternative way to describe this. The abstract machine is not described with time, but with sequencing of operations, and all valid executions must be consistent with this sequencing.
This sequencing is a DAG with potentially infinite points and edges.
If we establish that the statement after the loop is sequenced after all operations in the loop, then we can say that it's unspecified if there is forward progress between two observable operations if there are infinite unobservable operations sequenced between.
The model does not imply that the loop cndition eventually becomes false. Bur you are correct, it also means that optimizations that remove loops without proving that it eventually terminates can't infer the value of the loop condition in this model. But I think the model can be sound.
>
>It's not as if the program can be "converging", through an infinite sequence of states in which `cond` is true, to one in which it is false. We're talking about a situation where the program receives no external input, so it's a finite state machine. If the loop continues for long enough, the machine will eventually repeat some state it has already entered, and from then on we are just repeating that *finite* sequence of states, all of which have `cond` as true. A repeating finite sequence can't converge to something outside itself.
>
>We'd have to imagine some transfinite model of computation, e.g. with an infinite precision `real` type. You could imagine that
>```
>real x = 1;
>while (x > 0)
> x /= 4;
>```
>should terminate after an infinite number of iterations. But we also need an infinite amount of memory to represent `real`. That's definitely not the computation model that C++ works in. (For a typical floating point type in place of `real`, of course, the loop genuinely terminates after a finite number of iterations.)
>
>
>> On Sep 19, 2025, at 10:08, Lénárd Szolnoki via Std-Discussion <std-discussion_at_[hidden]> wrote:
>>
>>
>> I agree with this sentiment, and I think there might be room to allow the useful optimizations without the full-on UB.
>>
>> It feels that the useful optimizations can be exhausted by allowing the abstract machine to do infinite unobservable operations in finite time, which would equate with eliding the loop, but keeping the semantics of the program intact before and after the loop.
>
>That seems problematic.
>
>Given code like
>
>while (cond) {
> // no break or goto statements in the loop body
>}
>another_statement;
>
>it's a pretty fundamental principle of program flow that if `another_statement` is executed, it means that the loop terminated when `cond` evaluated to false, and the compiler can assume that fact in optimizing `another_statement` and subsequent code.
You are right. This looks like a useful optization to make, which wouldn't be available with my model. I missed this, and this mght be undesirable.
>
>Right now, that principle holds for all valid C++ programs whose behavior is defined. If the loop did not in fact terminate, then the compiler believes something that is false, and it's very hard to limit the negative consequences of that ("ex falso quodlibet"); but that's okay because the program's behavior is undefined anyway. But if you want the behavior to be defined, you're asking to derive some sort of consistent logical conclusion from contradictory hypotheses.
>
>I don't think eliding a loop can actually be described in terms of "infinite operations in finite time". If the loop does not terminate, it means that `cond` *never* evaluates to false. It doesn't matter how many times you iterate the loop, be it finite or infinite; that won't change.
There is an alternative way to describe this. The abstract machine is not described with time, but with sequencing of operations, and all valid executions must be consistent with this sequencing.
This sequencing is a DAG with potentially infinite points and edges.
If we establish that the statement after the loop is sequenced after all operations in the loop, then we can say that it's unspecified if there is forward progress between two observable operations if there are infinite unobservable operations sequenced between.
The model does not imply that the loop cndition eventually becomes false. Bur you are correct, it also means that optimizations that remove loops without proving that it eventually terminates can't infer the value of the loop condition in this model. But I think the model can be sound.
>
>It's not as if the program can be "converging", through an infinite sequence of states in which `cond` is true, to one in which it is false. We're talking about a situation where the program receives no external input, so it's a finite state machine. If the loop continues for long enough, the machine will eventually repeat some state it has already entered, and from then on we are just repeating that *finite* sequence of states, all of which have `cond` as true. A repeating finite sequence can't converge to something outside itself.
>
>We'd have to imagine some transfinite model of computation, e.g. with an infinite precision `real` type. You could imagine that
>```
>real x = 1;
>while (x > 0)
> x /= 4;
>```
>should terminate after an infinite number of iterations. But we also need an infinite amount of memory to represent `real`. That's definitely not the computation model that C++ works in. (For a typical floating point type in place of `real`, of course, the loop genuinely terminates after a finite number of iterations.)
Received on 2025-09-20 21:43:23