Abstract
Projection temporal logic programming language MSVL can be well used in modelling simulation and verification of concurrent programs. Non-blocking programs have been widely used in multiprocessor systems. In this paper, we combine separation logic and projection temporal logic to reason about non-blocking concurrency. To this end, we use separation logic as state assertions and projection temporal logic as interval assertions to specify the spatial and temporal properties. Then we extend the MSVL language with atomic blocks, the pointer assignment and the interleaving operator to simulate various of non-blocking programs. Further, we give a sound axiomatic system for the new extended MSVL and prove the lock-free property of Treiber’s stack using the axiomatic system.
This research was supported by NSFC 61100063 and by a Humboldt Fellowship (X.Y.) from Alexander von Humboldt Foundation.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Elsevier, Amsterdam (2009)
Ashcroft, Edward, A.: Proving assertions about parallel programs. J. Comput. Syst. Sci. 10(1), 110–135 (1975)
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338–349. ACM Press, New York (2003)
Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 317–331. Springer, Heidelberg (1998)
Jacobs, B., Piessens, F., et al.: Safe concurrency for aggregate objects with invariants. In: Proceedings of the 3rd IEEE Conference on Software Engineering and Formal Methods. pp. 137–147. (2005)
Jacobs, B., Smans, J., Piessens, F., Schulte, W.: A statically verifiable programming model for concurrent object-oriented programs. In: Liu, Z., Kleinberg, R.D. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 420–439. Springer, Heidelberg (2006)
Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. Electron. Notes Theor. Comput. Sci. 137(2), 93–110 (2005)
Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97–114. Springer, Heidelberg (2004)
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)
Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315–327. ACM Press, New York (2009)
Vafeiadis, V.: Modular Fine-Grained Concurrency Verification. Cambridge University, Cambridge (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)
Pnueli, A.: The temporal semantics of concurrent programs. In: Proceedings of the International Symposium Semantics of Concurrent Computation. LNCS, vol. 70, pp. 1–20. Springer-Verlag (1979)
Abadi, M., Manna, Z.: Temporal logic programming. J. Symbolic Comput. 8(1–3), 277–295 (1989)
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)
Rondogiannis, P., Gergatsoulis, M., Panayiotopoulos, T.: Branching-time logic programming: the language cactus and its applications. Comput. Lang. 24(3), 155–178 (1998)
Moszkowski, B.C.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986)
Duan, Z., Yang, X., Koutny, M.: Semantics of framed temporal logic programs. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 356–370. Springer, Heidelberg (2005)
Yang, X., Duan, Z.: Operational semantics of framed tempura. J. Log. Algebraic Program. 78(1), 22–51 (2008)
Duan, Z., Koutny, M.: A framed temporal logic programming language. J. Comput. Sci. Technol. 19(1), 341–351 (2004)
Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatic 45, 43–78 (2008)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). and 583
OHearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)
Yang, X., Zhang, Y., Fu, M., Feng, X.: A concurrent temporal programming model with atomic blocks. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 22–37. Springer, Heidelberg (2012)
Wang, X., Duan, Z.: Pointers in framing projection temporal logic programming language. J. Xidian Univ. 36(5), 1069–1074 (2008)
Yang, X., Duan, Z., Ma, Q.: Axiomatic semantics of projection temporal logic programs. Math. Struct. Comput. Sci. 20(5), 865–914 (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Yang, X. (2015). Combining Separation Logic and Projection Temporal Logic to Reason About Non-blocking Concurrency. In: Liu, S., Duan, Z. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2014. Lecture Notes in Computer Science(), vol 8979. Springer, Cham. https://doi.org/10.1007/978-3-319-17404-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-17404-4_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17403-7
Online ISBN: 978-3-319-17404-4
eBook Packages: Computer ScienceComputer Science (R0)