无锁进展

lock-free 是执行级而非单线程级保证：在任何持续有步骤发生的无限执行中，系统必须不断完成操作。某线程的 CAS 失败通常证明共享状态已被别人成功改变，这可作为“失败也见证全局进展”的摊还论证。它避免持锁者暂停导致全体冻结，但不控制哪一个请求获益，也不提供固定步数或延迟上界。

CAS 循环中，一个线程可能每次比较交换前都被其他线程抢先修改而无限重试；只要那些修改对应操作不断完成，算法仍可 lock-free。它因此不能推出个体无饥饿，也不能给指定调用提供步骤上界。

Treiber 栈的 push 读取栈顶、构造新节点并 CAS；若 CAS 失败，说明某次并发修改已在线性化点成功，线程可重读重试。一个恶意调度可让同一线程每次都在 CAS 前被抢先，永不完成而系统仍 lock-free。若所有线程在内存回收协议上相互等待，核心 CAS 算法无锁也不足以让完整实现 lock-free；hazard pointer 或 epoch 回收的进展性质必须一并分析。

lock-free 是安全性与活性公理库安全性与活性Safety and liveness · Correctness properties把系统正确性分为坏事永不发生与好事最终发生两类性质。中的系统级活性保证：无限执行中总有某个操作完成，但不保证指定线程完成；线性化点等安全证明仍需另行给出。

共享内存公理库共享内存系统Shared-memory system进程通过读写共享对象交互的并发模型。中的原子读改写公理库读改写原语Read-modify-write operation · RMW在单个原子步骤中读取旧值、计算并写入新值的共享内存操作。常实现 lock-free 对象，正确性还需与线性一致性公理库线性一致性Linearizability每次操作可放置在调用与返回之间的单点，使历史等价于满足实时顺序的顺序规范。分开证明。标准非阻塞层级为 wait-free公理库Wait-free 进展Wait-free progress · Wait-freedom · 无等待进展每个正确参与者的每次操作都在有限个自身步骤内完成的个体级非阻塞保证。 强于 lock-free，lock-free 强于obstruction-free公理库Obstruction-free 进展Obstruction-free progress · Obstruction-freedom · 无障碍进展一个操作只要最终获得足够长的独占执行区间，就会在有限步骤内完成的非阻塞保证。；相邻页面分别给出个体有限步骤与 solo-termination 的量词，本页只刻画系统级持续完成。

无锁队列、栈和哈希表需要把算法重试、调度公平与内存回收组合成端到端进展论证。核心 CAS 循环满足 lock-free，不代表分配器或回收协议阻塞时公开方法仍满足该性质。