Correctly Translating Concurrency Primitives

Abstract : 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.
Type de document :
Communication dans un congrès
Andreas Rossberg. The 2009 SIGPLAN Workshop on ML, Oct 2009, Edinburgh, United Kingdom. pp.27-38, 2009, ACM Digital Library
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00429239
Contributeur : Joachim Niehren <>
Soumis le : samedi 5 février 2011 - 12:38:47
Dernière modification le : jeudi 11 janvier 2018 - 06:22:13
Document(s) archivé(s) le : mardi 6 novembre 2012 - 13:31:10

Fichier

0.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00429239, version 1

Collections

Citation

Jan Schwinghammer, David Sabel, Manfred Schmidt-Schauss, Joachim Niehren. Correctly Translating Concurrency Primitives. Andreas Rossberg. The 2009 SIGPLAN Workshop on ML, Oct 2009, Edinburgh, United Kingdom. pp.27-38, 2009, ACM Digital Library. 〈inria-00429239〉

Partager

Métriques

Consultations de la notice

235

Téléchargements de fichiers

164