Systems From Components
Summary
The Big Picture
Ensemble
Design cycle:
- Specify
- IO Automata:
- C-like syntax
- composition operator
- IO Automata:
- Code
- OCaml
- Object Oriented
- Efficient code similar to C
- Nice complement to IOA
- OCaml
- Optimize
- NuPrl
- Optimization of OCaml code
- Output verified to be functionally equivalent
- NuPrl
- 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”