技术科普｜如何形式化验证一个分布式锁？

• 往服务端发送获取锁的请求
• 在响应中检查服务端是否授予分布式锁
• 如果授权，那么正常使用共享资源，然后释放锁
  

variable
    \* Status in distributed lock service: Available, Expired, Acquired
    \* id is the client id which hold the lock, InvalidId means no one
    distLock = [status |-> "Available", id |-> InvalidId],
    request_queue = <<>>,
    responses_queue = [k \in Clients |-> <<>>],

    \* Whether client hold lock by its view
    lock_held = [k \in Clients |-> FALSE];

• distLock 就是这个分布式锁服务提供的唯一一个锁，其状态可能是 Available, Expired, Acquired. id 则是目前获取到分布式锁服务的标识符，如果没有客户端已经获取分布式锁，id 为 InvalidId.
  

• Available 代表目前没有客户端获取到分布式锁


  
• Acquired 代表目前有客户端获取到分布式锁
  
• Expired 代表某个客户端已经获取到分布式锁，经过一段时间之后锁过期


  

• request_queue 是服务端接收和处理请求的队列
• responses_queue 则是服务端给每个客户端回复响应的队列
• lock_held 则是在每个客户端视角，自己是否获取到了分布式锁的标志位

接下来就可以描述这个系统的 Invariant 了：

TypeInvariant ==
  \ distLock \in {[status |-> "Available", id |-> InvalidId], [status |-> "Expired", id |-> InvalidId]}
                  \union
                  {[status |-> "Acquired", id |-> c] : c \in Clients}
  \ \A reqEntry \in SeqToSet(request_queue) : reqEntry.type \in {"acquire", "release"} \ reqEntry.id \in Clients
  \ \A c \in Clients : \A respEntry \in SeqToSet(responses_queue[c]) : respEntry \in {"granted", "rejected"}
  \ lock_held \in [Clients -> {TRUE, FALSE}]

AtMostOneClientHoldLock ==
  \ ~\E c1, c2 \in Clients :
    \ c1 = c2
    \ lock_held[c1] = TRUE
    \ lock_held[c2] = TRUE

• TypeInvariant 是为了检查下面行为逻辑中修改的变量都是合法值。
  分布式锁 distLock 的合法状态为：

• Available 和 Expired ，代表此时没有客户端获取锁，即 id 为 InvalidId.
• Acquired，代表已有客户端获取了分布式锁，id 为对应客户端标识符。
  

• AtMostOneClientHoldLock 则是为了检查任意时刻不会出现两个客户端同时认为自己获取了分布式锁。（也就是safety property）

（二）客户端和服务端行为

客户端：

fair process (client \in Clients)
{
C1:
    await lock_held[self] = FALSE;
    request_queue := Append(request_queue, [type |-> "acquire", id |-> self]);
C2:
    await Len(responses_queue[self]) > 0;
    if (Head(responses_queue[self]) = "granted") {
        lock_held[self] := TRUE;
    };
    responses_queue[self] := Tail(responses_queue[self]);
C3:
    await lock_held[self] = TRUE;
    \* use shared resources
    lock_held[self] := FALSE;
    request_queue := Append(request_queue, [type |-> "release", id |-> self]);
}

服务端

然后是服务端，直至所有客户端都完成，一直执行如下两个操作中的一个：

• 从请求队列中获取一个消息，然后开始处理（对应标签 S1, S2, S3）
• 将分布式锁设置为 Expired 过期状态（对应标签 S4）

fair process (service = Service)
variable req = <<>>, resp = <<>>;
{
SERVICE_MAIN:
    while (~ \A cli \in Clients : pc[cli] = "Done") {
        either {
            await Len(request_queue) > 0;
        S1:
            req := Head(request_queue);
            request_queue := Tail(request_queue);
        S2:
            if (req.type = "acquire") {
                if (distLock.status \in {"Available", "Expired"}) {
                    distLock := [status |-> "Acquired", id |-> req.id];
                    resp := "granted";
                } else {
                    resp := "rejected";
                };
            S3:
                responses_queue[req.id] := Append(responses_queue[req.id], resp);
            } elseif (req.type = "release") {
                if (distLock.status = "Acquired" /\ distLock.id = req.id) {
                    distLock := [status |-> "Available", id |-> InvalidId];
                }
            }
        } or {
            await distLock.status = "Acquired";
        S4:
            distLock := [status |-> "Expired", id |-> InvalidId];
        }
    }
}

标红的部分代表上一个状态和当前状态的 diff，省略掉一些不重要的状态

