C++ Logo

liaison

Advanced search

Re: [wg14/wg21 liaison] Semantics of angelic nondeterminism

From: Jens Gustedt <jens.gustedt_at_[hidden]>
Date: Sat, 13 Apr 2024 10:38:18 +0200
Hi,

Am 13. April 2024 10:03:29 MESZ schrieb Martin Uecker via Liaison <liaison_at_[hidden]>:
 
> I do not see why you cannot avoid the conclusion. We can simply
> say "once an operation which has UB is encountered, the standard
> allows arbitrary behavior." This eliminates a lot of problems
> and is far simpler to understand and to reason about. In
> particular, it makes the specification useful even in cases
> where some component is involved that does not have a full
> formal specification and where it is not clear what "game" this
> component would play with some angels and demons in the
> language spec, i.e. in 99% of all real world applications of C.

I agree with most of what you are saying, and actually the other Jens' argument how function calls obfuscate behavior shows to me how useless all of this Platonic idealism is. It just doesn't help to explain or predict program behavior in real life.

But I think the above should be formulated a bit more carefully, something like

      "All visible side effects that happened before an erroneous operation that has UB remain visible to the execution environment. Effects that are perceived after such an operation are not restricted and may partially or completely obfuscate the effects that happened prior to the operation."

By such a statement we'd guarantee for example that inside a debugger the rules of the language apply, even if the execution hits an erroneous operation at some point.

Jens

-- 
Jens Gustedt - INRIA & ICube, Strasbourg, France 

Received on 2024-04-13 08:39:31