Density threshold in pinwheel scheduling

This page provides the supporting data for Lemma 5 of my paper “Proof of the Density Threshold Conjecture for Pinwheel Scheduling”, which proves the “5/6 conjecture” for pinwheel scheduling.

• Paper: English, Japanese
• Slides (English)
• Presentation (English)

The lemma states that all pinwheel instances consisting of integers up to 21 and satisfying a certain modified density bound are schedulable. Let 𝓑 be the (finite) set of such instances. Rather than listing schedules for all (millions of) instances in 𝓑, we give schedules for a set 𝓒 of 13166 instances. This set 𝓒 fulfills our need, in the following sense:

For each 𝐵 in 𝓑, there is 𝐶_𝐵 in 𝓒 such that 𝑓^𝑛(𝐵) elementwise dominates 𝐶_𝐵, where n is the difference of the lengths of 𝐵 and 𝐶_𝐵, and 𝑓 is the operation of replacing the two largest periods 𝑎 and 𝑏 ≤ 𝑎 by a single (possibly fractional) period 𝑏/2.

Note that this proves the schedulability of 𝐵: Since 𝐶_𝐵 is schedulable, so is 𝑓^𝑛(𝐵) by part 1 of Lemma 3, and hence also 𝐵, again by Lemma 3.

• This file gives the set 𝓒 and a schedule for each instance therein. Each line consists of an instance 𝐶, followed by a colon and then a finite sequence S. The schedule for 𝐶 is the infinite sequence obtained by repeating S. For example, the line “(2 4 4): (1 2 1 3)” means that the pinwheel instance where we have three jobs 1, 2, 3 with periods 2, 4, 4, respectively, has a valid schedule where we repeat doing jobs 1, 2, 1, 3 indefinitely.
• This file lists all elements 𝐵 of 𝓑 in lexicograpical order, and for each of them gives a corresponding 𝐶_𝐵 after “<-”. For example, the line “(5 6 11 15 18 18 18 18 18 19 21) <- (5 6 8 9 9 11 14 16)” means that 𝑓³((5, 6, 11, 15, 18, 18, 18, 18, 18, 19, 21)) = (5, 6, 9, 9, 9.5, 11, 15, 18) dominates (5, 6, 8, 9, 9, 11, 14, 16), which is in 𝓒 and thus can be scheduled by looking up in the first file.