execution: remove redundant condition, reword doc for promises_may_allow

execution: remove redundant condition, reword doc for promises_may_allow

promises_may_allow() doesn't actually need to check for
promises.empty(), as the loop bounds take care of that. In the same
spirit, we can reword the comments/documentation so that

 (1) it is not redundant (condition (a) is subsumed by (b))
 (2) we are more explicit about what we actually mean by "crossing
     promises"