读写自旋锁的形式化定义是一个 6 元组（Q，O，T，S，q0，qf），其中：
- Q = {q0，q1，…，qn}，是一个有限集合，称为状态集。状态 qi描述了读写自旋锁在某时刻 t0所处于的一种真实状况。
- O = {o0，o1，…，om}，是一个有限集合，称为操作种类集。
- T：Q x O -> Q 是转移函数。T 是一个偏函数（Partial Function），即 T 的定义域是 Q x O 的子集。如果 T 在 (q, o) 有定义，即存在 q ’ = T(q, o)，我们称状态 q 允许操作 o，在状态 q 可以执行操作 o，成功完成后读写自旋锁转换到状态 q ’；反之，如果 T 在 (q, o) 没有定义，我们称状态 q 不允许操作 o，说明在状态 q 不能执行操作 o，例如在锁被写者持有时，不能选择 “读者申请获取锁”的操作。
- S 是选择函数，从已提交但未执行的操作实例集合中选择一个让读写自旋锁执行，后文详细讨论。由于任意时刻活跃线程的总数目是有限的，这个集合必然是有限集，因此我们认为 S 的每一次选择能在有限步骤内结束。
- q0是初始状态。
- qf是结束状态，对于任一种操作 o，T 在 (qf, o) 无定义。也就是说到达该状态后，读写自旋锁不再执行任何操作。
我们先画出与定义等价的状态图，然后描述 6 元组具体是什么。
图 1. 读写自旋锁的状态图 - 状态图中的每个圆圈代表一个状态。状态集合 Q 至少应该有 3 个状态：“未被持有”，“读者持有”和“写者持有”。因为可能执行“析构”操作，所以还需要增加一个结束状态“停止”。除此之外不需要新的状态。
- 有向边上的文字代表了一种操作。读写自旋锁需要 6 种操作： “初始化”，“析构”，“读者申请”， “读者释放”， “写者申请”和“写者释放”。操作后面括号内的文字，例如“最后持有者”，只是辅助理解，并不表示一种新的操作。
- 有向边及其上的操作定义了转移函数。如果一条有向边从状态 q 射向 q ’，且标注的操作是 o，那么表明状态 q 允许 o，且 q ’ = T(q, o)。
- 初始状态是“未被持有”。
- 结束状态是“停止”，双圆圈表示，该状态不射出任何有向边，表明此后锁停止执行任何操作。
结合状态图，我们描述读写自旋锁的工作原理：
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 时刻的执行序列，如果：
- oIk是操作，1 <= k <= (n + 1)。且 oI1，oI2，…，oIn属于集合 A(t)。
- qIk是状态，1 <= k <= (n + 1)。
- 读写自旋锁在 t 时刻的状态是 qI(n+1)。
- qI1= q0。
- T 在 (qIk, oIk) 有定义，且 qI(k+1)= T(qIk, oIk)（1 <= k <= n）。
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 在 t1> t0的时刻提交“读者申请”或“写者申请”的操作，那么锁在 t1时刻并不处于潜在死锁状态。
- “读者持有”。持有者必须在某个 t1> t0的时刻提交“读者释放”的操作，那么锁在 t1时刻并不处于潜在死锁状态。
- “写者持有”。持有者必须在某个 t1> t0的时刻提交“写者释放”的操作，那么锁在 t1时刻并不处于潜在死锁状态。
从线程 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限定为“读者申请”或“写者申请”操作。 |
