Towards type-theoretic semantics for transactional concurrency

ABSTRACT

We propose a dependent type theory that integrates programming, specifications, and reasoning about higher-order concurrent programs with shared transactional memory. The design builds upon our previous work on Hoare Type Theory (HTT), which we extend with types that correspond to Hoare-style specifications for transactions. The types track shared and local state of the process separately, and enforce that shared state always satisfies a given invariant, except at specific critical sections which appear to execute atomically. Atomic sections may violate the invariant, but must restore it upon exit. HTT follows Separation Logic in providing tight specifications of space requirements.

As a logic, we argue that HTT is sound and compositional. As a programming language, we define its operational semantics and show adequacy with respect to specifications.

REFERENCES

• 1: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 2: Martin Berger , Kohei Honda , Nobuko Yoshida, A logical analysis of aliasing in imperative higher-order functions, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 3: S. Brookes. A semantics for concurrent separation logic. In CONCUR'04, pages 16--34.
• 4: Chiyan Chen , Hongwei Xi, Combining programming with theorem proving, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 5: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 6: X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP'07, pages 173--188.
• 7: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 8: A. Gotsman, J. Berdine, B. Cook, N. Rinetzky, and M. Sagiv. Local reasoning for storable locks and threads. In APLAS'07, pages 19--38.
• 9: Tim Harris , Keir Fraser, Language support for lightweight transactions, ACM SIGPLAN Notices, v.38 n.11, November 2003
• 10: Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065952]
• 11: A. Hobor, A. W. Appel, and F. Z. Nardelli. Oracle Semantics for Concurrent Separation Logic. In ESOP'08, pages 353--367.
• 12: N. Krishnaswami. Separation logic for a higher-order typed language. In SPACE'06, pages 73--82.
• 13: Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.
• 14: Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.213-225, August 25-29, 2003, Uppsala, Sweden
• 15: The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0.
• 16: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 17: J. L. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.
• 18: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 19: K. F. Moore and D. Grossman. High level small step operational semantics for transactions. In Workshop on Transactional Computing, August 2007.
• 20: A. Nanevski, A. Ahmed, G. Morrisett, and L. Birkedal. Abstract Predicates and Mutable ADTs in Hoare Type Theory. In ESOP'07, pages 189--204.
• 21: A. Nanevski, P. Govereau, and G. Morriset. Type-theoretic semantics for transactional concurrency. Technical Report TR-09-07, Harvard University, July 2007.
• 22: A. Nanevski, G. Morrisett, and L. Birkedal. Hoare Type Theory, Polymorphism and Separation. Journal of Functional Programming, 18(5&6):865--911, 2008.
• 23: Aleksandar Nanevski , Greg Morrisett , Avraham Shinnar , Paul Govereau , Lars Birkedal, Ynot: dependent types for imperative programs, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, September 20-28, 2008, Victoria, BC, Canada
• 24: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 25: Peter W. OHearn, Resources, concurrency, and local reasoning, Theoretical Computer Science, v.375 n.1-3, p.271-307, April, 2007 [doi>10.1016/j.tcs.2006.12.035]
• 26: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 27: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 28: R. L. Petersen, L. Birkedal, A. Nanevski, and G. Morrisett. A realizability model for impredicative Hoare Type Theory. In ESOP'08, pages 337--352.
• 29: Zhong Shao , Valery Trifonov , Bratin Saha , Nikolaos Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.1-45, January 2005 [doi>10.1145/1053468.1053469]
• 30: Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028711]
• 31: V. Vafeiadis and M. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR'07, pages 256--271.
• 32: K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A concurrent logical framework: The propositional fragment. In Types for Proofs and Programs, volume 3085 of Lecture Notes in Computer Science, pages 355--377.
• 33: Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada
• 34: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• 35: D. Zhu and H. Xi. Safe programming with pointers through stateful views. In PADL'05, pages 83--97.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

General Terms:
Languages, Verification

Keywords:
hoare logic, monads, separation logic, type theory