Understanding concurrency with behavioural types
summary
Extraction tool called Miego behavioral types converts Go SSA form using the SSA package into abstract communication types, then compiles those to an LTS and runs a model checker. The system detects global and partial deadlocks, channel-safety errors (double close, send on closed), and eventual reception issues; demoed on two-gopher and dining-philosophers examples, fixes validated (default branch solution), and model-checking outperforms a previous non-model-checker approach (three philosophers: 16 minutes → 5 seconds); open-source release is planned.
AI-written summary · about
chapters (26)
- 0:00Introduction
- 0:35concurrency in Go
- 3:35implementation
- 4:02runtime dialogue detector
- 4:31deadlock detector
- 5:01partial deadlock
- 5:48runtime deadlock detection
- 8:01research aim
- 8:26channel operations
- 10:13process calculus
- 12:08behavioral types
- 14:13model extraction
- 15:32model checker
- 17:02example
- 21:48channel safety
- 24:17eventual reception
- 26:01dining philosophers
- 31:53conclusion
- 32:38questions
- 33:50model checkers
- 36:19limitations
- 37:43dining philosophers problem
- 39:55for now
- 41:52Behavioural types
- 42:38Solving the halting problem
- 44:56Termination checks
related talks
29mUsing Formal Reasoning to Build Concurrent Go Systems
29mVerifying Concurrent Go Code in Coq with Goose
20mMessage-Observing Sessions
30mCalculating Compilers for Concurrency
25mA Lazy, Concurrent Convertibility Checker
22mMechanised Semantics for Gated Static Single Assignment
14mSynchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
30mAnalyzing Programs with SMT Solvers