[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Xen-devel] [PATCH v6 1/4] xen: introduce SYMBOL



>>> On 22.01.19 at 00:15, <sstabellini@xxxxxxxxxx> wrote:
> On Mon, 21 Jan 2019, Jan Beulich wrote:
>> >>> On 21.01.19 at 11:22, <julien.grall@xxxxxxx> wrote:
>> > Hi Jan,
>> > 
>> > On 21/01/2019 09:34, Jan Beulich wrote:
>> >>>>> On 18.01.19 at 11:48, <julien.grall@xxxxxxx> wrote:
>> >>> On 18/01/2019 09:54, Jan Beulich wrote:
>> >>>>>>> On 18.01.19 at 02:24, <sstabellini@xxxxxxxxxx> wrote:
>> >>>>> On Thu, 17 Jan 2019, Jan Beulich wrote:
>> >>>>>>>>> On 17.01.19 at 01:37, <sstabellini@xxxxxxxxxx> wrote:
>> >>>>>>> On Wed, 16 Jan 2019, Jan Beulich wrote:
>> >>>> Stop. No. We very much can prove they are - _end points at
>> >>>> one past the last element of _start[]. It is the compiler which
>> >>>> can't prove the opposite, and hence it can't leverage
>> >>>> undefined behavior for optimization purposes.
>> >>>
>> >>> You keep saying the compiler can't leverage it for optimization purpose,
>> >>> however
>> >>> there are confirmations that GCC may actually leverage it (e.g [1]). You
>> >>> actually need to trick the compiler to avoid the optimization (e.g
>> >>> RELOC_HIDE).
>> >>>
>> >>> So obviously, this is not only a MISRA "problem" as you state here and
>> >>> below.
>> >>>
>> >>> I believe Stefano, Stewart and I provided plenty of documentation/thread 
>> >>> to
>> >>> support our positions. Can you provide us documentation/thread showing 
>> >>> the
>> >>> compiler will not try to leverage that case?
>> >>>
>> >>> Cheers,
>> >>>
>> >>> [1]
>> >>> 
>> > 
> https://kristerw.blogspot.com/2016/12/pointer-comparison-invalid-optimization.h
>  
> tml?m=1
>> >> 
>> >> Btw., the __start[] / __end[] example given there does not match
>> >> up with what I see.
>> > What you see in a specific version of GCC. This does not mean this 
>> > behavior 
> is 
>> > valid across all the released versions and future one.
>> 
>> Are you suggesting that for the purpose of certification we need to
>> deal with compiler bugs? Imo such a compiler should simply be
>> excluded for use to build Xen.
>> 
>> >> Only symbols defined in the same CU as where
>> >> the comparison sits get "optimized" this way. Externs as well as
>> >> weak symbols defined locally don't get dealt with like this. And how
>> >> could they? Nothing tells the compiler that two distinct symbols
>> >> refer to two distinct objects. It is easy to create objects with
>> >> multiple names, not only in assembly but also in C (using the "alias"
>> >> attribute).
>> > 
>> > Similarly, nothing tells the compiler that they are not two distinct 
> symbols. 
>> > You haven't yet provided evidence a compiler cannot use that for 
> optimization.
>> 
>> The compiler can leverage for optimization only what it can prove
>> (to be undefined behavior or symbols referring to distinct objects
>> or ...). A compiler may never use guesses for optimization. That
>> is in the case here it is not us who need to tell the compiler that
>> two different symbols may refer to the same object, but it is the
>> compiler which needs to prove that two symbols cannot possibly
>> refer to the same object. This is possible for automatic and static
>> objects. This is also possible for some non-static objects defined
>> in the CU under compilation. But this is not possible in the general
>> case.
> 
> Clearly from the GCC thread not everybody agrees with you:
> 
>  Just because two pointers print the same and have the same bit-pattern 
>  doesn't mean they need to compare equal
> 
>  So the only way within the C standard you could deduce that two objects 
>  follow each other in memory is that the address of one compares equal to 
>  one past the address of the other - but that does not mean they follow 
>  each other in memory for any other comparison.

I think continuing to hit on this aspect is just adding confusion: We
_do not_ leverage the "end" labels to happen to point at the end of
the previous object. That's a pattern the subsequent objects' "start"
label may happen to match. The "end" labels, otoh, don't point at
the start of any object, they point at what we point them at - the
end of the preceding object. Once again I'd like to emphasize the
difference between "object" and "symbol"; as said before I have
not been able to find anything in the spec saying that there's a
requirement that symbols can only point at the start of objects, or
that there can only be a single symbol pointing at a given object.

Jan


_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/mailman/listinfo/xen-devel

 


Rackspace

Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.