Proof of the density threshold conjecture for pinwheel scheduling

In the pinwheel scheduling problem, each task i is associated with a positive integer a _i called its period, and we want to (perpetually) schedule one task per day so that each task i is performed at least once every a _i days. An obvious necessary condition for schedulability is that the density, defined as the sum of execution rates 1/ a _i , does not exceed 1. We prove that all instances with density not exceeding 5/6 are schedulable, as was conjectured by Chan and Chin in 1993. Like some of the known partial progress toward the conjecture, our proof involves computer search for schedules for a large but finite set of instances. A key idea in our reduction to these finite cases is to generalize the problem to fractional (noninteger) periods in an appropriate way. As byproducts of our ideas, we obtain a simple proof that every instance with two distinct periods and density at most 1 is schedulable, as well as a fast algorithm for the bamboo garden trimming problem with approximation ratio 4/3.