怎么理解并发编程中的 invirants？

[RedBlackTree]

看 GOPl 那本蓝皮书时，第九章讲共享变量，其中讲到 sync.Mutex 是不可重入的，已经获得 Lock 的 goroutine 重复调用 Lock，也会阻塞。然后 9.2 节（英文版 265 页）有下面这段话：

There is a good reason Go's mutexes are not re-entrant. The purpose of a mutex is to ensure that certain invariants of the shared variables are maintained at critical points during program execution. One of the invariants is "no goroutine is accessing the shared variables", but there may be additional invariants specific to the data structures that the mutex guards. When a goroutine acquires a mutex lock, it may assume that the invirants hold. While it holds the lock, it may update the shared variables so that the invariants are temporarily violated. However, when it releases the lock, it must guarantee that the order has been restored and the invariants hold once again. Although a re-entrant mutex would ensure that no other goroutines are accessing the shared variables, it cannot protect the additional invariants of those variables.

读了很多遍还是觉得难以理解，invariants 应该是某些不变的属性，不变量的意思，但是原文所说的除了“没有其他 goroutine 访问这个变量”这个 invariant 之外，mutex 保护的还有别的 invariant 。具体是指什么有前辈指点下？

[RedBlackTree]

补充一下，在 MIT6.824 分布式系统那门课，有一节课那个印度助教在讲锁时也提到过 invariants，他说的是：“mutex 不是用来保护变量的，而是用来保护 invariants 的，除了只有一个 goroutine 访问这个变量，还有其他的 invariants”，大概这个意思。我估计他也是读了这本书，跟书上的说法基本一致，但是他也没有再详细解释。

[hxndg]

invariants 值得应该是不变式，多线程环境下，
锁保护的不变式应该是两个：
1 no share thread connect
2 sequency consistent

感觉这里的意思说的应该是第二个。不过这个都是跟内存模型有关的，我只能想到这个。
你去 stackoverflow 搜一下 lock invariants 应该有相关的。

[geelaw]

Invariant 的意思和并行、并发关系不大。不变量就是说“数据的组织形式符合该数据结构的要求”，比如一个双向链表里任何非尾节点 x 都有 x.next.prev 等于 x 且任何非头节点 x 都有 x.prev.next 等于 x 。

当编辑链表时，要对多个对象的 prev 、next 分别重新赋值，几个赋值操作之间的时刻，不满足不变量。编辑操作保证：操作前符合不变量，则操作完成后还是符合。

如果链表被并行修改则可能出问题，这是因为有的时候，编辑开始的时候链表不满足它的不变量（例如另一个人也在编辑它）。于是你可以用一个 mutex 保护链表，设原先的不变量是命题 P，则新的不变量改成：当 mutex 未锁定时，P 成立。

如果 mutex 不可重入，则上述命题的简单推论是：当 mutex 刚被获取时，P 成立。
如果 mutex 可重入，则上述推论不成立，因为重入时 P 不一定成立。

那段教程就是在说，大家都希望该推论成立（从而验证正确性会更简单），所以我们设计的 mutex 不可重入。

[momocraft]

一个数据结构的（无法直接用编程语言保证的）约定
比如有两个 mutable field，一个 a 一个 b，要求 b 是 a 的阶乘（"invariant"）

更新这两个 field 的线程不可能同时写 a 和 b，但可以用一个 mutex 限制别的线程看到
只要读写都发生在线程拿到 mutex lock 时，就不会观测到不一致

[carlclone]

不是不变量，是不变式，我觉得还是不要被这些理论的东西困太久了,直接做 lab 迟早会遇到的

[lance6716]

举个例子，假设有一个不变量，a+b=10 。有个操作是 a:=b，b:=a 。

在单线程的时候，这个操作前、后都满足不变量，在操作中有短暂的不满足。

在多线程的时候，如果操作中发生了调度，就不能保证“操作后还满足不变量了”。在这个意义上，锁是在保护不变量，将其变成一个单线程场景。也就是锁的保护范围下，就是那个“短暂的不满足”，离开这个范围，维护好了不变量。

重入锁是不能保护不变量的。举个复杂一点的例子，操作是 t:=a，a:=b，b:=t 。如果在 a:=b，b:=t 之间发生调度重入的话，原始 a 的值就丢失了，也就不能满足不变量了。

[lance6716]

6 楼应该两个操作都是“t:=a，a:=b，b:=t”🤣

[RedBlackTree]

@geelaw 理解了，非常感谢👍

[ziyitony]

@geelaw 谢谢你，讲的真好！