From patchwork Mon Dec 10 16:22:31 2018 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Alan Stern X-Patchwork-Id: 30611 Received: (qmail 118080 invoked by alias); 10 Dec 2018 16:22:38 -0000 Mailing-List: contact libc-alpha-help@sourceware.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Subscribe: List-Archive: List-Post: List-Help: , Sender: libc-alpha-owner@sourceware.org Delivered-To: mailing list libc-alpha@sourceware.org Received: (qmail 118064 invoked by uid 89); 10 Dec 2018 16:22:36 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.1 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, KAM_ASCII_DIVIDERS, KAM_LAZY_DOMAIN_SECURITY, RCVD_IN_DNSWL_NONE autolearn=ham version=3.3.2 spammy=refer, thoughts, deficient, relation X-HELO: iolanthe.rowland.org Date: Mon, 10 Dec 2018 11:22:31 -0500 (EST) From: Alan Stern To: "Paul E. McKenney" cc: David Goldblatt , , Florian Weimer , , , , , , , , , , , , , , Subject: Re: [PATCH] Linux: Implement membarrier function In-Reply-To: <20181206215405.GL4170@linux.ibm.com> Message-ID: MIME-Version: 1.0 On Thu, 6 Dec 2018, Paul E. McKenney wrote: > Hello, David, > > I took a crack at extending LKMM to accommodate what I think would > support what you have in your paper. Please see the very end of this > email for a patch against the "dev" branch of my -rcu tree. > > This gives the expected result for the following three litmus tests, > but is probably deficient or otherwise misguided in other ways. I have > added the LKMM maintainers on CC for their amusement. ;-) > > Thoughts? Since sys_membarrier() provides a heavyweight barrier comparable to synchronize_rcu(), the memory model should treat the two in the same way. That's what this patch does. The corresponding critical section would be any region of code bounded by compiler barriers. Since the LKMM doesn't currently handle plain accesses, the effect is the same as if a compiler barrier were present between each pair of instructions. Basically, each instruction acts as its own critical section. Therefore the patch below defines memb-rscsi as the trivial identity relation. When plain accesses and compiler barriers are added to the memory model, a different definition will be needed. This gives the correct results for the three C-Goldblat-memb-* litmus tests in Paul's email. Alan PS: The patch below is meant to apply on top of the SRCU patches, which are not yet in the mainline kernel. Index: usb-4.x/tools/memory-model/linux-kernel.bell =================================================================== --- usb-4.x.orig/tools/memory-model/linux-kernel.bell +++ usb-4.x/tools/memory-model/linux-kernel.bell @@ -24,6 +24,7 @@ instructions RMW[{'once,'acquire,'releas enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || 'mb (*smp_mb*) || + 'memb (*sys_membarrier*) || 'rcu-lock (*rcu_read_lock*) || 'rcu-unlock (*rcu_read_unlock*) || 'sync-rcu (*synchronize_rcu*) || Index: usb-4.x/tools/memory-model/linux-kernel.cat =================================================================== --- usb-4.x.orig/tools/memory-model/linux-kernel.cat +++ usb-4.x/tools/memory-model/linux-kernel.cat @@ -33,7 +33,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | ([M] ; po ; [UL] ; (co | po) ; [LKW] ; fencerel(After-unlock-lock) ; [M]) -let gp = po ; [Sync-rcu | Sync-srcu] ; po? +let gp = po ; [Sync-rcu | Sync-srcu | Memb] ; po? let strong-fence = mb | gp @@ -102,8 +102,10 @@ acyclic pb as propagation *) let rcu-gp = [Sync-rcu] (* Compare with gp *) let srcu-gp = [Sync-srcu] +let memb-gp = [Memb] let rcu-rscsi = rcu-rscs^-1 let srcu-rscsi = srcu-rscs^-1 +let memb-rscsi = id (* * The synchronize_rcu() strong fence is special in that it can order not @@ -119,15 +121,19 @@ let rcu-link = po? ; hb* ; pb* ; prop ; * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same * struct srcu_struct location. *) -let rec rcu-fence = rcu-gp | srcu-gp | +let rec rcu-fence = rcu-gp | srcu-gp | memb-gp | (rcu-gp ; rcu-link ; rcu-rscsi) | ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) | + (memb-gp ; rcu-link ; memb-rscsi) | (rcu-rscsi ; rcu-link ; rcu-gp) | ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) | + (memb-rscsi ; rcu-link ; memb-gp) | (rcu-gp ; rcu-link ; rcu-fence ; rcu-link ; rcu-rscsi) | ((srcu-gp ; rcu-link ; rcu-fence ; rcu-link ; srcu-rscsi) & loc) | + (memb-gp ; rcu-link ; rcu-fence ; rcu-link ; memb-rscsi) | (rcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; rcu-gp) | ((srcu-rscsi ; rcu-link ; rcu-fence ; rcu-link ; srcu-gp) & loc) | + (memb-rscsi ; rcu-link ; rcu-fence ; rcu-link ; memb-gp) | (rcu-fence ; rcu-link ; rcu-fence) (* rb orders instructions just as pb does *) Index: usb-4.x/tools/memory-model/linux-kernel.def =================================================================== --- usb-4.x.orig/tools/memory-model/linux-kernel.def +++ usb-4.x/tools/memory-model/linux-kernel.def @@ -20,6 +20,7 @@ smp_store_mb(X,V) { __store{once}(X,V); smp_mb() { __fence{mb}; } smp_rmb() { __fence{rmb}; } smp_wmb() { __fence{wmb}; } +smp_memb() { __fence{memb}; } smp_mb__before_atomic() { __fence{before-atomic}; } smp_mb__after_atomic() { __fence{after-atomic}; } smp_mb__after_spinlock() { __fence{after-spinlock}; }