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

[Johannes Doerfert via Phabricator via llvm-commits]

jdoerfert added a comment.

Somewhat related:
I was hoping that the following deduction will be valid:

  If all instructions in the loop do not synchronize (see `nosync`) then the loop cannot be infinite.

The reason is that any "progress" need to be observable and for that it needs to be "synchronized".
Now, the `nosync` definition might not be up to this (I hope it is though), but that is a different issue.
Having the above reasoning will (I think) allow us to deduce `willreturn` in the presence of various "common" loops.



================
Comment at: llvm/docs/LangRef.rst:10080
       %indvar = phi i32 [ 0, %LoopHeader ], [ %nextindvar, %Loop ]
+      call void @llvm.sideeffect() ; Ensure forward progress
       %nextindvar = add i32 %indvar, 1
----------------
Add a link to the forward progress requirement section please.


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

https://reviews.llvm.org/D65718