A structural approach to prophecy variables

作者：Zhang Zipeng^*; Feng Xinyu; Fu Ming; Shao Zhong; Li Yong

来源：9th Annual Conference on Theory and Applications of Models of Computation, TAMC 2012, 2012-05-16 to 2012-05-21.

DOI：10.1007/978-3-642-29952-0_12

• Atomic operation
• Auxiliary variables
• Backward reasoning
• Concurrent objects
• History variables
• Language constructs
• Program state
• Prophecy variables
• Structural approach
• Verification method

Verifying the implementation of concurrent objects essentially proves the fine-grained implementation of object methods refines the corresponding abstract atomic operations. To simplify the specifications and proofs, we usually need auxiliary history and prophecy variables to record historical events and to predict future events, respectively. Although the meaning of history variables is obvious, the semantics of prophecy variables and the corresponding auxiliary code is tricky and has never been clearly spelled out operationally. In this paper, we propose a new language construct, future blocks, that allows structural use of prophecy variables to refer to events in the future. The semantics of the construct is simple and easy to understand, without using any form of oracle or backward reasoning. Our language also separates auxiliary states from physical program states. With careful syntactic constraints, it ensures the use of history and prophecy variables would not affect the behaviors of the original program, which justifies the verification method based on the use of auxiliary variables.

• 出版日期2012
• 单位中国科学技术大学