[moca] [announcement] 2 papers on "Concurrency Theory for Distributed Algorithms"

[Uwe.Nestmann@xxxxxxx]

- You feel at home in the area of process calculi, or
  concurrency theory / operational semantics in general? 

- You have an interest in distributed algorithms? 

- You read about some of the classical Consensus algorithms,
  but you were not totally convinced by the semi-formal
  proof details for the algorithms given in pseudo code? 

- You always wanted to better understand the notion of
  "unreliable failure detectors" that are widely used in
  distributed algorithms, but you felt it difficult to get
  used to the notions and terminlogy used in that domain? 

Then our two papers that appeared at the CONCUR 2003 and
ASIAN 2003 conferences might be of interest for you ...



Paper 1 (CONCUR 2003) is a non-trivial case study of a
"standard" distributed algorithm that solves consensus in
the presence of crashes and a particular class of failure
detectors (Diamond-S).  It uses a process calculus model to
describe the algorithm, and it sketches what can be done on
that operational basis in order to formalize a correctness
proof for the algorithm w.r.t. the Consensus specification.

Title:   Modeling Consensus in a Process Calculus
Authors: Uwe Nestmann, Rachele Fuzzati
URL:     http://lampwww.epfl.ch/~uwe/doc/nestmann.fuzzati.merro-concur03.pdf



Paper 2 (ASIAN 2003) provides a fresh look at the original
model of unreliable failure detectors, using operational
semantics as a formal tool.  Inspired by this, we propose a
new failure detector model that we consider easier to
understand, easier to work with and more natural.  Since
both are defined by operational semantics, we prove formally
that representations of failure detectors in the new model
are equivalent to their original representations within the
model used by Chandra and Toueg.

Title:   Unreliable Failure Detectors via Operational Semantics
Authors: Uwe Nestmann, Rachele Fuzzati
URL:     http://lampwww.epfl.ch/~uwe/doc/nestmann.fuzzati-asian03.pdf

A veriant of the new failure detector model of paper 2 is
actually used in the process calculus model of paper 1.



Comments are most welcome!
Uwe Nestmann

  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html