Responsive Parallelism with Dynamic and First-Class Priorities
summary
Extends PriML to make priorities first class and dynamically changeable, adding a change command and typing each command with start/duration/end refinements (so threads carry a set of possible priorities, e.g., union of durations). Uses liquid-style refinement type inference, a DAG-based cost semantics and a well-formedness theorem that rules out priority inversion and yields formal throughput/response-time bounds. Implements extensions in the PriML compiler with a multi-core OCaml backend and validates them by fixing a priority-bug in a concurrent web server; artifacts evaluated and reusable.
AI-written summary · about
chapters (12)
- 0:00Responsive parallelism intro
- 1:01Cooperative vs competitive multithreading
- 2:06Primal commands and priority inversion
- 3:54Primal limitations before extension
- 4:58Need for dynamic priorities
- 5:41Challenges with dynamic priorities
- 6:48Refinement types for priorities
- 8:54Command typing with refinements
- 11:05Thread typing and sync rules
- 12:35Example thread type derivation
- 13:38Proving efficient response time
- 14:41Primal’s new implementation and demo
related talks
29mPredicate Dispatch
18mParallelism in a Region Inference Context
14mAchieving High-Performance the Functional Way - A Functional Pearl on Expressing High...
43mPriority Search Queues: 1.5 dimensional Tree Search
36mDependently Typed Multi-Stage Programming, Revisited
23mCorrect Compilation of Concurrent C Code
20mPulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
16mPomsets with Preconditions: A Simple Model of Relaxed Memory