Formal Methods &Distributed Systems
Mark Hayden
Cornell University

Joint work with:
Ken Birman
Robert Constable
Jason Hickey
Robbert Van Renesse
Christoph Kreitz
Reasons To Use ML in Layered Communication Systems

• Abstraction facilities, strong static typing
• Automatic memory management
• Automatic data marshaling
• Rapid, robust development
  5-10 decrease in code size
• But there is another compelling reason
  

Overview

• Group communication is natural application area for formal methods
• Many properties, protocols
• Need modular, layered approach
• But layering hurts performance
• Layering is almost functional
• Functional layers are ``easy'' to optimize with theorem provers

Group Communication Basics

• Generalization of point-to-point protocols (ex: TCP) to groups of processes
• Groups cooperate on task
• Key features:
  • Membership
  • Broadcast

broadcast.eps

Group Properties

• Broadcast ordering: total, causal, FIFO, ...
• Membership: virtual, synchrony 6 variations
• Flow control: credit, rate, ...
• Other properties: stability, state transfer, security, scalability
• Lots of implementations
• Total: token, sequencer, ...

Many Properties
Many Protocols
Example: Process Daemon (Takako Hickey)

• Servers execute remote processes for clients
• Clients and servers share group
• Group comm. used for:
  • Coordination
  • Failure management
  • Scheduling
  • Security

client.eps

Detour: Ensemble

• Group communication toolkit
• Derived from Horus
• Uses layered protocols
• >30 layers
• Supports UOP, TCP, ATM/U-Net
• Implemented in ML
• Interface TOC
  soon C++, Java
• Flexibility: layering, dynamic protocol linking, on-the-fly protocol switching

layers.eps

Layering

• State machine model
• Layers: State machines
• FIFO event queues
• Scheduler

application.eps

Costs of Layering

• Correctness: mixed benefits
• Performance: Inefficient
  • Costs: Scheduler, message headers, redundant checks
  • As much as: 50 ysec/layer
  • But, layers do little in common case
    • As low as 15 ysec
    • For whole stack

Functional Layers

• Layers have small, localized state
• Are not ``algorithmically complex''
• Means imperative &functional
• Representations are ``close''

  

• ``Syntactic'' translation back and forth

Verification (WIP)

• Goal: full/partial verification of layers
• Approach:
  (1) Simplify problem
  • Extensive layering small layers
  • Functional representation
  • Ex: GMP layer: >5000 lines C, <1600 lines ML, 7 layers
    

  (2) Import into symbolic theorem prover, NUPRL, with specification
  (3) Verify (Hard!)

Performance

• Goal: remove layering overhead in common case
• Approach: optimize ``vertically''
• Check conditions for common cases
• Intercept with optimized version

condition.eps

Effectiveness

• Protocol: FIFO virtual synchrony
• 2000 lines, 12 layers
• Optimized by hand (1) Opts (2) ML C

• But need automated method
• ML performance is converging on C

Optimizations

• Lots of tedious &error prone opts.
• Extract common code paths
• Eliminate intermediate datastructures
• Delay state updates
• Compress common message formats
• All in automated system
• Problems: lots of work and ``ad hoc''

Optimizing Functional Representation

• S: State, E: Event
• Layer:
• Example:
• Optimize:
• Example:
• Compose:
  (Not composition of functions)

Automated Method (WIP)

• Use theorem prover as transformer
• Simplify with equational reasoning
• Apply reduction rules
  

  

Conclusion

• Functional representation is natural for layered systems
• Supports unified approach to optimization
• Using general purpose tools for formal methods

• About this document ...