Automated Correctness Analysis for core.async
summary
Discourje lets Clojure programs declare channel protocols as textual sequence diagrams and wires a thin instrumentation layer around core.async so a runtime monitor verifies sends/receives. Forbidden puts/takes immediately throw an exception; non-compliance checks are sound and complete while deadlock detection is sound but incomplete. Demo uses a rock‑paper‑scissors example; benchmarks show overhead from under 5% to about 3–5x slowdown. Current state is a working prototype for debugging and testing.
AI-written summary · about
chapters (12)
- 0:00Start
- 5:11Plan for this Presentation
- 5:35Crash Course
- 8:58Function for the Judge
- 9:46Glue Code
- 11:38Programming Mistakes
- 16:36Automated Correctness Analysis for Core Async
- 17:24Instrumentation
- 21:32Deadlock
- 25:43Non-Compliance
- 26:44Conclusion
- 27:51Production Readiness
related talks
03h 29mConcurrency with Clojure
44mClojure core.async Evolution
01h 08mSimplifying Concurrent Programming via Synchronization Synthesis
34mComparing the Actor model & CSP concurrency with Elixir & Clojure
31mSynthesizing fine-grained synchronization protocols for implicit monitors
01h 04mcore.async: Concurrency without Callbacks
40mEvolving Clojure with Virtual Threads
47mDeadlocks: The Dark Side of Concurrency