REDEX ::= (Ptr32, Ptr32)

    A1 --|\        /|-- B2
         | |A0--B0| |
    A2 --|/        \|-- B1

REDEX_BAG ::= Vec<REDEX>

    [(A0,B0), (C0,D0), (E0,F0), ...]

REDEX_GRID ::= Matrix<128, 128 REDEX_BAG>

    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
     |      |      |      |      |      |      |      |
    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
     |      |      |      |      |      |      |      |
    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
     |      |      |      |      |      |      |      |
    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
     |      |      |      |      |      |      |      |
    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
     |      |      |      |      |      |      |      |
    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
     |      |      |      |      |      |      |      |
    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
     |      |      |      |      |      |      |      |
    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
     |      |      |      |      |      |      |      |
    ...    ...    ...    ...    ...    ...    ...    ... 

SQUAD ::= Vec<4, THREAD>

THREAD ::=

    loop {
      if (A, B) = pop_redex():
        atomic_rewrite(A, B)
      share_redexes()
    }

    atomic_rewrite(A, B):
      ... match redex type ...
      ... perform atomic links ...

    atomic_link(a, b):
      ... see algorithm on 'paper/' ...

RESULT:

    - thread 0 links A1 -> B1
    - thread 1 links B1 -> A1
    - thread 2 links A2 -> B2
    - thread 3 links B2 -> A2

OUTPUT:

    A1 <--------------> B1
    A2 <--------------> B2

交互

可用的交互与参考论文中描述的相同，即湮灭和交换规则，以及一些额外的交互，包括原始数值操作、条件操作和间接引用。核心交互包括

()---()
~~~~~~~ ERA-ERA
nothing

A1 --|\
     |a|-- ()
A2 --|/
~~~~~~~~~~~~~ CTR-ERA
A1 ------- ()
A2 ------- ()

A1 --|\     /|-- B2
     |a|---|b|   
A2 --|/     \|-- B1
~~~~~~~~~~~~~~~~~~~ CTR-CTR (if a ~~ b)
A1 -----, ,----- B2
         X
A2 -----' '----- B1

A1 --|\         /|-- B2
     |a|-------|b|   
A2 --|/         \|-- B1
~~~~~~~~~~~~~~~~~~~~~~~ CTR-CTR (if a !~ b)
      /|-------|\
A1 --|b|       |a|-- B2
      \|--, ,--|/
           X
      /|--' '--|\
A2 --|b|       |a|-- B1
      \|-------|/

解引用交互发生在 @REF 节点与其他节点交互时。当该节点是一个构造函数时，解引用将被高效地展开。这使得 HVM 变得实用，因为没有它，顶层定义就需要用 DUP 节点来实现。这会在实现函数时造成相当大的开销，因为 DUP 节点具有增量复制特性。当另一个节点是任何其他节点时，这意味着两个闭合网络已经从主图中断开，因此两个节点都被收集，允许递归函数在无限展开之前停止。

() -- @REF
~~~~~~~~~~ ERA-REF
nothing

A1 --|\
     | |-- @REF
A2 --|/
~~~~~~~~~~~~~~~~ CTR-REF
A1 --|\
     | |-- {val}
A2 --|/

由于交互组合器节点只有一个活动端口，这是强归约等关键计算特性所必需的属性，我们不能有二进制数值操作节点。相反，我们将数值操作分成两个节点：OP2，它处理第一个操作数并返回一个 OP1 节点，然后 OP1 节点处理第二个操作数，执行计算，并将结果连接到返回线。

A1 --,
     [}-- #X
