Reading Papers 04 - Verification
# Verification
# Concurrent Software Verification
# OSDI'18 - CSPEC
mover
# Verification of Other Types of Systems
# SOSP'21 - Velidating Amazon S3 (reading unfinished)
S3 是一个 key-value storage system ,测试目标是通过 lightweight formal verification 来检测 S3 的多种错误。
选择实现一个可执行的 reference model 来描述执行每个 API call 后期望的系统状态。
- reference model 仅支持受限的 failure ,例如不支持 IO error 和 resource exhaustion 等。这简化了 reference 的实现,但是让检测变得更复杂。
可以定义 durability property 为 reference 和 implementation 之间的 key-value mapping equivalence 。然而,这样的属性对于 crash consistency 和 correctness of concurrency 来说太强了:在实际实现中,可以容许 crash 时概率性的数据丢失,也存在并发操作 in-flight 的难以描述的中间状态。可以将 durability property 解构为三个部分并分别进行验证,分解的问题有利于更专注的处理。
sequential crash-free bugs :直接使用基础的 reference 来验证。
property-based testing :基于 fuzzing 扩展了 user-provided correctness property ,并且要求测试结果是 deterministic 的。
除了基础的验证之外,还要考虑验证 implementation 是否能正确处理各种 failure ——除了 crash consistency 外,还要考虑 disk IO failure :
扩展增加
FailDiskOnce(ExtentId)
操作,使下次对指定 Extent 的 IO 失败。使用更宽松的属性,当插入 IO failure 时,允许 reference 和 implementation 在规定的范围内有不同的状态,例如
Get
操作可以声称 no data to return ,但不能返回错误的结果(?:we expect ShardStore components to detect and fail operations that involve corruption even in the presence of IO errors (e.g., by validating checksums))。
不能处理 resource exhaustion :有一些难以应对的挑战,例如测试本身可能有额外的资源占用,但是找不到合适的 test oracle 将此类情况从真正的错误中分离。
To-be-readed : 5. Checking Crash Consistency
sequential crashing executions :使用扩展的 reference 描述系统崩溃时允许的数据丢失情形,并使用更弱的属性来验证。
concurrency crash-free bugs :另外实现一个 reference ,验证执行的 linearizability 。
concurrenct crashing executions :未处理。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01