精彩回顾|大咖面对面——上海交通大学王肇国：形式化方法在数据库和分布式系统中的应用

Gauss松鼠会 2023-05-18

1226

Gauss松鼠会

学习探索分享数据库知识和技术共建数据库技术交流圈

关注

5月16日，由Gauss松鼠会携手黄大年茶思屋，共同打造【大咖面对面】栏目第一期——形式化方法在数据库和分布式系统中的应用，在黄大年茶思屋（上海站）线下线上同步举行。上海交通大学王肇国副教授、华为数据库专家张琼、华为形式化专家李昊坤围绕数据库技术依次进行技术分享。除现场参会人员，本次活动线上观看人数达460余人。

近十年，形式化验证技术不断的发展与完善，在电路设计、嵌入式系统以及网络协议等软硬件中被广泛应用。王肇国老师的报告从SQL优化、系统一致性和共识协议三个方面出发，介绍形式化方法在数据库和分布式系统中的应用。

首先，介绍SQL Query等价性验证方法，在此基础上实现SQL改写规则的自动挖掘，相比SQL Server、Calcite等系统，该方法可以提供更有效的改写规则；
接着，介绍如何通过形式化方法构建Paxos与Raft之间的映射关系，并将Paxos优化方法（如Byzantine Paxos）自动扩展至Raft；
最后，介绍如何验证分布式程序的幂等一致性，针对错误程序进行自动修复，同时达到性能最优。

随后，华为数据库专家张琼、华为形式化专家李昊坤为现场的开发者朋友分享了——形式化方法在GaussDB分布式数据库中的应用，介绍了形式化方法在GaussDB中应用的原理和关键技术。

在最后的Panel环节，三位嘉宾与现场与会者一起，围绕形式化方法在业界的最新进展，以及如何在软件工程中应用形式化验证进行了深入探讨。大家一致认为，形式化方法未来在软件工程中将会发挥更大的价值。同时，针对如何在数据库内核中进一步应用形式化方法提升系统可靠性和数据一致性，初步形成了一些IDEA和合作意向。