Re: Adopting the Linux Kernel Memory Model in Xen?

[Julien Grall <julien@xxxxxxx>]

Hi Andrew,

On 11/09/2020 20:53, Andrew Cooper wrote:
> On 11/09/2020 17:33, Julien Grall wrote:
> > Hi all,
> >
> > At the moment, Xen doesn't have a formal memory model. Instead, we are
> > relying on intuitions. This can lead to heated discussion on what can
> > a processor/compiler do or not.
> >
> > We also have some helpers that nearly do the same (such as
> > {read,write}_atomic() vs ACCESS_ONCE()) with no clear understanding
> > where to use which.
> >
> > In the past few years, Linux community spent a lot of time to write
> > down their memory model and make the compiler communities aware of it
> > (see [1], [2]).
> >
> > There are a few reasons I can see for adopting LKMM:
> >     - Xen borrows a fair amount of code from Linux;
> >     - There are efforts to standardize it;
> >     - This will allow us to streamline the discussion.
> >
> > Any thoughts?
> It might not be formally written down, but we inherited an old version
> of it from Linux directly, and memory-barriers.txt is often referred to,
> and I have fixed our helpers several times to not have a semantic
> difference vs Linux.
>
> We even import some drivers verbatim, and they certainly are expecting
> to use LKMM.
>
>
> Memory ordering is a phenomenally complicated topic and getting it wrong
> usually results in very subtle memory corruption issues.  The Xen
> community does not have the expertise to invent something custom.  LKMM
> is already familiar to most people liable to contribute in areas where
> it is likely to matter.
>
> I don't mind how we go about formally stating that we use LKMM, but as
> far as I'm concerned, we already use it, and any semantic deviation is a
> bug needing fixing in Xen.
Thank you for the input! My plan is to:
   - Create a brief document (maybe docs/memory-barrier.txt) explaing 
that we follow LKMM.
   - Look for existing differences in the helpers and sync them if needed.

Cheers,

--
Julien Grall