分布式系统的正确性

Introduce

一般正确性的证明标准有两个,分别是safety properties 和 liveness properites

Safety Properites

通常safety properites是指:“bad things never happen”。

举例

例如互斥操作(不管单机还是分布式)的safety properites可以是: - 最多只能有一个process or thread进入临界区 - 至少有一个process or thread有资格进入临界区

Liveness Properites

通常liveness properites是指:”good things eventually happen”。

对应现实世界的一个例子就是“正义终将来临”,至于具体什么时候,不太好说。

liveness properites的描述经常带有”eventually”字样,例如eventually consistency就是liveness properites。

举例

例如互斥操作(不管单机还是分布式)的liveness properites可以是: - 每个试图进入临界区的process or thread最终都将进入临界区 - 至少有一个process or thread有资格进入临界区

Proof

常见的证明方式暂时未做了解 ☻

Comments