1Scheduler monitors 2================== 3 4- Name: sched 5- Type: container for multiple monitors 6- Author: Gabriele Monaco <gmonaco@redhat.com>, Daniel Bristot de Oliveira <bristot@kernel.org> 7 8Description 9----------- 10 11Monitors describing complex systems, such as the scheduler, can easily grow to 12the point where they are just hard to understand because of the many possible 13state transitions. 14Often it is possible to break such descriptions into smaller monitors, 15sharing some or all events. Enabling those smaller monitors concurrently is, 16in fact, testing the system as if we had one single larger monitor. 17Splitting models into multiple specification is not only easier to 18understand, but gives some more clues when we see errors. 19 20The sched monitor is a set of specifications to describe the scheduler behaviour. 21It includes several per-cpu and per-task monitors that work independently to verify 22different specifications the scheduler should follow. 23 24To make this system as straightforward as possible, sched specifications are *nested* 25monitors, whereas sched itself is a *container*. 26From the interface perspective, sched includes other monitors as sub-directories, 27enabling/disabling or setting reactors to sched, propagates the change to all monitors, 28however single monitors can be used independently as well. 29 30It is important that future modules are built after their container (sched, in 31this case), otherwise the linker would not respect the order and the nesting 32wouldn't work as expected. 33To do so, simply add them after sched in the Makefile. 34 35Specifications 36-------------- 37 38The specifications included in sched are currently a work in progress, adapting the ones 39defined in by Daniel Bristot in [1]. 40 41Currently we included the following: 42 43Monitor tss 44~~~~~~~~~~~ 45 46The task switch while scheduling (tss) monitor ensures a task switch happens 47only in scheduling context, that is inside a call to `__schedule`:: 48 49 | 50 | 51 v 52 +-----------------+ 53 | thread | <+ 54 +-----------------+ | 55 | | 56 | schedule_entry | schedule_exit 57 v | 58 sched_switch | 59 +--------------- | 60 | sched | 61 +--------------> -+ 62 63Monitor sco 64~~~~~~~~~~~ 65 66The scheduling context operations (sco) monitor ensures changes in a task state 67happen only in thread context:: 68 69 70 | 71 | 72 v 73 sched_set_state +------------------+ 74 +------------------ | | 75 | | thread_context | 76 +-----------------> | | <+ 77 +------------------+ | 78 | | 79 | schedule_entry | schedule_exit 80 v | 81 | 82 scheduling_context -+ 83 84Monitor snroc 85~~~~~~~~~~~~~ 86 87The set non runnable on its own context (snroc) monitor ensures changes in a 88task state happens only in the respective task's context. This is a per-task 89monitor:: 90 91 | 92 | 93 v 94 +------------------+ 95 | other_context | <+ 96 +------------------+ | 97 | | 98 | sched_switch_in | sched_switch_out 99 v | 100 sched_set_state | 101 +------------------ | 102 | own_context | 103 +-----------------> -+ 104 105Monitor scpd 106~~~~~~~~~~~~ 107 108The schedule called with preemption disabled (scpd) monitor ensures schedule is 109called with preemption disabled:: 110 111 | 112 | 113 v 114 +------------------+ 115 | cant_sched | <+ 116 +------------------+ | 117 | | 118 | preempt_disable | preempt_enable 119 v | 120 schedule_entry | 121 schedule_exit | 122 +----------------- can_sched | 123 | | 124 +----------------> -+ 125 126Monitor snep 127~~~~~~~~~~~~ 128 129The schedule does not enable preempt (snep) monitor ensures a schedule call 130does not enable preemption:: 131 132 | 133 | 134 v 135 preempt_disable +------------------------+ 136 preempt_enable | | 137 +------------------ | non_scheduling_context | 138 | | | 139 +-----------------> | | <+ 140 +------------------------+ | 141 | | 142 | schedule_entry | schedule_exit 143 v | 144 | 145 scheduling_contex -+ 146 147Monitor sncid 148~~~~~~~~~~~~~ 149 150The schedule not called with interrupt disabled (sncid) monitor ensures 151schedule is not called with interrupt disabled:: 152 153 | 154 | 155 v 156 schedule_entry +--------------+ 157 schedule_exit | | 158 +----------------- | can_sched | 159 | | | 160 +----------------> | | <+ 161 +--------------+ | 162 | | 163 | irq_disable | irq_enable 164 v | 165 | 166 cant_sched -+ 167 168References 169---------- 170 171[1] - https://bristot.me/linux-task-model 172