Date: Thu, 25 May 2023 21:09:48 +0000
I've spent some time thinking about this, and my current conclusion is that there are some things about the proposal that just gives me bad vibes, even though I don't have specific examples I can give to back it up.
As most of C and C++ are defined (albeit not formally) in an operational semantics manner, most of the UB we come across is similarly defined essentially operationally. Dereference a null pointer? UB. Read an uninitialized value? UB. Signed integer overflow? UB--all of the UB is defined in terms of an operational step that does not complete but instead produces UB. And this kind of UB is the one that is largely being considered when talking about this proposal.
But this is not the only kind of UB. Some of the semantics are defined in a more axiomatic semantics manner. The most salient example is data races. Essentially, the memory model of C and C++ generally pretends to be sequentially consistent, which is realizable if code uses proper synchronization, and code that doesn't do that properly is UB. There's already been discussion of data races, so I won't cover it in detail. But the idea of just declaring the UB to happen at the moment that the conflicting access happens to cause the data race doesn't feel sufficient to me; I can't convince myself that there's no way that the reordering couldn't cause observable changes before the data race happens. Others have already picked up on other cases where we have axiomatic rather than operational UB.
Overall, I think the basic sentiment that a "store volatile" that is postdominated by a known-UB statement (in LLVM terms, the `unreachable` instruction) shall not be deleted by the optimizer is a reasonable suggestion. I am somewhat less convinced that the "backwards time-travel" of inferred properties in such situations is reasonable, but I am not prepared to definitively rule such a rule out. However, I don't think this sentiment is expandable to fully cover *all* kinds of UB; it's something that has to be limited to a smaller set of UB (although this probably covers most of the UB that people are worrying about!). The wording proposed in WG14::N3128 feels insufficient to me; perhaps we need to actually provide two different UB-like concepts, and go through all existing uses of the term to work out which one is appropriate in every circumstance.
As most of C and C++ are defined (albeit not formally) in an operational semantics manner, most of the UB we come across is similarly defined essentially operationally. Dereference a null pointer? UB. Read an uninitialized value? UB. Signed integer overflow? UB--all of the UB is defined in terms of an operational step that does not complete but instead produces UB. And this kind of UB is the one that is largely being considered when talking about this proposal.
But this is not the only kind of UB. Some of the semantics are defined in a more axiomatic semantics manner. The most salient example is data races. Essentially, the memory model of C and C++ generally pretends to be sequentially consistent, which is realizable if code uses proper synchronization, and code that doesn't do that properly is UB. There's already been discussion of data races, so I won't cover it in detail. But the idea of just declaring the UB to happen at the moment that the conflicting access happens to cause the data race doesn't feel sufficient to me; I can't convince myself that there's no way that the reordering couldn't cause observable changes before the data race happens. Others have already picked up on other cases where we have axiomatic rather than operational UB.
Overall, I think the basic sentiment that a "store volatile" that is postdominated by a known-UB statement (in LLVM terms, the `unreachable` instruction) shall not be deleted by the optimizer is a reasonable suggestion. I am somewhat less convinced that the "backwards time-travel" of inferred properties in such situations is reasonable, but I am not prepared to definitively rule such a rule out. However, I don't think this sentiment is expandable to fully cover *all* kinds of UB; it's something that has to be limited to a smaller set of UB (although this probably covers most of the UB that people are worrying about!). The wording proposed in WG14::N3128 feels insufficient to me; perhaps we need to actually provide two different UB-like concepts, and go through all existing uses of the term to work out which one is appropriate in every circumstance.
Received on 2023-05-25 21:09:55