Data Refinement with Low-Level Pointer Operations
Data Refinement with Low-Level Pointer Operations
复制标题
使用低级指针操作进行数据细化
DOI：
10.1007/11575467_3
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Hongseok Yang
中科院分区：
文献类型：
--
作者：
Ivana Mijajlovic;Hongseok Yang
我们提出了一种在存在低级指针操作（例如内存分配和释放以及指针运算）的情况下证明数据精化的方法。令人惊讶的是，现有的数据精化方法，包括那些专门为指针设计的方法，在存在低级指针操作的情况下都不健全。原因是低级指针操作允许获取有关模块实现细节的额外可能性：通过使用内存分配和指针比较，模块的客户端即使不解除引用任何指针，也能找出模块内部使用了哪些单元。现有方法的不健全源于未能处理这种可能性。在本文中，我们提出了一种证明数据精化的新方法，称为幂模拟，并表明幂模拟即使在存在低级指针操作的情况下也是健全的。
We present a method for proving data refinement in the presence of low-level pointer operations, such as memory allocation and deallocation, and pointer arithmetic. Surprisingly, none of the existing methods for data refinement, including those specifically designed for pointers, are sound in the presence of low-level pointer operations. The reason is that the low-level pointer operations allow an additional potential for obtaining the information about the implementation details of the module: using memory allocation and pointer comparison, a client of a module can find out which cells are internally used by the module, even without dereferencing any pointers. The unsoundness of the existing methods comes from the failure of handling this potential. In the paper, we propose a novel method for proving data refinement, called power simulation, and show that power simulation is sound even with low-level pointer operations.
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds