On Fri, 23 Nov 2018 11:31:31 +0000 Catalin Marinas <catalin.marinas@xxxxxxx> wrote: > With qwrlocks, the readers will normally block if there is a pending > writer (to avoid starving the writer), unless in_interrupt() when the > readers are allowed to starve a pending writer. > > TLA+/PlusCal model here: ;) > > https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/tree/qrwlock.tla > And the code appears to confirm it too: void queued_read_lock_slowpath(struct qrwlock *lock) { /* * Readers come here when they cannot get the lock without waiting */ if (unlikely(in_interrupt())) { /* * Readers in interrupt context will get the lock immediately * if the writer is just waiting (not holding the lock yet), * so spin with ACQUIRE semantics until the lock is available * without waiting in the queue. */ atomic_cond_read_acquire(&lock->cnts, !(VAL & _QW_LOCKED)); return; } atomic_sub(_QR_BIAS, &lock->cnts); /* * Put the reader into the wait queue */ arch_spin_lock(&lock->wait_lock); atomic_add(_QR_BIAS, &lock->cnts); -- Steve
