[MUSIC] This lesson is about verifying monotonic schedulers mathematically. We have learned that monotonic schedulers dynamically adjust the priorities of the tasks based on parameters in the tasks such as period or deadline. With this feature assumed, we can construct a schedulability test. The mathematical verifier schedule, we don't have to run this system and this is what this lesson is about. Monotonic schedulers are easier to verify than the plain fixed priority schedulers, because their behavior is more deterministic. In this lecture, we will provide methods for verifying monotonic schedulers given certain thought sets. We must, however, assume that the number of thoughts is constant. Jobs are independent. Periodic and preemptable and all the jobs are schedulable at their release time. The most simple verification method is to calculate the system's utilization and this is done by summing the utilization of all the tasks, and the total utilization cannot be more than one for a single processor system. If the total utilization is more than one, the system is overloaded and it's impossible to find a feasible schedule. Checking the total utilization provides, however, no guarantees for a system being feasible. It only gives us a result of being guaranteed a non-feasible in case the utilization is more than one. Systems with utilization less than one can also be non-feasible. So we, therefore, need a schedulability test to determine if a set of tasks can be scheduled with a given algorithm. And if the test is computationally efficient, it can also be done at runtime. Assume we have a set of independent periodic tasks with periods Pi, execution time ei and relative deadline Di and the user pre-emptive algorithm. The feasibility of a schedule can be exhaustively proven by simulating a timeline of length 2H + max {Pi} + max{Di}. They must simulate two hyper-periods. It goes a system in the first type of period can be feasible. But if the deadline of the last task is inside the second hyper-period, this must also be taken into account. In practice, this can be computationally heavy and it would be nice with some simple verification methods. Less exact twos can give a much faster result and this is something we would like to look at, and RM test is such a method. The RM test can verify a guaranteed timeline for RM systems with the previously stated assumptions of the tasks. We define a limit called a URM, as a utilization limit under which the system is guaranteed feasible. For the above assumptions in RM system, the feasibility can be proven by comparing the total utilization U to the URM function. And a system is guaranteed feasible, if the utilization u is less or equal to URM for n tasks. This is equal to n multiplied by the parentheses 2 to the power of 1/n-1. So, let's write it out. A, consider the following task set T1, T2 and T3 with the parameters shown. So, the total utilization of this system is 1/5+0.5/4+1.2/6 and this equal to 0.525. The URM for 3 task is then 3(2 to the power of 1/3-1)=0.779. Since U now is less than URM for three task, the system is guaranteed feasible. We'll take another example. Consider the following task set, T1, T2 and T3 with the parameters shown again. The total utilization of this is 1.9/5+1.5/4+2.2/6=1.12. Since you know it's larger than one, we don't even have to worry about the URM, because the system is guaranteed not feasible. And finally, another example. Consider the following task at T1, T2t and T3 with the parameter shown. The total utilization of this system is 1/4+1/6+1/2=0.917. Since U now is less than one, but it is larger that URM. Feasibility or overloading cannot be guaranteed. More rigorous tests must then be applied on such a system to verify whether it is feasible and this will be covered in the following lectures. We have in this lesson seen a verification test for periodic jobs using the right monotonic scheduler. This test can mathematically prove, if a schedule is feasible without having to schedule the whole system. You also saw the limitations of the test in form of uncertain feasibility for some outcomes. And in other lessons, we will extend this test to these scenarios as well. So good job in completing this module and your next assignment is now in the ready state, and you can test your newly learned skill from this module. So, hurry up.