Transcript For User-Level Networks

ESP: A Language for
Programmable Devices
Sanjeev Kumar
Princeton University
Advisor : Kai Li
Programmable Devices
Main CPU
Main Memory
Bus
D
Network
Card
D
R CPU Mem
D
CPU
R
Mem
Disk
D
Network
Move functionality from main CPUs to devices
Sanjeev Kumar
ESP: A Language for Programmable Devices
2
Programming Devices
• Challenging
– Concurrent, low-overhead, and reliable
• Event-driven state machines (vs. Threads)
– 1 stack is shared by all state-machines
– Fast context switches
• Only need to save and restore the Program Counter
– Low overhead: memory & CPU
– Less functionality provided
Sanjeev Kumar
ESP: A Language for Programmable Devices
3
Programming Devices in C
• State machines communicating using events
• A state machine
event UserReq execute processUser()
event KernelReq execute processKernel()
WaitReq
event DmaFree execute
WaitDMA
WaitNet
event NetFree execute
Sanjeev Kumar
ESP: A Language for Programmable Devices
4
Programming Devices in C Cont’d
• Programming is hard
– Sequential code split into handlers
int i = 5;
block();
j = i;
• Difficult for C compiler to optimize
– Explicitly save values in global variables
• Hand optimizations make it worse
– Fast paths (violate modularity)
– Embed ad-hoc scheduling decisions
Sanjeev Kumar
ESP: A Language for Programmable Devices
5
Case Study: VMMC
• High-performance communication
Application
– Bypass OS for data transfers
Data
OS
• Used Myrinet network cards
Network Card
– Gigabit network
– 33 MHz CPU, 1 MB memory
Network
• VMMC firmware
– Event-driven state machines in C
Sanjeev Kumar
ESP: A Language for Programmable Devices
6
Our Experience with
Programming VMMC Firmware
• Event-driven state machines in C
– Hard to program
• VMMC: 15,600 lines of C code
• Add new functionality
– Hard to debug
• Complicated race conditions (still encounter bugs)
• Trusted by the OS
– Achieves good performance
• Requires hand optimization
Sanjeev Kumar
ESP: A Language for Programmable Devices
7
Outline
•
•
•
•
•
•
Motivation
ESP overview
ESP language
Verifying ESP programs
Performance of ESP programs
Conclusions
Sanjeev Kumar
ESP: A Language for Programmable Devices
8
ESP: Event-driven
State-machines Programming
• Domain-specific language
• Goals
– Easy to program
• Concise, modular programs
– Allow extensive testing
• Use existing model-checking verifiers like Spin
– Performance
• Low overhead
• Case study: VMMC firmware
Sanjeev Kumar
ESP: A Language for Programmable Devices
9
ESP Approach
pgm.ESP
pgm1.spin
Spin
ModelsDevelop
test1.spin
pgmN.spin
Detailed Model and
Memory SafetyTest
Model
using
Abstract
testN.spin Models
ESP Compiler
pgm.C
Sanjeev Kumar
Verifier
ESP: A Language for Programmable Devices
help.C
Generate
Firmware
10
Related Work
• Verification + Code generation
–
–
–
–
Esterel: Control of reactive systems
Teapot: Coherence protocols for shared memory
Promela++: Layered network protocols
@-format: C extension for state machines
• Concurrent languages
– CSP, Squeak, OCCAM, Java, CML, Devil
• Debugging Tools
– Meta-level compilation, SLAM, Verisoft
Sanjeev Kumar
ESP: A Language for Programmable Devices
11
Outline
•
•
•
•
•
•
Motivation
ESP overview
ESP language
Verifying ESP programs
Performance of ESP programs
Conclusions
Sanjeev Kumar
ESP: A Language for Programmable Devices
12
The ESP Language
• Concurrent language
• Processes & Channels
– in : Receive a message on a channel
– out : Send a message on a channel
– alt : Wait on multiple in/out operations
• Channels are synchronous or unbuffered
• Processes and channels are static
Sanjeev Kumar
ESP: A Language for Programmable Devices
13
A Process Encodes
a State Machine
channel chan1: int
channel chan2: int
process add5 {
$v: int = 0;
while( true) {
in( chan1, v);
out( chan2, v+5);
}
}
• States are implicit
• Events are messages on
channels
• Easy to read & optimize
– Control flow is obvious
Initial
waitChan1
waitChan2
Sanjeev Kumar
ESP: A Language for Programmable Devices
14
Data Types and
Control Constructs
• Data types
– Simple types: int, bool
– Complex data types: records, unions, arrays
– No recursive data types
• Control constructs
– if-then-else, while, etc.
– No functions; Use processes instead
Sanjeev Kumar
ESP: A Language for Programmable Devices
15
Channels for Communication
• Processes communicate only using channels
– Pure message passing communications
• To enforce this
– No shared mutable data structure
• No global variables
• Only immutable objects on channels
• Immutable
Sanjeev Kumar
mutable objects
ESP: A Language for Programmable Devices
16
Memory Management
• Explicit
• Automatic
– malloc/free
– Fast
– Unsafe
– Garbage collection
– More CPU & memory
– Safe
Concurrent program
Safe
Limited CPU & memory
Fast
Sanjeev Kumar
ESP: A Language for Programmable Devices
17
Memory Management Cont’d
• ESP supports explicit management
• Explicit management is difficult
– Global property of program
• ESP makes this a local property
– Objects are not shared by processes
– Objects sent over channels are “copied”
• Use verifiers to check correctness
– Check each process separately
• ESP supports safety through verification
Sanjeev Kumar
ESP: A Language for Programmable Devices
18
Support for Dispatch
channel pktc: union of { ping: int, status: bool }
process A { ...; out( pktc, v); ...}
process B { ...; in( pktc, { ping |> $node}); ...}
process C { ...; in( pktc, { status |> $flag}); ...}
Pattern-matching supports dispatch
Sanjeev Kumar
ESP: A Language for Programmable Devices
19
External Interface
•
•
•
•
C interface: volatile memory, device registers
Spin interface: specify properties to be verified
Traditional approach: function interface
ESP uses channels
– Some channels have external reader or writer
– Unified mechanism (C and Spin)
– Use in/out to block on external events
Sanjeev Kumar
ESP: A Language for Programmable Devices
20
Case Study: VMMC Firmware
• Implemented VMMC using ESP
– 8 processes, 19 channels
– 500 lines ESP + 3000 lines C code
• Modular programs that are easy to maintain
• Order of magnitude less code
Sanjeev Kumar
ESP: A Language for Programmable Devices
21
Outline
•
•
•
•
•
•
Motivation
ESP overview
ESP language
Verifying ESP programs
Performance of ESP programs
Conclusions
Sanjeev Kumar
ESP: A Language for Programmable Devices
22
Using Model-Checking Verifiers
• State-space exploration
– Try all possible scheduling options
• Advantages
– Automatic
– Produces counter example
• Disadvantages
– Computationally expensive (exponential)
• ESP currently uses Spin model checker
Sanjeev Kumar
ESP: A Language for Programmable Devices
23
Spin Model-Checking Verifier
• Designed for software systems
– Supports processes and synchronous channels
• Specify properties to be verified
– Assertions, deadlocks, Linear Temporal Logic
• 3 levels of checking with varying coverage
– Exhaustive
– Partial
– Simulation
Sanjeev Kumar
ESP: A Language for Programmable Devices
24
ESP Approach
• Models extracted automatically
– Reduces programmer effort
– Avoids mismatch
• Debugged using verifier
• Test files can be reused
pgm.ESP
Sanjeev Kumar
pgm1.spin
test1.spin
pgmN.spin
testN.spin
pgm.C
help.C
Develop
and
Test
using
Verifier
ESP Compiler
ESP: A Language for Programmable Devices
Generate
Firmware
25
Extracting Spin Models
• Detailed models
• Memory-safety models
– Detailed model + additional checks
• Abstract models
– Necessary for larger subsystems
– Drop unnecessary details
• Depending on the property being verified
• Abstraction specified by the programmer
• Compiler makes safe conservative approximation
Sanjeev Kumar
ESP: A Language for Programmable Devices
26
Conservative Approximations
in Abstract Models
$b2:
X boolean = true;
...
$b1: boolean = X
b2;
if
:: b1 = true
:: b1 = false
fi
type recT = #record of { int count; }
$r1:
X recT = {0};
if (b)
{ r2 = r1;
X }
...
r1.count
= 5;
X
Sanjeev Kumar
if
:: r2.count = 5
:: skip
fi
ESP: A Language for Programmable Devices
27
Case Study: VMMC Firmware
• Develop and debug retransmission protocol
– Easier to debug than on the network card
– Took 2 days (10 days in earlier implementation)
• Check for memory safety and leaks
– Found deliberately introduced bugs, an earlier bug
• Check for deadlocks
– Hard-to-find bugs
– Found 7 bugs using abstract models
Sanjeev Kumar
ESP: A Language for Programmable Devices
28
Case Study: VMMC Firmware Cont’d
remoteReply
localReq
Time
Memory
Property
(in seconds) (in Mbytes)
Safety
2.3
30.55
Safety
0.1
25.30
reliableSend
All
All
Safety
Deadlock
Deadlock
Process
67.6
84.0
14250.0
34.45
268.35
167.92
Complete
search?
Yes
Yes
Yes
No
No*
* Using partial mode
Sanjeev Kumar
ESP: A Language for Programmable Devices
29
Outline
•
•
•
•
•
•
Motivation
ESP overview
ESP language
Verifying ESP programs
Performance of ESP programs
Conclusions
Sanjeev Kumar
ESP: A Language for Programmable Devices
30
ESP Code Generation
• Compiling for sequential execution
– Combine them [Berry et al., Proebsting et al.]
• No context switching overhead
• Worst-case exponential increase in executable size
– Low-overhead process management
• Small context switching overhead
– Only the program counter needs to be saved
• Small executable
Sanjeev Kumar
ESP: A Language for Programmable Devices
31
ESP Code Generation Cont’d
• C as back-end language
– Generates one large C function
– Links with other functions provided by the
programmer
• Compiler optimizations
– Whole program analysis
• Avoid indirect jumps, unnecessary allocation
– Per process
• Constant folding, copy propagation
Sanjeev Kumar
ESP: A Language for Programmable Devices
32
Case Study: VMMC Firmware
• Measure overhead of using ESP
– Microbenchmarks
– Applications
• Compare performance
– Earlier implementation (vmmcOrig)
– Earlier implementation without fast paths
(vmmcOrigNoFastPaths)
– New implementation using ESP (vmmcESP)
Sanjeev Kumar
ESP: A Language for Programmable Devices
33
Microbenchmarks
• Impact of fast paths
Latency
140
– 4 Bytes: 100%
– 4 Kbyte: 38%
vmmcOrig
vmmcOrigNoFastPaths
vmmcESP
120
100
s
80
60
• Impact of using ESP
40
– 64 Bytes: 35%
– 4 Kbytes: 0%
20
0
4
16
64
256
1K
4K
Message size (in Bytes)
Sanjeev Kumar
ESP: A Language for Programmable Devices
34
Applications
16
vmmcOrig
vmmcOrigNoFastPaths
vmmcESP
Speedup
12
8
4
0
FFT
LU
WaterSpatial
WaterNSq
Barnes
Volrend
SPLASH2 applications on a 16 (4 X 4) node cluster
Fast paths: < 1% on average
Sanjeev Kumar
ESP: 3.5 % on average
ESP: A Language for Programmable Devices
35
Performance Summary
• Significant difference in microbenchmarks
– Most due to the brittle fast paths
– Required the programmer to manually optimize
• Small impact on applications
– Applications are less sensitive
• Microbenchmarks represent worst case
• New functionality can help a lot more
– 40% for SVM applications [ Bilas et al. ]
Sanjeev Kumar
ESP: A Language for Programmable Devices
36
Outline
•
•
•
•
•
•
Motivation
ESP overview
ESP language
Verifying ESP programs
Performance of ESP programs
Conclusions
Sanjeev Kumar
ESP: A Language for Programmable Devices
37
Conclusions
• ESP: Domain-specific language
– Supports concise, modular programs
• Order of magnitude less code
– Extensive testing with Spin
• Develop code
• Check for memory safety & absence of deadlocks
• Effective but has limitations
– Low performance overhead
• 3.5% for applications
• Could use further optimizations
Sanjeev Kumar
ESP: A Language for Programmable Devices
38
Future Directions
• More experience with ESP
– Other devices e.g. Intel IXP
– Other protocols e.g. TCP/IP
• Compiler optimizations
– Selective process inlining
– Support for fast paths
• Using model checking more effectively
– Partial searches
Sanjeev Kumar
ESP: A Language for Programmable Devices
39
Acknowledgements
Kai Li
Andrew Appel
Randy Wang
Doug Clark
Steve
Dirk
Tammo
Edward Felten
Larry Peterson
Jaswinder Pal Singh
Rudro
Patrick Yuanyuan
George
Angelos
Stef
Liviu
Others
Melissa and the rest of administrative staff
Technical staff
Sanjeev Kumar
ESP: A Language for Programmable Devices
40
- The End -
Sanjeev Kumar
ESP: A Language for Programmable Devices
41
Esterel
• Synchronous programming language
– Encode control of reactive systems
• Generate software or hardware
• Deterministic reaction
• But
– Only encodes control flow
– Constraints on the language
– Harder to compile efficiently
Sanjeev Kumar
ESP: A Language for Programmable Devices
42
Teapot
• Domain-specific language
– Implement coherence protocols
• Specify a state machine
• Use continuations to simplify programming
• But
– Only encodes control flow
– Uses handlers: Code fragmentation
– Similar approach would be less modular
Sanjeev Kumar
ESP: A Language for Programmable Devices
43
Promela++
• Language for Layered Network Protocol
– Non-strict extension of promela
• Asynchronous communication
• But
– Layered structure
– Asynchronous: overhead, ordering
– No support for memory management
Sanjeev Kumar
ESP: A Language for Programmable Devices
44
Bandwidth Microbenchmarks
One-way Bandwidth
125
75
50
75
50
25
25
0
0
64
256
1K
4K
16K
64K
Message Size (in Bytes)
Sanjeev Kumar
vmmcOrig
vmmcOrigNoFastpath
vmmcESP
100
MB/s
MB/s
125
vmmcOrig
vmmcOrigNoFastpath
vmmcESP
100
Bidirectional Bandwidth
64
256
1K
4K
16K
64K
Message Size (in Bytes)
ESP: A Language for Programmable Devices
45
Fast Paths
• Challenges
– Identify fast paths in a concurrent program
– Fast path extraction
– Robust fast paths
Sanjeev Kumar
ESP: A Language for Programmable Devices
46