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

[Juneyoung Lee via Phabricator via llvm-commits]

aqjune added a comment.

In D65718#2205183 <https://reviews.llvm.org/D65718#2205183>, @sassa.nf wrote:

>> the compiled program must only exhibit behaviors that were possible behaviors of the source program
>
> That's good. Now define what the possible behaviours of the source program are. We can skip this question all the way to what causes the infinite loop to be executed before the statement following it, and not after. There needs to be some form of happens-before rule.
>
> ...
> The order of execution of:
>
>   while n != 0 {n += 2;}
>   return 0
>
> is harder to define, because `return 0` does not depend on the computation of `n`. What happens-before rule would you add that should require this specific loop to be executed before this specific return of a constant, and yet not forbid other execution reorderings that the optimizer should be allowed to do?

I think the happens-before rule used in general is simply the syntactic order of instructions; regardless of whether there is a data dependency or not, no out-of-order execution is assumed. So, whenever the last statement is `return 0` or `return n`, it has to be executed after the while statement.
This is used by e.g. CompCert, which is a formally verified C compiler. It defines the behavior of a program (using Coq) that way, and proves (using Coq) that the behavior of target refines that of source after a translation is done.

Since it isn't good to discourage 'what-if' questions simply because a well-known software isn't doing that... What would be a main benefit for allowing out-of-order execution between instructions having no data dependency in a sequential program? I believe a rule of thumb of a theory is that it has to be simple - more complex it is, harder it is to use for human's reasoning.
For example, how can we prove this optimization?

  while (x != 1) { x := f(x); }
  use(x);
    =>
  while (x != 1) { x := f(x); }
  use(1);


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

https://reviews.llvm.org/D65718