C++ Logo

liaison

Advanced search

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

From: Martin Uecker <ma.uecker_at_[hidden]>
Date: Sat, 13 Apr 2024 12:16:56 +0200
Am Samstag, dem 13.04.2024 um 11:22 +0200 schrieb Jens Maurer via Liaison:
>
> On 13/04/2024 10.38, Jens Gustedt via Liaison wrote:
> > 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.
>
> On the other hand, recent improvements in optimizer technologies
> (such as link-time optimization) do introduce a whole-program
> view, with very real consequences.

At least for Clang and GCC LTO does not do whole-program analysis.
It merely optimizes larger parts of a program together.

> The whole point of the
> specification is to be abstract enough so that all these
> improvements in optimizer technology are actually possible.

The are actually possible without having a specification
that makes partial correctness analysis much harder.

>
> For example, declaring arbitrary non-inline function calls
> as barriers for undefined behavior isn't a good approach once
> "inline" becomes meaningless because the compiler has a whole-
> program view due to LTO.

Making function calls optimization barriers would already
be problematic inside a single traditional translation unit
where compilers can do inlining. LTO does not make this more
or less hard.
>
> I think we'll have a lot more long-term maintenance effort
> with a more "real-world" specification rather than having a
> clear abstract model.
>
> For example, the multi-threading aspects of the memory model
> feel rather abstract to me, but have aged quite well so far.

There are some unresolved semantic issues with multi-threading,
e.g. out-of-thin-air values and also issues connected to UB.

Martin


>
> > 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.
>
> I don't think we can meaningfully specify what happens in a debugger.
> We can rely on implementations not being intentionally user-hostile,
> including for interactions with the environment, though.
>
> Jens (the other one)
> _______________________________________________
> Liaison mailing list
> Liaison_at_[hidden]
> Subscription: https://lists.isocpp.org/mailman/listinfo.cgi/liaison
> Link to this post: http://lists.isocpp.org/liaison/2024/04/1386.php

Received on 2024-04-13 10:17:00