1. TLA+
TLA+ 背后的思想很简单，TLA+ 会通过一套自己的 DSL（符号很接近数学语言）描述程序的初始状态以及后续状态之间的转换关系，同时根据你的业务逻辑来定义在这些状态切换中的不变量，然后 TLA+ 的 TLC model checker 对状态机的所有可达状态进行穷举，在穷举过程中不断检验不变量约束是否被破坏。
举个简单的例子，分布式事务最简单的两阶段提交算法，对于 TLA+ Spec 来说，需要你定义好初始状态（例如事务要操作的 keys、有几个并发客户端等），然后定义状态间跳转的操作（ Begin / Write / Read / Commit 等），最后定义不变量（例如任何处于 Committed 状态的 write ops 一定是按照 commit timestamp 排序的，或者 Read 的操作一定不会读到脏数据之类的），写完以后放到 TLC Checker 里面运行，等待结果就好。
但是，我们活在一个不完美的世界，即使你写出了完美的证明，也很难保证你就是对的。第一， Simulator 并没有办法模拟出无限多的 paticipants 和并发度， 一般也就是三五个；第二，聪明的你可能也看出来了，一般 TLA+ 的推广文章也不会告诉你 Spec 的关键是定义不变量，如果不变量定义不完备，或者定义出错，那么证明就是无效的。因此，我认为形式化验证的意义在于让工程师在写代码之前提高信心，在写证明的过程中也能更加深对算法的理解，此外，如果在 TLC Checker 里就跑出异常，那就更好了。
目前 PingCAP 应该是国内唯一一个使用 TLA+ 证明关键算法，并且将证明的 Spec 开源出来的公司，大家可以参考 pingcap/tla-plus 这个 Repo。
2. Chaos Engineering
1. TLA+
TLA+ 背后的思想很简单，TLA+ 会通过一套自己的 DSL（符号很接近数学语言）描述程序的初始状态以及后续状态之间的转换关系，同时根据你的业务逻辑来定义在这些状态切换中的不变量，然后 TLA+ 的 TLC model checker 对状态机的所有可达状态进行穷举，在穷举过程中不断检验不变量约束是否被破坏。
举个简单的例子，分布式事务最简单的两阶段提交算法，对于 TLA+ Spec 来说，需要你定义好初始状态（例如事务要操作的 keys、有几个并发客户端等），然后定义状态间跳转的操作（ Begin / Write / Read / Commit 等），最后定义不变量（例如任何处于 Committed 状态的 write ops 一定是按照 commit timestamp 排序的，或者 Read 的操作一定不会读到脏数据之类的），写完以后放到 TLC Checker 里面运行，等待结果就好。
但是，我们活在一个不完美的世界，即使你写出了完美的证明，也很难保证你就是对的。第一， Simulator 并没有办法模拟出无限多的 paticipants 和并发度， 一般也就是三五个；第二，聪明的你可能也看出来了，一般 TLA+ 的推广文章也不会告诉你 Spec 的关键是定义不变量，如果不变量定义不完备，或者定义出错，那么证明就是无效的。因此，我认为形式化验证的意义在于让工程师在写代码之前提高信心，在写证明的过程中也能更加深对算法的理解，此外，如果在 TLC Checker 里就跑出异常，那就更好了。
目前 PingCAP 应该是国内唯一一个使用 TLA+ 证明关键算法，并且将证明的 Spec 开源出来的公司，大家可以参考 pingcap/tla-plus 这个 Repo。
2. Chaos Engineering
（编辑：济宁站长网）
【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!
|
