Board logo

标题: 读写自旋锁详解,第 1 部分(2) [打印本页]

作者: look_w    时间: 2018-4-23 15:29     标题: 读写自旋锁详解,第 1 部分(2)

读写自旋锁的形式化定义是一个 6 元组(Q,O,T,S,q0,qf),其中:
我们先画出与定义等价的状态图,然后描述 6 元组具体是什么。
图 1. 读写自旋锁的状态图结合状态图,我们描述读写自旋锁的工作原理:
1. 我们规定在时刻 0 执行全局唯一一次的“初始化”操作,将锁置为初始状态“未被持有”,图中即为那条没有起点、标注“初始化“操作的有向边。如果决定停止使用读写自旋锁,则执行全局唯一一次的“析构”操作,将锁置为结束状态“停止”。
2. 读写自旋锁可以被看成一个从初始状态“未被持有”开始依次“吃”操作、不断转换状态的 串行机器。令 W(t) 为时间段 (0, t] 内已提交但未执行的操作构成的集合,W(t) 是 所有提交的操作集合 A(t) 的子集。在时刻 t,如果锁准备执行新的操作,假设当前处于状态 q,W(t) 不是空集且存在状态 q 允许的操作,那么读写自旋锁使用选择函数 S 在 W(t) 集合中选出一个来执行,执行完成后将自身状态置为 q ’ = T(q, o)。
3. 我们称序列 < qI1,oI1,qI2,oI2,…,oIn,qI(n+1)> 是读写自旋锁在 t 时刻的执行序列,如果:
3.  假如执行序列的最后一个状态 qI(n+1)不是结束状态 qf,且在时刻 t0,W(t0) 为空或者 qI(n+1)不允许 W(t0) 中的任一个操作 o,我们称读写自旋锁在时刻 t0处于潜在死锁状态。这并不表明读写自旋锁真的死锁了,因为随后线程可以提交新的操作,使其继续工作下去。例如 qI(n+1)是“写者持有”状态,而 W(t0) 中全是“读者申请”的操作。但是我们知道锁的持有者一会定在 t0之后的有限时间内提交“写者释放”操作,届时读写自旋锁可以选择执行它,将状态置为“未被持有”,而现存的“读者申请”的操作随后也可被执行了。
4. 如果存在 t0> 0,且对于任意 t >= t0,读写自旋锁在时刻 t 都处于潜在死锁状态,我们称读写自旋锁从时刻 t0开始“死锁”。
以下是状态图正确性的证明概要:
1. 互斥。从图可知,状态“读者持有”只能转换到自身和“未被持有”,不能转换到“写者持有”,同时状态“写者持有”只能转换到“未被持有”,不能转换到“读者持有”,所以锁一旦被持有,另一种角色的线程只有等到“未被持有”的状态才有机会获得锁,因此读者和写者不可能同时获得锁。状态“写者持有”不允许“写者申请”操作,故而任何时刻只有至多一个写者获得锁。
2. 读者并发。状态“读者持有”允许“读者申请”操作,因此可以有多个读者同时持有锁。
3. 无死锁。证明依赖第一章中关于线程执行的 3 个假设。反证法,假设对任意 t >= t0,锁在时刻 t 都处于潜在死锁状态。令 q 为 t0时刻锁的状态,分 3 种情况讨论:
从线程 A 申请锁的角度来看,由状态图知对于任意时刻 t0,不论锁在 t0的状态如何,总存在 t1> t0,锁在时刻 t1必定处于“未被持有”的状态,那么在时刻 t1允许锁申请操作,不是 A 就是别的线程获得锁。如果 A 永远不能获得锁,说明锁一旦处于“未被持有”的状态,就选择了别的线程提交的锁申请操作,那么某个或某些线程必然无限次地获得锁。
上面提到读写自旋锁有一种选择未执行的操作的能力,即选择函数 S,正是这个函数的差异,导致锁展现不同属性:
1. 读者优先。在任意时刻 t,如果锁处于状态“读者持有”,S 以大于 0 的概率选择一个尚未执行的“读者申请”操作。这意味着:首先,即使有先提交但尚未执行的“写者申请”操作,“读者申请”操作可以被优先执行;其次,没有刻意规定如何选“读者申请”操作,因此多个“读者申请”操作间的执行顺序是不确定的;最后,不排除连续选择“读者释放”操作,使得锁状态迅速变为“未被持有”,只不过这种几率很小。
2. 写者优先。在任意时刻 t,如果 o1是尚未执行的“写者申请”操作,o2是尚未执行的“读者申请”或“写者申请”操作,且 o1在 o2之前提交,那么 S 保证一定在 o2之前选择 o1。
3. 无饥饿。如果线程提交了操作 o,那么 S 必定在有限时间内选择 o。即存在时刻 t,读写自旋锁在 t 的执行序列 < qI1,oI1,qI2,oI2,…,oIn,qI(n+1)> 满足 o = oIn。狭义上, o 限定为“读者申请”或“写者申请”操作。
4. 公平。如果操作 o1在 o2之前提交,那么 S 保证一定在在 o2之前选择执行 o1。狭义上,o1和 o2限定为“读者申请”或“写者申请”操作。




欢迎光临 电子技术论坛_中国专业的电子工程师学习交流社区-中电网技术论坛 (http://bbs.eccn.com/) Powered by Discuz! 7.0.0