From: Andrea Parri <andrea.parri@amarulasolutions.com> To: Catalin Marinas <catalin.marinas@arm.com> Cc: Will Deacon <will.deacon@arm.com>, peterz@infradead.org, boqun.feng@gmail.com, linux-kernel@vger.kernel.org, paulmck@linux.vnet.ibm.com, mingo@kernel.org, linux-arm-kernel@lists.infradead.org Subject: Re: [PATCH 00/10] kernel/locking: qspinlock improvements Date: Wed, 11 Apr 2018 17:39:01 +0200 [thread overview] Message-ID: <20180411153901.GA14205@andrea> (raw) In-Reply-To: <20180411102003.rjfrcmc4fjukehst@armageddon.cambridge.arm.com> On Wed, Apr 11, 2018 at 11:20:04AM +0100, Catalin Marinas wrote: > On Fri, Apr 06, 2018 at 03:22:49PM +0200, Andrea Parri wrote: > > On Thu, Apr 05, 2018 at 05:58:57PM +0100, Will Deacon wrote: > > > I've been kicking the tyres further on qspinlock and with this set of patches > > > I'm happy with the performance and fairness properties. In particular, the > > > locking algorithm now guarantees forward progress whereas the implementation > > > in mainline can starve threads indefinitely in cmpxchg loops. > > > > > > Catalin has also implemented a model of this using TLA to prove that the > > > lock is fair, although this doesn't take the memory model into account: > > > > > > https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/commit/ > > > > Nice! I'll dig into this formalization, but my guess is that our model > > (and axiomatic models "a-la-herd", in general) are not well-suited when > > it comes to study properties such as fairness, liveness... > > Maybe someone with a background in formal methods could give a better > answer. How TLA+ works is closer to rmem [1] (operational model, > exhaustive memoised state search) than herd. Liveness verification > requires checking that, under certain fairness properties, some state is > eventually reached. IOW, it tries to show that either all state change > graphs lead to (go through) such state or that there are cycles in the > graph and the state is never reached. I don't know whether herd could be > modified to check liveness. I'm not sure it can handle infinite loops > either (the above model checks an infinite lock/unlock loop on each > CPU and that's easier to implement in a tool with memoised states). > > The TLA+ model above assumes sequential consistency, so no memory > ordering taken into account. One could build an operational model in > TLA+ that's equivalent to the axiomatic one (e.g. following the Flat > model equivalence as in [2]), however, liveness checking (at least with > TLA+) is orders of magnitude slower than safety. Any small variation has > an exponential impact on the state space, so likely to be impractical. > For specific parts of the algorithm, you may be able to use a poor man's > ordering by e.g. writing two accesses in two different orders so the > model checks both combinations. > > There are papers (e.g. [3]) on how to convert liveness checking to > safety checking but I haven't dug further. I think it's easier/faster if > you do liveness checking with a simplified model and separately check > the safety with respect to memory ordering on tools like herd. Indeed. A fundamental problem, AFAICT, is to formalize that concept of '[it] will _eventually_ happen'. Consider a simple example: { x = 0} P0 | P1 | x = 1 | while (!x) | ; herd 'knows' that: - on the 1st iteration of the 'while' loop, the load from x can return the value 0 or 1 (only); - on the 2nd iteration of the 'while' loop, the load from x can return the value 0 or 1; - [ ... and 'so on'! ] but this is pretty much all herd knows about this snippet by now ... ;) Thanks, Andrea > > [1] http://www.cl.cam.ac.uk/~sf502/regressions/rmem/ > [2] http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf > [3] https://www.sciencedirect.com/science/article/pii/S1571066104804109 > > -- > Catalin
WARNING: multiple messages have this Message-ID (diff)
From: andrea.parri@amarulasolutions.com (Andrea Parri) To: linux-arm-kernel@lists.infradead.org Subject: [PATCH 00/10] kernel/locking: qspinlock improvements Date: Wed, 11 Apr 2018 17:39:01 +0200 [thread overview] Message-ID: <20180411153901.GA14205@andrea> (raw) In-Reply-To: <20180411102003.rjfrcmc4fjukehst@armageddon.cambridge.arm.com> On Wed, Apr 11, 2018 at 11:20:04AM +0100, Catalin Marinas wrote: > On Fri, Apr 06, 2018 at 03:22:49PM +0200, Andrea Parri wrote: > > On Thu, Apr 05, 2018 at 05:58:57PM +0100, Will Deacon wrote: > > > I've been kicking the tyres further on qspinlock and with this set of patches > > > I'm happy with the performance and fairness properties. In particular, the > > > locking algorithm now guarantees forward progress whereas the implementation > > > in mainline can starve threads indefinitely in cmpxchg loops. > > > > > > Catalin has also implemented a model of this using TLA to prove that the > > > lock is fair, although this doesn't take the memory model into account: > > > > > > https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/commit/ > > > > Nice! I'll dig into this formalization, but my guess is that our model > > (and axiomatic models "a-la-herd", in general) are not well-suited when > > it comes to study properties such as fairness, liveness... > > Maybe someone with a background in formal methods could give a better > answer. How TLA+ works is closer to rmem [1] (operational model, > exhaustive memoised state search) than herd. Liveness verification > requires checking that, under certain fairness properties, some state is > eventually reached. IOW, it tries to show that either all state change > graphs lead to (go through) such state or that there are cycles in the > graph and the state is never reached. I don't know whether herd could be > modified to check liveness. I'm not sure it can handle infinite loops > either (the above model checks an infinite lock/unlock loop on each > CPU and that's easier to implement in a tool with memoised states). > > The TLA+ model above assumes sequential consistency, so no memory > ordering taken into account. One could build an operational model in > TLA+ that's equivalent to the axiomatic one (e.g. following the Flat > model equivalence as in [2]), however, liveness checking (at least with > TLA+) is orders of magnitude slower than safety. Any small variation has > an exponential impact on the state space, so likely to be impractical. > For specific parts of the algorithm, you may be able to use a poor man's > ordering by e.g. writing two accesses in two different orders so the > model checks both combinations. > > There are papers (e.g. [3]) on how to convert liveness checking to > safety checking but I haven't dug further. I think it's easier/faster if > you do liveness checking with a simplified model and separately check > the safety with respect to memory ordering on tools like herd. Indeed. A fundamental problem, AFAICT, is to formalize that concept of '[it] will _eventually_ happen'. Consider a simple example: { x = 0} P0 | P1 | x = 1 | while (!x) | ; herd 'knows' that: - on the 1st iteration of the 'while' loop, the load from x can return the value 0 or 1 (only); - on the 2nd iteration of the 'while' loop, the load from x can return the value 0 or 1; - [ ... and 'so on'! ] but this is pretty much all herd knows about this snippet by now ... ;) Thanks, Andrea > > [1] http://www.cl.cam.ac.uk/~sf502/regressions/rmem/ > [2] http://www.cl.cam.ac.uk/~pes20/armv8-mca/armv8-mca-draft.pdf > [3] https://www.sciencedirect.com/science/article/pii/S1571066104804109 > > -- > Catalin
next prev parent reply other threads:[~2018-04-11 15:39 UTC|newest] Thread overview: 94+ messages / expand[flat|nested] mbox.gz Atom feed top 2018-04-05 16:58 [PATCH 00/10] kernel/locking: qspinlock improvements Will Deacon 2018-04-05 16:58 ` Will Deacon 2018-04-05 16:58 ` [PATCH 01/10] locking/qspinlock: Don't spin on pending->locked transition in slowpath Will Deacon 2018-04-05 16:58 ` Will Deacon 2018-04-05 16:58 ` [PATCH 02/10] locking/qspinlock: Remove unbounded cmpxchg loop from locking slowpath Will Deacon 2018-04-05 16:58 ` Will Deacon 2018-04-05 17:07 ` Peter Zijlstra 2018-04-05 17:07 ` Peter Zijlstra 2018-04-06 15:08 ` Will Deacon 2018-04-06 15:08 ` Will Deacon 2018-04-05 17:13 ` Peter Zijlstra 2018-04-05 17:13 ` Peter Zijlstra 2018-04-05 21:16 ` Waiman Long 2018-04-05 21:16 ` Waiman Long 2018-04-06 15:08 ` Will Deacon 2018-04-06 15:08 ` Will Deacon 2018-04-06 20:50 ` Waiman Long 2018-04-06 20:50 ` Waiman Long 2018-04-06 21:09 ` Paul E. McKenney 2018-04-06 21:09 ` Paul E. McKenney 2018-04-07 8:47 ` Peter Zijlstra 2018-04-07 8:47 ` Peter Zijlstra 2018-04-07 23:37 ` Paul E. McKenney 2018-04-07 23:37 ` Paul E. McKenney 2018-04-09 10:58 ` Will Deacon 2018-04-09 10:58 ` Will Deacon 2018-04-07 9:07 ` Peter Zijlstra 2018-04-07 9:07 ` Peter Zijlstra 2018-04-09 10:58 ` Will Deacon 2018-04-09 10:58 ` Will Deacon 2018-04-09 14:54 ` Will Deacon 2018-04-09 14:54 ` Will Deacon 2018-04-09 15:54 ` Peter Zijlstra 2018-04-09 15:54 ` Peter Zijlstra 2018-04-09 17:19 ` Will Deacon 2018-04-09 17:19 ` Will Deacon 2018-04-10 9:35 ` Peter Zijlstra 2018-04-10 9:35 ` Peter Zijlstra 2018-09-20 16:08 ` Peter Zijlstra 2018-09-20 16:08 ` Peter Zijlstra 2018-09-20 16:22 ` Peter Zijlstra 2018-09-20 16:22 ` Peter Zijlstra 2018-04-09 19:33 ` Waiman Long 2018-04-09 19:33 ` Waiman Long 2018-04-09 17:55 ` Waiman Long 2018-04-09 17:55 ` Waiman Long 2018-04-10 13:49 ` Sasha Levin 2018-04-10 13:49 ` Sasha Levin 2018-04-05 16:59 ` [PATCH 03/10] locking/qspinlock: Kill cmpxchg loop when claiming lock from head of queue Will Deacon 2018-04-05 16:59 ` Will Deacon 2018-04-05 17:19 ` Peter Zijlstra 2018-04-05 17:19 ` Peter Zijlstra 2018-04-06 10:54 ` Will Deacon 2018-04-06 10:54 ` Will Deacon 2018-04-05 16:59 ` [PATCH 04/10] locking/qspinlock: Use atomic_cond_read_acquire Will Deacon 2018-04-05 16:59 ` Will Deacon 2018-04-05 16:59 ` [PATCH 05/10] locking/mcs: Use smp_cond_load_acquire() in mcs spin loop Will Deacon 2018-04-05 16:59 ` Will Deacon 2018-04-05 16:59 ` [PATCH 06/10] barriers: Introduce smp_cond_load_relaxed and atomic_cond_read_relaxed Will Deacon 2018-04-05 16:59 ` Will Deacon 2018-04-05 17:22 ` Peter Zijlstra 2018-04-05 17:22 ` Peter Zijlstra 2018-04-06 10:55 ` Will Deacon 2018-04-06 10:55 ` Will Deacon 2018-04-05 16:59 ` [PATCH 07/10] locking/qspinlock: Use smp_cond_load_relaxed to wait for next node Will Deacon 2018-04-05 16:59 ` Will Deacon 2018-04-05 16:59 ` [PATCH 08/10] locking/qspinlock: Merge struct __qspinlock into struct qspinlock Will Deacon 2018-04-05 16:59 ` Will Deacon 2018-04-07 5:23 ` Boqun Feng 2018-04-07 5:23 ` Boqun Feng 2018-04-05 16:59 ` [PATCH 09/10] locking/qspinlock: Make queued_spin_unlock use smp_store_release Will Deacon 2018-04-05 16:59 ` Will Deacon 2018-04-05 16:59 ` [PATCH 10/10] locking/qspinlock: Elide back-to-back RELEASE operations with smp_wmb() Will Deacon 2018-04-05 16:59 ` Will Deacon 2018-04-05 17:28 ` Peter Zijlstra 2018-04-05 17:28 ` Peter Zijlstra 2018-04-06 11:34 ` Will Deacon 2018-04-06 11:34 ` Will Deacon 2018-04-06 13:05 ` Andrea Parri 2018-04-06 13:05 ` Andrea Parri 2018-04-06 15:27 ` Will Deacon 2018-04-06 15:27 ` Will Deacon 2018-04-06 15:49 ` Andrea Parri 2018-04-06 15:49 ` Andrea Parri 2018-04-07 5:47 ` Boqun Feng 2018-04-07 5:47 ` Boqun Feng 2018-04-09 10:47 ` Will Deacon 2018-04-09 10:47 ` Will Deacon 2018-04-06 13:22 ` [PATCH 00/10] kernel/locking: qspinlock improvements Andrea Parri 2018-04-06 13:22 ` Andrea Parri 2018-04-11 10:20 ` Catalin Marinas 2018-04-11 10:20 ` Catalin Marinas 2018-04-11 15:39 ` Andrea Parri [this message] 2018-04-11 15:39 ` Andrea Parri
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=20180411153901.GA14205@andrea \ --to=andrea.parri@amarulasolutions.com \ --cc=boqun.feng@gmail.com \ --cc=catalin.marinas@arm.com \ --cc=linux-arm-kernel@lists.infradead.org \ --cc=linux-kernel@vger.kernel.org \ --cc=mingo@kernel.org \ --cc=paulmck@linux.vnet.ibm.com \ --cc=peterz@infradead.org \ --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.