Skip to main content
SpringerLink
Log in

Combining Separation Logic and Projection Temporal Logic to Reason About Non-blocking Concurrency

  • Conference paper
  • First Online:
Structured Object-Oriented Formal Language and Method (SOFL+MSVL 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8979))

  • 469 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Elsevier, Amsterdam (2009)

    Google Scholar 

  2. Ashcroft, Edward, A.: Proving assertions about parallel programs. J. Comput. Syst. Sci. 10(1), 110–135 (1975)

    Google Scholar 

  3. Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338–349. ACM Press, New York (2003)

    Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. 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)

    Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. Electron. Notes Theor. Comput. Sci. 137(2), 93–110 (2005)

    Article  Google Scholar 

  8. 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)

    Chapter  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. Feng, X.: Local rely-guarantee reasoning. In: POPL, pp. 315–327. ACM Press, New York (2009)

    Google Scholar 

  11. Vafeiadis, V.: Modular Fine-Grained Concurrency Verification. Cambridge University, Cambridge (2008)

    Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. 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)

    Google Scholar 

  14. Abadi, M., Manna, Z.: Temporal logic programming. J. Symbolic Comput. 8(1–3), 277–295 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  15. Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)

    Article  Google Scholar 

  16. Rondogiannis, P., Gergatsoulis, M., Panayiotopoulos, T.: Branching-time logic programming: the language cactus and its applications. Comput. Lang. 24(3), 155–178 (1998)

    Article  MATH  Google Scholar 

  17. Moszkowski, B.C.: Executing Temporal Logic Programs. Cambridge University Press, Cambridge (1986)

    Google Scholar 

  18. 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)

    Chapter  Google Scholar 

  19. Yang, X., Duan, Z.: Operational semantics of framed tempura. J. Log. Algebraic Program. 78(1), 22–51 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  20. Duan, Z., Koutny, M.: A framed temporal logic programming language. J. Comput. Sci. Technol. 19(1), 341–351 (2004)

    Article  MathSciNet  Google Scholar 

  21. Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatic 45, 43–78 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  22. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)

    Google Scholar 

  23. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). and 583

    Article  MATH  Google Scholar 

  24. OHearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)

    Article  MathSciNet  Google Scholar 

  25. 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)

    Chapter  Google Scholar 

  26. Wang, X., Duan, Z.: Pointers in framing projection temporal logic programming language. J. Xidian Univ. 36(5), 1069–1074 (2008)

    Google Scholar 

  27. Yang, X., Duan, Z., Ma, Q.: Axiomatic semantics of projection temporal logic programs. Math. Struct. Comput. Sci. 20(5), 865–914 (2010)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, 100190, China

    Xiaoxiao Yang

Authors
  1. Xiaoxiao Yang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Xiaoxiao Yang .

Editor information

Editors and Affiliations

  1. Hosei University, Tokyo, Japan

    Shaoying Liu

  2. Xidian University, Xi’an, China

    Zhenhua Duan

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation