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

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

  • 声明:CONSTANT Send(_,_,_,_)\text{CONSTANT } Send(\_, \_, \_, \_)CONSTANT Send(_,_,_,_)
  • 类型假设:ASSUME p,d,miOld,miNew:Send(p,d,miOld,miNew)BOOLEAN\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章描述的异步接口中我们使用了握手协议,在发送下一个数据之前必须确认原先的数据已被接收。在本节的内存接口中,我们将这种细节抽象出来,并将数据的发送和接收都归入单个步骤。处理器将数据发送到内存中,我们称之为SendSendSend步骤,内存发送数据给处理器,称之为ReplyReplyReply步骤。处理器之间不互相发送数据,内存一次只发送数据给一个处理器。

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

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

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

这意味着对于任何表达式ppp, ddd, miOldmiOldmiOld,和miNewmiNewmiNew, Send(p,d,miOld,miNew)Send(p, d, miOld, miNew)Send(p,d,miOld,miNew)也是一个表达式,不过这里还没有说明表达式的值是什么,我们希望它是一个布尔值,其值为真当且仅当memIntmemIntmemInt在第一个状态中等于miOldmiOldmiOld,在第二个状态中等于miNewmiNewmiNew,且是描述处理器ppp将值ddd发送到内存的步骤。我们可以通过下面这个假设来断言这个值是布尔值。
ASSUME p,d,miOld,miNew:Send(p,d,miOld,miNew)BOOLEAN\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

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

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

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

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

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

  • ProcProcProc 处理器标识符集合。(在提及ProcProcProc集合的元素时,我们通常将处理器标识符简称为处理器。)
  • AdrAdrAdr 内存地址集
  • ValValVal 某个内存地址的合理取值集合

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

该集合所有元素的opopop字段等于“RdRdRd”,adradradr字段是AdrAdrAdr集合的一个元素。写请求必须指定要写的地址和要写的值,也由一条记录表示,其opopop字段等于“WrWrWr”,adradradr和valvalval字段分别指定地址和值。我们定义MReqMReqMReq为所有请求的集合,是读写请求两个集合的并集。(集合操作,包括并集,参见在第11页第1.2节。)

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

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

TLA+ 《Specifying Systems》翻译初稿——Section 5.1 The Memory Interface(内存接口)
完整的内存接口规约见上图5.1模块MemoryInterfaceMemoryInterfaceMemoryInterface。

TLA+ 《Specifying Systems》翻译初稿——Section 5.1 The Memory Interface(内存接口)TLA+ 《Specifying Systems》翻译初稿——Section 5.1 The Memory Interface(内存接口) 知之为知知 发布了4 篇原创文章 · 获赞 1 · 访问量 5744 私信 关注
上一篇:Evans PDE 讲义, 视频讲解, 练习参考解答 (更多见小锦教学微信公众号)


下一篇:Java并发编程实战~不安全的单例