Advertisement

Journal of Philosophical Logic

, Volume 40, Issue 5, pp 583–632 | Cite as

Fine-grained Concurrency with Separation Logic

  • Kalpesh Kapoor
  • Kamal Lodaya
  • Uday S. Reddy
Article

Abstract

Reasoning about concurrent programs involves representing the information that concurrent processes manipulate disjoint portions of memory. In sophisticated applications, the division of memory between processes is not static. Through operations, processes can exchange the implied ownership of memory cells. In addition, processes can also share ownership of cells in a controlled fashion as long as they perform operations that do not interfere, e.g., they can concurrently read shared cells. Thus the traditional paradigm of distributed computing based on locations is replaced by a paradigm of concurrent computing which is more tightly based on program structure. Concurrent Separation Logic with Permissions, developed by O’Hearn, Bornat et al., is able to represent sophisticated transfer of ownership and permissions between processes. We demonstrate how these ideas can be used to reason about fine-grained concurrent programs which do not employ explicit synchronization operations to control interference but cooperatively manipulate memory cells so that interference is avoided. Reasoning about such programs is challenging and appropriate logical tools are necessary to carry out the reasoning in a reliable fashion. We argue that Concurrent Separation Logic with Permissions provides such tools. We illustrate the logical techniques by presenting the proof of a concurrent garbage collector originally studied by Dijkstra et al., and extended by Lamport to handle multiple user processes.

Keywords

