Files
2025-10-25 03:02:53 +03:00

182 lines
7.5 KiB
Markdown
Raw Permalink Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

[intro.abstract]
# 4 General principles [[intro]](./#intro)
## 4.1 Implementation compliance [[intro.compliance]](intro.compliance#intro.abstract)
### 4.1.2 Abstract machine [intro.abstract]
[1](#1)
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/intro.tex#L904)
The semantic descriptions in this document define a
parameterized nondeterministic abstract machine[.](#1.sentence-1)
This document
places no requirement on the structure of conforming
implementations[.](#1.sentence-2)
In particular, they need not copy or emulate the
structure of the abstract machine[.](#1.sentence-3)
Rather, conforming implementations are required to emulate (only) the observable
behavior of the abstract machine as explained below[.](#1.sentence-4)[5](#footnote-5 "This provision is sometimes called the “as-if” rule, because an implementation is free to disregard any requirement of this document as long as the result is as if the requirement had been obeyed, as far as can be determined from the observable behavior of the program. For instance, an actual implementation need not evaluate part of an expression if it can deduce that its value is not used and that no side effects affecting the observable behavior of the program are produced.")
[2](#2)
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/intro.tex#L929)
Certain aspects and operations of the abstract machine are described in this
document as implementation-defined behavior (for example,sizeof(int))[.](#2.sentence-1)
These constitute the parameters of the abstract machine[.](#2.sentence-2)
Each implementation shall include documentation describing its characteristics
and behavior in these respects[.](#2.sentence-3)[6](#footnote-6 "This documentation also includes conditionally-supported constructs and locale-specific behavior. See [intro.compliance.general].")
Such documentation shall define the instance of the
abstract machine that corresponds to that implementation (referred to as the
“corresponding instance” below)[.](#2.sentence-4)
[3](#3)
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/intro.tex#L945)
Certain other aspects and operations of the abstract machine are
described in this document as unspecified behavior (for example,
order of evaluation of arguments in a function call ([[expr.call]](expr.call "7.6.1.3Function call")))[.](#3.sentence-1)
Where possible, this
document defines a set of allowable behaviors[.](#3.sentence-2)
These
define the nondeterministic aspects of the abstract machine[.](#3.sentence-3)
An instance
of the abstract machine can thus have more than one possible execution
for a given program and a given input[.](#3.sentence-4)
[4](#4)
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/intro.tex#L956)
Certain other operations are described in this document as
undefined behavior (for example, the effect of
attempting to modify a const object)[.](#4.sentence-1)
[5](#5)
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/intro.tex#L962)
Certain events in the execution of a program
are termed [*observable checkpoints*](#def:checkpoints,observable "4.1.2Abstract machine[intro.abstract]")[.](#5.sentence-1)
[*Note [1](#note-1)*:
A call to std::observable_checkpoint ([[utility.undefined]](utility.undefined "22.2.9Undefined behavior"))
is an observable checkpoint,
as are certain parts of
the evaluation of contract assertions ([[basic.contract]](basic.contract "6.11Contract assertions"))[.](#5.sentence-2)
— *end note*]
[6](#6)
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/intro.tex#L972)
The [*defined prefix*](#def:prefix,defined "4.1.2Abstract machine[intro.abstract]") 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 andC happens before U[.](#6.sentence-1)
[*Note [2](#note-2)*:
The undefined behavior that arises from a data race ([[intro.races]](intro.races "6.10.2.2Data races"))
occurs on all participating threads[.](#6.sentence-2)
— *end note*]
A conforming implementation executing a well-formed program shall
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[.](#6.sentence-3)
If the selected execution contains an undefined operation,
the implementation executing that program with that input
may produce arbitrary additional observable behavior afterwards[.](#6.sentence-4)
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
at an unspecified time after that operation[.](#6.sentence-5)
[7](#7)
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/intro.tex#L1003)
*Recommended practice*: An implementation should issue a diagnostic when such an operation is executed[.](#7.sentence-1)
[*Note [3](#note-3)*:
An implementation can issue a diagnostic
if it can determine that erroneous behavior is reachable
under an implementation-specific set of assumptions about the program behavior,
which can result in false positives[.](#7.sentence-2)
— *end note*]
[8](#8)
[#](http://github.com/Eelis/draft/tree/9adde4bc1c62ec234483e63ea3b70a59724c745a/source/intro.tex#L1013)
The following specify the[*observable behavior*](#def:behavior,observable "4.1.2Abstract machine[intro.abstract]") of the program:
- [(8.1)](#8.1)
Accesses through volatile glvalues are evaluated strictly according to the
rules of the abstract machine[.](#8.1.sentence-1)
- [(8.2)](#8.2)
Data is delivered to the host environment to be written into files (See also: ISO/IEC 9899:2024, 7.21.3)[.](#8.2.sentence-1)
[*Note [4](#note-4)*:
Delivering such data
is followed by an observable checkpoint ([[cstdio.syn]](cstdio.syn "31.13.1Header <cstdio> synopsis"))[.](#8.2.sentence-2)
Not all host environments provide access to file contents before program termination[.](#8.2.sentence-3)
— *end note*]
- [(8.3)](#8.3)
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[.](#8.3.sentence-1)
What constitutes an interactive device isimplementation-defined[.](#8.3.sentence-2)
[*Note [5](#note-5)*:
More stringent correspondences between abstract and actual
semantics can be defined by each implementation[.](#8.sentence-2)
— *end note*]
[5)](#footnote-5)[5)](#footnoteref-5)
This provision is
sometimes called the “as-if” rule, because an implementation is free to
disregard any requirement of this document as long as the result
is as if the requirement had been obeyed, as far as can be determined
from the observable behavior of the program[.](#footnote-5.sentence-1)
For instance, an actual
implementation need not evaluate part of an expression if it can deduce that its
value is not used and that noside effects affecting the
observable behavior of the program are produced[.](#footnote-5.sentence-2)
[6)](#footnote-6)[6)](#footnoteref-6)
This documentation also includes
conditionally-supported constructs and locale-specific behavior[.](#footnote-6.sentence-1)
See [[intro.compliance.general]](intro.compliance.general "4.1.1General")[.](#footnote-6.sentence-2)