Looks like this should be phrased as "A thread that does not eventually do one of the following ... has undefined behavior."

It's underspecified that how can a permissive rule can lead to undefined behavior, but it should be clear that in current wording there is no UB in [intro.progress]/1, whether the permission of having such assumption is actually used by the implementation.

The wording looks bad because the process of reasoning is not clear, so there is room to improve, definitely. However, whether we need [intro.progress] to imply such UB is another question. Simply specifying it UB is too hurry, and it is definitely not editorial.

I don't like the idea of the the non-editorial change (to add UB here) for various reasons:

• It turns a normatively well-defined case to undefined before it is widely adopted by implementations.
• It is error-prone. It is quite unintuitive to prevent the UB in real programs for average users. Even if the loop elimination can be also unexpected, it is still far easier to debug (e.g. to locate the wrong code) compared to the cases like invoking unrelated code.
• There are alternative manners to introduce the UB available to the optimizer, with better readability, e.g. by attributes.

So the change would just make the language less expressive (by reducing a well-defined way to get previously controllable unspecified behavior), and it will encourage non-idiomatic and fragmented coding styles to get chances of optimization in a way that difficult to use and difficult to teach. Such direction is quite suspicous, whatever the original intent of the current rules is.

Im writing a paper to address this.

Im writing a paper to address this.

Oh... P2809R0 has addressed cases for trivial infinity loops. However, if I understood currectly, the paper hasn't address the issue whether [intro.progress]/1 introduces some kind of UB. When an infinity loop is non-trivial but doesn't contain an execution step, the original concern still exists.

There seems another issue:

Once a thread has done one of the operations in [intro.progress]/1 other than termination, can we claimed that the assumption has been met, and hence the validity of the rest of execution will no longer be affected by [intro.progress]/1?

If so, transformations of possibly infinity loops can only be performed in extremely restricted cases, which seems unintended.

P2809R0 has addressed cases for trivial infinity loops.

P2809R0 has not yet been approved by the committee, and it's not obvious its approach will achieve consensus.

I recommend closing this issue in favor of cplusplus/papers#1496

Well, P2809R2 still fails to whether clarify such allowance of assumption is specifying some kind of UB.

IIUC, the wording changes are still orthogonal to the original concerns.