On correctness of buffer implementations in a concurrent lambda calculus with futures

  • Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence. This also shows correctness wrt. program semantics, since the encodings are adequate translations wrt. contextual semantics. While these translations encode blocking into queuing and waiting, we also provide an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Jan Schwinghammer, David SabelORCiDGND, Joachim Niehren, Manfred Schmidt-SchaußORCiDGND
Parent Title (English):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 37
Series (Serial Number):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (37)
Publisher:Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
Place of publication:Frankfurt [am Main]
Document Type:Working Paper
Date of Publication (online):2009/03/02
Date of first Publication:2009/03/02
Publishing Institution:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2009/07/07
GND Keyword:Funktionale Programmiersprache; Pufferspeicher; Lambda-Kalkül; Nebenläufigkeit
Issue:Version: March 2, 2009
Institutes:Informatik und Mathematik / Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoDeutsches Urheberrecht