All of lore.kernel.org
 help / color / mirror / Atom feed
From: Stefano Stabellini <sstabellini@kernel.org>
To: Jan Beulich <JBeulich@suse.com>
Cc: Juergen Gross <jgross@suse.com>,
	Stefano Stabellini <stefanos@xilinx.com>,
	Stefano Stabellini <sstabellini@kernel.org>,
	Wei Liu <wei.liu2@citrix.com>,
	Andrew Cooper <andrew.cooper3@citrix.com>,
	Julien Grall <julien.grall@gmail.com>,
	Julien Grall <julien.grall@arm.com>,
	Stewart Hildebrand <Stewart.Hildebrand@dornerworks.com>,
	xen-devel <xen-devel@lists.xenproject.org>
Subject: Re: [PATCH v6 1/4] xen: introduce SYMBOL
Date: Mon, 21 Jan 2019 15:15:54 -0800 (PST)	[thread overview]
Message-ID: <alpine.DEB.2.10.1901211512290.12685@sstabellini-ThinkPad-X260> (raw)
In-Reply-To: <5C459F9A020000780020FA17@prv1-mh.provo.novell.com>

On Mon, 21 Jan 2019, Jan Beulich wrote:
> >>> On 21.01.19 at 11:22, <julien.grall@arm.com> wrote:
> > Hi Jan,
> > 
> > On 21/01/2019 09:34, Jan Beulich wrote:
> >>>>> On 18.01.19 at 11:48, <julien.grall@arm.com> wrote:
> >>> On 18/01/2019 09:54, Jan Beulich wrote:
> >>>>>>> On 18.01.19 at 02:24, <sstabellini@kernel.org> wrote:
> >>>>> On Thu, 17 Jan 2019, Jan Beulich wrote:
> >>>>>>>>> On 17.01.19 at 01:37, <sstabellini@kernel.org> 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.html?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.

  > Are you saying it's possible that y immediately follows x in the
  > address space when that line of output is printed, and that y *doesn't*
  > immediately follow x in the address space when "inconsistent behavior:"
  > is printed?
  
  Yes.

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

  reply	other threads:[~2019-01-21 23:15 UTC|newest]

Thread overview: 102+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-01-09 23:41 [PATCH v6 0/4] misc safety certification fixes Stefano Stabellini
2019-01-09 23:42 ` [PATCH v6 1/4] xen: introduce SYMBOL Stefano Stabellini
2019-01-10  2:40   ` Julien Grall
2019-01-10  8:24     ` Jan Beulich
2019-01-10 17:29       ` Stefano Stabellini
2019-01-10 18:46         ` Stewart Hildebrand
2019-01-10 19:03           ` Stefano Stabellini
2019-01-11 10:35           ` Jan Beulich
2019-01-11 17:01             ` Stefano Stabellini
2019-01-10 19:24         ` Julien Grall
2019-01-10 21:36           ` Stefano Stabellini
2019-01-10 23:31             ` Julien Grall
2019-01-11  2:14               ` Stefano Stabellini
2019-01-11  6:52                 ` Juergen Gross
2019-01-11 16:52                   ` Stefano Stabellini
2019-01-11 10:48                 ` Jan Beulich
2019-01-11 18:04                   ` Stefano Stabellini
2019-01-11 18:53                     ` Stewart Hildebrand
2019-01-11 20:35                       ` Julien Grall
2019-01-11 20:46                         ` Stewart Hildebrand
2019-01-11 21:37                           ` Stefano Stabellini
2019-01-14  3:45                             ` Stewart Hildebrand
2019-01-14 10:26                               ` Jan Beulich
2019-01-14 21:18                                 ` Stefano Stabellini
     [not found]                                   ` <1CACC1FB020000D800417A66@prv1-mh.provo.novell.com>
2019-01-15  8:21                                     ` Jan Beulich
2019-01-15 11:51                                       ` Julien Grall
     [not found]                                         ` <AB1DA25B020000B95C475325@prv1-mh.provo.novell.com>
2019-01-15 12:04                                           ` Jan Beulich
2019-01-15 12:23                                             ` Julien Grall
     [not found]                                               ` <BAE986750200003A5C475325@prv1-mh.provo.novell.com>
2019-01-15 12:44                                                 ` Jan Beulich
2019-01-15 20:03                                       ` Stewart Hildebrand
2019-01-16  6:01                                         ` Juergen Gross
2019-01-16 10:19                                         ` Jan Beulich
2019-01-17  0:37                                           ` Stefano Stabellini
     [not found]                                             ` <B4D3ABC30200003B88BF86FB@prv1-mh.provo.novell.com>
     [not found]                                               ` <529ED2F90200004D00417A66@prv1-mh.provo.novell.com>
2019-01-17 11:45                                                 ` Jan Beulich
2019-01-18  1:24                                                   ` Stefano Stabellini
     [not found]                                                     ` <76A2DEED0200005600417A66@prv1-mh.provo.novell.com>
2019-01-18  9:54                                                       ` Jan Beulich
2019-01-18 10:48                                                         ` Julien Grall
     [not found]                                                           ` <9F511FC70200005E5C475325@prv1-mh.provo.novell.com>
2019-01-18 11:09                                                             ` Jan Beulich
2019-01-18 15:22                                                               ` Julien Grall
     [not found]                                                                 ` <3A8206D8020000035C475325@prv1-mh.provo.novell.com>
2019-01-21  9:39                                                                   ` Jan Beulich
2019-01-21  9:34                                                             ` Jan Beulich
2019-01-21 10:22                                                               ` Julien Grall
     [not found]                                                                 ` <E16AB350020000435C475325@prv1-mh.provo.novell.com>