• (State 1)初始化，所有客户端都没有获取分布式锁
• (State 2)客户端 C1 发送了获取分布式锁的请求
• (State 5)服务端检查分布式锁状态为 Available，因此将分布式锁授予给 C1
• (State 6)服务端将授予分布式锁的回复加入到客户端 C1 的响应队列中。由于某些特殊情况（比如网络延迟，GC 等），C1 此时还未说到对应回复。
• (State 8)服务端此时认为分布式分布式锁已经过期，因此将分布式锁设置为过期状态
• (State 9)客户端 C1 此时收到了回复，认为自己持有了分布式锁
• (State 10)客户端 C2 发送了获取分布式锁的请求
• (State 13)服务端检查分布式锁状态为 Expired，因此将分布式锁授予给 C2
• (State 14)服务端回复客户端 C2
• (State 15)客户端 C2 收到回复，认为自己持有了分布式锁

因此客户端 C1 和 C2 都认为自己持有了分布式锁，违背了同一时间只有一个客户端持有分布式锁的 Invariant，二者可能同时操作共享资源。

其实仔细观察这个 error trace，和上一篇中的 Martin Kleppmann 举的例子几乎如出一辙，都是客户端 1 在获取分布式锁之后，由于各种问题（error trace 中是客户端 1 没有收到回复，而在原始的例子中是客户端 1 出现了 GC），导致服务端认为分布式锁过期，进而将分布式锁授予给了另一个客户端。

（四）Fencing Token

我们来验证一下 Martin Kleppmann 说的 Fencing Token 能否解决上面出现的问题。

首先我们需要引入 token，用 history 保存使用共享资源时的 token，将其加入到系统的变量中。

variable
    \* Status in distributed lock service: Available, Expired, Acquired
    \* id is the client id which hold the lock, InvalidId means no one
    distLock = [status |-> "Available", id |-> InvalidId],
    request_queue = <<>>,
    responses_queue = [k \in Clients |-> <<>>],

    \* Whether client hold lock by its view
    lock_held = [k \in Clients |-> FALSE],

    \* The token usage history in shared resource's view
    history = <<>>;

在服务端会记录 token，每次授予分布式锁时，会自增这个 token，并且会将 token 告知客户端，以便客户端携带这个 token 操作共享资源。

fair process (service = Service)
variable req = <<>>, resp = <<>>, service_token = 1;
{
SERVICE_MAIN:
    while (~ \A cli \in Clients : pc[cli] = "Done") {
        either {
            await Len(request_queue) > 0;
        S1:
            req := Head(request_queue);
            request_queue := Tail(request_queue);
        S2:
            if (req.type = "acquire") {
                if (distLock.status \in {"Available", "Expired"}) {
                    distLock := [status |-> "Acquired", id |-> req.id];
                    resp := [status |-> "granted", token |-> service_token];
                    service_token := service_token + 1;
                } else {
                    resp := [status |-> "rejected"];
                };
            S3:
                responses_queue[req.id] := Append(responses_queue[req.id], resp);
            } elseif (req.type = "release") {
                if (distLock.status = "Acquired" /\ distLock.id = req.id) {
                    distLock := [status |-> "Available", id |-> InvalidId];
                }
            }
        } or {
            await distLock.status = "Acquired";
        S4:
            distLock := [status |-> "Expired", id |-> InvalidId];
        }
    }
}

在客户端则保存服务端发送的 token，当且仅当目前的 token 比共享资源已经见过的最大 token 还要大时，才能使用共享资源。（也就是共享资源能够拒绝掉过期请求的能力）

fair process (client \in Clients)
\* 0 means invalid
variable token = 0;
{
C1:
    await lock_held[self] = FALSE;
    request_queue := Append(request_queue, [type |-> "acquire", id |-> self]);
C2:
    await Len(responses_queue[self]) > 0;
    if (Head(responses_queue[self]).status = "granted") {
        lock_held[self] := TRUE;
        token := Head(responses_queue[self]).token;
    };
    responses_queue[self] := Tail(responses_queue[self]);
C3:
    if (token = 0) {
        \* Lock aquired, use the share resource with given token
        if (Len(history) = 0 \/ history[Len(history)] < token) {
            history := Append(history, token);
        }
    };
C4:
    await lock_held[self] = TRUE;
    lock_held[self] := FALSE;
    request_queue := Append(request_queue, [type |-> "release", id |-> self]);
}

TokenIsMonotonical ==
  ~\E i, j \in DOMAIN history :
    \ i < j
    /\ history[i] >= history[j]

二、结论

我们在这一篇中用 TLA+ 对分布式锁服务进行了建模，成功找到了因为 NPC 问题导致两个客户端同时认为自己获取到了分布式锁的反例，也基于 FencingToken 对我们的模型进行了修正，事实也证明如果共享资源如果具有拒绝掉过期资源的能力，分布式锁的 safety 就能得到保证。

整个分布式锁系列相关的文章也就到此结束，再一起回顾往期两篇文章吧～

技术科普｜深入理解分布式锁的原理与实现 part 1

技术科普｜Redis 作者与 DDIA 作者激辩：Redlock 到底安不安全？

Reference

[1]How to do distributed locking：https://martin.kleppmann.com/2016/02/08/how-to-do-distributed-locking.html