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 enco
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, and as a consequence also yields soundness of the encodings with respect to a contextually defined notion of program equivalence. While these translations encode blocking into queuing and waiting, we also describe 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.
show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

    Share in Twitter Search Google Scholar
Metadaten
Author:Jan Schwinghammer, David Sabel, Joachim Niehren, Manfred Schmidt-Schauß
URN:urn:nbn:de:hebis:30:3-344351
URL:http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-37_v2.pdf
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 [v.2])
Publisher:Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik
Place of publication:Frankfurt am Main
Document Type:Working Paper
Language:English
Date of Publication (online):2009/05/12
Date of first Publication:2009/05/12
Publishing Institution:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2014/07/08
SWD-Keyword:Funktionale Programmiersprache; Lambda-Kalkül; Nebenläufigkeit; Pufferspeicher
Issue:Version: 12 Mai 2005
Pagenumber:48
Last Page:48
HeBIS PPN:344379760
Institutes:Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License Logo Veröffentlichungsvertrag für Publikationen

$Rev: 11761 $