Controlled Scheduling of Concurrent Elixir Programs
summary
Library implements a user-level scheduler for Elixir that instruments KV-style calls via the Elixir macro facility and exposes scheduling algorithms: random search, depth-first search, and a novel random-schedule-selection explorer. It runs the program under a scheduler process that grants put/get permissions, records repeatable execution traces and choice points, and can exhaust or randomly sample schedules. Applied to snapshot algorithms: a deterministic run of ~1,000 trials misses a bug that a randomized run exposes after roughly ≈30 scheduling decisions; prototype uses a balanced tree for schedule storage and is on GitLab.
AI-written summary · about
chapters (10)
- 0:00Controlled scheduling in Elixir
- 1:48Motivating example for snapshot APIs
- 8:35Linearizability and correctness
- 13:07Limitations of deterministic scheduling
- 14:14Randomizing the scheduler
- 19:12Model checking with controlled scheduling
- 23:27Randomized schedule exploration
- 25:36Tool for practical testing
- 26:41Research group and resources
- 27:02Q&A
related talks
12mComposing Schedulers using Effect Handlers
16mscx_chaos: Pushing the sched_ext API to schedule badly
08mUnlucky Simulation
06mLightning talk - Parallel static analysis in Elixir
37mReal-time Scheduling Fault Simulation
15mLearning-Based Controlled Concurrency Testing
33mLets Generate Tests
42mRuntime scheduling: theory and reality