P1494R5 Partial program correctness

Author: notadragon

source/intro.tex

@@ -919,23 +919,42 @@
 Certain other operations are described in this document as
 undefined behavior (for example, the effect of
 attempting to modify a const object).
+
+\pnum
+\indextext{observable checkpoint}
+Certain events in the execution of a program
+are termed \defn{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 \defn{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 aferwards. 
 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
@@ -953,23 +972,28 @@
 
 \pnum
 \indextext{conformance requirements}%
-The least requirements on a conforming implementation are:
+The following specify the
+\defnx{observable behavior}{behavior!observable}
+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.

source/iostreams.tex

@@ -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
@@ -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
@@ -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}
@@ -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
@@ -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

source/utilities.tex

@@ -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}%
@@ -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}
 
 \indexlibraryglobal{unreachable}%
 \begin{itemdecl}
@@ -704,6 +705,16 @@
 \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}