lkml.org 
[lkml]   [2018]   [Apr]   [13]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [PATCH v2 00/13] kernel/locking: qspinlock improvements
On Wed, Apr 11, 2018 at 07:01:07PM +0100, Will Deacon wrote:
> * Spin for a bounded duration while lock is observed in the
> pending->locked transition

FWIW, I updated my model [1] to include the bounded handover loop and,
as expected, it passes the liveness check (well, assuming fairness of
other operations like fetch_or, cmpxchg etc).

[1] https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/tree/qspinlock.tla

--
Catalin

\
 
 \ /
  Last update: 2018-04-13 11:25    [W:0.116 / U:0.668 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site