Re: [GIT PULL tools] Linux kernel memory model

On Fri, Feb 09, 2018 at 01:41:12PM +0100, Andrea Parri wrote: > On Fri, Feb 09, 2018 at 03:29:37AM -0800, Paul E. McKenney wrote: > > On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote: > > > On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote: > > > > On Thu, Feb 08, 2018 at

Re: [GIT PULL tools] Linux kernel memory model

On Fri, Feb 09, 2018 at 01:41:12PM +0100, Andrea Parri wrote: > On Fri, Feb 09, 2018 at 03:29:37AM -0800, Paul E. McKenney wrote: > > On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote: > > > On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote: > > > > On Thu, Feb 08, 2018 at

Re: [GIT PULL tools] Linux kernel memory model

On Fri, Feb 09, 2018 at 03:29:37AM -0800, Paul E. McKenney wrote: > On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote: > > On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote: > > > On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > > > > Hi Paul, > > > >

Re: [GIT PULL tools] Linux kernel memory model

On Fri, Feb 09, 2018 at 03:29:37AM -0800, Paul E. McKenney wrote: > On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote: > > On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote: > > > On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > > > > Hi Paul, > > > >

Re: [GIT PULL tools] Linux kernel memory model

On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > Hi Paul, > thanks to you and all the involved guys for this useful tool. > > I give it a try today and found that by installing herd7 by just > following the instruction in herdtools7/INSTALL.md, and precisely > installing it via:

Re: [GIT PULL tools] Linux kernel memory model

On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > Hi Paul, > thanks to you and all the involved guys for this useful tool. > > I give it a try today and found that by installing herd7 by just > following the instruction in herdtools7/INSTALL.md, and precisely > installing it via:

Re: [GIT PULL tools] Linux kernel memory model

On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote: > On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote: > > On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > > > Hi Paul, > > > thanks to you and all the involved guys for this useful tool. > > > > > > I

Re: [GIT PULL tools] Linux kernel memory model

On Fri, Feb 09, 2018 at 10:11:10AM +0100, Andrea Parri wrote: > On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote: > > On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > > > Hi Paul, > > > thanks to you and all the involved guys for this useful tool. > > > > > > I

Re: [GIT PULL tools] Linux kernel memory model

On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote: > On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > > Hi Paul, > > thanks to you and all the involved guys for this useful tool. > > > > I give it a try today and found that by installing herd7 by just > > following

Re: [GIT PULL tools] Linux kernel memory model

On Thu, Feb 08, 2018 at 09:02:19PM +0100, Peter Zijlstra wrote: > On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > > Hi Paul, > > thanks to you and all the involved guys for this useful tool. > > > > I give it a try today and found that by installing herd7 by just > > following

Re: [GIT PULL tools] Linux kernel memory model

On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > Hi Paul, > thanks to you and all the involved guys for this useful tool. > > I give it a try today and found that by installing herd7 by just > following the instruction in herdtools7/INSTALL.md, and precisely > installing it via:

Re: [GIT PULL tools] Linux kernel memory model

On Thu, Feb 08, 2018 at 06:41:06PM +, Patrick Bellasi wrote: > Hi Paul, > thanks to you and all the involved guys for this useful tool. > > I give it a try today and found that by installing herd7 by just > following the instruction in herdtools7/INSTALL.md, and precisely > installing it via:

Re: [GIT PULL tools] Linux kernel memory model

Hi Paul, thanks to you and all the involved guys for this useful tool. I give it a try today and found that by installing herd7 by just following the instruction in herdtools7/INSTALL.md, and precisely installing it via: opam install herdtools7 it seems to give you a tool which fails to run

Re: [GIT PULL tools] Linux kernel memory model

Hi Paul, thanks to you and all the involved guys for this useful tool. I give it a try today and found that by installing herd7 by just following the instruction in herdtools7/INSTALL.md, and precisely installing it via: opam install herdtools7 it seems to give you a tool which fails to run

Re: [GIT PULL tools] Linux kernel memory model

On Sun, Feb 04, 2018 at 11:37:59AM -0500, Alan Stern wrote: > On Sun, 4 Feb 2018, Paul E. McKenney wrote: > > > --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus > > +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus > > @@ -1,5 +1,11 @@ > > C CoRW+poonceonce+Once

Re: [GIT PULL tools] Linux kernel memory model

On Sun, Feb 04, 2018 at 11:37:59AM -0500, Alan Stern wrote: > On Sun, 4 Feb 2018, Paul E. McKenney wrote: > > > --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus > > +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus > > @@ -1,5 +1,11 @@ > > C CoRW+poonceonce+Once

Re: [GIT PULL tools] Linux kernel memory model

On Sun, Feb 04, 2018 at 05:29:00PM +0100, Andrea Parri wrote: > On Sun, Feb 04, 2018 at 02:17:00AM -0800, Paul E. McKenney wrote: > > [...] > > > And here is the updated commit adding comments to the litmus test, > > which adds comments for the three litmus tests added above. I have also > >

Re: [GIT PULL tools] Linux kernel memory model

