ARM内存模型工具：Morello(和一些内存标记)

这篇文章介绍了Morello在内存模型工具中的实现。读者应该对该工具有一些了解，该工具已在前面的文章中介绍：如何使用herd7 Memory Model工具以及如何使用diy7工具自动生成石蕊测试的工作示例。

Morello是ARM开发的基于功能硬件增强型RISC指令(CHERI)的安全架构。更多信息可以在ARM Morello计划中找到。

扩展内存模型工具以包括Morello指令集增加了工具的覆盖范围。在Morello评估板及其上运行的代码的原型制作过程中，这对硬件开发人员和软件开发人员都有好处。在Memory Model Tool中实现Morello有几个方面令人感兴趣，即添加：

在我们开始讨论Morello之前，让我们先简要介绍一下ARM内存标记扩展(MTE)，因为它在本文后面会很有用。MTE实现对内存的锁定和密钥访问。更多信息可在ARMv8-A安全功能中找到。

MTE作为内存模型工具的一部分已经有一段时间了(与https://github.com/herd/herdtools7/commit/6378f2fb0ce9a489d76544dd07bfcb32116d6e76).一起引入。

MTE和Morello都有称为“标签”的对象。在MTE和Morello中，标签的目标都是作为附加在其余数据上的标签。因此，该工具中MTE和Morello标记的实现有一些相似之处。因此，我们在这里简要描述MTE变体的工作方式，以支持Morello变体的呈现。

在内存模型工具中，MTE标签可以采用的不同值用颜色表示：“绿色”、“红色”、“蓝色”、“…。它们可以用“LDG”指令读取，用“STG”指令写入。

>；diyone7-ARCH AArch64-Variant Memtag PodWWTT RFE PodRRTT Fre-name MP-MTE AArch64 MP-MTE { 0：x0=x：红色；0：x1=x：绿色；0：x2=y：红色；0：x3=y：绿色； 1：x1=y：红色；1：x3=x：绿色； } P0|P1； STG X0，[X1]|MOV X0，X1； STG X2，[X3]|LDG X0，[X1]； |MOV X2、X3； |LDG X2，[X3]； 存在(1：x0=y：红色/\1：x2=x：绿色)

请注意，使用了新的“memtag”变体和新的“T”注释来生成在MTE标记(而不是数据)上操作的MTE指令。

>；herd7-Variant memtag MP-MTE.litmus 测试MP-允许的MTE 州4 1：x0=y：绿色；1：x2=x：绿色； 1：x0=y：绿色；1：x2=x：红色； 1：x0=y：红色；1：x2=x：绿色； 1：x0=y：red；1：x2=x：red； 好的 证人 阳性：1阴性：3 存在条件(1：x0=y：红色/\1：x2=x：绿色) 观测MP-MTE有时为1 3 Time MP-MTE 0.03 散列=8955f3049e5ad93e9d858b99d7d6ef22。

Morello有两个指令集：A64和C64。这两者之间的区别在于对某些指令中的操作数的解释。以加载指令为例：

在A64中，“LDR X0，[X1]”检查系统寄存器中是否允许加载。

在C64中，“LDR X0，[C1]”检查“C1”能力寄存器中是否允许加载。

在没有扩展的ARMv8中，地址和数值是无法区分的。选择将寄存器视为保存地址还是数值取决于程序员的意图。

但在Memory Model工具中情况并非如此，在Memory Model工具中，内存位置与数值不同：内存位置用字符串表示。这使得在内存中读取或写入的内容以及它们发生的位置之间有了明确的区别。那么，诸如“wx=1”这样的符号显然意味着值1被写入内存位置“x”，而“rx=1”意味着相同的内存位置是用值1读取的。换句话说，该工具在符号内存位置上工作，而不是在字节内存位置上工作。

在处理混合内存访问大小(例如，对同一内存位置的32位和64位访问)时，能够仅引用内存位置的一部分非常重要。根据Litmus测试，该工具确定“最小访问大小”，并将和内存位置划分为该大小的子块。可以将偏移量添加到基本存储器位置以访问其他子块。如果混合大小的石蕊测试包含W和X大小的内存访问，那么一个64位的“x”位置将被分成两个32位的子块：“x”和“x+4”。

但是不可能通过添加任何数量的偏移量来从另一个符号存储器位置“x”引用符号存储器位置“y”。这是对该工具的设计选择，我们将在本文的其余部分提到这一点。这使我们能够解释在实现Morello变体时所做的某些选择，以及在处理数值和地址的方式上的区别。

Morello引入了一种新的数据类型，即功能。此数据类型保存在容量寄存器中，寄存器为129位宽。这些寄存器由以下字段组成：

对象类型，确定有效功能是密封(对象类型≠0)还是解封(对象类型=0)。

标记，确定功能是否有效(标记=1)或无效(标记=0)。

标志和能力界限的低位与能力值共享编码。

下面的图表显示了功能中的字段组织，摘自ARM架构参考手册附录-Morello，A.F版，第58页：

能力寄存器存储在能力标记存储器中，其中每16字节位置存在一个能力标记位置。

在启用Morello变量的情况下使用内存模型工具时，这必须反映在内存模型工具中：

Herd7的内存表示需要考虑到这个额外的功能标签位置。

这是通过添加包含CAPABILITY标签的内存子区块来实现的，类似于对MTE标签所做的操作。一个显著的区别在于，访问特定存储器位置的MTE标签独立于保存在该位置中的值。但莫雷洛的情况并非如此。对于Morello来说，这种额外的内存子区块的处理方式更接近于混合大小变量，因为它们在内存中被一起访问。

出于性能原因以及实现的简单性，在编写本文时，在工具中使用Morello变量会触发混合变量的使用。对于用户来说，这意味着读取执行图表可能会显示出比Litmus测试所建议的更小的“最小访问大小”(如3.1个内存位置中所述)。

Morello架构确保某些检查保护每次内存访问。这些检查检查是否允许访问。如果检查失败，则会生成同步数据中止，具体故障取决于原因。实现的错误有能力标签错误、能力密封错误和能力许可错误。由于目前无法在内存模型工具中表示边界，因此未实现功能边界错误。

为了不出错，存储器访问需要使用有效且未密封的功能，该功能具有执行相关类型的访问(加载或存储)所需的权限。

Morello引入的其他类型的故障不会在工具中实现。这些故障是：

Morello指令集扩展了“经典”内存指令(str、ldr、swp、cas、…)。使用功能寄存器，创建128位对齐访问。请注意，功能寄存器是129位宽，但虚拟地址是128位对齐的。

它还添加了两条专门操作功能标签的新指令：STCT(存储功能标签)和LDCT(加载功能标签)。它们与内存有独特的交互作用，因此对该工具特别感兴趣。也正是由于这个原因，他们在DIY工具中获得了自己的注释(稍后将详细介绍)。理论上，指令STCT和LDCT在存储器中的4个连续能力位置上操作。但是，该工具不能引用内存位置“x”中的内存位置“y”(参见3.1中的内存位置)。因此，这些指令只在指定位置运行。这一限制将转化为变量是512位对齐的实际系统。

在幕后，DIY工具使用不同的“库”来管理它创建的周期中写入和读取的值。存储体对于每个存储位置都是唯一的。当没有指定变量时，只使用一个银行：“ORD”。

当发生写入时，该工具将内存位置的存储体加1，并根据期望值生成周期的最终状态。在上面的例子中，读取“y”发生在值为1的y写入之后，因此读取y的期望值为1。读取“x”发生在写入x之前，因此读取x的期望值为0。

该工具的memtag变体添加了第二个库：“tag”，独立于Ord库存储MTE标记值。读取和写入标签库是通过使用DIY工具的“T”注释来完成的。

本着同样的精神，Morello变体引入了新的银行来处理不同的功能字段，“CapaTag”用于功能标记，“CapaSeal”用于对象类型。

在这里，您可以看到，写入同一内存位置的不同存储体(这里后跟“Wy.seal”)会将所有写入的值保存在内存中，而从其中一个存储体(标记为“Ry.Seal”)读取只会检索指定存储体的值：

与MTE标签库不同的是，能力库与ORD一起作为一个值的元组。原因在于，为了不丢失信息，将能力标签或对象类型写入寄存器需要与其余存储体相关联。这可能会在石蕊测试中产生更多的说明。

>；diyone7拱AArch64变种Morello PodWW Cs PosWW RFE Cs PodRR Fre AArch64 A { Uint128_t y；uint128_t x； 0：x1=0xffffc0000：x：1；0：x2=0xffffc0000：y：1； 1：x1=0xffffc0000：Y：1；1：x3=0xffffc0000：x：1； } P0|P1； MOV X0，#1|LDR C0，[C1]； 字符串X0，[C1]|GCTYPE X0，C0； MOV X3，#0|LDR X2，[C3]； MOV X4，#1|； SCVALUE C3、C2、X3|； 密封C3、C3、C4|； 字符串C3，[C2]|； MOV X5，#1|； 字符串X5，[C2]|； 存在(1：x0=1/\1：x2=0)。

使用“-Variant Morello”时，保存非存储位置的值的功能寄存器表示为：

其中C是表示能力的比特127：0的整数，T是标签(比特128)。当“T”为0时，只显示“C”。

标签与其他字段分开，以便在使用专注于标签的循环时简化阅读。例如，值为2的标记功能表示为“0x2：1”，而不是更经典的“0x1000000000000000000000000000002”。

请注意，使用“-HEXA TRUE”可以更容易理解地读取功能寄存器的权限和对象类型字段，这可能很有用。例如，所有权限和值为3的标记功能表示为：

“340281068846723829756467474807685906435：1”，带“-HEXA FALSE”(或无六进制标志，因为FALSE是缺省值)。

内存位置表示工具中的符号：“x”、“y”、…。(参见3.1：内存位置)。存储位置的容量的位<；91：0和gt；合并为代表该位置的字母。这就是该工具使用以下表示形式的原因：

“C”是一个整数，表示容量的位127：92。这些位是：

当“C”和“T”都为0时，只显示“m”。

在上例中，“0xffffc0000：x：1”表示具有完全权限的标记和解封能力，包含内存位置“x”。

请注意，在本例中，“C”始终表示为十六进制值，忽略“-HEXA”标志。

石蕊测试的初始化部分包含每个处理元件的寄存器的初始状态。输入格式与前面描述的输出格式匹配。

例如，使用DIY工具获得带有“-Variant Morello”的消息传递循环会带来以下试金石：

>；diyone7拱AArch64变种Morello PodWW RFE PodRR Fre AArch64 MP { Uint128_t y；uint128_t x； 0：x1=0xffffc0000：x：1；0：x3=0xffffc0000：y：1； 1：x1=0xffffc0000：Y：1；1：x3=0xffffc0000：x：1； } P0|P1； MOV X0，#1|LDR X0，[C1]； 字符串X0，[C1]|LDR X2，[C3]； MOV X2，#1|； 字符串X2，[C3]|； 存在(1：x0=1/\1：x2=0)。

与之前的MP-MTE石蕊测试相比，此周期不包含额外的注释。与消息通过石蕊测试的无变化版本相比，存储器访问没有变化。使用“-Variant Morello”只是对地址进行了初始化，以便它们在Morello环境中执行时不会出错。

观察同一程序中混合Morello和非Morello指令的行为可能很有趣。经典的“P”、“L”、“A”和“Q”批注正在接收可选的修饰符来反映这一点。它们可以以小写的“c”作为后缀，以生成指定访问的Morello变体。

>；diyone7拱AArch64变种Morello PodRW L RFE A PodRW L RFE A AArch64 A { Uint128_t y；uint128_t x； 0：x1=0xffffc0000：x：1；0：x3=0xffffc0000：y：1； 1：x1=0xffffc0000：Y：1；1：x3=0xffffc0000：x：1； } P0|P1； 激光雷达X0，[C1]|激光雷达X0，[C1]； MOV X2，#1|MOV X2，#1； STLR X2，[C3]|STLR X2，[C3]； 存在(0：x0=1/\1：x0=1) >；Diyone7拱AArch64变种Morello PodRW L RFE ac PodRW LC RFE A AArch64 A { Uint128_t y；uint128_t x； 0：x1=0xffffc0000：x：1；0：x3=0xffffc0000：y：1； 1：x1=0xffffc0000：Y：1；1：x3=0xffffc0000：x：1； } P0|P1； 激光雷达X0，[C1]|激光雷达C0，[C1]； MOV X2，#1|GCVALUE X0，C0； STLR X2，[C3]|MOV X2，#1； |STLR C2，[C3]； 存在(0：x0=1/\1：x0=1)。

请注意，在第二个示例中使用了P1中的功能寄存器，并将“GCVALUE”添加到加载中以从功能中提取功能值字段。

还有一些新的注释作用于功能的特定字段：“ct”和“cs”。这些注释是第3.5段中提出的银行概念的用户端：介绍新银行。它们分别对应于“CapaTag”和“CapaSeal”银行。“CT”以修改标签的存储器访问为特征。“Cs”表示修改ObjectType的内存访问。请注意，因为功能标签要么是0，要么是1，所以每个内存位置只能执行一次“CT”写入。

>；diyone7拱AArch64-Variant Morello PodWWCtCt RFE PodRRCtCt Fre AArch64 A { Uint128_t y；uint128_t x； 0：x1=0xffffc0000：x：1；0：x3=0xffffc0000：y：1； 1：x1=0xffffc0000：Y：1；1：x3=0xffffc0000：x：1； } P0|P1； MOV X0，#1|LDCT X0，[C1]； STCT X0，[C1]|LDCT X2，[C3]； MOV X2，#1|； STCT X2，[C3]|； 存在(1：x0=1/\1：x2=0)。

当没有选择变量时，DIY工具会创建内存位置(或地址)和值是两个完全独立的实体的循环。包含内存位置的寄存器用表示该位置的字符串(“x”，“y”，...)初始化一次；它们的内容在Litmus测试执行期间不会改变。另一方面，值是每次写入相同内存位置时递增的数字。

Morello以检查每次内存访问的形式提供内存保护。如果这些检查失败，则会导致功能故障(参见3.3功能内存保护)。我们在工具中处理此行为。

但是，创建根据执行顺序显示故障可能性的DIY周期需要摆脱值和内存位置的分离。

当没有选择变量时，DIY工具使用“异或”操作创建依赖项。这样，地址不会改变，但寄存器值确实取决于前一次加载。

Morello变体构建在地址依赖之上，以引入可能发生故障的场景。当与新的“Ct”或“Cs”批注一起使用时，DpAddr的依赖项仍然存在，但形式不同。在这种情况下，用于第二次存储器访问的能力的内容仍然取决于在第一次访问期间读取的值。然而，周期中读取的值与期望值之间的差值用于填充地址的指定能力字段：指定“DpAddr(s|d)(R|W)Ct”时的标记，指定“DpAddr(s|d)(R|W)Cs”时的对象类型。在工具中可以通过以下方式观察到这一点：

AArch64 A "；DpAddrdWPC RfeCsP PodRW RFE"； 生成器=diyone7(版本7.56+02~dev) 预取=0：X=F、0：Y=W、1：Y=F、1：X=W COM=射频射频 ORIG=DpAddrdWPCS RfeCsP PodRW RFE { Uint128_t y；uint128_t x； 0：x1=0xffffc0000：x：1；0：x3=0xffffc0000：y：1； 1：x1=0xffffc0000：Y：1；1：x3=0xffffc0000：x：1； } P0|P1； LDR X0，[X1]|LDR X0，[X1]； Subs X4，X0，#1|MOV X2，#1； 和X4、X4、#4095|STR X2、[X3]； SCVALUE C4、C3、X4|； CSEAL C4、C3、C4|； MOV X5，#0|； MOV X6，#1|； SCVALUE C5、C3、X5|； 密封C5、C5、C6|； 字符串C5，[X4]|； 存在(0：x0=1/\1：x0=0)/\~故障(P0，y)

例如，由于与普通写入相比，需要考虑的字段要多得多，因此创建该功能需要几条指令。

AArch64 A { Uint128_t y；uint128_t x； 0：x1=0xffffc0000：x：1；0：x3=0xffffc0000：y：1； 1：x1=0xffffc0000：Y：1；1：x3=0xffffc0000：x：1； } P0|P1； LDR X0，[C1]|LDR C0，[C1]； Subs X4，X0，#1|GCTYPE X0，C0； 和X4、X4、#4095|MOV X2、#1； SCVALUE C4，C3，X4|STR X2，[C3]； CSEAL C4、C3、C4|； MOV X5，#0|； MOV X6，#1|； SCVALUE C5、C3、X5|； 密封C5、C5、C6|； 字符串C5，[C4]|； 存在(0：x0=1/\1：x0=1)/\~故障(P0，y)