Skip to content

[2025-02 CWG Motion 4] P1494R5 Partial program correctness #7681

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 24, 2025
Merged

[2025-02 CWG Motion 4] P1494R5 Partial program correctness #7681

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 37 additions & 14 deletions source/intro.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -919,23 +919,41 @@
Certain other operations are described in this document as
undefined behavior (for example, the effect of
attempting to modify a const object).

\pnum
Certain events in the execution of a program
are termed \defnadj{observable}{checkpoints}.
\begin{note}
This document imposes no requirements on the
behavior of programs that contain undefined behavior.
A call to \tcode{std::observable}\iref{utility.undefined}
is an observable checkpoint.
\end{note}

\pnum
\indextext{program!well-formed}%
\indextext{behavior!observable}%
The \defnadj{defined}{prefix} of an execution
comprises the operations $O$
for which for every undefined operation $U$
there is an observable checkpoint $C$
such that $O$ happens before $C$ and
$C$ happens before $U$.

\begin{note}
The undefined behavior that arises from a data race\iref{intro.races}
occurs on all participating threads.
\end{note}

A conforming implementation executing a well-formed program shall
produce the same observable behavior as one of the possible executions
of the corresponding instance of the abstract machine with the
produce the observable behavior
of the defined prefix
of one of the possible executions
of the corresponding instance
of the abstract machine with the
same program and the same input.
\indextext{behavior!undefined}%
However, if any such execution contains an undefined operation, this document places no
requirement on the implementation executing that program with that input
(not even with regard to operations preceding the first undefined
operation).
If the selected execution contains an undefined operation,
the implementation executing that program with that input
may produce arbitrary additional observable behavior afterwards.
If the execution contains an operation specified as having erroneous behavior,
the implementation is permitted to issue a diagnostic and
is permitted to terminate the execution
Expand All @@ -953,23 +971,28 @@

\pnum
\indextext{conformance requirements}%
The least requirements on a conforming implementation are:
The following specify the
\defnadj{observable}{behavior}
of the program:
\begin{itemize}
\item
Accesses through volatile glvalues are evaluated strictly according to the
rules of the abstract machine.
\item
At program termination, all data written into files shall be
identical to one of the possible results that execution of the program
according to the abstract semantics would have produced.
Data is delivered to the host environment to be written into files (\xrefc{7.21.3}).

\begin{note}
Delivering such data
is followed by an observable checkpoint\iref{cstdio.syn}.
Not all host environments provide access to file contents before program termination.
\end{note}

\item
The input and output dynamics of interactive devices shall take
place in such a fashion that prompting output is actually delivered before a program waits for input. What constitutes an interactive device is
\impldef{interactive device}.
\end{itemize}

These collectively are referred to as the
\defnx{observable behavior}{behavior!observable} of the program.
\begin{note}
More stringent correspondences between abstract and actual
semantics can be defined by each implementation.
Expand Down
16 changes: 16 additions & 0 deletions source/iostreams.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -480,6 +480,12 @@
declares objects that associate objects with the
standard C streams provided for by the functions declared in
\libheader{cstdio}, and includes all the headers necessary to use these objects.
The dynamic types of the stream buffers
initially associated with these objects are unspecified,
but they have the behavior specified for
\tcode{std::basic_filebuf<char>}
or
\tcode{std::basic_filebuf<wchar_t>}.

\pnum
The objects are constructed and the associations are established at some
Expand Down Expand Up @@ -6872,6 +6878,7 @@
if \tcode{out} contains invalid code units,
\indextext{undefined}%
the behavior is undefined.
Then establishes an observable checkpoint\iref{intro.abstract}.
\item
Otherwise
inserts the character sequence
Expand Down Expand Up @@ -7852,6 +7859,7 @@
if \tcode{out} contains invalid code units,
\indextext{undefined}%
the behavior is undefined.
Then establishes an observable checkpoint\iref{intro.abstract}.
\item
Otherwise writes \tcode{out} to \tcode{stream} unchanged.
\end{itemize}
Expand Down Expand Up @@ -11571,6 +11579,7 @@
At this point if \tcode{b != p} and \tcode{b == end} (\tcode{xbuf} isn't large
enough) then increase \tcode{XSIZE} and repeat from the beginning.
\end{itemize}
Then establishes an observable checkpoint\iref{intro.abstract}.

