Abstract
Unlike sequential programs, concurrent programs have to account for interference on shared variables. Static verification of a desired property for such programs crucially depends on precisely asserting the conditions for interference. In a static proof system, in addition to program variables, auxiliary (history) variables summarizing the past of the program execution are used in these assertions. Capable of expressing reachability only, assertions (and history variables) are not as useful in the proofs of programs using optimistic concurrency. Pessimistic implementations which allow access to shared data only after synchronization (e.g. locks) guarantee exclusivity; optimistic concurrency implementations which check for interference after shared data is accessed abandon exclusivity in favor of performance.
In this paper, we propose a new construct, tressa, to express properties, including interference, about the future of an execution. A tressa claim states a condition for reverse reachability from an end state of the program, much like an assert claim states a condition for forward reachability from the initial state of the program. As assertions employ history variables, tressa claims employ prophecy variables, originally introduced for refinement proofs. Being the temporal dual of history variables, prophecy variables summarize the future of the program execution. We present the proof rules and the notion of correctness of a program for two-way reasoning in a static setting: forward in time for assert claims, backward in time for tressa claims. We have incorporated our proof rules into the QED verifier and have used our implementation to verify a small but sophisticated algorithm. Our experience shows that the proof steps and annotations follow closely the intuition of the programmer, making the proof itself a natural extension of implementation.
This research was supported by a career grant (104E058) from the Scientific and Technical Research Council of Turkey, the Turkish Academy of Sciences Distinguished Young Scientist Award (TUBA-GEBIP), and a research gift from the Software Reliability Research group at Microsoft Research, Redmond, WA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Elmas, T., Qadeer, S., Tasiran, S.: A calculus of atomic actions. In: POPL 2009, pp. 2–15. ACM, New York (2009)
Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)
Larus, J.R., Rajwar, R.: Transactional Memory. Morgan & Claypool (2006)
Ashcroft, E.A.: Proving assertions about parallel programs. J. Comput. Syst. Sci. 10(1), 110–135 (1975)
Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279–285 (1976)
Wang, L., Stoller, S.D.: Static analysis for programs with non-blocking synchronization. In: PPoPP 2005. ACM Press, New York (2005)
O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1-3), 271–307 (2007)
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. SIGPLAN Not. 38(5), 338–349 (2003)
Freund, S.N., Qadeer, S.: Checking concise specifications for multithreaded software. Journal of Object Technology 3 (2004)
Freund, S.N., Qadeer, S., Flanagan, C.: Exploiting purity for atomicity. IEEE Trans. Softw. Eng. 31(4), 275–291 (2005)
Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253–284 (1991)
Hesselink, W.H.: Simulation refinement for concurrency verification. Electr. Notes Theor. Comput. Sci. 214, 3–23 (2008)
Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.D.: Network invariants in action. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002)
Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 475–488. Springer, Heidelberg (2006)
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2, 219–246 (1989)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sezgin, A., Tasiran, S., Qadeer, S. (2010). Tressa: Claiming the Future. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2010. Lecture Notes in Computer Science, vol 6217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15057-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-15057-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15056-2
Online ISBN: 978-3-642-15057-9
eBook Packages: Computer ScienceComputer Science (R0)