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 𝐶_{𝐵}, wherenis 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 𝑓^{3}((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.