| Title: |
Correctly Translating Concurrency Primitives |
| Authors: |
Schwinghammer, Jan; Sabel, David; Schmidt-Schauss, Manfred; Niehren, Joachim |
| Contributors: |
Programming Systems Lab Saarland; Saarland University Saarbrücken; Goethe-Universität Frankfurt am Main; Modeling Tree Structures, Machine Learning, and Information Extraction (MOSTRARE); Laboratoire d'Informatique Fondamentale de Lille (LIFL); Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)-Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)-Inria Lille - Nord Europe; Institut National de Recherche en Informatique et en Automatique (Inria); Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS); Andreas Rossberg |
| Source: |
The 2009 SIGPLAN Workshop on ML ; https://hal.inria.fr/inria-00429239 ; The 2009 SIGPLAN Workshop on ML, Oct 2009, Edinburgh, United Kingdom. pp.27-38 |
| Publisher Information: |
HAL CCSD |
| Publication Year: |
2009 |
| Collection: |
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
| Subject Terms: |
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
| Subject Geographic: |
Edinburgh; United Kingdom |
| Description: |
International audience ; 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. |
| Document Type: |
conference object |
| Language: |
English |
| Relation: |
inria-00429239; https://hal.inria.fr/inria-00429239; https://hal.inria.fr/inria-00429239/document; https://hal.inria.fr/inria-00429239/file/0.pdf |
| Availability: |
https://hal.inria.fr/inria-00429239; https://hal.inria.fr/inria-00429239/document; https://hal.inria.fr/inria-00429239/file/0.pdf |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.6CCAFFC3 |
| Database: |
BASE |