Topic: [std-proposals] Re: [[assert: disjoint(...)]]: Contr


Author: Arthur O'Dwyer <arthur.j.odwyer@gmail.com>
Date: Sun, 7 Oct 2018 20:35:05 -0700 (PDT)
Raw View
------=_Part_1263_651555396.1538969705727
Content-Type: multipart/alternative;
 boundary="----=_Part_1264_1924513075.1538969705728"

------=_Part_1264_1924513075.1538969705728
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

On Saturday, October 6, 2018 at 9:55:04 AM UTC-7, Phil Miller wrote:
>
> The full text of the proposal I'm preparing to submit is on Google Docs=
=20
> <https://docs.google.com/document/d/1ZSwJ5k-kvdHCtE6qVMMHbRvT0a32_pAe1ScT=
1K7gbB8/edit?usp=3Dsharing>.=20
> The most critical excerpt is copied below. There's a bunch more data and=
=20
> discussion there.
>
> I *particularly* want to hear from compiler optimization implementers=20
> about whether the form presented will provide suitable input to alias=20
> analysis.
> Introduction
>
> There have been many calls over the years for code to have a way to signa=
l=20
> compilers that certain objects do not alias, allowing the compiler to=20
> optimize more aggressively. These include at least
>
>
>    -=20
>   =20
>    C99's `restrict` keyword and associated `__restrict__` extensions in=
=20
>    C++ compilers
>    -=20
>   =20
>    the alias sets proposed in N4150
>    -=20
>   =20
>    `may_alias` attributes
>    -=20
>   =20
>    IBM XL's `#pragma disjoint`
>    -=20
>   =20
>    `restrict_ptr` proposals
>   =20
>
> However, specification of how C=E2=80=99s restrict extends to C++-specifi=
c=20
> constructs has seemingly been comparatively fraught with difficulties, an=
d=20
> hence has not proceeded.=20
>
> With the addition of standard contract syntax and semantics to the C++=20
> language, I believe that similar effects can be achieved with no language=
=20
> impact and greater clarity for programmers by adding a predicate to the=
=20
> standard library, tentatively named `disjoint` here. This predicate could=
=20
> be used in [[expects]] and [[assert]] contracts to convey the desired=20
> information.
> Present Proposal
>
> Add a free function defined as follows to namespace std, in an appropriat=
e=20
> header TBD:
>
> template <typename T, typename U>
>
> bool disjoint(const T* pt, size_t nt, const U* pu, size_t nu)
>
> {
>
>  intptr_t bt =3D pt, et =3D pt+nt;
>
>  intptr_t bu =3D pu, eu =3D pu+nu;
>
>  return (et <=3D bu) || (eu <=3D bt);
>
> }
>
> Requirements:
>
>    -=20
>   =20
>    The pointers pt and pu are valid.
>    -=20
>   =20
>    The expressions pt+nt and pu+nu are valid. (i.e. they point to=20
>    elements within the same array as pt and pu, respectively, or to one p=
ast=20
>    the end, including the case where pt is a pointer is to a non-array ob=
ject=20
>    and nt is 1 (or pu and nu, respectively))
>   =20
>
I don't know if this nit is really relevant to the rest of the proposal,=20
but that definition of `disjoint` has problems with boundary conditions,=20
e.g. if (et < bt) or (eu < bu).  (I mean, if the addition bt+nt would have=
=20
overflowed.)  It would be interesting and useful to come up with a=20
bulletproof definition of `disjoint` that actually worked in practice, just=
=20
to get the implementation out there in the wild, even if it never gets=20
standardized.

=E2=80=93Arthur

--=20
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 e=
mail 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/48fe1f8b-c381-4c78-818b-2b606b0e89ad%40isocpp.or=
g.

------=_Part_1264_1924513075.1538969705728
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">On Saturday, October 6, 2018 at 9:55:04 AM UTC-7, Phil Mil=
ler wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-left:=
 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr"><di=
