Date: Tue, 27 Aug 2013 19:28:45 +0200
On 27/08/13 17:48, Jeffrey Yasskin wrote:
>> - As a semanticist, I think it would be challenging to formalize, for
>> the general reasons given above.
>
> How do you model std::less<T*>, which already requires this total but
> unspecified order?
No one tried, as far as I know. We (as a community) are still a long
way from formalizing the complete semantics of a "big" language like
C++, but an even longer way from formalizing specs for its standard
library...
There are plausible ways to formalize this total order at the source
language level. But, as Gabriel wrote, the difficulty is to ensure
that your source-level semantics is not making predictions that the
compiler could invalidate later.
In other words: at the end of the day, your pointers are just bit
patterns that the hardware compares as if they were integers. If you
could chase this hardware ordering of pointers back every compilation
pass, it should be the case that the source-level ordering you obtain
is one of those allowed by your source-level semantics. Proving this
kind of properties sounds very challenging to me.
- Xavier Leroy
>> - As a semanticist, I think it would be challenging to formalize, for
>> the general reasons given above.
>
> How do you model std::less<T*>, which already requires this total but
> unspecified order?
No one tried, as far as I know. We (as a community) are still a long
way from formalizing the complete semantics of a "big" language like
C++, but an even longer way from formalizing specs for its standard
library...
There are plausible ways to formalize this total order at the source
language level. But, as Gabriel wrote, the difficulty is to ensure
that your source-level semantics is not making predictions that the
compiler could invalidate later.
In other words: at the end of the day, your pointers are just bit
patterns that the hardware compares as if they were integers. If you
could chase this hardware ordering of pointers back every compilation
pass, it should be the case that the source-level ordering you obtain
is one of those allowed by your source-level semantics. Proving this
kind of properties sounds very challenging to me.
- Xavier Leroy
Received on 2013-08-27 19:29:06