Formal and Incremental Construction of a Distributed Reference Counting Algorithm.

Abstract : We present a complete and proved development of a distributed reference counting algorithm. This algorithm is used to share and remove resources in a distributed way and also in distributed garbage collection. A resource is created by a site (the owner) and can be used by other sites. The owner of a resource can remove it only when it is sure that this resource is not used by another site. L. Moreau has developed such an algorithm and has proved it with J. Duprat using the proof assistant Coq. We present a complete and proved development of a distributed reference counting algorithm. The main contribution of this paper is the incremental construction starting from a simple abstraction without any distribution until a distributed and concrete algorithm which looks like the Moreau's one. This incremental construction allows us to validate step by step the real algorithm and to prove it more easily. We conclude all refinement with an explanation on the termination of this algorithm using specific constraints (limited messages like L. Moreau.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00000788
Contributor : Dominique Cansell <>
Submitted on : Saturday, November 19, 2005 - 11:56:54 AM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM

Identifiers

  • HAL Id : inria-00000788, version 1

Citation

Dominique Cansell, Dominique Méry. Formal and Incremental Construction of a Distributed Reference Counting Algorithm.. APPSEM 2005, Martin Hofmann, Sep 2005, Frauenchiemsee Germany. ⟨inria-00000788⟩

Share

Metrics

Record views

29