A Fine-Grained Concurrent Completion Procedure

Claude Kirchner 1 Christopher Lynch Christelle Scharff
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a concurrent Completion procedure based on the use of a SOUR graph as data structure. The procedure has the following characteristics. It is asynchronous, there is no need for a global memory or global control, equations are stored in a SOUR graph with maximal structure sharing, and each vertex is a process, representing a term. Therefore, the parallelism is at the term level. Each edge is a communication link, representing a (subterm, ordering, unification or rewrite) relation between terms. Completion is performed on the graph as local graph transformations by cooperation between processes. We show that this concurrent Completion procedure is sound and complete with respect to the sequential one, provided that the information is locally time stamped in order to detect out of date information.
Type de document :
[Research Report] RR-2990, INRIA. 1996, pp.56
Liste complète des métadonnées

Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:34:29
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : dimanche 4 avril 2010 - 21:39:16



  • HAL Id : inria-00073707, version 1



Claude Kirchner, Christopher Lynch, Christelle Scharff. A Fine-Grained Concurrent Completion Procedure. [Research Report] RR-2990, INRIA. 1996, pp.56. 〈inria-00073707〉



Consultations de la notice


Téléchargements de fichiers