[PATCH v2 0/2] Refactor snapshot vs nocow writers locking

[Nikolay Borisov]

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