Manticore编程语言并行特性全解析

### Manticore 编程语言并行特性全解析 #### 1. 并行绑定 Manticore 提供了并行绑定形式 `pval p = e`，它将表达式 `e` 的求值作为一个并行线程启动。其顺序语义类似于惰性求值，只有当主控制线程中的某个表达式需要模式 `p` 中绑定的变量时，绑定才会被求值，且仅求值一次。若绑定求值过程中抛出异常，该异常会被推迟到变量被访问时抛出。 例如，计算树的叶子节点乘积的函数： ```sml datatype tree = Lf of int | Br of tree * tree fun trProd t = case t of Lf i => i | Br (t1, t2) => let pval p1 = trProd t1 pval p2 = trProd t2 in if p1 = 0 then 0 else p1 * p2 end ``` 当左子树的乘积为 0 时，该实现会短路，自动取消右子树的计算。 另外，分析何时可以取消并行计算并不简单，例如： ```sml let pval x = f 0 pval y = (| g 1, x |) in if b then x else h y end ``` 在这个条件表达式中，`y` 的计算在 `then` 分支可以取消，但 `x` 的计算在两个分支都不能取消。 并行元组的行为也可以用并行绑定来编码，如 `(|e1, ..., en |)` 可编码为： ```sml let pval x1 = e1 ... pval xn = en in (x1, ..., xn) end ``` #### 2. 并行情况表达式 并行情况表达式 `pcase` 是 Standard ML 顺序情况表达式的非确定性对应形式。在并行情况表达式中，判别式并行求值，匹配规则可以包含通配符模式，即使对应的判别式尚未完全求值也能匹配。 其语法如下： ```sml pcase e1 & ... & en of pp11 & ... & pp1n => e’1 | ... | ppm1 & ... & ppmn => e’m | otherwise => e ``` 其中，并行模式 `pp` 可以是： - 非确定性通配符 `?` - 处理模式 `handle p` - 模式 `p` 非确定性通配符可用于实现短路行为，例如： ```sml | false & ? => 9 ``` 当第一个判别式的计算结果匹配到 `false` 时，程序无需等待第二个判别式计算完成，可立即返回 9。 处理模式用于捕获判别式计算中抛出的异常，并可将异常绑定到模式供后续计算使用。 `otherwise` 分支可以看作是： ```sml | (_ | handle _) & ... & (_ | handle _) => e ``` 它只有在所有计算都完成时才能匹配，且在其他分支也匹配时优先级最低。若没有显式的 `otherwise` 分支，并行情况表达式会被视为： ```sml | otherwise => raise Match ``` 并行选择表达式 `e1 |?| e2` 可用于非确定性地返回 `e1` 或 `e2` 的结果，它可以用 `pcase` 表示为： ```sml pcase e1 & e2 of x & ? => x | ? & x => x ``` 下面是使用并行情况表达式的几个例子： - **trPick 函数**：获取树的某个叶子节点的值 ```sml datatype tree = Lf of int | Br of tree * tree fun trPick t = case t of Lf i => i | Br (t1, t2) => (trPick t1) |?| (trPick t2) ``` - **trProd 函数的另一种实现**： ```sml datatype tree = Lf of int | Br of tree * tree fun trProd t = case t of Lf i => i | Br (t1, t2) => (pcase trProd t1 & trProd t2 of 0 & ? => 0 | ? & 0 => 0 | p1 & p2 => p1 * p2) ``` - **trFind 函数**：查找树中满足谓词的叶子节点值 ```sml fun trFind (p, t) = case t of Lf i => if p i then SOME i else NONE | Br (t1, t2) => (pcase trFind (p, t1) & trFind (p, t2) of SOME i & ? => SOME i | ? & SOME i => SOME i | NONE & NONE => NONE) ``` 并行情况表达式还可用于编码短路并行布尔合取表达式，Manticore 提供了 `|andalso|` 作为派生形式： ```sml val r = pcase e1 & e2 of false & ? => false | ? & false => false | true & true => true ``` #### 3. 异常处理 在并行构造的实现中，必须考虑异常与并行构造的交互。异常抛出和异常处理程序是一等表达式，可出现在程序的任意位置，包括并行构造中。 例如，并行数组表达式 `[| 2+3, 5-7, raise A |]` 求值时会抛出异常 `A`。由于编译器和运行时系统可以按任意顺序执行并行数组表达式的子计算，因此需要补偿代码来确保按顺序语义抛出第一个异常。 可以通过程序分析消除部分或全部补偿代码，例如当确定某个并行数组表达式的子计算不会抛出异常时，就可以省略补偿代码。 当并行上下文中抛出异常时，实现应释放那些由于异常抛出而不再需要结果的并行计算所占用的资源。 #### 4. 示例 ##### 4.1 并行类型检查解释器 考虑为一个简单的模型编程语言编写并行类型检查器和求值器。该语言是纯表达式语言，包含布尔和算术运算符、条件语句、`let` 绑定、函数定义和应用等基本特性。 语言的类型定义如下： ```sml datatype ty = NatTy | BoolTy | ArrowTy of ty * ty ``` 表达式由位置和项组成： ```sml datatype term = NatTerm of int | AddTerm of exp * exp | BoolTerm of bool | IfTerm of exp * exp * exp | VarTerm of var | LetTerm of var * exp * exp | LamTerm of var * ty * exp | AppTerm of exp * exp ... withtype exp = loc * term ``` 类型检查函数 `typeOfExp` 的签名为： ```sml val typeOfExp : env * exp -> ty res ``` 其中，`ty res` 定义为： ```sml datatyp ```