Model Checking: 使用 Stateright 形式化验证 Raft Lite

2024-02-24
4 min read

你可以在这里找到源代码.

Model checking的背景

分布式系统由于消息可能丢失、延迟或重复，因此相对复杂。很难推断分布式系统的正确性。

手写证明是验证分布式系统正确性的一种常见方式。例如，Raft论文在第5.4节提供了Raft安全性属性的证明。许多证明看起来似乎是正确的，但实际上可能是错误的（我并不是说Raft论文的证明是错误的）。许多经过同行评审的论文在其证明方面被发现是错误的（例如SOCT2、SDT等）。

Model checking是一种形式化验证技术，可以用来验证分布式系统的正确性。它是一种系统性的方法，用于检查模型是否满足给定的规范。Model checking探索模型的所有可能状态。如果在任何状态下违反了属性，模型检查器将报告它，开发人员可以相应地修复错误。

然而，model checking并不是万能的。检查模型的所有可能状态是不可行的。模型的状态空间可能非常大。在实践中，我们通常会将状态空间限制在一个合理的大小。例如，我们可以指定搜索的深度为20步，或者我们可以指定最大消息数为100。即使有这些限制，model checking仍然是一个强大的工具，可以发现分布式系统中的错误。

很多公司使用TLA+来验证他们的核心算法（例如AWS、Azure等）。然而，TLA+通常用于验证高层算法。即使算法本身被验证了，算法的实现可能仍然是错误的，因为程序员可能会犯错误。

Stateright 是一个model checking的Rust库。与使用高级语言如TLA+不同，stateright使用Rust来建模系统。这意味着我们可以直接验证低级实现，而无需将高级算法转换为低级实现。

Stateright 介绍

你可以在Stateright的Github仓库 找到stateright的详细信息，也可以在这里找到一个很好的教程。如果你不想阅读它们，我将在这里简要介绍stateright。如果你已经熟悉stateright，可以跳过这一部分。

我们通常将分布式系统建模为通过网络通信的多个节点。Stateright提供了一个抽象，称为ActorModel.

指定节点逻辑

为了定义节点的逻辑，你需要实现Actor trait，即on_start、on_msg和on_timeout方法。

pub trait Actor: Sized {
    ...

    fn on_start(&self, id: Id, o: &mut Out<Self>) -> Self::State;