A2 --' 
~~~~~~~~~~~~~~ OP2-NUM
A2 --[#X}-- A1

A1 --[#X}-- #Y
~~~~~~~~~~~~~~ OP1-NUM
A1 -- #Z

请注意，OP2 操作符不存储操作类型。相反，它存储在左操作数的 4 个未使用的位上。因此，使用一个名为 "load-op-type" 的附加操作来加载左操作数上的下一个操作。有关更多信息，请参阅 /examples 目录。以下是一个包含所有可用操作的表格：

由于 HVM 已经提供了大量针对分支的解决方案（全局引用、lambda 编码布尔值和模式匹配等），因此模式匹配操作仅用于从数字中读取位：否则，数字将是无法与程序其他部分交互的 "黑盒"。其工作方式很简单：它接收一个数字、两个分支（case-zero 和 case-succ，存储在 CON 节点中）和返回线。如果数字是 0，则删除 case-succ 分支并返回 case-zero 分支。否则，删除 case-zero 分支并返回应用于数字前驱的 case-succ 分支。

A1 --,
     (?)-- #X
A2 --' 
~~~~~~~~~~~~~~~~~~ MAT-NUM (#X > 0)
           /|-- A2
      /|--| |
A1 --| |   \|-- #(X-1)
      \|-- ()

A1 --,
     (?)-- #X
A2 --' 
~~~~~~~~~~~~~~~~~~ MAT-NUM (#X == 0)
      /|-- ()
A1 --| |   
      \|-- A2

请注意，省略了一些交互，如 NUM-ERA，但它们在逻辑上应从上述描述中推导出来。

内存布局

内存布局针对效率进行了优化。从概念上讲，它等于

// A pointer is a 64-bit word
type Ptr = u64;

// A node stores its two aux ports
struct Node {
  p1: Ptr, // this node's fst aux port
  p2: Ptr, // this node's snd aux port 
}

// A redex links two main ports
struct Redex {
  a: Ptr, // main port of node A
  b: Ptr, // main port of node B
}

// A closed net
struct Net {
  root: Ptr,       // a free wire
  redexes: Vec<Redex> // a vector of redexes
  heap: Vec<Node>  // a vector of nodes
}

如您所见，内存布局类似于文本语法，其中网络表示为树向量，'redex' 缓冲区存储树根（作为活动对），而 'nodes' 缓冲区存储所有节点。每个节点有两个 32 位指针，因此恰好使用 64 位。指针包括 4 位标签、28 位标签（用于 DUP 颜色、OP2 操作符）和 32 位 addr，这允许每个实例寻址 2 GB 的空间。有 12 种指针类型

VR1: Tag = 0x0; // Variable to aux port 1
VR2: Tag = 0x1; // Variable to aux port 2
RD1: Tag = 0x2; // Redirect to aux port 1
RD2: Tag = 0x3; // Redirect to aux port 2
REF: Tag = 0x4; // Lazy closed net
ERA: Tag = 0x5; // Unboxed eraser
NUM: Tag = 0x6; // Unboxed number
OP2: Tag = 0x7; // Binary numeric operation
OP1: Tag = 0x8; // Unary numeric operation
MAT: Tag = 0x9; // Numeric pattern-matching
LAM: Tag = 0xA; // Main port of lam node
TUP: Tag = 0xB; // Main port of tup node
DUP: Tag = 0xC; // Main port of dup node

这种内存高效格式允许在许多情况下快速实现；例如，交互组合器湮灭可以仅用 2 个原子 CAS 执行。

请注意，LAM、TUP 和 DUP 节点是相同的：它们是交互组合器节点，并且根据它们的标签是否相同而湮灭/交换。这种区分是为了更好的打印，但在内部并不使用。

我们还提供了未装箱的 60 位无符号整数，这使得 HVMC 能够以最小的损失存储原始数据。例如，为了存储一个原始 3.75 KB 缓冲区，可以使用深度为 8 的完美二叉树 CON 节点，如下所示：

@buff = (((((((((X0 X1) (X2 X3)) ((X4 X5) (X6 X7))) ...)))))))

这将使用总共 511 个节点，在 HVMC 上占用大约 8 KB 的空间。因此，尽管缓冲区不是规范的一部分，但我们可以使用基于交互网络树以 ~46% 的效率存储原始数据。这种结构不如数组紧凑，但它允许我们并行访问和转换数据，这在实践中是一个很好的权衡。

无锁算法

HVM-Core的大规模并行评估器的核心是一个无锁算法，它允许在并发环境中以最小的竞争和完全避免锁和回退的方式执行交互组合重写。要了解差异，请参见下面的图片。

之前：使用锁

在一个基于锁的交互网络评估器中，线程在减少一个活动对（红黑树）之前必须锁定其整个周围区域。这是一个竞争源，可能会导致回退，从而完全阻止线程进步，降低性能。

之后：无锁

无锁方法通过尝试使用单一的比较和交换来执行链接。当它成功时，不需要做任何事情。当它失败时，我们放置重定向线，语义上完成重写而无需任何交互。然后，当主端口连接到重定向线时，它遍历并消耗整个路径，达到其目标位置。如果是辅助端口，我们使用比较和交换存储，本质上是将节点移动到另一个线程。如果是主端口，我们创建一个新的红黑树，然后可以并行减少。这本质上是一种“隐式所有权”方案，允许线程在避免竞争的精确手术式舞蹈中进行协作。

有关更多信息，请参阅论文/草案.pdf。

贡献

验证没有性能回归

git checkout main
cargo bench -- --save-baseline main # save the unchanged code as "main"
git checkout <your-branch>
cargo bench -- --baseline main      # compare your changes with the "main" branch

验证没有正确性回归，运行cargo test。您可以使用cargo-insta（使用cargo install cargo-insta安装）并运行cargo insta test来查看是否所有测试用例都通过。如果某些测试用例未通过且需要更改，您可以运行cargo insta review来审查快照并在必要时进行纠正。

社区

HVM-Core是Higher Order Company利用大规模并行计算的尝试的一部分。加入我们的Discord吧！