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

[Sassa Nf via Phabricator via llvm-commits]

sassa.nf added a comment.

> 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 simplest form of a happens-before rule is: everything must be done in exactly the evaluation order specified by the language expression. However, this means no optimization whatsoever is possible.

So you'll end up with rules that talk about the data dependencies - the expression must be evaluated in such an order that conforms to the language semantics. However, this usually specifies only the order of expressions that relate to the same variables. It is very difficult (if at all possible) to rigidly specify the order of things that are not referring to the same variables.

The order of execution of:

  while n != 0 {n += 2;}
  return n

is easy to define - can't return such an `n` that does not correspond to the execution of a loop. Execution time is not specified. For all we know, the compiler is allowed to precompute the result of the function at specific invocation sites and plug the constant there.

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?


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

https://reviews.llvm.org/D65718