Re: [OTish] Proving compiler algorithms implement same semantics as language specs? [was Re: [PATCH][RFC] Re-implement restrict support]

[Richard Guenther <richard dot guenther at gmail dot com>]

On Tue, Jun 23, 2009 at 4:53 PM, Dave
Korn<dave.korn.cygwin@googlemail.com> wrote:
> [ redirected away from the -patches list because I want to ask a more general
> theoretical question about compiler development ]
>
> Richard Guenther wrote:
>
>> During points-to pointer equivalence sets are computed by adding
>> special RESTRICT heap-variables to points-to sets of targets of
>> pointer conversions to restrict, global restrict qualified pointers
>> and restrict qualified pointer arguments.
>>
>> A RESTRICT in the points-to set of a restrict qualified pointer
>> acts as a filter for NONLOCAL and ANYTHING. ?The RESTRICT in the
>> points-to sets make pointers based on each other conflict,
>> non-restrict qualified pointers conflict with restrict qualified
>> pointers if they point to anonymous memory (NONLOCAL or ANYTHING)
>> or otherwise.
>
>> Comments? ?Holes in my treatment of restrict?
>
> ?I'd guess there has to be some way in formal logic or propositional calculus
> by which we could take descriptions such as Richard's above, and the
> description of restrict semantics in the standard, and reduce them each to a
> pile of propositions that we could feed into a theorem-proving system and get
> it to prove they were identical.
>
> ?But I'm guessing: this kind of area is a million miles outside anything I'm
> familiar with. ?However, we've got a load of very clever academic types on the
> list here, so I thought I'd throw it open for discussion. ?There have been a
> bunch of papers and a few big projects in academia on provable compiler
> correctness, but they all seem very ambitious and not like anything we could
> make an applied use of in GCC; but is there some simpler, practical and
> well-understood tool-set already existing that we could put into use for small
> jobs such as the above?

We should have proper testsuite coverage for language features.
In this case the XPASS on the vector testcase shows me a major
flaw in my implementation:

int a[N];

__attribute__ ((noinline)) int
foo (int * __restrict__ b, int k){
...

with the proposed patch b would not alias a.  Maybe desirable
for optimization but certainly not what the C language suggests.

Thus I'm back to a separate representation and oracle treatment
for restrict.  Bah.  That'll cost.

Richard.