skip to main content
10.1145/1596638.1596648acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
research-article

A compositional theory for STM Haskell

Published: 03 September 2009 Publication History

Abstract

We address the problem of reasoning about Haskell programs that use Software Transactional Memory (STM). As a motivating example, we consider Haskell code for a concurrent non-deterministic tree rewriting algorithm implementing the operational semantics of the ambient calculus. The core of our theory is a uniform model, in the spirit of process calculi, of the run-time state of multi-threaded STM Haskell programs. The model was designed to simplify both local and compositional reasoning about STM programs. A single reduction relation captures both pure functional computations and also effectful computations in the STM and I/O monads. We state and prove liveness, soundness, completeness, safety, and termination properties relating source processes and their Haskell implementation. Our proof exploits various ideas from concurrency theory, such as the bisimulation technique, but in the setting of a widely used programming language rather than an abstract process calculus. Additionally, we develop an equational theory for reasoning about STM Haskell programs, and establish for the first time equations conjectured by the designers of STM Haskell. We conclude that using a pure functional language extended with STM facilitates reasoning about concurrent implementation code.

Supplementary Material

JPG File (acompositionaltheoryforstmhaskellonvimeo.jpg)
MP4 File (acompositionaltheoryforstmhaskellonvimeo.mp4)

References

[1]
ABADI, M., BIRRELL, A., HARRIS, T., AND ISARD, M. Semantics of transactional memory and automatic mutual exclusion. In Proc. POPL'08 (2008), pp. 63--74.
[2]
ACCIAI, L., BOREALE, M., AND DAL-ZILIO, S. A concurrent calculus with atomic transactions. In Proc. ESOP'07 (2007), R. D. Nicola, Ed., vol. 4421 of LNCS, Springer, pp. 48--63.
[3]
BORGSTRÖM, J., BHARGAVAN, K., AND GORDON, A. D. A compositional theory for STM Haskell. Tech. Rep. MSR-TR-2009-66, Microsoft Research, 2009.
[4]
CARDELLI, L. Mobile ambient synchronization. Technical Note 1997-013, Digital Equipment Corporation, Systems Research Center, 1997.
[5]
CARDELLI, L., AND GORDON, A. D. Mobile ambients. Theoretical Computer Science 240 (2000), 177--213.
[6]
FOURNET, C., L´EVY, J.-J., AND SCHMITT, A. An asynchronous, distributed implementation of mobile ambients. In Proc. TCS'00 (2000), Springer, pp. 348--364.
[7]
GIANNINI, P., SANGIORGI, D., AND VALENTE, A. Safe ambients: Abstract machine and distributed implementation. Science of Computer Programming 59, 3 (2006), 209--249.
[8]
GUERRAOUI, R., HENZINGER, T. A., AND SINGH, V. Completeness and nondeterminism in model checking transactional memories. In Proc. CONCUR'08 (2008), F. van Breugel and M. Chechik, Eds., vol. 5201 of LNCS, Springer, pp. 21--35.
[9]
HARRIS, T., AND FRASER, K. Language support for lightweight transactions. In Proc. OOPSLA'03 (2003), pp. 388--402.
[10]
HARRIS, T., MARLOW, S., PEYTON JONES, S., AND HERLIHY, M. Composable memory transactions. In Proc. PPOPP'05 (2005), K. Pingali, K. A. Yelick, and A. S. Grimshaw, Eds., ACM, pp. 48--60.
[11]
HARRIS, T., MARLOW, S., PEYTON JONES, S., AND HERLIHY, M. Composable memory transactions. Communications of ACM 51, 8 (2008), 91--100.
[12]
HARRIS, T., AND PEYTON JONES, S. Transactional memory with data invariants. In Proc. TRANSACT'06 (2006).
[13]
HU, L., AND HUTTON, G. Towards a verified implementation of software transactional memory. In The Symposium on Trends in Functional Programming (2008). To appear.
[14]
HUCH, F., AND KUPKE, F. A high-level implementation of composable memory transactions in Concurrent Haskell. In Proc. Implementation and Application of Functional Languages (2005), vol. 4015 of LNCS, Springer, pp. 124--141.
[15]
HUGHES, J. Why functional programming matters. Computer Journal 32, 2 (Apr. 1989), 98--107.
[16]
JEFFREY, A., AND RATHKE, J. A theory of bisimulation for a fragment of concurrent ML with local names. Theoretical Computer Science 323, 1--3 (2004), 1--48.
[17]
KOUTAVAS, V., AND WAND, M. Small bisimulations for reasoning about higher-order imperative programs. In Proc. POPL '06 (2006), ACM, pp. 141--152.
[18]
LEE, E. The problem with threads. COMPUTER (2006), 33--42.
[19]
MILNER, R. Communication and Concurrency. Prentice Hall, 1989.
[20]
MOORE, K. F., AND GROSSMAN, D. High-level small-step operational semantics for transactions. In Proc. POPL'08 (2008), pp. 51--62.
[21]
NANEVSKI, A., GOVEREAU, P., AND MORRISETT, G. Typetheoretic semantics for transactional concurrency. Tech. Rep. TR-08-07, Harvard University, July 2007.
[22]
O'LEARY, J., SAHA, B., AND TUTTLE, M. R. Model checking transactional memory with Spin. In Proc. PODC'08 (2008), R. A. Bazzi and B. Patt-Shamir, Eds., ACM, p. 424.
[23]
OUSTERHOUT, J. Why threads are a bad idea (for most purposes). In Presentation given at the 1996 Usenix Annual Technical Conference, January (1996).
[24]
PEYTON JONES, S., GORDON, A., AND FINNE, S. Concurrent Haskell. In Proc. POPL'96 (1996), pp. 295--308.
[25]
PHILLIPS, A., YOSHIDA, N., AND EISENBACH, S. A distributed abstract machine for boxed ambient calculi. In Proc. ESOP'04 (2004), D. A. Schmidt, Ed., vol. 2986 of LNCS, Springer, pp. 155--170.
[26]
REGEV, A., PANINA, E. M., SILVERMAN, W., CARDELLI, L., AND SHAPIRO, E. BioAmbients: An abstraction for biological compartments. Theoretical Computer Science 325, 1 (2004), 141--167.
[27]
RINGENBURG, M. F., AND GROSSMAN, D. AtomCaml: first-class atomicity via rollback. In Proc. ICFP '05 (2005), ACM, pp. 92--104.
[28]
SANGIORGI, D. On the bisimulation proof method. Mathematical Structures in Computer Science 8 (1998), 447--479.
[29]
SANGIORGI, D., KOBAYASHI, N., AND SUMII, E. Environmental bisimulations for higher-order languages. In Proc. LICS'07 (2007), IEEE Computer Society, pp. 293--302.
[30]
SCOTT, M. L. Sequential specification of transactional memory semantics. In Proc. TRANSACT'06 (2006).
[31]
SHAVIT, N., AND TOUITOU, D. Software transactional memory. Distributed Computing 10, 2 (1997), 99--116.
[32]
SUNSHINE-HILL, B., AND ZARKO, L. STM versus locks, ambiently, May 2008. CIS 552 Final Project, University of Pennsylvania.
[33]
VITEK, J., JAGANNATHAN, S., WELC, A., AND HOSKING, A. L. A semantic framework for designer transactions. In Proc. ESOP'04 (2004), D. A. Schmidt, Ed., vol. 2986 of LNCS, Springer, pp. 249--263.

