Systems From Components

Summary

• The Big Picture
• Digging Deeper from Spec to Implementation
• Putting Methodology to Work
  • How to Optimize the Protocol Stack
  • NuPrl to the Rescue

The Big Picture

Ensemble Design cycle:

• Specify
  • IO Automata:
    • C-like syntax
    • composition operator
• Code
  • OCaml
    • Object Oriented
    • Efficient code similar to C
    • Nice complement to IOA
• Optimize
  • NuPrl
    • Optimization of OCaml code
    • Output verified to be functionally equivalent
• Deploy

Digging Deeper from Spec to Implementation

Putting Methodology to Work

• Start with IOA spec
  • Abstract Spec
  • Concrete Spec

How to synthesize the stack from concrete spec?

Getting to an unoptimized OCaml implementation

• Ensemble suite of microprotocols
  • flow control
  • sliding window
  • encryption
  • scatter/gather
• well-defined interfaces allow composition

How to Optimize the Protocol Stack

Layering could lead to inefficiencies

• Analogy to VLSI component-based design breaks down

Several sources of optimization:

• Explicit memory management instead of GC
• Avoid marshaling/unmarshaling across layers
• Buffering in paralle with transmission
• Header compression
• locality enhancement for common sequences

How do we automate this process?

NuPrl to the Rescue

Static Optimization

• NuPrl expert + OCaml expert
• layer by layer

Dynamic Optimization

• Collapse layers
• Generate bypass code if CCP is statisfied

The trick to dynamic optimization is to recognize the state of the protocol is at any time and how the protocol has to react to an input event, known as “Common Case Predicate”