knossos.model
和jepsen.checker
::f :read
或:f :cas
的含义,就其而言,他们可以是任意值。然而,当它基于(case (:f op) :read ...)
进行控制流转时,我们的client知道如何解释这些操作。现在,我们需要一个能够理解这些相同操作的系统模型。Knossos已经为我们定义好了模型数据类型,它接受一个模型或者操作作为输入进行运算,并返回该操作产生的新模型。knossos.model内部代码如下:Model
接口,它的step
函数接收当前寄存器r
和操作op
作为参数。当我们需要写入新值时,只需要简单返回一个已经赋值的CASRegister
。为了对两个值进行cas,我们在操作中将当前值和新值分开,如果当前值和新值相匹配,则构建一个带有新值的寄存器。如果它们不匹配,则返回带有inconsistent
的特定的模型类型,它表明上一操作不能应用于寄存器。读操作也是类似,除了我们始终允许读取到nil
这一点。这允许我们有从未返回过的读操作历史。:checker
,同时需要提供一个:model
来指明系统应该如何运行。
checker/linearizable
使用Knossos线性checker来验证每一个操作是否自动处于调用和返回之间的位。线性checker需要一个模型并指明一个特定的算法,然后在选项中将map传递给该算法。1
,可以确信,checker中的最终值也是1
,该历史记录是线性一致的。gnuplot
,Jepsen可以帮我们生成吞吐量和延迟图。让我们使用checker/compose
来进行线性分析并生成性能图吧!jepsen.checker.timeline
命名空间吧!