Cited By

View all
  • (2015)Implementing Software Transactional Memory Using STM HaskellAdvanced Computing and Systems for Security10.1007/978-81-322-2653-6_16(235-248)Online publication date: 19-Nov-2015
  • (2013)Static Application-Level Race Detection in STM Haskell using ContractsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.137.10137(115-134)Online publication date: 8-Dec-2013
  • (2013)Correctness of an STM Haskell implementationACM SIGPLAN Notices10.1145/2544174.250058548:9(161-172)Online publication date: 25-Sep-2013
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
Haskell '09: Proceedings of the 2nd ACM SIGPLAN symposium on Haskell
September 2009
148 pages
ISBN:9781605585086
DOI:10.1145/1596638
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 September 2009

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. ambient calculus
  2. compositional reasoning
  3. transactional memory

Qualifiers

  • Research-article

Conference

ICFP '09
Sponsor:

Acceptance Rates

Overall Acceptance Rate 57 of 143 submissions, 40%

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2015)Implementing Software Transactional Memory Using STM HaskellAdvanced Computing and Systems for Security10.1007/978-81-322-2653-6_16(235-248)Online publication date: 19-Nov-2015
  • (2013)Static Application-Level Race Detection in STM Haskell using ContractsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.137.10137(115-134)Online publication date: 8-Dec-2013
  • (2013)Correctness of an STM Haskell implementationACM SIGPLAN Notices10.1145/2544174.250058548:9(161-172)Online publication date: 25-Sep-2013
  • (2013)Correctness of an STM Haskell implementationProceedings of the 18th ACM SIGPLAN international conference on Functional programming10.1145/2500365.2500585(161-172)Online publication date: 25-Sep-2013
  • (2011)Maintaining database integrity with refinement typesProceedings of the 25th European conference on Object-oriented programming10.5555/2032497.2032530(484-509)Online publication date: 25-Jul-2011
  • (2011)Maintaining Database Integrity with Refinement TypesECOOP 2011 – Object-Oriented Programming10.1007/978-3-642-22655-7_23(484-509)Online publication date: 2011

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media