On Sun, Feb 04, 2018 at 05:29:00PM +0100, Andrea Parri wrote: > On Sun, Feb 04, 2018 at 02:17:00AM -0800, Paul E. McKenney wrote: > > [...] > > > And here is the updated commit adding comments to the litmus test, > > which adds comments for the three litmus tests added above. I have also > >

Re: [GIT PULL tools] Linux kernel memory model

On Sun, 4 Feb 2018, Paul E. McKenney wrote: > --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus > +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus > @@ -1,5 +1,11 @@ > C CoRW+poonceonce+Once > > +(* > + * Test of read-write coherence, that is, whether or not a

Re: [GIT PULL tools] Linux kernel memory model

On Sun, 4 Feb 2018, Paul E. McKenney wrote: > --- a/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus > +++ b/tools/memory-model/litmus-tests/CoRW+poonceonce+Once.litmus > @@ -1,5 +1,11 @@ > C CoRW+poonceonce+Once > > +(* > + * Test of read-write coherence, that is, whether or not a

Re: [GIT PULL tools] Linux kernel memory model

On Sun, Feb 04, 2018 at 02:17:00AM -0800, Paul E. McKenney wrote: [...] > And here is the updated commit adding comments to the litmus test, > which adds comments for the three litmus tests added above. I have also > marked this commit with "EXP" indicating that it has not yet had time > for

Re: [GIT PULL tools] Linux kernel memory model

On Sun, Feb 04, 2018 at 02:17:00AM -0800, Paul E. McKenney wrote: [...] > And here is the updated commit adding comments to the litmus test, > which adds comments for the three litmus tests added above. I have also > marked this commit with "EXP" indicating that it has not yet had time > for

Re: [GIT PULL tools] Linux kernel memory model

On Sun, Feb 04, 2018 at 01:16:01AM -0800, Paul E. McKenney wrote: > On Sat, Feb 03, 2018 at 05:10:06PM -0500, Alan Stern wrote: > > On Sat, 3 Feb 2018, Paul E. McKenney wrote: > > > > > Please see below for an initial patch to this effect. This activity > > > proved to be more productive than

Re: [GIT PULL tools] Linux kernel memory model

On Sun, Feb 04, 2018 at 01:16:01AM -0800, Paul E. McKenney wrote: > On Sat, Feb 03, 2018 at 05:10:06PM -0500, Alan Stern wrote: > > On Sat, 3 Feb 2018, Paul E. McKenney wrote: > > > > > Please see below for an initial patch to this effect. This activity > > > proved to be more productive than

Re: [GIT PULL tools] Linux kernel memory model

On Sat, Feb 03, 2018 at 05:10:06PM -0500, Alan Stern wrote: > On Sat, 3 Feb 2018, Paul E. McKenney wrote: > > > Please see below for an initial patch to this effect. This activity > > proved to be more productive than expected for these tests, which certainly > > supports our assertion that

Re: [GIT PULL tools] Linux kernel memory model

On Sat, Feb 03, 2018 at 05:10:06PM -0500, Alan Stern wrote: > On Sat, 3 Feb 2018, Paul E. McKenney wrote: > > > Please see below for an initial patch to this effect. This activity > > proved to be more productive than expected for these tests, which certainly > > supports our assertion that

Re: [GIT PULL tools] Linux kernel memory model

On Sat, 3 Feb 2018, Paul E. McKenney wrote: > Please see below for an initial patch to this effect. This activity > proved to be more productive than expected for these tests, which certainly > supports our assertion that locking needs more testing... > > MP+polocks.litmus >

Re: [GIT PULL tools] Linux kernel memory model

On Sat, 3 Feb 2018, Paul E. McKenney wrote: > Please see below for an initial patch to this effect. This activity > proved to be more productive than expected for these tests, which certainly > supports our assertion that locking needs more testing... > > MP+polocks.litmus >

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote: > * Paul E. McKenney wrote: > > On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote: [ . . . ] > A couple of questions: > > - Would it be possible to include all the nice descriptions of the litmus

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote: > * Paul E. McKenney wrote: > > On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote: [ . . . ] > A couple of questions: > > - Would it be possible to include all the nice descriptions of the litmus > tests in > the tests

Re: [GIT PULL tools] Linux kernel memory model

On Fri, Feb 02, 2018 at 12:46:03PM +0800, Boqun Feng wrote: > On Wed, Jan 31, 2018 at 05:17:28PM -0800, Paul E. McKenney wrote: > [...] > > > - A long term question: have you considered and would it make sense to > > > generate a > > > memory-barriers.txt like file directly into

Re: [GIT PULL tools] Linux kernel memory model

On Fri, Feb 02, 2018 at 12:46:03PM +0800, Boqun Feng wrote: > On Wed, Jan 31, 2018 at 05:17:28PM -0800, Paul E. McKenney wrote: > [...] > > > - A long term question: have you considered and would it make sense to > > > generate a > > > memory-barriers.txt like file directly into

Re: [GIT PULL tools] Linux kernel memory model

On Thu, Feb 01, 2018 at 07:57:42AM +0100, Ingo Molnar wrote: > > * Paul E. McKenney wrote: > > > > I believe these additional improvements (to the extent you agree with > > > doing them!) > > > could/should be done as add-on commits on top of this existing commit.

Re: [GIT PULL tools] Linux kernel memory model

On Thu, Feb 01, 2018 at 07:57:42AM +0100, Ingo Molnar wrote: > > * Paul E. McKenney wrote: > > > > I believe these additional improvements (to the extent you agree with > > > doing them!) > > > could/should be done as add-on commits on top of this existing commit. > > > > Sounds good! > > >

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 05:17:28PM -0800, Paul E. McKenney wrote: [...] > > - A long term question: have you considered and would it make sense to > > generate a > > memory-barriers.txt like file directly into Documentation/locking/, using > > the > > formal description? That way any

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 05:17:28PM -0800, Paul E. McKenney wrote: [...] > > - A long term question: have you considered and would it make sense to > > generate a > > memory-barriers.txt like file directly into Documentation/locking/, using > > the > > formal description? That way any

Re: [GIT PULL tools] Linux kernel memory model

* Paul E. McKenney wrote: > > I believe these additional improvements (to the extent you agree with doing > > them!) > > could/should be done as add-on commits on top of this existing commit. > > Sounds good! > > Would you prefer a pull request or a patch series

Re: [GIT PULL tools] Linux kernel memory model

* Paul E. McKenney wrote: > > I believe these additional improvements (to the extent you agree with doing > > them!) > > could/should be done as add-on commits on top of this existing commit. > > Sounds good! > > Would you prefer a pull request or a patch series for these? Patch series

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote: > > * Paul E. McKenney wrote: > > > On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote: > > > > > > hi Paul, > > > > > > * Paul E. McKenney wrote: > > > > > > >

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote: > > * Paul E. McKenney wrote: > > > On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote: > > > > > > hi Paul, > > > > > > * Paul E. McKenney wrote: > > > > > > > Hello, Ingo, > > > > > > > > This pull request contains a

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 11:08:22AM +0100, Peter Zijlstra wrote: > On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote: > > - Similary, some of the high level descriptions in tools/memory-model/README > > should probably propagated into the source code files as well: for example > >

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 11:08:22AM +0100, Peter Zijlstra wrote: > On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote: > > - Similary, some of the high level descriptions in tools/memory-model/README > > should probably propagated into the source code files as well: for example > >

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote: > - Similary, some of the high level descriptions in tools/memory-model/README > should probably propagated into the source code files as well: for example > both tools/memory-model/lock.cat and linux-kernel.cat could be improved

Re: [GIT PULL tools] Linux kernel memory model

On Wed, Jan 31, 2018 at 10:00:06AM +0100, Ingo Molnar wrote: > - Similary, some of the high level descriptions in tools/memory-model/README > should probably propagated into the source code files as well: for example > both tools/memory-model/lock.cat and linux-kernel.cat could be improved

Re: [GIT PULL tools] Linux kernel memory model

* Paul E. McKenney wrote: > On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote: > > > > hi Paul, > > > > * Paul E. McKenney wrote: > > > > > Hello, Ingo, > > > > > > This pull request contains a single commit that adds a

Re: [GIT PULL tools] Linux kernel memory model

* Paul E. McKenney wrote: > On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote: > > > > hi Paul, > > > > * Paul E. McKenney wrote: > > > > > Hello, Ingo, > > > > > > This pull request contains a single commit that adds a memory model to > > > the tools directory. This memory

Re: [GIT PULL tools] Linux kernel memory model

On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote: > > hi Paul, > > * Paul E. McKenney wrote: > > > Hello, Ingo, > > > > This pull request contains a single commit that adds a memory model to > > the tools directory. This memory model can (roughly

Re: [GIT PULL tools] Linux kernel memory model

On Mon, Jan 29, 2018 at 07:57:24AM +0100, Ingo Molnar wrote: > > hi Paul, > > * Paul E. McKenney wrote: > > > Hello, Ingo, > > > > This pull request contains a single commit that adds a memory model to > > the tools directory. This memory model can (roughly speaking) be thought > > of as an

Re: [GIT PULL tools] Linux kernel memory model

hi Paul, * Paul E. McKenney wrote: > Hello, Ingo, > > This pull request contains a single commit that adds a memory model to > the tools directory. This memory model can (roughly speaking) be thought > of as an automated version of memory-barriers.txt. It is

Re: [GIT PULL tools] Linux kernel memory model

hi Paul, * Paul E. McKenney wrote: > Hello, Ingo, > > This pull request contains a single commit that adds a memory model to > the tools directory. This memory model can (roughly speaking) be thought > of as an automated version of memory-barriers.txt. It is written in the > "cat" language,

[GIT PULL tools] Linux kernel memory model

Hello, Ingo, This pull request contains a single commit that adds a memory model to the tools directory. This memory model can (roughly speaking) be thought of as an automated version of memory-barriers.txt. It is written in the "cat" language, which is executable by the externally provided

[GIT PULL tools] Linux kernel memory model

Hello, Ingo, This pull request contains a single commit that adds a memory model to the tools directory. This memory model can (roughly speaking) be thought of as an automated version of memory-barriers.txt. It is written in the "cat" language, which is executable by the externally provided