无锁算法正确性必须通过形式化验证而非经验测试，变量状态转换图（STG）将所有可能状态作为节点、原子操作作为有向边，可严格暴露竞态、ABA等问题；需定义完整状态空间、跃迁规则与初始终态约束，覆盖多线程交错路径，并利用图论性质检验线性一致性、死锁及ABA风险。
无锁算法的正确性不能靠“运行几次没出错”来保证，必须从状态演化逻辑上严格验证。变量状态转换图（State Transition Graph, STG）是一种形式化建模工具，它把共享变量的所有可能取值作为节点，把线程执行一次原子操作（如CAS）导致的状态变化画成有向边。用它能直观暴露竞态、丢失更新、ABA等本质问题。
状态建模：先定义合法状态与原子跃迁
设计STG的第一步不是写代码，而是明确三个要素：
- 变量的完整状态空间：比如一个无锁栈的top指针，其状态不只是“指向某个Node”，还要包含Node中next字段的值、是否被其他线程标记为已删除等；AtomicStampedReference的stamp字段必须和value一起构成联合状态。
- 每个原子操作对应的状态跃迁规则：例如CAS(v, e, n)成功时，仅当当前v == e，才允许从状态e跳转到n；失败则不改变状态，但可能触发重试逻辑——这在图中要体现为自环或分支路径。
- 初始状态与终态约束：如计数器初始为0，所有合法操作后值必须为非负整数；队列的enqueue/dequeue必须满足“先进先出”的可达性约束，不能出现某元素入队后永远不可达的情况。
转换图需覆盖并发交错：不止单线程路径
单线程下的STG是条直线，毫无意义。真正的挑战在于刻画多个线程对同一变量的交错操作。例如两个线程同时对AtomicInteger做incrementAndGet：
- 线程A读到值100，准备CAS(100, 101)；
- 线程B在同一时刻也读到100，也准备CAS(100, 101)；
- 其中一者成功，另一者失败并重试——重试时读到的是101，于是尝试CAS(101, 102)。
这个过程在STG中必须呈现为：从状态100出发，两条边分别指向101（第一次成功）和101（第二次成功），而失败路径不是消失，而是导向“重读→再跃迁”的子图。漏掉任何一种交错，图就不完备，证明就不可靠。
用图性质检验关键正确性属性
画完STG后，不是结束，而是开始验证。几个核心属性可直接映射为图论特征：
- 线性一致性（Linearizability）：检查是否存在一个全局顺序，使得每条执行路径都对应图中一条从初始态出发的路径，且每个操作的生效点（linearization point）在图中唯一可定位。例如CAS成功的那一刻，就是状态跃迁发生的边。
- 无死锁与活锁：图中不能存在无限循环的路径（如两个线程反复CAS失败又重试，且始终无法推进）。可通过检测强连通分量（SCC）中是否有非终态节点来判断。
- ABA问题暴露：若状态A→B→A形成环，但中间B状态曾被其他线程修改过（如指针被释放又重分配到同一地址），则该环在图中必须标注为“危险环”，并需引入stamp或版本号打破它——这正是AtomicStampedReference的设计动机。
实践提示：图会爆炸，得靠抽象与工具辅助
真实无锁数据结构的状态空间极容易组合爆炸。一个含3个节点的无锁链表，其拓扑+标记+指针状态可能超百万。因此实际中常用：
- 对称性约简：把相同结构但节点ID不同的状态合并为一类（如“长度为2的已排序链表”）；
- 谓词抽象：不追踪每个字段值，只关注关键谓词，如“栈非空”“head.next == null”“tail已滞后”；
- 模型检测工具：用TLA+、Spin或Java Pathfinder对简化后的STG自动验证死锁、不变量违反等；JDK源码中ConcurrentLinkedQueue的测试就曾借助类似方法发现边界竞态。
