Publication details

Saarland University Computer Science

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               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009