Lincheck

Lincheck 是一个用于测试并发数据结构的 Rust 库，用于 线性化。简单来说，它检查并发数据结构的行为是否类似于更简单的顺序实现。它受到了 Kotlin 的 Lincheck 的启发，并建立在 loom（一个并发模型检查器）的基础上。

功能

• Lincheck 使用 proptest 生成随机的并发场景，并将其自动缩小到最小失败场景。
• Lincheck 在 loom 模型检查器中运行每个场景，以检查操作的所有可能的交错。
• Lincheck 提供了一个简单的 API 来定义并发数据结构和它们的顺序对应物。
• 执行跟踪的记录旨在引入尽可能少的线程间同步。

教程

在这个教程中，我们将使用以下内容

use lincheck::{ConcurrentSpec, Lincheck, SequentialSpec};
use loom::sync::atomic::{AtomicBool, Ordering};
use proptest::prelude::*;

让我们实现一个简单的并发数据结构：一对布尔标志 x 和 y，它可以被多个线程读取和写入。标志初始化为 false，可以切换到 true。

我们首先定义操作及其结果

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
enum Op {
    WriteX, // set x to true
    WriteY, // set y to true
    ReadX, // get the value of x
    ReadY, // get the value of y
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
enum Ret {
    Write, // the result of a write operation
    Read(bool), // the result of a read operation
}

我们需要为我们的操作实现 Arbitrary 特性，以便能够随机生成它们

impl Arbitrary for Op {
    type Parameters = ();
    type Strategy = BoxedStrategy<Self>;

    fn arbitrary_with(_: Self::Parameters) -> Self::Strategy {
        prop_oneof![
            Just(Op::WriteX),
            Just(Op::WriteY),
            Just(Op::ReadX),
            Just(Op::ReadY),
        ]
        .boxed()
    }
}

我们定义了与测试对应的顺序实现

#[derive(Default)]
struct TwoSlotsSequential {
    x: bool,
    y: bool,
}

我们为我们的实现实现了 SequentialSpec 特性

impl SequentialSpec for TwoSlotsSequential {
    type Op = Op;
    type Ret = Ret;

    fn exec(&mut self, op: Op) -> Ret {
        match op {
            Op::WriteX => {
                self.x = true;
                Ret::Write
            }
            Op::WriteY => {
                self.y = true;
                Ret::Write
            }
            Op::ReadX => Ret::Read(self.x),
            Op::ReadY => Ret::Read(self.y),
        }
    }
}

然后定义我们想要测试的并发实现

#[derive(Default)]
struct TwoSlotsParallel {
    x: AtomicBool,
    y: AtomicBool,
}

然后为我们的实现实现 ConcurrentSpec 特性，并设置顺序规范

impl ConcurrentSpec for TwoSlotsParallel {
    type Seq = TwoSlotsSequential;

    fn exec(&self, op: Op) -> Ret {
        match op {
            Op::WriteX => {
                self.x.store(true, Ordering::Relaxed);
                Ret::Write
            }
            Op::WriteY => {
                self.y.store(true, Ordering::Relaxed);
                Ret::Write
            }
            Op::ReadX => Ret::Read(self.x.load(Ordering::Relaxed)),
            Op::ReadY => Ret::Read(self.y.load(Ordering::Relaxed)),
        }
    }
}

我们必须能够创建我们实现的实例并对其执行操作。 exec 方法不应引发 panic。

请注意，并发规范接收了对自身的共享引用（&self），而顺序规范接收了对自身的独占引用（&mut self）。这是因为并发规范在多个线程之间共享，而顺序规范不是。

我们现在可以编写我们的测试了

#[test]
fn two_slots() {
    Lincheck {
        num_threads: 2,
        num_ops: 5,
    }.verify::<TwoSlotsParallel, TwoSlotsSequential>();
}

如果我们运行测试，我们会得到一个失败和执行跟踪

running 1 test
test two_slots ... FAILED

failures:

---- two_slots stdout ----
thread 'two_slots' panicked at 'Non-linearizable execution: 

 INIT PART:
|================|
|  MAIN THREAD   |
|================|
|                |
| WriteX : Write |
|                |
|----------------|

PARALLEL PART:
|=====================|================|
|      THREAD 0       |    THREAD 1    |
|=====================|================|
|                     |                |
|                     |----------------|
|                     |                |
| ReadY : Read(false) | WriteY : Write |
|                     |                |
|                     |----------------|
|                     |                |
|---------------------|                |
|                     |                |
| ReadY : Read(false) |                |
|                     |                |
|---------------------|----------------|

POST PART:
|================|
|  MAIN THREAD   |
|================|
|                |
| WriteX : Write |
|                |
|----------------|

限制

• Lincheck 运行器设置了它自己的 panic 钩。这与并行测试执行不兼容。要解决这个问题，您可以使用以下方式运行您的测试，带上 --test-threads=1 标志

$ cargo test -- --test-threads=1

• loom 无法模拟所有弱内存模型效果。这意味着在某些真实硬件上可能出现的某些执行可能不会被 loom 探索。这就是为什么并发数据结构应该在真实硬件上额外进行模糊测试。Lincheck 计划支持模糊测试。
• proptest 只探索所有可能场景的随机样本。这意味着可能不会探索一些失败的执行。

语义版本兼容性和 MSRV

Lincheck 遵循 semver。然而，API 尚未稳定，在第一个稳定版本发布之前可能会以破坏性的方式进行更改。目前也没有关于 MSRV（最低支持 Rust 版本）的保证。

许可证

Lincheck 在 MIT 许可证 下授权。

贡献

除非您明确声明，否则您提交给 Lincheck 的任何贡献，都应按照 MIT 许可证授权，没有任何额外的条款或条件。