v>The full text of the proposal I&#39;m preparing to submit is <a href=3D"h=
ttps://docs.google.com/document/d/1ZSwJ5k-kvdHCtE6qVMMHbRvT0a32_pAe1ScT1K7g=
bB8/edit?usp=3Dsharing" target=3D"_blank" rel=3D"nofollow" onmousedown=3D"t=
his.href=3D&#39;https://docs.google.com/document/d/1ZSwJ5k-kvdHCtE6qVMMHbRv=
T0a32_pAe1ScT1K7gbB8/edit?usp\x3dsharing&#39;;return true;" onclick=3D"this=
..href=3D&#39;https://docs.google.com/document/d/1ZSwJ5k-kvdHCtE6qVMMHbRvT0a=
32_pAe1ScT1K7gbB8/edit?usp\x3dsharing&#39;;return true;">on Google Docs</a>=
.. The most critical excerpt is copied below. There&#39;s a bunch more data =
and discussion there.</div><div><br></div><div>I <i>particularly</i>
 want to hear from compiler optimization implementers about whether the=20
form presented will provide suitable input to alias analysis.<br></div><h3 =
dir=3D"ltr" style=3D"line-height:1.38;margin-top:16pt;margin-bottom:4pt"><s=
pan style=3D"font-size:14pt;font-family:Arial;color:rgb(67,67,67);backgroun=
d-color:transparent;font-weight:400;font-style:normal;font-variant:normal;t=
ext-decoration:none;vertical-align:baseline;white-space:pre-wrap"></span></=
h3><h3 dir=3D"ltr" style=3D"line-height:1.38;margin-top:16pt;margin-bottom:=
4pt"><span style=3D"font-size:14pt;font-family:Arial;color:rgb(67,67,67);ba=
ckground-color:transparent;font-weight:400;font-style:normal;font-variant:n=
ormal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">In=
troduction</span></h3><p dir=3D"ltr" style=3D"line-height:1.38;margin-top:0=
pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-family:Arial;color=
:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;=
font-variant:normal;text-decoration:none;vertical-align:baseline;white-spac=
e:pre-wrap">There have been many calls over the years for code to have a wa=
y to signal compilers that certain objects do not alias, allowing the compi=
ler to optimize more aggressively. These include at least</span></p><br><ul=
 style=3D"margin-top:0pt;margin-bottom:0pt"><li dir=3D"ltr" style=3D"list-s=
