# Early Deadline First (EDF) scheduling in real-time systems feasibility test proof

I am trying to prove Theorem 6.2 on page 127 of the book Real-Time Systems by Jane W. S. Liu:

http://www.cse.hcmut.edu.vn/~thai/books/2000%20_%20Liu-%20Real%20Time%20Systems.pdf

It is based on Early Deadline First(EDF) scheduling.

It says on the book that the proof is similar to the proof for Theorem 6.1 on page 124-126. However, I am still stuck.

Here is what I have so far:

• This is not the right forum for this question. I would try stackoverflow.com or math.stackexchange.com – mhaselup Nov 3 '20 at 5:27
• from a first look I noticed something that may be wrong in the sums indices. A sum index is bound not free. So how come you are using k =/= l while k is an index in a sum and l is an index in an independent sum? – Paul Ghobril Nov 3 '20 at 5:49
• It is just showing the tasks in the three terms in 1st eq. are mutually exclusive – Matt Nov 3 '20 at 6:54
• @mhaselup RTOS questions are on-topic here. – Lundin Nov 3 '20 at 7:18

## 1 Answer

Yhe text you quote says it is only a sufficient condition not a necessary condition. If Δ>1 then that implies that t < tΔ + any positive number. Which is exactly what you've proved.

• No, it means that if its density(Δ) <= 1 then tasks can be feasibly scheduled, so density <= 1 is a sufficient condition for feasible scheduling. What I am proving is the contrapositive: if tasks CANNOT be feasibly scheduled(deadline(s) missed) then density > 1. – Matt Nov 4 '20 at 0:52
• The second last sentence may be misleading. I changed it to "So I prove up to..." – Matt Nov 4 '20 at 1:27