---
title: "Expressiveness proof"
description: "Dex 有一个经计算机检查的证明，说明它能表达什么。"
canonical_url: "https://docs.superdurable.io/zh-Hans/correctness-and-expressiveness/expressiveness-proof/"
source: "docs/i18n/zh-Hans/docusaurus-plugin-content-docs/current/correctness-and-expressiveness/expressiveness-proof.mdx"
locale: "zh-Hans"
---

# 表达能力证明

Dex 有一个经计算机检查的证明，说明它能表达什么。

- [下载论文（PDF）](https://docs.superdurable.io/zh-Hans/papers/dex-expressiveness.pdf)
- [GitHub 上的形式化源码](https://github.com/superdurable/dex/tree/main/formal)

<a id="the-claim"></a>

## 结论

论文定义了一门小型并发语言。它具备并发编程的常用工具：

- 线程，以及 **fork** 和 **join**；
- 共享变量、局部变量，以及可递归的过程；
- 互斥锁（mutex）和条件变量（condition variable）；
- 定时：**sleep**，以及等待一条消息或超时的 **select**；
- 取消线程；
- 异常；
- 外部副作用，例如发送一封邮件；
- 程序退出。

结论：这门语言中的每个程序，都能翻译成一个从外部看行为相同的 Dex Flow。确切的条件见论文。

“行为相同”包含两部分。

- **相同的事件。** 程序能产生的任何事件序列，Flow 都能产生，反过来也一样。
- **相同的结局。** 程序和 Flow 在相同的情况下完成、卡住或一直运行。

“从外部看”指输入、外部副作用和结果。Flow 内部的 Channel 和 Attribute 不算在内。

<a id="why-it-matters"></a>

## 这对你意味着什么

Dex 没有会阻塞的线程，也没有跨等待持有的锁。一个 Flow 是一组 Step：它们读写 Attribute，发布和消费 Channel 消息，并等待 Timer。所以你可能会担心：有些并发逻辑是不是没法写成 Flow？

这个证明表明：凡是能用上面这些构件写出的并发逻辑，都能写成 Flow。

这个翻译是为证明而做的构造，不是 Dex 附带的编译器。它大致为每条语句使用一个 Step，这不是建模应用的方式。建模你自己的 Flow 时，请参考[设计模式](https://docs.superdurable.io/zh-Hans/design-patterns.md)。

<a id="how-each-construct-is-built"></a>

## 每个构件如何搭建

| 构件              | Dex 构件                                                                                                                                                  | 相关设计模式                                                                                         |
| --------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------- | ---------------------------------------------------------------------------------------------- |
| 线程              | 一串 Step，通常每条语句一个。**wait** 用三个 Step，**sleep** 和带超时的 **select** 会多一个入口 Step。线程的位置和局部状态放在 Step 输入中传递。任一时刻，一个运行中的线程就是一个活跃的 Step 执行。                         |                                                                                                |
| **fork**        | **GoToMany** 到父线程的下一个 Step 和子线程的第一个 Step。                                                                                                               |                                                                                                |
| **join**        | 结束的线程向自己的 join Channel 发布一条消息，然后返回 **DeadEnd**。执行 join 的 Step 用 **AnyOf** 等待这个 Channel 和自己的取消 Channel。                                                  | [Await Parallel Steps](https://docs.superdurable.io/zh-Hans/design-patterns/parallel/await.md) |
| 互斥锁             | 一个 Channel，在互斥锁空闲时持有一个 token。**lock** 用 **ForOne** 等待这个 token，等待者按开始等待的顺序获得服务。**unlock** 把 token 发布回去。                                                  | [Critical Section](https://docs.superdurable.io/zh-Hans/design-patterns/critical-section.md)   |
| 条件变量            | 一个 Attribute 保存等待线程的列表，每个等待者有自己的 Channel。**wait** 把线程加入列表，释放互斥锁，等待自己的 Channel，然后重新获取互斥锁。**signal** 移除第一个等待者，并向它的 Channel 发布消息。**broadcast** 对每个等待者都这样做。 |                                                                                                |
| **sleep**       | 一个定时 Step。它的 **WaitFor** 返回 **AnyOf**，包含一个 Timer 和线程的取消 Channel。                                                                                        |                                                                                                |
| 带超时的 **select** | 同一个定时 Step。它用 **AnyOf** 等待一个 Timer、输入 Channel 和取消 Channel。只有胜出的 Condition 会消费消息。                                                                        | [Deferred Choice](https://docs.superdurable.io/zh-Hans/design-patterns/deferred-choice.md)     |
| 取消              | 向被取消线程的取消 Channel 发布一条消息。线程只在本会阻塞的位置看到它。                                                                                                                |                                                                                                |
| 异常              | 处理器栈放在 Step 输入中传递。**throw** 是一次 **GoTo**，跳到处理器的 Step。                                                                                                   |                                                                                                |
| 退出或失败           | 带结果的 **ForceComplete**，或带错误的 **ForceFail**。                                                                                                             |                                                                                                |
| 外部副作用           | 一个 **Execute**，它唯一的副作用就是这次外部调用。                                                                                                                         |                                                                                                |

互斥锁不能用 Attribute 锁实现，因为它只覆盖一个 Step 方法，不覆盖等待。Channel token 可以跨多个 Step 和等待持有。

<a id="how-it-was-checked"></a>

## 如何验证

证明用 Lean 证明助手写成，它检查每一步。

<a id="what-it-does-not-cover"></a>

## 故障

这个证明覆盖没有故障的运行。[故障透明性证明](https://docs.superdurable.io/zh-Hans/correctness-and-expressiveness/failure-transparency-proof.md)把它扩展到崩溃、恢复、重试和消息重投。在那个页面列出的条件下，从有故障的运行中去掉重复的外部副作用，剩下的就是一次无故障的运行。两个证明合起来表明：这门语言中格式良好的程序在 Dex 上运行时，产生的是一次无故障运行的事件，只是外部副作用可能重复。

<a id="related-evidence"></a>

## 相关证据

[Workflow Patterns 评估](https://docs.superdurable.io/zh-Hans/correctness-and-expressiveness/workflow-patterns.md)按 43 个 workflow 模式为 Dex 评级，每个评级都配有可运行的示例和针对真实 server 的测试。这些模式在真实 server 上测试常见情形；证明则覆盖这门语言的每个程序。