tyle-type:disc;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background=
-color:transparent;font-weight:400;font-style:normal;font-variant:normal;te=
xt-decoration:none;vertical-align:baseline;white-space:pre-wrap"><p dir=3D"=
ltr" style=3D"line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span styl=
e=3D"font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:tra=
nsparent;font-weight:400;font-style:normal;font-variant:normal;text-decorat=
ion:none;vertical-align:baseline;white-space:pre-wrap">C99&#39;s `</span><s=
pan style=3D"font-size:11pt;font-family:&quot;Courier New&quot;;color:rgb(0=
,0,0);background-color:transparent;font-weight:400;font-style:normal;font-v=
ariant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-=
wrap">restrict</span><span style=3D"font-size:11pt;font-family:Arial;color:=
rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;f=
ont-variant:normal;text-decoration:none;vertical-align:baseline;white-space=
:pre-wrap">` keyword and associated `</span><span style=3D"font-size:11pt;f=
ont-family:&quot;Courier New&quot;;color:rgb(0,0,0);background-color:transp=
arent;font-weight:400;font-style:normal;font-variant:normal;text-decoration=
:none;vertical-align:baseline;white-space:pre-wrap">__restrict__</span><spa=
n style=3D"font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-col=
or:transparent;font-weight:400;font-style:normal;font-variant:normal;text-d=
ecoration:none;vertical-align:baseline;white-space:pre-wrap">` extensions i=
n C++ compilers</span></p></li><li dir=3D"ltr" style=3D"list-style-type:dis=
c;font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transp=
arent;font-weight:400;font-style:normal;font-variant:normal;text-decoration=
:none;vertical-align:baseline;white-space:pre-wrap"><p dir=3D"ltr" style=3D=
"line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style=3D"font-siz=
e:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font=
-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vert=
ical-align:baseline;white-space:pre-wrap">the alias sets proposed in N4150<=
/span></p></li><li dir=3D"ltr" style=3D"list-style-type:disc;font-size:11pt=
;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weigh=
t:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-a=
lign:baseline;white-space:pre-wrap"><p dir=3D"ltr" style=3D"line-height:1.3=
8;margin-top:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-fami=
ly:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font=
-style:normal;font-variant:normal;text-decoration:none;vertical-align:basel=
ine;white-space:pre-wrap">`</span><span style=3D"font-size:11pt;font-family=
:&quot;Courier New&quot;;color:rgb(0,0,0);background-color:transparent;font=
-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vert=
ical-align:baseline;white-space:pre-wrap">may_alias</span><span style=3D"fo=
nt-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparen=
t;font-weight:400;font-style:normal;font-variant:normal;text-decoration:non=
e;vertical-align:baseline;white-space:pre-wrap">` attributes</span></p></li=
><li dir=3D"ltr" style=3D"list-style-type:disc;font-size:11pt;font-family:A=
rial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-sty=
le:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;=
white-space:pre-wrap"><p dir=3D"ltr" style=3D"line-height:1.38;margin-top:0=
pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-family:Arial;color=
:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;=
font-variant:normal;text-decoration:none;vertical-align:baseline;white-spac=
e:pre-wrap">IBM XL&#39;s `</span><span style=3D"font-size:11pt;font-family:=
&quot;Courier New&quot;;color:rgb(0,0,0);background-color:transparent;font-=
weight:400;font-style:normal;font-variant:normal;text-decoration:none;verti=
cal-align:baseline;white-space:pre-wrap">#pragma disjoint</span><span style=
=3D"font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:tran=
sparent;font-weight:400;font-style:normal;font-variant:normal;text-decorati=
on:none;vertical-align:baseline;white-space:pre-wrap">`</span></p></li><li =
dir=3D"ltr" style=3D"list-style-type:disc;font-size:11pt;font-family:Arial;=
color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:no=
rmal;font-variant:normal;text-decoration:none;vertical-align:baseline;white=
-space:pre-wrap"><p dir=3D"ltr" style=3D"line-height:1.38;margin-top:0pt;ma=
rgin-bottom:0pt"><span style=3D"font-size:11pt;font-family:Arial;color:rgb(=
0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-=
variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre=
-wrap">`</span><span style=3D"font-size:11pt;font-family:&quot;Courier New&=
quot;;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-st=
yle:normal;font-variant:normal;text-decoration:none;vertical-align:baseline=
;white-space:pre-wrap">restrict_ptr</span><span style=3D"font-size:11pt;fon=
t-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:40=
0;font-style:normal;font-variant:normal;text-decoration:none;vertical-align=
:baseline;white-space:pre-wrap">` proposals</span></p></li></ul><br><p dir=
=3D"ltr" style=3D"line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span =
style=3D"font-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color=
:transparent;font-weight:400;font-style:normal;font-variant:normal;text-dec=
oration:none;vertical-align:baseline;white-space:pre-wrap">However, specifi=
cation of how C=E2=80=99s </span><span style=3D"font-size:11pt;font-family:=
&quot;Courier New&quot;;color:rgb(0,0,0);background-color:transparent;font-=
weight:400;font-style:normal;font-variant:normal;text-decoration:none;verti=
cal-align:baseline;white-space:pre-wrap">restrict</span><span style=3D"font=
-size:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;=
font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;=
vertical-align:baseline;white-space:pre-wrap"> extends to C++-specific cons=
tructs has seemingly been comparatively fraught with difficulties, and henc=
e has not proceeded. </span></p><br><p dir=3D"ltr" style=3D"line-height:1.3=
8;margin-top:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-fami=
ly:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font=
-style:normal;font-variant:normal;text-decoration:none;vertical-align:basel=
ine;white-space:pre-wrap">With the addition of standard contract syntax and=
 semantics to the C++ language, I believe that similar effects can be achie=
ved with no language impact and greater clarity for programmers by adding a=
 predicate to the standard library, tentatively named `</span><span style=
=3D"font-size:11pt;font-family:&quot;Courier New&quot;;color:rgb(0,0,0);bac=
kground-color:transparent;font-weight:400;font-style:normal;font-variant:no=
rmal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">dis=
joint</span><span style=3D"font-size:11pt;font-family:Arial;color:rgb(0,0,0=
);background-color:transparent;font-weight:400;font-style:normal;font-varia=
nt:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap=
">` here. This predicate could be used in </span><span style=3D"font-size:1=
1pt;font-family:&quot;Courier New&quot;;color:rgb(0,0,0);background-color:t=
ransparent;font-weight:400;font-style:normal;font-variant:normal;text-decor=
ation:none;vertical-align:baseline;white-space:pre-wrap">[[expects]]</span>=
<span style=3D"font-size:11pt;font-family:Arial;color:rgb(0,0,0);background=
-color:transparent;font-weight:400;font-style:normal;font-variant:normal;te=
xt-decoration:none;vertical-align:baseline;white-space:pre-wrap"> and </spa=
n><span style=3D"font-size:11pt;font-family:&quot;Courier New&quot;;color:r=
gb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;fo=
nt-variant:normal;text-decoration:none;vertical-align:baseline;white-space:=
pre-wrap">[[assert]] </span><span style=3D"font-size:11pt;font-family:Arial=
;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:n=
ormal;font-variant:normal;text-decoration:none;vertical-align:baseline;whit=
e-space:pre-wrap">contracts to convey the desired information.</span></p><h=
3 dir=3D"ltr" style=3D"line-height:1.38;margin-top:16pt;margin-bottom:4pt">=
<span style=3D"font-size:14pt;font-family:Arial;color:rgb(67,67,67);backgro=
und-color:transparent;font-weight:400;font-style:normal;font-variant:normal=
;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">Present=
 Proposal</span></h3><p dir=3D"ltr" style=3D"line-height:1.38;margin-top:0p=
t;margin-bottom:0pt"><span style=3D"font-size:11pt;font-family:Arial;color:=
rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;f=
ont-variant:normal;text-decoration:none;vertical-align:baseline;white-space=
:pre-wrap">Add a free function defined as follows to namespace std, in an a=
ppropriate header TBD:</span></p><br><p dir=3D"ltr" style=3D"line-height:1.=
38;margin-top:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-fam=
ily:&quot;Courier New&quot;;color:rgb(0,0,0);background-color:transparent;f=
ont-weight:400;font-style:normal;font-variant:normal;text-decoration:none;v=
ertical-align:baseline;white-space:pre-wrap">template &lt;typename T, typen=
ame U&gt;</span></p><p dir=3D"ltr" style=3D"line-height:1.38;margin-top:0pt=
;margin-bottom:0pt"><span style=3D"font-size:11pt;font-family:&quot;Courier=
 New&quot;;color:rgb(0,0,0);background-color:transparent;font-weight:400;fo=
nt-style:normal;font-variant:normal;text-decoration:none;vertical-align:bas=
eline;white-space:pre-wrap">bool disjoint(const T* pt, size_t nt, const U* =
pu, size_t nu)</span></p><p dir=3D"ltr" style=3D"line-height:1.38;margin-to=
p:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-family:&quot;Co=
urier New&quot;;color:rgb(0,0,0);background-color:transparent;font-weight:4=
00;font-style:normal;font-variant:normal;text-decoration:none;vertical-alig=
n:baseline;white-space:pre-wrap">{</span></p><p dir=3D"ltr" style=3D"line-h=
eight:1.38;margin-top:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;=
font-family:&quot;Courier New&quot;;color:rgb(0,0,0);background-color:trans=
parent;font-weight:400;font-style:normal;font-variant:normal;text-decoratio=
n:none;vertical-align:baseline;white-space:pre-wrap"> =C2=A0intptr_t bt =3D=
 pt, et =3D pt+nt;</span></p><p dir=3D"ltr" style=3D"line-height:1.38;margi=
