On Proving the Equivalence of Concurrency Primitives

Jan Schwinghammer; David Sabel; Joachim Niehren; Manfred Schmidt-Schauß

Publication details

On Proving the Equivalence of Concurrency Primitives

Jan Schwinghammer, David Sabel, Joachim Niehren, Manfred Schmidt-Schauß

Technical Report, Research group for Artificial Intelligence and Software Technology, Goethe Universität Frankfurt, Germany, 2008

Various concurrency primitives have been added to sequential programming languages, in order to turn them concurrent. Prominent examples are concurrent buffers for Haskell, channels in Concurrent ML, joins in JoCaml, and handled futures in Alice ML. Even though one might conjecture that all these primitives provide the same expressiveness, proving this equivalence is an open challenge in the area of program semantics. In this paper, we establish a first instance of this conjecture. We show that concurrent buffers can be encoded in the lambda calculus with futures underlying Alice ML. Our correctness proof results from a systematic method, based on observational semantics with respect to may and must convergence.

Download PDF Show BibTeX

@TECHREPORT{Schwinghammer:Sabel:Niehren:Schmidt-Schauss:08,
  title = {On Proving the Equivalence of Concurrency Primitives},
  author = {Jan Schwinghammer and David Sabel and Joachim Niehren and Manfred Schmidt-Schauß},
  year = {2008},
  type = {{Frank-34}},
  address = {{Goethe Universität Frankfurt, Germany}},
  institution = {{Research group for Artificial Intelligence and Software Technology}},
}

Legal notice, Privacy policy