Uniform Confluence in Concurrent Computation

Abstract : Indeterminism is typical for concurrent computation. If several concurrent actors compete for the same resource then at most one of them may succeed, whereby the choice of the successful actor is indeterministic. As a consequence, the execution of a concurrent program may be nonconfluent. Even worse, most observables (termination, computational result, and time complexity) typically depend on the scheduling of actors created during program execution. This property contrast concurrent programs from purely functional programs. A functional program is uniformly confluent in the sense that all its possible executions coincide modulo reordering of execution steps. In this paper, we investigate concurrent programs that are uniformly confluent and their relation to eager and lazy functional programs. We study uniform confluence in concurrent computation within the applicative core of the pi-calculus which is widely used in different models of concurrent programming (with interleaving semantics). In particular, the applicative core of the pi-calculus serves as a kernel in foundations of concurrent constraint programming with first-class procedures (as provided by the programming language Oz). We model eager functional programming in the lambda-calculus with weak call-by-value reduction and lazy functional programming in the call-by-need lambda-calculus with standard reduction. As a measure of time complexity, we count application steps. We encode the lambda-calculus with both above reduction strategies into the applicative core of the pi-calculus and show that time complexity is preserved. Our correctness proofs employs a new technique based on uniform confluence and simulations. The strength of our technique is illustrated by proving a folk theorem, namely that the call-by-need complexity of a functional program is smaller than its call-by-value complexity. The unabridged version of this article is available from Uniform:99. Due to lack of space, the journal version does not contain the encoding of the delta-calculus (introduced in the paper) into the applicative core of the pi-calculus which is of its own interest.
Type de document :
Article dans une revue
Journal on Functional Programming, Elsevier, 2000, 10 (5), pp.453-499
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00536801
Contributeur : Joachim Niehren <>
Soumis le : mardi 16 novembre 2010 - 23:09:12
Dernière modification le : mardi 31 octobre 2017 - 14:22:18
Document(s) archivé(s) le : jeudi 17 février 2011 - 03:13:23

Fichiers

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

Identifiants

  • HAL Id : inria-00536801, version 1

Citation

Joachim Niehren. Uniform Confluence in Concurrent Computation. Journal on Functional Programming, Elsevier, 2000, 10 (5), pp.453-499. 〈inria-00536801〉

Partager

Métriques

Consultations de la notice

104

Téléchargements de fichiers

81