[PATCH] D65718: [LangRef] Document forward-progress requirement

[Sassa Nf via Phabricator via llvm-commits]

sassa.nf added a comment.

> In general, it is *not* valid for a compiler to remove an infinite loop.

I don't know what this statement is based on. It is up to the computational semantics of the expression. On the contrary, I can say that in general the compiler is free to move the computation around, as long as the observability of the computed value produces a partial order of reads/writes/synchronization actions/IO that is consistent with the program and the language semantics.

Besides, in order to know whether the loop is finite or not, one needs to perform a termination check, which cannot be done in general. So we can either speak about loops in general, or not at all.

> But that's exactly what the progress guarantee is about?

No. It is about proof-relevance. Computing `n` is not relevant to computing what the effects (side-effects + return value) of the `loop_it` function are.

Also, I've seen an argument about time. Time is not a side-effect of the infinite loop. There is no language specification that says that infinite loops (or any loops for that matter) consume time. (ok, if there is, then it would be great to quote it)

When you want time to be a side-effect, you use `micropause()` (which can be a no-op).


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D65718/new/

https://reviews.llvm.org/D65718