Advertisement

Verification of Scalable Synchronous Queue

  • Jinjiang Lei
  • Zongyan Qiu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)

Abstract

Lock-free algorithms are extremely hard to be built correct due to their fine-grained concurrency natures. Formal techniques for verifying them are crucial. We present a framework for verification of CAS-based lock-free algorithms, and prove a nontrivial lock-free algorithm Scalable Synchronous Queue that is practically adopted in Java 6. The strength of our approach lies on that it relieves the dependence on auxiliary variables/commands, thus is relatively easier to conduct and comprehend, comparing to existing works.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bornat, R., Calcagno, C., Yang, H.: Variables as resource in separation logic. Electr. Notes Theor. Comput. Sci. 155, 247–276 (2006)CrossRefzbMATHGoogle Scholar
  2. 2.
    Brookes, S.D.: A Semantics for Concurrent Separation Logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16–34. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  3. 3.
    Coleman, J.W.: Expression Decomposition in a Rely/Guarantee Context. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 146–160. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 4.
    Colvin, R., Groves, L.: A scalable lock-free stack algorithm and its verification. In: SEFM, pp. 339–348 (2007)Google Scholar
  5. 5.
    Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent Abstract Predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Fu, M., Li, Y., Feng, X., Shao, Z., Zhang, Y.: Reasoning about Optimistic Concurrency using a Program Logic for History. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 388–402. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  8. 8.
    Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that non-blocking algorithms don’t block. In: POPL, pp. 16–28 (2009)Google Scholar
  9. 9.
    Hailpern, B., Owicki, S.S.: Modular verification of concurrent programs. In: POPL, pp. 322–336 (1982)Google Scholar
  10. 10.
    Hur, C.-K., Dreyer, D., Vafeiadis, V.: Separation logic in the presence of garbage collection. In: LICS (2011)Google Scholar
  11. 11.
    Scherer III, W.N., Lea, D., Scott, M.L.: Scalable synchronous queues. Commun. ACM 52(5), 100–111 (2009)CrossRefGoogle Scholar
  12. 12.
    Lei, J., Qiu, Z.: Verification of Scalable Synchronous Queue. Technical Report 2011-32, School of Math., Peking University (September 2011), http://www.mathinst.pku.edu.cn/index.php?styleid=2
  13. 13.
    Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)Google Scholar
  14. 14.
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)CrossRefzbMATHGoogle Scholar
  15. 15.
    O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1-3), 271–307 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279–285 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982)CrossRefzbMATHGoogle Scholar
  18. 18.
    Parkinson, M.J., Bornat, R., Calcagno, C.: Variables as resource in hoare logics. In: LICS, pp. 137–146 (2006)Google Scholar
  19. 19.
    Parkinson, M.J., Bornat, R., O’Hearn, P.W.: Modular verification of a non-blocking stack. In: POPL, pp. 297–302 (2007)Google Scholar
  20. 20.
    Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55–74 (2002)Google Scholar
  21. 21.
    Turon, A.J., Wand, M.: A separation logic for refining concurrent objects. In: POPL, pp. 247–258 (2011)Google Scholar
  22. 22.
    Vafeiadis, V.: Modular fine-grained concurrency verification. Technical Report UCAM-CL-TR-726, University of Cambridge, Computer Laboratory (July 2008)Google Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    Yahav, E., Sagiv, S.: Automatically verifying concurrent queue algorithms. Electr. Notes Theor. Comput. Sci. 89(3) (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Jinjiang Lei
    • 1
    • 2
  • Zongyan Qiu
    • 1
    • 2
  1. 1.LMAM and Department of Informatics, School of Math.Peking UniversityBeijingChina
  2. 2.State Key Laboratory of Computer ScienceISCASChina

Personalised recommendations