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