Topic: Proposed alternative approach to specifying required


Author: "'Walt Karas' via ISO C++ Standard - Future Proposals" <std-proposals@isocpp.org>
Date: Wed, 15 Feb 2017 11:17:51 -0800 (PST)
Raw View
------=_Part_2651_567680057.1487186271333
Content-Type: multipart/alternative;
 boundary="----=_Part_2652_414698277.1487186271333"

------=_Part_2652_414698277.1487186271333
Content-Type: text/plain; charset=UTF-8

- In a program execution, each thread defines a nominal order of (thread
local) memory and fence operations.
- For any operations X and Y in thread T, either X before Y, or Y before X.
- A program execution defines a nominal global order of global memory
operations.
- If X and Y are atomic global operations, then either X before Y or Y
before X in the global order.
- If X is a global operation, and there exists a global store S where
neither X before S nor S before X in the global order, then the result of X
is undefined.
- A program execution defines a partial function f(T, LO) -> GO where LO is
a local memory operation in thread T, and GO is a global operation.  If LO
is atomic, then GO must be atomic. The result of LO is the result of GO.
If the result of GO is undefined, the result of LO is undefined.  (Even if
f(T, LO) is not required to exist, it none the less _may_ exist.)
- If LO1 and LO2 are operations in thread T, and LO1 before LO2 in T, and
f(T, LO1) and f(T, LO2) both exist, then f(T, LO2) before f(T, LO1) in the
global order is not allowed.
- If:
1.  In a thread T, X and Y are memory operations, and F is a fence
operation.
2.  X before F and F before Y.
3.  F is sequentially consistent and both X and Y are atomic, or
4.  F is acquire and both X and Y are loads, or
5.  F is release and both X and Y are stores.
then F is activated for X and Y.
- In a thread T, if X and Y are memory operations (where X before Y) with
an activated fence F, then f(T, X) must exist.
- For every global operation GO, there must exist a local operation LO in
some thread T where f(T, LO) -> GO.  (Assuming no intense gamma radiation.)
- A sequentially consistent (thread local) atomic memory operation implies
two sequentially consistent fences, one before and one after it (as well as
a preceding release for a store, and a succeeding acquire for a load).

--
You received this message because you are subscribed to the Google Groups "ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an email to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
To view this discussion on the web visit https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/d0fdabcd-f04a-46e6-b93a-0b9ea85cb5bd%40isocpp.org.

------=_Part_2652_414698277.1487186271333
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>- In a program execution,=C2=A0each thread defines a =
nominal order of (thread local) memory and fence operations.</div><div>- Fo=
r any operations X and Y in thread T, either X before Y, or Y before X.</di=
v><div>- A program execution defines a nominal global order of global memor=
y operations.</div><div>- If X and Y are atomic global operations, then eit=
her X before Y or Y before X in the global order.</div><div>- If X is a glo=
bal operation, and there exists a global store S where neither X before S n=
or S before X in the global order, then the result of X is undefined.</div>=
<div>- A program execution defines a partial function f(T, LO) -&gt; GO whe=
re LO is a local memory operation in thread T, and GO is a global operation=
..=C2=A0 If LO is atomic, then GO must be atomic. The result of LO is the re=
sult of GO.=C2=A0 If the result of GO is undefined, the result of LO is und=
efined.=C2=A0 (Even if f(T, LO) is not required to exist, it none the less =
_may_ exist.)</div><div>- If LO1 and LO2 are operations in thread T, and LO=
1 before LO2 in T, and f(T, LO1) and f(T, LO2) both exist, then f(T, LO2) b=
efore f(T, LO1) in the global order is not allowed.</div><div>- If:</div><d=
iv>1.=C2=A0 In a thread T, X and Y are memory operations, and F is a fence =
operation.</div><div>2.=C2=A0 X before=C2=A0F and=C2=A0F before Y.</div><di=
v>3.=C2=A0 F is sequentially consistent and both X and Y are atomic, or</di=
v><div>4.=C2=A0 F is acquire and both X and Y are loads, or</div><div>5.=C2=
=A0 F is release and both X and Y are stores.</div><div>then F is activated=
 for X and Y.</div><div>-=C2=A0In a thread T, if X and Y are memory operati=
ons (where X before Y) with an activated fence F, then f(T, X) must exist.<=
/div><div>- For every global operation GO, there must exist a local operati=
on LO in some thread T where f(T, LO) -&gt; GO.=C2=A0 (Assuming no intense =
gamma radiation.)</div><div>- A sequentially consistent (thread local) atom=
ic memory operation implies two sequentially consistent fences, one before =
and one after it (as well as a preceding release for a store, and a succeed=
ing acquire for a load).</div></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/d0fdabcd-f04a-46e6-b93a-0b9ea85cb5bd%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/d0fdabcd-f04a-46e6-b93a-0b9ea85cb5bd=
%40isocpp.org</a>.<br />

------=_Part_2652_414698277.1487186271333--

------=_Part_2651_567680057.1487186271333--

.