Re: Adopting the Linux Kernel Memory Model in Xen?

[Julien Grall <julien@xxxxxxx>]

Hi Jan,

On 14/09/2020 10:03, Jan Beulich wrote:
> On 11.09.2020 18:33, Julien Grall wrote:
> > 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.
> While I agree with the goal, I'm uncertain about the last of the
> three points above, at least as long as we're "blindly" taking
> whatever they do or decide. Over the years they've changed their
> implementation a number of time afaict, in order to deal with
> "disagreements" between it and what compilers actually do and/or can
> be expected to guarantee. Yes, the Linux community is much bigger
> than ours, and hence chances are far better for someone there to
> notice and correct flaws or oversights, yet I still think it cannot
> be the goal to silence discussions on our side, even if they tend to
> be unpleasant for (almost) everyone involved.
Xen-devel (or security@) is not suited for arguing on how a 
compiler/processor should behave (or not). We don't have the expertise 
for making a proper decision.
Don't get me wrong, I am not trying to silence discussion but rather 
move them to the correct forum.
If we adopt the LKMM, then all the discussions on Xen-devel could be 
reduced to whether the code match the formal model.
If there are any questions on the model, then they would be raised 
directly with the LKMM team. They can then assess if they need to update
the model.

> One additional thing needs to be kept in mind imo, especially also
> having seen Andrew's reply: If we more formally tie ourselves to
> their model (and I agree with him that informally we already do so
> anyway in sufficiently large a degree), we need to take measures to
> make sure we also adjust our code when they adjust theirs.
This makes perfect sense. I would expect the effort to be quite minimal 
in long term.
Cheers,

--
Julien Grall