Adopting the Linux Kernel Memory Model in Xen?

Adopting the Linux Kernel Memory Model in Xen?

[Julien Grall]

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?

Cheers,

[1] https://www.kernel.org/doc/Documentation/memory-barriers.txt
[2] http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p0124r7.html


-- 
Julien Grall

Re: Adopting the Linux Kernel Memory Model in Xen?

[Andrew Cooper]

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.

~Andrew

RE: Adopting the Linux Kernel Memory Model in Xen?

[Paul Durrant]

> -----Original Message-----
> From: Xen-devel <xen-devel-bounces@lists.xenproject.org> On Behalf Of Julien Grall
> Sent: 11 September 2020 17:34
> To: xen-devel@lists.xenproject.org; committers@xenproject.org
> Cc: Roger Pau Monné <roger.pau@citrix.com>; Bertrand Marquis <Bertrand.Marquis@arm.com>
> Subject: Adopting the Linux Kernel Memory Model in Xen?
> 
> 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.
> 

...which, in turn, may well lead us into decisions that harm performance.

> 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;

...and essentially the same toolchain(s)

>     - There are efforts to standardize it;
>     - This will allow us to streamline the discussion.
> 
> Any thoughts?
> 

It seems like a very good idea to me.

  Paul

> Cheers,
> 
> [1] https://www.kernel.org/doc/Documentation/memory-barriers.txt
> [2] http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p0124r7.html
> 
> 
> --
> Julien Grall

Re: Adopting the Linux Kernel Memory Model in Xen?

[Jan Beulich]

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.

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.

Jan

Re: Adopting the Linux Kernel Memory Model in Xen?

[Julien Grall]

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

Re: Adopting the Linux Kernel Memory Model in Xen?

[Julien Grall]

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