Abstract
Optimistic concurrency algorithms provide good performance for parallel programs but they are extremely hard to reason about. Program logics such as concurrent separation logic and rely-guarantee reasoning can be used to verify these algorithms, but they make heavy uses of history variables which may obscure the high-level intuition underlying the design of these algorithms. In this paper, we propose a novel program logic that uses invariants on history traces to reason about optimistic concurrency algorithms. We use past tense temporal operators in our assertions to specify execution histories. Our logic supports modular program specifications with history information by providing separation over both space (program states) and time. We verify Michael’s non-blocking stack algorithm and show that the intuition behind such algorithm can be naturally captured using trace invariants.
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
Dice, D., Shalev, O., Shavit, N.: Transactional locking II. In: Dolev, S. (ed.) DISC 2006. LNCS, vol. 4167, pp. 194–208. Springer, Heidelberg (2006)
Feng, X.: Local rely-guarantee reasoning. In: Proc. 36th ACM Symp. on Principles of Prog. Lang., pp. 315–327. ACM Press, New York (January 2009)
Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 173–188. Springer, Heidelberg (2007)
Fu, M., Li, Y., Feng, X., Shao, Z., Zhang, Y.: Reasoning about optimistic concurrency using a program logic for history. Technical Report YALEU/DCS/TR-1428, Dept. of Computer Science, Yale University, New Haven, CT (June 2010), http://flint.cs.yale.edu/publications/roch.html
Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that non-blocking algorithms don’t block. In: Proc. 36th ACM Symp. on Principles of Prog. Lang., pp. 16–28. ACM, New York (2009)
Herlihy, M.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 124–149 (1991)
Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. In: Proc. 20th Annual Int’l Symp. on Computer Architecture (ISCA), pp. 289–300 (1993)
Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems 5(4), 596–619 (1983)
Lamport, L., Schneider, F.B.: The “Hoare Logic” of CSP, and all that. ACM Trans. Program. Lang. Syst. 6(2), 281–296 (1984)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)
Michael, M.M.: Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst. 15(6), 491–504 (2004)
Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417–426 (1981)
O’Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49–67. Springer, Heidelberg (2004)
Parkinson, M., Bornat, R., O’Hearn, P.: Modular verification of a non-blocking stack. In: Proc. 34th ACM Symp. on Principles of Prog. Lang, pp. 297–302. ACM Press, New York (January 2007)
Parkinson, M.J., Bornat, R., Calcagno, C.: Variables as resource in hoare logics. In: Proc. 21st Annual IEEE Symposium on Logic in Computer Science (LICS’06), pp. 137–146. IEEE Computer Society, Los Alamitos (August 2006)
Pnueli, A.: In transition from global to modular temporal resoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series, pp. 123–144. Springer, Heidelberg (1984)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55–74. IEEE Computer Society, Los Alamitos (July 2002)
Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis, Computer Laboratory. University of Cambridge, Cambridge, UK (July 2007)
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)
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
Fu, M., Li, Y., Feng, X., Shao, Z., Zhang, Y. (2010). Reasoning about Optimistic Concurrency Using a Program Logic for History. In: Gastin, P., Laroussinie, F. (eds) CONCUR 2010 - Concurrency Theory. CONCUR 2010. Lecture Notes in Computer Science, vol 6269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_27
Download citation
DOI: https://doi.org/10.1007/978-3-642-15375-4_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15374-7
Online ISBN: 978-3-642-15375-4
eBook Packages: Computer ScienceComputer Science (R0)