为获得更多的并发和更好的性能，程序开发者会尽可能地采用细粒度同步技术来实现并发数据结构。然而这些数据结构通常复杂灵巧、易出错、可靠性难以保证。因此，形式化验证并发数据结构对提高并发软件的可靠性和安全性有着重要意义。可线性化是一个主流的并发数据结构安全性标准。本书针对并发数据结构可线性化标准及其验证方法方面进行了深入研究。本书分析了可线性化标准的局限性，在此基础上提出了强可线性化标准。本书致力于提供简单易用的方法验证并发数据结构的可线性化。

文堂柳，武汉大学计算机软件与理论专业博士毕业，获工学博士学位。现任赣南科技学院教师，研究方向包括并发分布式计算、软件形式化方法等方向。

第1章 概述
1.1 研究的背景和意义
1.2 并发数据结构正确性标准研究现状
1.3 并发数据结构可线性化的验证方法研究现状
1.4 本书的研究内容
1.5 本书的组织结构
第2章 研究基础
2.1 相关数学知识
2.2 程序逻辑
2.3 刻画并发数据结构的行为
2.4 并发数据结构的可线性化
2.5 观察精化与观察等价
2.6 本章小结
第3章 强可线性化
3.1 研究动机
3.2 强可线性化的定义
3.3 强可线性化蕴含观察等价
3.4 顺序规约下的强可线性化及其属性
3.5 本章小结
第4章 基于抽象约简的可线性化验证方法
4.1 Lipton约简理论
4.2 基于单路径的抽象约简
4.3 验证不可约简的读方法
4.4 基于双路径的抽象约简
4.5 验证封装扩展的并发数据结构
4.6 本章小结
第5章 基于偏序属性的可线性化验证方法
5.1 验证并发队列
5.2 验证并发栈
5.3 本章小结
第6章 规约和验证语义松弛的并发数据结构
6.1 语义松弛的并发数据结构概述
6.2 松弛并发数据结构的正确性研究现状
6.3 规约语义松弛的并发数据结构
6.4 验证随机出队队列
6.5 本章小结
第7章 结论与展望
7.1 研究总结
7.2 后续研究工作展望
参考文献