|
| 1 | +Scheduler monitors |
| 2 | +================== |
| 3 | + |
| 4 | +- Name: sched |
| 5 | +- Type: container for multiple monitors |
| 6 | +- Author: Gabriele Monaco < [email protected]>, Daniel Bristot de Oliveira < [email protected]> |
| 7 | + |
| 8 | +Description |
| 9 | +----------- |
| 10 | + |
| 11 | +Monitors describing complex systems, such as the scheduler, can easily grow to |
| 12 | +the point where they are just hard to understand because of the many possible |
| 13 | +state transitions. |
| 14 | +Often it is possible to break such descriptions into smaller monitors, |
| 15 | +sharing some or all events. Enabling those smaller monitors concurrently is, |
| 16 | +in fact, testing the system as if we had one single larger monitor. |
| 17 | +Splitting models into multiple specification is not only easier to |
| 18 | +understand, but gives some more clues when we see errors. |
| 19 | + |
| 20 | +The sched monitor is a set of specifications to describe the scheduler behaviour. |
| 21 | +It includes several per-cpu and per-task monitors that work independently to verify |
| 22 | +different specifications the scheduler should follow. |
| 23 | + |
| 24 | +To make this system as straightforward as possible, sched specifications are *nested* |
| 25 | +monitors, whereas sched itself is a *container*. |
| 26 | +From the interface perspective, sched includes other monitors as sub-directories, |
| 27 | +enabling/disabling or setting reactors to sched, propagates the change to all monitors, |
| 28 | +however single monitors can be used independently as well. |
| 29 | + |
| 30 | +It is important that future modules are built after their container (sched, in |
| 31 | +this case), otherwise the linker would not respect the order and the nesting |
| 32 | +wouldn't work as expected. |
| 33 | +To do so, simply add them after sched in the Makefile. |
| 34 | + |
| 35 | +Specifications |
| 36 | +-------------- |
| 37 | + |
| 38 | +The specifications included in sched are currently a work in progress, adapting the ones |
| 39 | +defined in by Daniel Bristot in [1]. |
| 40 | + |
| 41 | +Currently we included the following: |
| 42 | + |
| 43 | +Monitor tss |
| 44 | +~~~~~~~~~~~ |
| 45 | + |
| 46 | +The task switch while scheduling (tss) monitor ensures a task switch happens |
| 47 | +only 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 | + |
| 63 | +Monitor sco |
| 64 | +~~~~~~~~~~~ |
| 65 | + |
| 66 | +The scheduling context operations (sco) monitor ensures changes in a task state |
| 67 | +happen 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 | + |
| 84 | +Monitor snroc |
| 85 | +~~~~~~~~~~~~~ |
| 86 | + |
| 87 | +The set non runnable on its own context (snroc) monitor ensures changes in a |
| 88 | +task state happens only in the respective task's context. This is a per-task |
| 89 | +monitor:: |
| 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 | + |
| 105 | +Monitor scpd |
| 106 | +~~~~~~~~~~~~ |
| 107 | + |
| 108 | +The schedule called with preemption disabled (scpd) monitor ensures schedule is |
| 109 | +called 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 | + |
| 126 | +Monitor snep |
| 127 | +~~~~~~~~~~~~ |
| 128 | + |
| 129 | +The schedule does not enable preempt (snep) monitor ensures a schedule call |
| 130 | +does 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 | + |
| 147 | +Monitor sncid |
| 148 | +~~~~~~~~~~~~~ |
| 149 | + |
| 150 | +The schedule not called with interrupt disabled (sncid) monitor ensures |
| 151 | +schedule 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 | + |
| 168 | +References |
| 169 | +---------- |
| 170 | + |
| 171 | +[1] - https://bristot.me/linux-task-model |
0 commit comments