梁红瑾等：处理指针相等关系不确定的指针逻辑 341 在GNU C Library中，使用请求队列实现异步I/O操作.请求队列中的每个节点保存对某文件描述符的I/O 请求.同一文件描述符可以有多个/O请求，这些请求对应的节点按优先级排序形成单链表（指针域为 nex1pio,不同文件描述符的请求对应不同的单链表，这些单链表的首节点按照对应的文件描述符排序形成一 个双向链表（指针域为las1a,nex1fd.该双向链表以及链在该双向链表上的所有单链表构成请求队列，它们之 间的指针相等关系都是精确的.针对请求队列中的所有节点，那些处于就绪状态的节点（必在请求队列的双向链 表中)又链成一个单向链（指针域为nxt_um),称为就绪队列，导致表示就绪队列的单链表和整个请求队列的双 向链表的指针相等关系部分不确定如图1所示3和r分别是请求队列和就绪队列的头指针. next_run next run next ru Fig.I Request queue and ready queue 图1请求队列与就绪队列 删除请求函数void_aio_remove._request(struct requestlist*lasl,struct requestlist*req,int all0在所有链关 系（包括请求队列和就绪队列）中删除reg节点.参数las1是req所在的单链表上eq的前驱节点指针，当eq指向 的节点在双向链表上时，las1为NULL.参数all指示删除节点的方式，当al=1时，req节点所链的部分都将随eg 一起移走；当al=0时，仅别除eg节点，eg节点所链的部分将取代eq的位置. 在验证该函数的性质时，由于请求队列和就绪队列涉及不确定的指针相等关系，不容易准确描述这种结构 的对象以及在函数每一步操作后它的变化；另一方面，该函数代码十分简练却涵盖了多种情况，使得指针逻辑断 言分情况较多，手工证明十分繁琐因此，使用指针逻辑验证实际程序有待良好工具的支持.限于篇幅，比较详细 的介绍和证明见文献[12] 3相关工作 本文扩展的指针逻辑可以用来描述图等指针相等关系不确定的数据结构指针逻辑本质上是一种精确的 指针分析的方法，用访问路径集合来表示程序点的指针信息，用Hoar©风格的推理规则来表示语句引起的指针 信息变化 Bornat也使用Hoare风格的逻辑来推导指针程序的性质l).他把堆看成由指针索引的一群对象，并把每个对 象看成由域名索引的一组成员这样，堆上对象成员的引用对应到两次索引.他基于域名相同与否引入了对象成 员代换公理，由此扩展了Hoare逻辑的赋值公理，用于证明指针程序的性质.在数据结构的归纳定义方面，Bornat 通过归纳定义不同的操作符来描述不同的数据结构，例如有向图的定义： A if A=nil then else (A)A.Ii A.ri.,fi. 而有向无环图的定义则是通过在有向图定义的基础上，引入一个“exclusion set'”破坏环结构： Asif A=nilvAeS then else (A)04.Ii A.s fi. 我们扩展的指针逻辑则通过引入指针不从属断言来破坏环结构.在Bornat的描述方法中，节点的共享或分 离关系并不明确，只是假定除了有向图外，其他数据结构都是无环的，这样很容易使树与图的定义产生混淆.另 一方面，节点共享或分离关系不明确，也容易造成在对特定节点赋值时无意义地展开其他无关的结构.因此， 中国科学院软件研究所 http://www.c-s-a.org.cn梁红瑾 等:处理指针相等关系不确定的指针逻辑 341 在 GNU C Library 中,使用请求队列实现异步 I/O 操作.请求队列中的每个节点保存对某文件描述符的 I/O 请求.同一文件描述符可以有多个 I/O 请求,这些请求对应的节点按优先级排序形成单链表(指针域为 next_prio);不同文件描述符的请求对应不同的单链表.这些单链表的首节点按照对应的文件描述符排序形成一 个双向链表(指针域为 last_fd,next_fd).该双向链表以及链在该双向链表上的所有单链表构成请求队列,它们之 间的指针相等关系都是精确的.针对请求队列中的所有节点,那些处于就绪状态的节点(必在请求队列的双向链 表中)又链成一个单向链(指针域为 next_run),称为就绪队列,导致表示就绪队列的单链表和整个请求队列的双 向链表的指针相等关系部分不确定.如图 1 所示,s 和 r 分别是请求队列和就绪队列的头指针. next_run next_run next_fd r next_prio last_fd s next_run Fig.1 Request queue and ready queue 图 1 请求队列与就绪队列 删除请求函数 void __aio_remove_request(struct requestlist *last, struct requestlist *req, int all)在所有链关 系(包括请求队列和就绪队列)中删除 req 节点.参数 last 是 req 所在的单链表上 req 的前驱节点指针,当 req 指向 的节点在双向链表上时,last 为 NULL.参数 all 指示删除节点的方式,当 all=1 时,req 节点所链的部分都将随 req 一起移走;当 all=0 时,仅删除 req 节点,req 节点所链的部分将取代 req 的位置. 在验证该函数的性质时,由于请求队列和就绪队列涉及不确定的指针相等关系,不容易准确描述这种结构 的对象以及在函数每一步操作后它的变化;另一方面,该函数代码十分简练却涵盖了多种情况,使得指针逻辑断 言分情况较多,手工证明十分繁琐.因此,使用指针逻辑验证实际程序有待良好工具的支持.限于篇幅,比较详细 的介绍和证明见文献[12]. 3 相关工作 本文扩展的指针逻辑可以用来描述图等指针相等关系不确定的数据结构.指针逻辑本质上是一种精确的 指针分析的方法,用访问路径集合来表示程序点的指针信息,用 Hoare 风格的推理规则来表示语句引起的指针 信息变化. Bornat也使用Hoare风格的逻辑来推导指针程序的性质[13].他把堆看成由指针索引的一群对象,并把每个对 象看成由域名索引的一组成员.这样,堆上对象成员的引用对应到两次索引.他基于域名相同与否引入了对象成 员代换公理,由此扩展了Hoare逻辑的赋值公理,用于证明指针程序的性质.在数据结构的归纳定义方面, Bornat 通过归纳定义不同的操作符来描述不同的数据结构,例如有向图的定义: * Al r, if A=nil then {} else {A}∪A. ∪A. fi. * l r, l * l r, r 而有向无环图的定义则是通过在有向图定义的基础上,引入一个“exclusion set”破坏环结构: * AlrS , , if A=nil∨A∈S then {} else {A}∪A. ∪A. fi. * lrS A ,, { } l ∪ * lrS A ,, { } r ∪ 我们扩展的指针逻辑则通过引入指针不从属断言来破坏环结构.在 Bornat 的描述方法中,节点的共享或分 离关系并不明确,只是假定除了有向图外,其他数据结构都是无环的,这样很容易使树与图的定义产生混淆.另 一方面,节点共享或分离关系不明确,也容易造成在对特定节点赋值时无意义地展开其他无关的结构.因此, a1 b1 a2 c2 c1 d1 e1 c3 f1 f2