Modeling IPC in Fluke

• Large, important component of kernel
• IPC protocol is complicated:
  • fine-grained locking
  • rollback (thread cancel)
  • optimized