面向分布式细粒度一致性模型的编程语言设计与实现

目录

声明

摘要

第1章绪论

1．1 研究动机

1．2国内外相关工作

1．2．1 一致性模型

1．2．2基于混合一致性模型的数据备份系统

1．2．3 弱内存模型和并发程序逻辑

1．2．4面向分布式混合一致性模型的编程语言

1．3主要贡献

1．3．1 细粒度一致性模型及语言设计

1．3．2与一致性相关的性质及证明

1．3．3与程序语义相关的性质及证明

1．3．4细粒度一致性模型的系统实现

1．4论文组织结构

第2章背景介绍

2．1 系统模型

2．1．1 运行流程和历史轨迹

2．1．2历史轨迹示例

2．2一个启发性的实例

2．2．1同步和依赖

2．2．2明确操作的副作用

2．3本章小结

第3章细粒度一致性语言设计

3．1语法的定义

3．2语言的应用实例

3．2．1 银行系统

3．2．2 add-win集合

3．2．3拍卖系统

3．3操作语义的定义

3．3．1 客户端状态转换规则

3．3．2服务器端状态转换规则

3．4语言的性质

3．4．1 操作同步和操作依赖

3．4．2 仲裁顺序

3．4．3 同步关系、依赖关系和程序顺序

3．4．4一致性

3．4．5示例：银行系统同时取钱

3．5不同的一致性保证

3．5．1 因果一致性

3．5．2基于变量的因果一致性

3．5．3顺序一致性

3．5．4基于变量的顺序一致性

3．6本章小结

第4章程序逻辑与验证

4．1 验证程序满足收敛性的程序逻辑

4．1．1 收敛性和可交换性

4．1．2稳定的存储状态

4．1．3独一的请求

4．1．4示例1：验证拍卖系统的收敛性

4．1．5示例2：验证add-win集合的收敛性

4．2验证程序满足特定不变量的程序逻辑

4．2．1 不变量

4．2．2 独立执行

4．2．3独立接受

4．2．4示例：银行系统账户余额不小于0的条件

4．3使用Coq验证程序逻辑的正确性

4．3．1 Coq简介

4．3．2使用Coq验证收敛性和不变量程序逻辑的可靠性

4．4本章小结

第5章细粒度一致性协议与系统的设计和实现

5．1 服务器端系统设计的几个关键问题

5．1．1 如何模拟全局消息缓冲区?

5．1．2 如何决定全局历史记录和仲裁顺序?

5．1．3如何进行垃圾回收?

5．2服务器端系统运行流程

5．3使用TLA+验证服务器端实现的正确性

5．3．1 TLA+简介

5．3．2使用PlusCal算法语言对服务器端建模

5．3．3 使用TLC工具检查服务器的死锁和活性

5．4其他实现细节

5．5本章小节

第6章实验与分析

6．1 实验环境

6．1．1 站点配置

6．1．2工作负载

6．1．3性能评估指标

6．2实验结果和结果分析

6．2．1 三个应用实例运行时的吞吐量和延迟

6．2．2不同的一致性保证对延迟的影响

6．2．3公平性对延迟的影响

6．3本章小结

第7章结论

7．1本文工作总结

7．2 进一步工作

参考文献

附录

致谢

在读期间发表的学术论文与取得的研究成果