# Publication details

##
Correctly Translating Concurrency Primitives

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

2009 ACM SIGPLAN Workshop on ML (ML'09), ACM, 2009

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. Our translations map waiting on handled futures to queuing of concurrent buffers and vice versa. Correctness of translations means that they preserve and reflect the observations of may- and must-convergence. As a consequence of compositionality, they are also adequate with respect to a contextually defined notion of observational program semantics.

We demonstrate that our approach to the correctness of implementations applies uniformly to the whole compilation process from high-level to low-level concurrent languages.

Based on earlier technical reports TR Frank-34 and TR Frank-37

Download PDF
Show BibTeX

@INPROCEEDINGS{Schwinghammer:Sabel:Schmidt-Schauss:Niehren:09b,
title = {Correctly Translating Concurrency Primitives},
author = {Jan Schwinghammer and David Sabel and Manfred Schmidt-Schauß and Joachim Niehren},
year = {2009},
publisher = {{ACM}},
booktitle = {2009 ACM SIGPLAN Workshop on ML (ML'09)},
note = {{To appear}},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009