Hello,
Here is the second version of the DRW lock for btrfs. Main changes from v1:
* Fixed all checkpatch warnings (Andrea Parri)
* Properly call write_unlock in btrfs_drw_try_write_lock (Filipe Manana)
* Comment fix.
* Stress tested it via locktorture. Survived for 8 straight days on a 4 socket
48 thread machine.
I have also produced a PlusCal specification which I'd be happy to discuss with
people since I'm new to formal specification and I seem it doesn't have the
right fidelity:
---- MODULE specs ----
EXTENDS Integers, Sequences, TLC
CONSTANT NumLockers
ASSUME NumLockers > 0
(*--algorithm DRW
variables
lock_state = "idle",
states = {"idle", "write_locked", "read_locked", "read_waiting",
"write_waiting"},
threads = [thread \in 1..NumLockers |-> "idle" ] \* everyone is in idle
state at first, this generates a tuple
define
INV_SingleLockerType == \/ lock_state = "write_locked" /\ ~\E thread \in
1..Len(threads): threads[thread] = "read_locked"
\/ lock_state = "read_locked" /\ ~\E thread \in
1..Len(threads): threads[thread] = "write_locked"
\/ lock_state = "idle" /\ \A thread \in
1..Len(threads): threads[thread] = "idle"
end define;
macro ReadLock(tid) begin
if lock_state = "idle" \/ lock_state = "read_locked" then
lock_state := "read_locked";
threads[tid] := "read_locked";
else
assert lock_state = "write_locked";
threads[tid] := "write_waiting"; \* waiting for writers to finish
await lock_state = "" \/ lock_state = "read_locked";
end if;
end macro;
macro WriteLock(tid) begin
if lock_state = "idle" \/ lock_state = "write_locked" then
lock_state := "write_locked";
threads[tid] := "write_locked";
else
assert lock_state = "read_locked";
threads[tid] := "reader_waiting"; \* waiting for readers to finish
await lock_state = "idle" \/ lock_state = "write_locked";
end if;
end macro;
macro ReadUnlock(tid) begin
if threads[tid] = "read_locked" then
threads[tid] := "idle";
if ~\E thread \in 1..Len(threads): threads[thread] = "read_locked" then
lock_state := "idle"; \* we were the last read holder, everyone
else should be waiting, unlock the lock
end if;
end if;
end macro;
macro WriteUnlock(tid) begin
if threads[tid] = "write_locked" then
threads[tid] := "idle";
if ~\E thread \in 1..Len(threads): threads[thread] = "write_locked" then
lock_state := "idle"; \* we were the last write holder, everyone
else should be waiting, unlock the lock
end if;
end if;
end macro;
process lock \in 1..NumLockers
begin LOCKER:
while TRUE do
either
ReadLock(self);
or
WriteLock(self);
or
ReadUnlock(self);
or
WriteUnlock(self);
end either;
end while;
end process;
end algorithm; *)
====
Nikolay Borisov (2):
btrfs: Implement DRW lock
btrfs: convert snapshot/nocow exlcusion to drw lock
fs/btrfs/ctree.h | 10 ++---
fs/btrfs/disk-io.c | 46 ++++++----------------
fs/btrfs/extent-tree.c | 35 -----------------
fs/btrfs/file.c | 11 +++---
fs/btrfs/inode.c | 8 ++--
fs/btrfs/ioctl.c | 10 ++---
fs/btrfs/locking.c | 88 ++++++++++++++++++++++++++++++++++++++++++
fs/btrfs/locking.h | 20 ++++++++++
8 files changed, 134 insertions(+), 94 deletions(-)
--
2.17.1
