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

[Sassa Nf via Phabricator via llvm-commits]

sassa.nf added a comment.

I am unable to go through all the examples of infinite loops, but please consider that it is not so much about forward progress in many cases.

**Pure computation case**:

  fn loop_it(n) {
     while(n != 0) {}
     return 0
  }



1. Abstract away a loop performing a computation into a function
2. Call the function everywhere where the variable is accessed

Basically, allow to move the computation into the future, but so that it still happens-before the first use of the result of the computation.

If there are no accesses to the variable, there are no calls of the function. Throwing away the infinite loop is valid.

**Bad synchronization case**:

A static variable reflects readiness, an incorrectly constructed loop polls.

  bool ready;
  
  fn bad_sync() {
     while(!ready) {}
     return true
  }

This should be optimizable into:

  fn bad_sync() {
     if (!ready) {
        for(;;) {} // do not elide this loop for the purpose of this discussion
     }
     return true
  }

Observe that badly synchronized code should expect that the changes to ready may never be observed, so will potentially hang.

**Good synchronization case**:

  bool ready
  
  fn good_sync() {
     while(!ready) {
        read_acquire_fence();
     }
     return true;
  }

This should not be optimizeable: there is a requirement that either ready is observed to be true immediately, or the return is placed after some release fence executed by some other thread.

If you can prove there are no release fences, it should be optimizeable into the bad synchronization case.


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

https://reviews.llvm.org/D65718