\pnum
\returns
Expand Down Expand Up @@ -18941,6 +18950,13 @@
The contents and meaning of the header \libheader{cstdio}
are the same as the C standard library header \libheader{stdio.h}.

\pnum
The return from each function call
that delivers data
to the host environment
to be written to a file (\xrefc{7.21.3})
is an observable checkpoint\iref{intro.abstract}.

\pnum
Calls to the function \tcode{tmpnam} with an argument that is a null pointer value may
introduce a data race\iref{res.on.data.races} with other calls to \tcode{tmpnam} with
Expand Down
16 changes: 14 additions & 2 deletions source/utilities.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,9 @@
template<class T>
constexpr underlying_type_t<T> to_underlying(T value) noexcept;

// \ref{utility.unreachable}, unreachable
// \ref{utility.undefined}, undefined behavior
[[noreturn]] void unreachable();
void observable() noexcept;

// \ref{intseq}, compile-time integer sequences%
\indexlibraryglobal{index_sequence}%
Expand Down Expand Up @@ -670,7 +671,7 @@
\tcode{static_cast<underlying_type_t<T>>(value)}.
\end{itemdescr}

\rSec2[utility.unreachable]{Function \tcode{unreachable}}
\rSec2[utility.undefined]{Undefined behavior}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This needs a \movedxref entry in xrefdelta.tex

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

xrefprev seems to be missing utility.unreachable. I'll add it, but it also seems to be missing about 500 other stable names from N4950 that are not in xrefprev. would you like me to add those? (It's unclear to me what the intent of the contents of xrefprev is --- whether it should be removed names, or just all names that were previously in use -- either way that is not what it is).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

xrefprev is supposed to be the list of xrefs in C++17, so that we get warnings from our tooling when a label vanishes without mention in xrefdelta.tex. Maybe that went wrong when I added that; Alisdair has a patch in a nearby pull request, too.

So, until we fix xrefprev for real, we need to manually add the old label.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok. shouldn't it be the list of stable names from any previously published standard? Or from C++17 to C++23 inclusive? I could grab that pretty easily if it helps (I already extracted it from C++23), but for this PR I have added utility.uncreachable manually to xrefprev.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem is we've added the label since C++17, and now we're renaming it. So, it's technically not correct that it was a label in C++17, which xrefprev attempts to represent.

The once-off fix feels reasonable for now.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I merged Alisdair's changes, but I don't think it touches on this. But we can follow this up later I suppose?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My understanding of @StephanTLavavej's request is that we don't just want the diff of the stable labels relative to one arbitrary point in the past, but rather, we want a full history of things that have happened, so that if you've been working with any one version of the document and are switching to a newer one, you can look up what happened to the label you had been working with.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I definitely think that'd be way more useful than just "here's things that were in C++17 that might have moved". It might be even more useful to have the index list when the name was moved (i.e, "utility.unreachable (moved in C++26, see utility.undefined)"


\indexlibraryglobal{unreachable}%
\begin{itemdecl}
Expand Down Expand Up @@ -704,6 +705,17 @@
\end{example}
\end{itemdescr}

\indexlibraryglobal{observable}%
\begin{itemdecl}
void observable() noexcept;
\end{itemdecl}

\begin{itemdescr}
\pnum
\effects
Establishes an observable checkpoint\iref{intro.abstract}.
\end{itemdescr}

\rSec1[pairs]{Pairs}

\rSec2[pairs.general]{General}
Expand Down
3 changes: 3 additions & 0 deletions source/xrefdelta.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -487,6 +487,9 @@
\movedxref{stmt.stmt}{stmt}
\movedxref{dcl.dcl}{dcl}

% P1494R5 added more to this section and expanded its scope
\movedxref{utility.unreachable}{utility.undefined}

%%% Deprecated features.
%%% Example:
%
Expand Down
1 change: 1 addition & 0 deletions source/xrefprev
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2700,6 +2700,7 @@ utility.requirements
utility.swap
utility.syn
utility.to.chars
utility.unreachable
valarray.access
valarray.assign
valarray.binary
Expand Down