本节定义了一个内存系统的通用接口,给出了其设计考虑,并重点说明了为什么以及如何将一个表达式声明为常量参数。
- 声明:
CONSTANT Send(_,_,_,_)
- 类型假设:
ASSUME ∀p,d,miOld,miNew:Send(p,d,miOld,miNew)∈BOOLEAN
在第3章描述的异步接口中我们使用了握手协议,在发送下一个数据之前必须确认原先的数据已被接收。在本节的内存接口中,我们将这种细节抽象出来,并将数据的发送和接收都归入单个步骤。处理器将数据发送到内存中,我们称之为
Send步骤,内存发送数据给处理器,称之为
Reply步骤。处理器之间不互相发送数据,内存一次只发送数据给一个处理器。
我们用变量
memInt的值表示内存接口的状态。
Send步骤用某种方式改变了
memInt,但是我们不想具体说明它是如何改变的,这种情况下,我们将其设为规约的常量参数,就如在4.4节的有限制FIFO中,我们将缓冲区大小设为常量参数
N一样。
这样,我们希望声明一个参数
Send,使得表达式
Send(p,d)是一个步骤,描述处理器
p向内存发送数据
d的操作是如何改变
memInt的。但是,
TLA+只提供了
CONSTANT和
VARIABLE参数,没有提供动作参数。因此,我们将
Send声明为常量运算符,并记成
Send(p,d,memInt,memInt′)而不是
Send(p,d)。
在
TLA+中,我们这样将
Send声明为一个常量运算符,携带四个入参:
CONSTANT Send(_,_,_,_)
这意味着对于任何表达式
p,
d,
miOld,和
miNew,
Send(p,d,miOld,miNew)也是一个表达式,不过这里还没有说明表达式的值是什么,我们希望它是一个布尔值,其值为真当且仅当
memInt在第一个状态中等于
miOld,在第二个状态中等于
miNew,且是描述处理器
p将值
d发送到内存的步骤。我们可以通过下面这个假设来断言这个值是布尔值。
ASSUME ∀p,d,miOld,miNew:Send(p,d,miOld,miNew)∈BOOLEAN
上述语句表明对所有的
p,
d,
miOld,
miNew值,
Send(p,d,miOld,miNew)∈BOOLEAN为真,内置符号
BOOLEAN表示集合
{TRUE, FALSE},它的元素是两个布尔值
TRUE和
FALSE。
这个
ASSUME语句正式断言
Send(p,d,miOld,miNew)的值是一个布尔值。但是,正式断言该值含义的唯一方法是声明它真正是什么——也就是说,给出
Send的定义而不是将其作为参数。我们不想那样做,所以这里我们只是非正式地声明了它的含义,它是表征我们的数学抽象与物理内存系统之间内在关系的非正式描述的一部分。
为了让读者理解规约,我们必须非正式地描述
Send的含义,用
ASSUME语句断言
Send(…)是一个布尔值,不管怎么说,把它包含进来是个不错的用法。
使用内存接口的规约可以使用
Send和
Reply运算符来描述变量
memInt是如何改变的。此规约还必须给出
memInt的初始值,这里我们声明一个常量参数
InitMemInt,使其为
memInt可取的初始值的集合。
我们还需要引入3个常量参数来定义此接口:
-
Proc 处理器标识符集合。(在提及
Proc集合的元素时,我们通常将处理器标识符简称为处理器。)
-
Adr 内存地址集
-
Val 某个内存地址的合理取值集合
最后,我们定义处理器和内存通过接口互相发送的值的集合。处理器向内存发送一个请求,在
TLA+中我们将其表示成一条记录,其中
op字段指定请求的类型,其他字段指定请求的参数。本节定义的简单内存只允许读写请求。一条读请求的
op字段为“
Rd”,其
adr字段指定要读的地址。因此,所有读请求的集合就是:
[op:"Rd",adr:Adr]
该集合所有元素的
op字段等于“
Rd”,
adr字段是
Adr集合的一个元素。写请求必须指定要写的地址和要写的值,也由一条记录表示,其
op字段等于“
Wr”,
adr和
val字段分别指定地址和值。我们定义
MReq为所有请求的集合,是读写请求两个集合的并集。(集合操作,包括并集,参见在第11页第1.2节。)
内存通过返回读取的内存值来响应读请求,那如何定义写请求的响应值呢?我们认为与读请求不同的话会比较清晰,这里设返回值为
NoVal,
NoVal被声明为常量参数并假设
NoVal∈/Val(
∈/符号在
ASCIl中键入为“\notin”)。不过最好尽可能避免引入参数,我们还可以这样定义
NoVal
NoVal≜CHOOSE v:v∈/Val
表达式
CHOOSE x:F等于满足公式
F的任意值。(如果不存在这样的值,则该表达式是一个完全随机的值)。这个语句没有定义
Val是什么,只定义了它不是
Val的一个元素。
CHOOSE运算符参见第73页的第6.6节。
完整的内存接口规约见上图5.1模块
MemoryInterface。