    fn on_msg(&self, id: Id, state: &mut Cow<'_, Self::State>, src: Id, msg: Self::Msg, o: &mut Out<Self>);

    fn on_timeout(&self, id: Id, state: &mut Cow<'_, Self::State>, _timer: &Self::Timer, o: &mut Out<Self>);

}

指定系统模型

关于分布式系统的假设可以分为以下几种类型：

  1. 网络行为（例如消息丢失）
  2. 时间行为（例如延迟）
  3. 节点行为（例如崩溃）

对于1和2，stateright提供了一个现成的网络实现：

pub enum Network<Msg>
where
    Msg: Eq + Hash,
{
    UnorderedDuplicating(HashableHashSet<Envelope<Msg>>),
    UnorderedNonDuplicating(HashableHashMap<Envelope<Msg>, usize>),
    Ordered(BTreeMap<(Id, Id), VecDeque<Msg>>),
}

As long as invariants do not check the network state, losing a message is indistinguishable from an unlimited delay.

对于3，stateright提供了一种方式来指定系统中的最多崩溃的节点数：

pub fn max_crashes(mut self, max_crashes: usize) -> Self;

指定要检查的属性

最后，你需要使用Property结构体来指定要检查的属性。

条件本质上是一个返回布尔值的闭包。如果条件为真，则属性满足。你需要提供闭包来指定要检查的属性。

pub struct Property<M: Model> {
    pub expectation: Expectation,
    pub name: &'static str,
    pub condition: fn(&M, &M::State) -> bool,
}

使用Stateright验证Raft Lite

指定节点逻辑

Raft Lite是这样设计的，算法是运行时不可知的。任何实现了Runner trait的运行时环境都可以用来运行Raft Lite算法。

Raft Lite 算法使用Runner与其他节点交互（例如发送投票请求）。我之前实现了一个RealRunner来在真实环境中运行Raft Lite算法。利用RealRunner，我使用Raft Lite构建了StorgataDB, 一个分布式的RESP兼容的KV数据库系统。

为了验证Raft Lite算法，我实现了一个CheckerRunner，它将Raft Lite算法包装到模型检查器中。

pub trait Runner {
    fn init_state(&mut self) -> NodeState;
    fn vote_request(&mut self, peer_id: u64, vote_request_args: VoteRequestArgs);
    fn log_request(&mut self, peer_id: u64, log_request_args: LogRequestArgs);
    fn forward_broadcast(&mut self, broadcast_args: BroadcastArgs);
    ...
}

实现的关键部分是step函数，它处理任何事件，并返回节点应该采取的操作。这使得算法的行为类似于状态机。

impl RaftProtocol<CheckerRunner> {
    pub(crate) fn step(&mut self, event: Event) -> Vec<StepOutput> {
        self.dispatch_event(event); // dispatch_event is the core logic of the Raft Lite algorithm
        self.runner.collect_output()
    }
}

而对于Actor trait的实现，只是在每次收到消息或触发超时时调用step函数。

impl Actor for CheckerActor {
    ...

    fn on_msg(
        &self,
        state: &mut Cow<Self::State>,
        msg: Self::Msg,
        o: &mut Out<Self>,
    ) {
        // translate the message to the event input of the step function
        let event = match msg {
            CheckerMessage::VoteRequest(vote_request_args) => Event::VoteRequest(vote_request_args),
            CheckerMessage::VoteResponse(vote_response_args) => {
                Event::VoteResponse(vote_response_args)
            }
            CheckerMessage::LogRequest(log_request_args) => Event::LogRequest(log_request_args),
            CheckerMessage::LogResponse(log_response_args) => Event::LogResponse(log_response_args),
            CheckerMessage::Broadcast(payload) => Event::Broadcast(payload),
        };
        process_event(state, event, o);
    }

    fn on_timeout(
        &self,
        _id: Id,
        state: &mut Cow<Self::State>,
        timer: &Self::Timer,
        o: &mut Out<Self>,
    ) {
        // translate the timer to the event input of the step function
        let event = match timer {
            CheckerTimer::ElectionTimeout => Event::ElectionTimeout,
            CheckerTimer::ReplicationTimeout => Event::ReplicationTimeout,
        };
        process_event(state, event, o);
    }
}

fn process_event(
    state: &mut Cow<CheckerState>,
    event: Event,
    o: &mut Out<CheckerActor>,
) {
    let state = state.to_mut();
    // call the step function to process the event, and get the actions that the node should take
    let step_output = state.raft_protocol.step(event);
    // take the actions
    for output in step_output {
        match output {
            StepOutput::DeliverMessage(payload) => {
                state.delivered_messages.push(payload);
            }
            StepOutput::VoteRequest(peer_id, vote_request_args) => {
                o.send(
                    Id::from(peer_id as usize),
                    CheckerMessage::VoteRequest(vote_request_args),
                );
            }
            ...
            StepOutput::ElectionTimerReset => {
                o.set_timer(CheckerTimer::ElectionTimeout, model_timeout());
            }
            ...
        }
    }
}

指定系统模型

  1. 网络行为：Raft Lite使用一个非重复的无序网络。这意味着消息不会重复，也不会按顺序到达。这是Raft Lite的默认行为，但可以通过传递参数来更改。
  2. 节点假设：节点是崩溃-停止的，最多可以容忍少于大多数节点的崩溃-停止。

指定要检查的属性

我指定了两个属性来检查正确性：Election Safety和State Machine Safety：

  1. Election Safety: 对于某一个给定的term，最多只有一个leader被选举（也可能没有）。
  2. State Machine Safety: 如果某个节点已经将某个日志条目交付给应用层，那么没有其他节点将会在相同的位置交付不同的日志条目。

实际上，State Machine Safety是我们唯一需要关心的属性（Raft的目标是实现一个复制状态机）。然而，为了给读者提供一个更简单的例子，我也检查了Election Safety：

.property(Expectation::Always, "Election Safety", |_, state| {
    // at most one leader can be elected in a given term
    let mut leaders_term = HashSet::new(); // `term` set if we found a leader in the term already
    for s in &state.actor_states {
        if s.raft_protocol.state.current_role == crate::raft_protocol::Role::Leader
            && !leaders_term.insert(s.raft_protocol.state.current_term)
        {
            return false;
        }
    }
    true
})

你可以看到，这个属性在Rust语言中非常容易表达。你只需要编写一个返回布尔值的闭包。

严格来说，Election Safety属性应该在所有状态的上下文中一起检查，而不是分别检查每个状态。为了简单起见，我只是分别检查了每个状态。

运行model checker

我们可以通过指定最大步数来运行model checker，以限制状态空间。

它会打印出所有违反属性的反例。此外，它还会打印出满足某些属性的例子。例如，这里我指定了两个liveness属性，模型检查器打印出了满足属性的例子。

由于没有在Raft Lite算法中找到反例，这意味着算法在指定的属性上是正确的。

$ cargo run -- -m check --depth 10
Checking. states=4, unique=4, depth=1
Checking. states=475674, unique=133824, depth=10
Checking. states=917040, unique=256771, depth=10
Done. states=924710, unique=259150, depth=10, sec=3
Discovered "Election Liveness" example Path[3]:
- Timeout(Id(0), ElectionTimeout)
- Deliver { src: Id(0), dst: Id(1), msg: VoteRequest(VoteRequestArgs { cid: 0, cterm: 1, clog_length: 0, clog_term: 0 }) }
- Deliver { src: Id(1), dst: Id(0), msg: VoteResponse(VoteResponseArgs { voter_id: 1, term: 1, granted: true }) }
Fingerprint path: 13280538127433316798/18417327358524522001/10876327409151634344/11261648250825353397
Discovered "Log Liveness" example Path[6]:
- Timeout(Id(2), ElectionTimeout)
- Deliver { src: Id(2), dst: Id(0), msg: VoteRequest(VoteRequestArgs { cid: 2, cterm: 1, clog_length: 0, clog_term: 0 }) }
- Deliver { src: Id(0), dst: Id(2), msg: VoteResponse(VoteResponseArgs { voter_id: 0, term: 1, granted: true }) }
- Deliver { src: Id(2), dst: Id(2), msg: Broadcast([50]) }
- Deliver { src: Id(2), dst: Id(0), msg: LogRequest(LogRequestArgs { leader_id: 2, term: 1, prefix_len: 0, prefix_term: 0, leader_commit: 0, suffix: [LogEntry { term: 1, payload: [50] }] }) }
- Deliver { src: Id(0), dst: Id(2), msg: LogResponse(LogResponseArgs { follower: 0, term: 1, ack: 1, success: true }) }
Fingerprint path: 13280538127433316798/5012304960666992246/2656658050571602193/12788966706765998312/12610557528799436519/6208176474896103011/7212898540444505159

另外，我们也可以在Web UI中运行模型检查器：

$ cargo run -- -m explore
Exploring state space for Raft on http://localhost:3000

你可以点击选择下一步操作，并在操作后查看状态转换。此外，你还可以找到系统的时序图。

下面是Web UI的截图，我模拟了选举过程，两个节点在不同的term中被选举为leader。

#formal verification #Raft Lite
Next Raft Lite: 一个易于理解和且经过形式验证的Raft共识算法实现

See Also

Raft Lite: 一个易于理解和且经过形式验证的Raft共识算法实现