From: Alan Stern <stern@rowland.harvard.edu> To: "Paul E. McKenney" <paulmck@linux.ibm.com> Cc: David Goldblatt <davidtgoldblatt@gmail.com>, <mathieu.desnoyers@efficios.com>, Florian Weimer <fweimer@redhat.com>, <triegel@redhat.com>, <libc-alpha@sourceware.org>, <andrea.parri@amarulasolutions.com>, <will.deacon@arm.com>, <peterz@infradead.org>, <boqun.feng@gmail.com>, <npiggin@gmail.com>, <dhowells@redhat.com>, <j.alglave@ucl.ac.uk>, <luc.maranget@inria.fr>, <akiyks@gmail.com>, <dlustig@nvidia.com>, <linux-arch@vger.kernel.org>, <linux-kernel@vger.kernel.org> Subject: Re: [PATCH] Linux: Implement membarrier function Date: Wed, 12 Dec 2018 16:32:50 -0500 (EST) [thread overview] Message-ID: <Pine.LNX.4.44L0.1812121604430.1543-100000@iolanthe.rowland.org> (raw) In-Reply-To: <20181212194225.GB4170@linux.ibm.com> On Wed, 12 Dec 2018, Paul E. McKenney wrote: > OK. How about this one? > > P0 P1 P2 P3 > Wa=2 rcu_read_lock() Wc=2 Wd=2 > memb Wb=2 Rd=0 synchronize_rcu(); > Rb=0 Rc=0 Ra=0 > rcu_read_unlock() > > The model should say that it is allowed. Taking a look... > > P0 P1 P2 P3 > Rd=0 > Wd=2 > synchronize_rcu(); > Ra=0 > Wa=2 > membs > rcu_read_lock() > [m01] > Rc=0 > Wc=2 > [m02] [m03] > membe > Rb=0 > Wb=2 > rcu_read_unlock() > > Looks allowed to me. If the synchronization of P1 and P2 were > interchanged, it should be forbidden: > > P0 P1 P2 P3 > Wa=2 Wb=2 rcu_read_lock() Wd=2 > memb Rc=0 Wc=2 synchronize_rcu(); > Rb=0 Rd=0 Ra=0 > rcu_read_unlock() > > Taking a look... > > P0 P1 P2 P3 > rcu_read_lock() > Rd=0 > Wa=2 Wb=2 Wd=2 > membs synchronize_rcu(); > [m01] > Rc=0 > Wc=2 > rcu_read_unlock() > [m02] Ra=0 [Forbidden?] > membe > Rb=0 Have you tried writing these as real litmus tests and running them through herd? > I believe that this ordering forbids the cycle: > > Wa=1 > membs -> [m01] -> Rc=0 -> Wc=2 -> rcu_read_unlock() -> > return from synchronize_rcu() -> Ra > > Does this make sense, or am I missing something? It's hard to tell. What you have written here isn't justified by the litmus test source code, since the position of m01 in P1's program order is undetermined. How do you justify m01 -> Rc, for example? Write it this way instead, using the relations defined in the sys_membarrier patch for linux-kernel.cat: memb ->memb-gp memb ->rcu-link Rc ->memb-rscsi Rc ->rcu-link rcu_read_unlock ->rcu-rscsi rcu_read_lock ->rcu-link synchronize_rcu ->rcu-gp synchronize_rcu ->rcu-link memb Recall that: memb-gp is the identity relation on sys_membarrier events, rcu-link includes (po? ; fre ; po), memb-rscsi is the identity relation on all events, rcu-rscsi links unlocks to their corresponding locks, and rcu-gp is the identity relation on synchronize_rcu events. These facts justify the cycle above. Leaving off the final rcu-link step, the sequence matches the definition of rcu-fence (the relations are memb-gp, memb-rscsi, rcu-rscsi, rcu-gp with rcu-links in between). Therefore the cycle is forbidden. Alan
WARNING: multiple messages have this Message-ID (diff)
From: Alan Stern <stern@rowland.harvard.edu> To: "Paul E. McKenney" <paulmck@linux.ibm.com> Cc: David Goldblatt <davidtgoldblatt@gmail.com>, mathieu.desnoyers@efficios.com, Florian Weimer <fweimer@redhat.com>, triegel@redhat.com, libc-alpha@sourceware.org, andrea.parri@amarulasolutions.com, will.deacon@arm.com, peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com, dlustig@nvidia.com, linux-arch@vger.kernel.org, linux-kernel@vger.kernel.org Subject: Re: [PATCH] Linux: Implement membarrier function Date: Wed, 12 Dec 2018 16:32:50 -0500 (EST) [thread overview] Message-ID: <Pine.LNX.4.44L0.1812121604430.1543-100000@iolanthe.rowland.org> (raw) In-Reply-To: <20181212194225.GB4170@linux.ibm.com> On Wed, 12 Dec 2018, Paul E. McKenney wrote: > OK. How about this one? > > P0 P1 P2 P3 > Wa=2 rcu_read_lock() Wc=2 Wd=2 > memb Wb=2 Rd=0 synchronize_rcu(); > Rb=0 Rc=0 Ra=0 > rcu_read_unlock() > > The model should say that it is allowed. Taking a look... > > P0 P1 P2 P3 > Rd=0 > Wd=2 > synchronize_rcu(); > Ra=0 > Wa=2 > membs > rcu_read_lock() > [m01] > Rc=0 > Wc=2 > [m02] [m03] > membe > Rb=0 > Wb=2 > rcu_read_unlock() > > Looks allowed to me. If the synchronization of P1 and P2 were > interchanged, it should be forbidden: > > P0 P1 P2 P3 > Wa=2 Wb=2 rcu_read_lock() Wd=2 > memb Rc=0 Wc=2 synchronize_rcu(); > Rb=0 Rd=0 Ra=0 > rcu_read_unlock() > > Taking a look... > > P0 P1 P2 P3 > rcu_read_lock() > Rd=0 > Wa=2 Wb=2 Wd=2 > membs synchronize_rcu(); > [m01] > Rc=0 > Wc=2 > rcu_read_unlock() > [m02] Ra=0 [Forbidden?] > membe > Rb=0 Have you tried writing these as real litmus tests and running them through herd? > I believe that this ordering forbids the cycle: > > Wa=1 > membs -> [m01] -> Rc=0 -> Wc=2 -> rcu_read_unlock() -> > return from synchronize_rcu() -> Ra > > Does this make sense, or am I missing something? It's hard to tell. What you have written here isn't justified by the litmus test source code, since the position of m01 in P1's program order is undetermined. How do you justify m01 -> Rc, for example? Write it this way instead, using the relations defined in the sys_membarrier patch for linux-kernel.cat: memb ->memb-gp memb ->rcu-link Rc ->memb-rscsi Rc ->rcu-link rcu_read_unlock ->rcu-rscsi rcu_read_lock ->rcu-link synchronize_rcu ->rcu-gp synchronize_rcu ->rcu-link memb Recall that: memb-gp is the identity relation on sys_membarrier events, rcu-link includes (po? ; fre ; po), memb-rscsi is the identity relation on all events, rcu-rscsi links unlocks to their corresponding locks, and rcu-gp is the identity relation on synchronize_rcu events. These facts justify the cycle above. Leaving off the final rcu-link step, the sequence matches the definition of rcu-fence (the relations are memb-gp, memb-rscsi, rcu-rscsi, rcu-gp with rcu-links in between). Therefore the cycle is forbidden. Alan
next prev parent reply other threads:[~2018-12-12 21:32 UTC|newest] Thread overview: 38+ messages / expand[flat|nested] mbox.gz Atom feed top [not found] <8736rldyzm.fsf@oldenburg.str.redhat.com> [not found] ` <1543444466.5493.220.camel@redhat.com> [not found] ` <87y39c2dsg.fsf@oldenburg.str.redhat.com> [not found] ` <1689938209.14804.1543502662882.JavaMail.zimbra@efficios.com> [not found] ` <20181129150433.GH4170@linux.ibm.com> [not found] ` <CAHD6eXcvx1bskbp-X+vuMYoMQiCLOt0PiCZ5FT1yFsda9Ud-yA@mail.gmail.com> 2018-12-06 21:54 ` [PATCH] Linux: Implement membarrier function Paul E. McKenney 2018-12-10 16:22 ` Alan Stern 2018-12-10 16:22 ` Alan Stern 2018-12-10 18:25 ` Paul E. McKenney 2018-12-11 16:21 ` Alan Stern 2018-12-11 16:21 ` Alan Stern 2018-12-11 19:08 ` Paul E. McKenney 2018-12-11 20:09 ` Alan Stern 2018-12-11 20:09 ` Alan Stern 2018-12-11 21:22 ` Paul E. McKenney 2018-12-12 17:07 ` Paul E. McKenney 2018-12-12 18:04 ` Alan Stern 2018-12-12 18:04 ` Alan Stern 2018-12-12 19:42 ` Paul E. McKenney 2018-12-12 21:32 ` Alan Stern [this message] 2018-12-12 21:32 ` Alan Stern 2018-12-12 21:52 ` Paul E. McKenney 2018-12-12 22:12 ` Alan Stern 2018-12-12 22:12 ` Alan Stern 2018-12-12 22:49 ` Paul E. McKenney 2018-12-13 15:49 ` Alan Stern 2018-12-13 15:49 ` Alan Stern 2018-12-14 0:20 ` Paul E. McKenney 2018-12-14 2:26 ` Alan Stern 2018-12-14 2:26 ` Alan Stern 2018-12-14 5:20 ` Paul E. McKenney 2018-12-14 15:31 ` Alan Stern 2018-12-14 15:31 ` Alan Stern 2018-12-14 18:43 ` Paul E. McKenney 2018-12-14 21:39 ` Alan Stern 2018-12-14 21:39 ` Alan Stern 2018-12-16 18:51 ` Paul E. McKenney 2018-12-17 16:02 ` Alan Stern 2018-12-17 16:02 ` Alan Stern 2018-12-17 18:32 ` Paul E. McKenney 2018-12-12 22:19 ` Paul E. McKenney 2018-12-11 6:42 ` David Goldblatt 2018-12-11 14:49 ` Paul E. McKenney
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=Pine.LNX.4.44L0.1812121604430.1543-100000@iolanthe.rowland.org \ --to=stern@rowland.harvard.edu \ --cc=akiyks@gmail.com \ --cc=andrea.parri@amarulasolutions.com \ --cc=boqun.feng@gmail.com \ --cc=davidtgoldblatt@gmail.com \ --cc=dhowells@redhat.com \ --cc=dlustig@nvidia.com \ --cc=fweimer@redhat.com \ --cc=j.alglave@ucl.ac.uk \ --cc=libc-alpha@sourceware.org \ --cc=linux-arch@vger.kernel.org \ --cc=linux-kernel@vger.kernel.org \ --cc=luc.maranget@inria.fr \ --cc=mathieu.desnoyers@efficios.com \ --cc=npiggin@gmail.com \ --cc=paulmck@linux.ibm.com \ --cc=peterz@infradead.org \ --cc=triegel@redhat.com \ --cc=will.deacon@arm.com \ /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: linkBe 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.