n-top:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-family:&quo=
t;Courier New&quot;;color:rgb(0,0,0);background-color:transparent;font-weig=
ht:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-=
align:baseline;white-space:pre-wrap"> =C2=A0intptr_t bu =3D pu, eu =3D pu+n=
u;</span></p><br><p dir=3D"ltr" style=3D"line-height:1.38;margin-top:0pt;ma=
rgin-bottom:0pt"><span style=3D"font-size:11pt;font-family:&quot;Courier Ne=
w&quot;;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-=
style:normal;font-variant:normal;text-decoration:none;vertical-align:baseli=
ne;white-space:pre-wrap"> =C2=A0return (et &lt;=3D bu) || (eu &lt;=3D bt);<=
/span></p><p dir=3D"ltr" style=3D"line-height:1.38;margin-top:0pt;margin-bo=
ttom:0pt"><span style=3D"font-size:11pt;font-family:&quot;Courier New&quot;=
;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:n=
ormal;font-variant:normal;text-decoration:none;vertical-align:baseline;whit=
e-space:pre-wrap">}</span></p><br><p dir=3D"ltr" style=3D"line-height:1.38;=
margin-top:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-family=
:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-s=
tyle:normal;font-variant:normal;text-decoration:none;vertical-align:baselin=
e;white-space:pre-wrap">Requirements:</span></p><ul style=3D"margin-top:0pt=
;margin-bottom:0pt"><li dir=3D"ltr" style=3D"list-style-type:disc;font-size=
:11pt;font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-=
weight:400;font-style:normal;font-variant:normal;text-decoration:none;verti=
cal-align:baseline;white-space:pre-wrap"><p dir=3D"ltr" style=3D"line-heigh=
t:1.38;margin-top:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font=
-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400=
;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:=
baseline;white-space:pre-wrap">The pointers pt and pu are valid.</span></p>=
</li><li dir=3D"ltr" style=3D"list-style-type:disc;font-size:11pt;font-fami=
ly:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font=
-style:normal;font-variant:normal;text-decoration:none;vertical-align:basel=
ine;white-space:pre-wrap"><p dir=3D"ltr" style=3D"line-height:1.38;margin-t=
op:0pt;margin-bottom:0pt"><span style=3D"font-size:11pt;font-family:Arial;c=
olor:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:nor=
mal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-=
space:pre-wrap">The expressions pt+nt and pu+nu are valid. (i.e. they point=
 to elements within the same array as pt and pu, respectively, or to one pa=
st the end, including the case where pt is a pointer is to a non-array obje=
ct and nt is 1 (or pu and nu, respectively))</span></p></li></ul></div></bl=
ockquote><div><br></div><div>I don&#39;t know if this nit is really relevan=
t to the rest of the proposal, but that definition of `disjoint` has proble=
ms with boundary conditions, e.g. if (et &lt; bt) or (eu &lt; bu). =C2=A0(I=
 mean, if the addition bt+nt would have overflowed.) =C2=A0It would be inte=
resting and useful to come up with a bulletproof definition of `disjoint` t=
hat actually worked in practice, just to get the implementation out there i=
n the wild, even if it never gets standardized.</div><div><br></div><div>=
=E2=80=93Arthur</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/48fe1f8b-c381-4c78-818b-2b606b0e89ad%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/48fe1f8b-c381-4c78-818b-2b606b0e89ad=
%40isocpp.org</a>.<br />

------=_Part_1264_1924513075.1538969705728--

------=_Part_1263_651555396.1538969705727--

.