Resource logics Separation logic Program correctness Concurrent programs Garbage collection Heap storage 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Andrews, G. R. (1991). Concurrent programming: Principles and practice. Menlo Park: Addison Wesley.Google Scholar
  2. 2.
    Ashcroft, E. A. (1975). Proving assertions about parallel programs. Journal of Computer and System Sciences, 10(1), 110–135.CrossRefGoogle Scholar
  3. 3.
    Ben-Ari, M. (1984). Algorithms for on-the-fly garbage collection. ACM Transactions on Programming Languages and Systems, 6(3), 333–344.CrossRefGoogle Scholar
  4. 4.
    Bornat, R., Calcagno, C., O’Hearn, P. W., & Parkinson, M. (2005). Permission accounting in separation logic. In Symposium on principles of programming languages (pp. 59–70). ACM Press.Google Scholar
  5. 5.
    Boyland, J. (2003). Checking interference with fractional permissions. In R. Cousot (Ed.), Stat ic anlysis: 10th intern. symp.. Springer lecture notes in computer science (Vol. 2694, pp. 55–72). Springer.Google Scholar
  6. 6.
    Brinch Hansen, P. (1973). Operating system principles. Englewood Cliffs: Prentice-Hall.Google Scholar
  7. 7.
    Brookes, S. D. (2007). A semantics for concurrent separation logic. Theoretical Computer Science, 375(1–3), 227–270.CrossRefGoogle Scholar
  8. 8.
    de Roever, W.-P. (2001). Concurrency verification: Introduction to compositional and noncompositional methods. Cambdridge: Cambridge University Press.Google Scholar
  9. 9.
    Dijkstra, E. W. (1968). Cooperating sequential processes. In F. Genuys (Ed.), Programming languages (pp. 43–112). New York: Academic Press.Google Scholar
  10. 10.
    Dijkstra, E. W., Lamport, L., Martin, A. J., Scholten, C. S., & Steffens, E. F. M. (1975). On-the-fly garbage collection: An exercise in cooperation. Technical Report EWD496B, University of Texas.Google Scholar
  11. 11.
    Dijkstra, E. W., Lamport, L., Martin, A. J., Scholten, C. S., & Steffens, E. F. M. (1978). On-the-fly garbage collection: An exercise in cooperation. Communications of the ACM, 21(11), 966–975.CrossRefGoogle Scholar
  12. 12.
    Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science, 50, 1–102.CrossRefGoogle Scholar
  13. 13.
    Gries, D. (1977). An exercise in proving parallel programs correct. Communications of the ACM, 20(12), 921–930.CrossRefGoogle Scholar
  14. 14.
    Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12, 576–583.CrossRefGoogle Scholar
  15. 15.
    Hoare, C. A. R. (1972). Towards a theory of parallel programming. In C. A. R. Hoare & R. H. Perrott (Eds.), Operating systems techniques (pp. 61–71). Academic Press.Google Scholar
  16. 16.
    Hoare, C. A. R. (1974). Monitors: An operating system structuring concept. Communications of the ACM, 17(10), 549–558.CrossRefGoogle Scholar
  17. 17.
    Ishtiaq, S. S., & O’Hearn, P. W. (2001). BI as an assertion language for mutable data structures. In Symposium on principles of programming languages (pp. 14–26).Google Scholar
  18. 18.
    Lamport, L. (1976). Garbage collection with multiple processes: An exercise in parallelism. In Parallel processing (pp. 50–54).Google Scholar
  19. 19.
    Lamport, L. (1980). The “Hoare logic” of concurrent programs. Acta Informatica, 14, 21–37.CrossRefGoogle Scholar
  20. 20.
    Prensa Nieto, L., & Esparza, J. (2000). Verifying single and multi-mutator garbage collectors with Owicki/Gries in Isabelle/HOL. In M. Nielson & B. Rovan (Eds.), MFCS. Springer lecture notes in computer science (Vol. 1893, pp. 619–628).Google Scholar
  21. 21.
    O’Hearn, P. W. (2007). Resources, concurrency and local reasoning. Theoretical Computer Science, 375(1–3), 271–307.CrossRefGoogle Scholar
  22. 22.
    O’Hearn, P. W., & Pym, D. J. (1999). The logic of bunched implications. Bulletin Symbolic Logic, 5(2), 215–244.CrossRefGoogle Scholar
  23. 23.
    Owicki, S., & Gries, D. (1976). Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM, 19(5), 279–285.CrossRefGoogle Scholar
  24. 24.
    Owicki, S. S., & Gries, D. (1976). An axiomatic proof technique for parallel programs. Acta Informatica, 6, 319–340.CrossRefGoogle Scholar
  25. 25.
    Parkinson, M., Bornat, R., & O’Hearn, P. W. (2007). Modular verification of a non-blocking stack. In Principles of programming languages (pp. 297–302). ACM.Google Scholar
  26. 26.
    Pratt, V. R. (1976). Semantical considerations on Floyd–Hoare logic. In Proc. 17th symp. found. comp. sci. (pp. 109–121). IEEE.Google Scholar
  27. 27.
    Pym, D. J. (2002). The semantics and proof theory of the logic of the logic of bunched implications. Applied logic series (Vol. 26). Kluwer Academic Publishers.Google Scholar
  28. 28.
    Read, S. (1988). Relevant logic: A philosophical examination of inference. Basil Blackwell.Google Scholar
  29. 29.
    Reynolds, J. C. (2000). Intuitionistic reasoning about shared mutable data structure. In J. Davis, B. Roscoe, & J. Woodcock (Eds.), Millennial perspectives in computer science. Palgrave, Houndsmill, Hampshire.Google Scholar
  30. 30.
    Reynolds, J. C. (2002). Separation logic: A logic for shared mutable data structures. In LICS (pp. 55–74).Google Scholar
  31. 31.
    Russinoff, D. M. (1994). A mechanically verified incremental garbage collector. Formal Aspects Computing, 6(4), 359–390.CrossRefGoogle Scholar
  32. 32.
    Torp-Smith, N., Birkedal, L., & Reynolds, J. C. (2008). Local reasoning about a copying garbage collector. ACM Transactions on Programming Lamguages and Systems, 30(4), 1–58.CrossRefGoogle Scholar
  33. 33.
    Vafeiadis, V., & Parkinson, M., (2007). A marriage of rely/guarantee and separation logic. In CONCUR 2007. Springer lecture notes in computer science (Vol. 4703, pp. 256–271).Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2011

Authors and Affiliations

  1. 1.Department of MathematicsIndian Institute of Technology GuwahatiGuwahatiIndia
  2. 2.The Institute of Mathematical SciencesChennaiIndia
  3. 3.School of Computer SciencesUniversity of BirminghamBirminghamUnited Kingdom

Personalised recommendations