Topic: How PODC Began, and Where Formal Models Fit In
Author: Nancy Lynch

Plan:

-- How PODC started: 

   Who (me, Fischer, Probert, some input from Lamport)
   Intent (forum for systems + theory to exchange ideas)
   Few algorithms initially---more papers on systems, applications
   How it has evolved.

-- Interplay between formal modeling and algorithms

   A particular feature of PODC-style work is the role played by
       formal models.
   I'll try to describe some of the reasons, status, remaining issues.

   Models are needed to prove things about distributed algorithms. 
       More than for other kinds of algorithms.
       Because they are complicated, nondeterministic.
       Can't understand everything they do---can only understand
         properties.
   Models also needed for lower bounds/impossibility results:
       Lower bound/impossibility results were an important part of
         theory of distributed systems from the start. 
           Cremers/Hibbard, Burns, Lamport,...
       Formal models arose from the beginning because of the need to
         be very precise:  lower bounds require this.

   Kinds of models needed? 
       For algorithms, need 
         Mathematical precision 
         Expressiveness
         Formal languages, proof techniques, tools, ...
         Support for structure:  composition, abstraction
       For lower bounds, need 
         Math precision 
         Simplicity
           Lower bound arguments are hard, need to be stated in simple
             setting.
         Set-theory, not linguistic.
         Express what the algorithm can control and what is under the
           control of the environment.
         Support for structure (the piece we're studying has to
           interact with others).

   Led to interacting state machine models like I/O automata.
       Like process algebra models, but those are linguistic.
       
   Fischer-Lynch paper on shared memory models
       Early model for interacting components 
       Interacting via shared variables, somewhat complicated
       Composition, input-enabled, trace inclusion, fair executions, etc.

   Why need composition?
       To describe layered systems, composed of separate logical
         services.
       To capture interactions between the system we are studying and
         its environment.
     
   How it turned out: 
       Algorithms:
         Many (most?) papers are informal. 
           But underneath, some general fair state-machine model is
             usually assumed.
           Can get into trouble where things aren't precise.
           Proofs can be hard to understand precisely.
       Lower bounds:
         Some reliance on generic models.
         Some define their own models. 
           More self-contained.
           Simpler?
       Generic models aren't enough:
         Need features for timing, failures
         Application-specific models (failure detectors, etc.)
              
   New models needed now, because of new complexities of systems:
       timing, hybrid continuous/discrete (needed for mobile
       computing), dynamic systems, probabilistic,...
   Not clear how we combine these.
   Yet needed for development of the theory for algorithms involving
       these features.