形式陈述
并发对象实现一个顺序抽象数据类型,允许多个线程的操作区间重叠。其正确性把并发历史与顺序规格关联,例如线性一致性要求每个完成操作可放置一个位于调用与返回之间的线性化点。对象还需说明进展条件,如阻塞、lock-free 或 wait-free;安全与进展是独立维度。
直觉
外部看见的是一个共享栈、队列或寄存器,内部却有许多交错步骤;正确性要证明这些交错仍像某种合法顺序执行。
例子与边界
并发队列的两个入队可重叠,输出次序由某个合法线性化顺序决定。线程安全不等于 wait-free:互斥锁可保证线性一致性但停住持锁线程会阻塞别人。对象组合性依正确性条件而异,线性一致性具有局部组合性。
推论与应用
并发对象是多核数据结构、事务内存和共享内存可计算性研究的基本单元。
参考资料
- Maurice Herlihy and Nir Shavit, The Art of Multiprocessor Programming, rev. 1st ed., Morgan Kaufmann, 2012,Chs. 1–18。
- Hagit Attiya and Jennifer Welch, Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd ed., Wiley, 2004,Chs. 1–18。