TLA+ 《Specifying Systems》翻译初稿——Section 5.1 The Memory Interface（内存接口）

本节定义了一个内存系统的通用接口，给出了其设计考虑，并重点说明了为什么以及如何将一个表达式声明为常量参数。

• 声明：$\text{CONSTANT } Send(\_, \_, \_, \_)$CONSTANT Send(_,_,_,_)
• 类型假设：$\text{ASSUME } \forall p, d, miOld, miNew:\\\qquad \qquad \qquad Send (p, d, miOld, miNew) \in \text{BOOLEAN}$ASSUME ∀p,d,miOld,miNew:Send(p,d,miOld,miNew)∈BOOLEAN

在第3章描述的异步接口中我们使用了握手协议，在发送下一个数据之前必须确认原先的数据已被接收。在本节的内存接口中，我们将这种细节抽象出来，并将数据的发送和接收都归入单个步骤。处理器将数据发送到内存中，我们称之为$Send$Send步骤，内存发送数据给处理器，称之为$Reply$Reply步骤。处理器之间不互相发送数据，内存一次只发送数据给一个处理器。

我们用变量$memInt$memInt的值表示内存接口的状态。$Send$Send步骤用某种方式改变了$memInt$memInt，但是我们不想具体说明它是如何改变的，这种情况下，我们将其设为规约的常量参数，就如在4.4节的有限制FIFO中，我们将缓冲区大小设为常量参数$N$N一样。

这样，我们希望声明一个参数$Send$Send，使得表达式$Send(p, d)$Send(p,d)是一个步骤，描述处理器$p$p向内存发送数据$d$d的操作是如何改变$memInt$memInt的。但是，$TLA^+$TLA+只提供了$\text{CONSTANT}$CONSTANT和$\text{VARIABLE}$VARIABLE参数，没有提供动作参数。因此，我们将$Send$Send声明为常量运算符，并记成$Send(p, d, memInt, memInt')$Send(p,d,memInt,memInt′)而不是$Send(p, d)$Send(p,d)。

在$TLA^+$TLA+中，我们这样将$Send$Send声明为一个常量运算符，携带四个入参：
$\text{CONSTANT } Send(\_, \_, \_, \_)$CONSTANT Send(_,_,_,_)

这意味着对于任何表达式$p$p, $d$d, $miOld$miOld，和$miNew$miNew, $Send(p, d, miOld, miNew)$Send(p,d,miOld,miNew)也是一个表达式，不过这里还没有说明表达式的值是什么，我们希望它是一个布尔值，其值为真当且仅当$memInt$memInt在第一个状态中等于$miOld$miOld，在第二个状态中等于$miNew$miNew，且是描述处理器$p$p将值$d$d发送到内存的步骤。我们可以通过下面这个假设来断言这个值是布尔值。
$\text{ASSUME } \forall p, d, miOld, miNew:\\\qquad \qquad \qquad Send (p, d, miOld, miNew) \in \text{BOOLEAN}$ASSUME ∀p,d,miOld,miNew:Send(p,d,miOld,miNew)∈BOOLEAN

上述语句表明对所有的$p$p, $d$d, $miOld$miOld, $miNew$miNew值，$Send(p, d, miOld, miNew) \in \text{BOOLEAN}$Send(p,d,miOld,miNew)∈BOOLEAN为真，内置符号$\text{BOOLEAN}$BOOLEAN表示集合$\{\text{TRUE, FALSE}\}${TRUE, FALSE}，它的元素是两个布尔值$\text{TRUE}$TRUE和$\text{FALSE}$FALSE。

这个$\text{ASSUME}$ASSUME语句正式断言$Send(p, d, miOld, miNew)$Send(p,d,miOld,miNew)的值是一个布尔值。但是，正式断言该值含义的唯一方法是声明它真正是什么——也就是说，给出$Send$Send的定义而不是将其作为参数。我们不想那样做，所以这里我们只是非正式地声明了它的含义，它是表征我们的数学抽象与物理内存系统之间内在关系的非正式描述的一部分。

为了让读者理解规约，我们必须非正式地描述$Send$Send的含义，用$\text{ASSUME}$ASSUME语句断言$Send(…)$Send(…)是一个布尔值，不管怎么说，把它包含进来是个不错的用法。

使用内存接口的规约可以使用$Send$Send和$Reply$Reply运算符来描述变量$memInt$memInt是如何改变的。此规约还必须给出$memInt$memInt的初始值，这里我们声明一个常量参数$InitMemInt$InitMemInt，使其为$memInt$memInt可取的初始值的集合。

我们还需要引入3个常量参数来定义此接口：

• $Proc$Proc 处理器标识符集合。（在提及$Proc$Proc集合的元素时，我们通常将处理器标识符简称为处理器。）
• $Adr$Adr 内存地址集
• $Val$Val 某个内存地址的合理取值集合

最后，我们定义处理器和内存通过接口互相发送的值的集合。处理器向内存发送一个请求，在$TLA^+$TLA+中我们将其表示成一条记录，其中$op$op字段指定请求的类型，其他字段指定请求的参数。本节定义的简单内存只允许读写请求。一条读请求的$op$op字段为“$Rd$Rd”，其$adr$adr字段指定要读的地址。因此，所有读请求的集合就是：
$[op: {"Rd"}， adr: Adr]$[op:"Rd"，adr:Adr]

该集合所有元素的$op$op字段等于“$Rd$Rd”，$adr$adr字段是$Adr$Adr集合的一个元素。写请求必须指定要写的地址和要写的值，也由一条记录表示，其$op$op字段等于“$Wr$Wr”，$adr$adr和$val$val字段分别指定地址和值。我们定义$MReq$MReq为所有请求的集合，是读写请求两个集合的并集。(集合操作，包括并集，参见在第11页第1.2节。)

内存通过返回读取的内存值来响应读请求，那如何定义写请求的响应值呢？我们认为与读请求不同的话会比较清晰，这里设返回值为$NoVal$NoVal，$NoVal$NoVal被声明为常量参数并假设$NoVal\notin Val$NoVal∈/​Val($\notin$∈/​符号在$ASCIl$ASCIl中键入为“\notin”)。不过最好尽可能避免引入参数，我们还可以这样定义$NoVal$NoVal
$NoVal \triangleq \text{CHOOSE }v:v \notin Val$NoVal≜CHOOSE v:v∈/​Val

表达式$\text{CHOOSE }x:F$CHOOSE x:F等于满足公式$F$F的任意值。(如果不存在这样的值，则该表达式是一个完全随机的值)。这个语句没有定义$Val$Val是什么，只定义了它不是$Val$Val的一个元素。$\text{CHOOSE}$CHOOSE运算符参见第73页的第6.6节。

完整的内存接口规约见上图5.1模块$MemoryInterface$MemoryInterface。

• 点赞
• 收藏
• 分享
• • 文章举报

标签：5.1,miOld,miNew,Send,ASSUME,TLA,Specifying,text,内存
来源： https://blog.csdn.net/robinhzp/article/details/104100398