On the distribution of an assertion

ABSTRACT

Given an n-nodes network and an assertion G expressing its correctness, it is shown that G can be decomposed into collection of n local assertions and n.(n-1) “communication” assertions. The special case of a 2-nodes network is first examined, and it is shown how the notion of Galois connections in lattice theory is a basic tool for the assertion decomposition. The principles of a communication protocol that allow to maintain the resulting assertions are described. For the n-nodes network it is shown that assertion G induces Galois connections between any two parts of the network. General formulae for the local and communication assertions are found using this fact. It is also shown that the communication assertions do involve only a pair of nodes each one, which makes possible the use of techniques taken from the 2-nodes network for their maintenance. As an application example a distributed algorithm to solve the “2-out-of-3” problem is proposed.

REFERENCES

• 1: ORE, O. Galois Connections - Trans. Amer. Math. Soc. 55(1944) 493-513
• 2: SZASZ, G. Introduction to Lattice Theory Academic Press, 1963
• 3: WARD, M. The closure operations of a lattice - Annals Math 43 (1942) 191-196
• 4: BIRKOFF, G. Lattice Theory - Amer. Math. Soc. Colloquium Publ. 25, revised edition New-York, 1948
• 5: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 6: Glenn Ricart , Ashok K. Agrawala, An optimal algorithm for mutual exclusion in computer networks, Communications of the ACM, v.24 n.1, p.9-17, Jan. 1981 [doi>10.1145/358527.358537]
• 7: CARVALHO, O. and ROUCAIROL, G. Une amélioration de l'Algorithme d'Exclusion Mutuelle de Ricart et Agrawala - Laboratoire Informatique Théorique et Programmation. Internal Report no 81-58, novembre 1981

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Assertions

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Distributed programming

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

General Terms:
Algorithms, Languages, Performance, Verification