2019-01-21 10:31                                                                   ` Jan Beulich
2019-01-21 23:15                                                                     ` Stefano Stabellini [this message]
     [not found]                                                                       ` <5EA2B4FA0200008000417A66@prv1-mh.provo.novell.com>
2019-01-22  9:06                                                                         ` Jan Beulich
2019-01-18 23:05                                                         ` Stefano Stabellini
2019-01-21  5:24                                                           ` Stewart Hildebrand
     [not found]                                                           ` <5A96F2FD0200008D00417A66@prv1-mh.provo.novell.com>
2019-01-21  9:50                                                             ` Jan Beulich
2019-01-21 23:41                                                               ` Stefano Stabellini
2019-01-22  6:08                                                                 ` Juergen Gross
     [not found]                                                                 ` <42A2C4FA0200009000417A66@prv1-mh.provo.novell.com>
2019-01-22  9:16                                                                   ` Jan Beulich
2019-02-01 18:52                                                                     ` George Dunlap
2019-02-01 20:53                                                                       ` Stefano Stabellini
     [not found]                                                             ` <58377FAD0200004688BF86FB@prv1-mh.provo.novell.com>
2019-01-21 10:06                                                               ` Jan Beulich
2019-02-06 15:41                                                                 ` Ian Jackson
     [not found]                                           ` <C8F95655020000CAB8D7C7D4@prv1-mh.provo.novell.com>
     [not found]                                             ` <5867EFE6020000DB00417A66@prv1-mh.provo.novell.com>
     [not found]                                               ` <DACE7A5F020000B1B8D7C7D4@prv1-mh.provo.novell.com>
2019-02-07 14:51                                                 ` Jan Beulich
2019-01-15 23:36                                       ` Stefano Stabellini
2019-01-16  8:47                                         ` Juergen Gross
     [not found]                                         ` <2EA6D6FD0200001F00417A66@prv1-mh.provo.novell.com>
2019-01-16 10:25                                           ` Jan Beulich
2019-01-17  0:41                                             ` Stefano Stabellini
     [not found]                                               ` <4EA2F2F90200004D00417A66@prv1-mh.provo.novell.com>
2019-01-17 11:46                                                 ` Jan Beulich
     [not found]                                     ` <95DC675902000028AB59E961@prv1-mh.provo.novell.com>
2019-02-04  9:37                                       ` Jan Beulich
2019-02-04 19:08                                         ` Stefano Stabellini
2019-02-05  6:02                                           ` Juergen Gross
     [not found]                                           ` <2E9DDEFD0200007B00417A66@prv1-mh.provo.novell.com>
2019-02-05  7:53                                             ` Jan Beulich
2019-02-05 14:56                                         ` George Dunlap
     [not found]                                           ` <E730A9F90200001DAB59E961@prv1-mh.provo.novell.com>
2019-02-06 11:59                                             ` Jan Beulich
     [not found]                                 ` <7A8C0A4F020000EEB8D7C7D4@prv1-mh.provo.novell.com>
2019-02-06 16:21                                   ` Jan Beulich
2019-02-06 16:37                                     ` Ian Jackson
     [not found]                                       ` <08D440470200001BB8D7C7D4@prv1-mh.provo.novell.com>
2019-02-06 16:47                                         ` Jan Beulich
2019-02-06 16:52                                           ` Ian Jackson
2019-02-06 23:39                                             ` Stefano Stabellini
2019-02-07 11:48                                               ` Ian Jackson
2019-02-07 18:18                                                 ` Stefano Stabellini
2019-02-12 11:31                                                   ` Ian Jackson
2019-02-13  0:09                                                     ` Stefano Stabellini
2019-01-15 11:46                             ` Julien Grall
2019-01-15 12:23                               ` Julien Grall
2019-01-14 10:11                     ` Jan Beulich
2019-01-14 15:41                       ` Julien Grall
2019-01-14 15:52                         ` Jan Beulich
2019-01-14 16:26                           ` Stewart Hildebrand
2019-01-14 16:39                             ` Jan Beulich
2019-01-14 16:28                           ` Julien Grall
2019-01-14 16:44                             ` Jan Beulich
2019-01-14 17:24                               ` Julien Grall
2019-01-15  8:04                                 ` Jan Beulich
2019-01-10 17:22     ` Stefano Stabellini
2019-01-10  8:34   ` Jan Beulich
2019-01-10 18:09     ` Stefano Stabellini
2019-01-09 23:42 ` [PATCH v6 2/4] xen/arm: use SYMBOL when required Stefano Stabellini
2019-01-10  8:41   ` Jan Beulich
2019-01-10 17:44     ` Stefano Stabellini
2019-01-11 10:52       ` Jan Beulich
2019-01-11 16:58         ` Stefano Stabellini
2019-01-14  9:23           ` Jan Beulich
2019-01-09 23:42 ` [PATCH v6 3/4] xen/x86: " Stefano Stabellini
2019-01-10  8:43   ` Jan Beulich
2019-01-10 17:45     ` Stefano Stabellini
2019-01-09 23:42 ` [PATCH v6 4/4] xen/common: " Stefano Stabellini
2019-01-10  8:49   ` Jan Beulich
2019-01-10 17:48     ` Stefano Stabellini

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=alpine.DEB.2.10.1901211512290.12685@sstabellini-ThinkPad-X260 \
    --to=sstabellini@kernel.org \
    --cc=JBeulich@suse.com \
    --cc=Stewart.Hildebrand@dornerworks.com \
    --cc=andrew.cooper3@citrix.com \
    --cc=jgross@suse.com \
    --cc=julien.grall@arm.com \
    --cc=julien.grall@gmail.com \
    --cc=stefanos@xilinx.com \
    --cc=wei.liu2@citrix.com \
    --cc=xen-devel@lists.xenproject.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.