Abstract
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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82, 253–284 (1991)
Cook, B., Koskinen, E.: Making prophecies with decision predicates. In: Proc. 38th ACM Symp. on Principles of Prog. Lang. (POPL 2011), pp. 399–410 (2011)
Feng, X.: Local rely-guarantee reasoning. In: Proc. 36th ACM Symp. on Principles of Prog. Lang. (POPL 2009), pp. 315–327. ACM (2009)
Harris, T., Fraser, K., Pratt, I.A.: A practical multi-word compare-and-swap operation. In: 16th International Symposium on Distributed Computing, pp. 265–279 (October 2002)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)
Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network Invariants in Action. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002)
Marcus, M., Pnueli, A.: Using Ghost Variables to Prove Refinement. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 226–240. Springer, Heidelberg (1996)
Sezgin, A., Tasiran, S., Qadeer, S.: Tressa: Claiming the Future. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 25–39. Springer, Heidelberg (2010)
Vafeiadis, V.: Modular fine-grained concurrency verification. Technical Report UCAM-CL-TR-726, University of Cambridge, Computer Laboratory (July 2008)
Vafeiadis, V., Parkinson, M.: A Marriage of Rely/Guarantee and Separation Logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)
Zhang, Z., Feng, X., Fu, M., Shao, Z., Li, Y.: A structural approach to prophecy variables. Technical report, University of Science and Technology of China (March 2012), http://kyhcs.ustcsz.edu.cn/projects/concur/struct_prophecy
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Zhang, Z., Feng, X., Fu, M., Shao, Z., Li, Y. (2012). A Structural Approach to Prophecy Variables. In: Agrawal, M., Cooper, S.B., Li, A. (eds) Theory and Applications of Models of Computation. TAMC 2012. Lecture Notes in Computer Science, vol 7287. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29952-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-29952-0_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29951-3
Online ISBN: 978-3-642-29952-0
eBook Packages: Computer ScienceComputer Science (R0)