Responsive Parallelism with Dynamic and First-Class Priorities
PriML, a language developed in recent work on {\em responsive parallelism}, extends traditional fine-grained parallel languages such as Cilk by allowing programmers to annotate threads with {\em priorities}. Programmers thus get the substantial throughput benefits of lightweight threads scheduled by a user-level runtime, while retaining the ability to use threads for responsive applications typically programmed with lower-level threading systems. PriML's type system guarantees the absence of {\em priority inversions}, costly performance errors in which high-priority threads are delayed by low-priority threads, enabling formal bounds on throughput and responsiveness, but at the cost of expressiveness: threads may not change priority once spawned and the priority of a thread is specified as a priority literal in the code (i.e., priorities are not {\em first-class}). This work relaxes the two assumptions above by tracking {\em sets of priorities} using techniques drawn from the literature on refinement types. We extend the graph-based cost models of responsive parallelism to incorporate first-class and changing priorities, and prove bounds on the throughput and responsiveness of well-typed programs in our extended language. We implement our type system extensions in the PriML compiler, and demonstrate the benefits of the extension using a concurrent web server as a case study.
Fri 19 JunDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:40 | Verified Compilation and Type SystemsPLDI Research Papers at Flatirons 3 Chair(s): Charles Yuan University of Wisconsin-Madison | ||
11:00 20mTalk | Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow PLDI Research Papers Zhengyao Lin Carnegie Mellon University, Yi Cai University of Maryland at College Park, Milijana Surbatovich University of Maryland at College Park DOI | ||
11:20 20mTalk | Compiling to Recurrent Neurons PLDI Research Papers Joey Velez-Ginorio University of Pennsylvania, Nada Amin Harvard University, Konrad Kording University of Pennsylvania, Steve Zdancewic University of Pennsylvania DOI | ||
11:40 20mTalk | [TOPLAS] Denotation-based Compositional Compiler Verification PLDI Research Papers Zhang Cheng Shanghai Jiao Tong University, Jiyang Wu , Di Wang Peking University, Qinxiang Cao Shanghai Jiao Tong University | ||
12:00 20mTalk | Responsive Parallelism with Dynamic and First-Class Priorities PLDI Research Papers Marelle León Illinois Institute of Technology, My Dinh Illinois Institute of Technology, Stefan K. Muller University of Connecticut DOI | ||
12:20 20mTalk | Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types PLDI Research Papers Songlin Jia Purdue University, Guannan Wei Tufts University, Siyuan He Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University DOI | ||