Scheduler 모니터

설명

`sched`는 Gabriele Monaco와 Daniel Bristot de Oliveira가 작성한 여러 monitor의 컨테이너이다. scheduler처럼 복잡한 시스템을 하나의 monitor로 설명하면 가능한 state transition이 많아져 이해하기 어려워질 수 있다.

이런 설명은 일부 또는 모든 event를 공유하는 더 작은 monitor로 나눌 수 있다. 작은 monitor들을 동시에 활성화하면 하나의 큰 monitor로 시스템을 시험하는 것과 같은 효과를 얻는다. 여러 명세로 분리하면 이해하기 쉬울 뿐 아니라 오류가 발생했을 때 원인을 좁힐 단서도 더 많아진다.

`sched` monitor는 scheduler 동작을 기술하는 명세 모음이다. 여러 per-CPU 및 per-task monitor가 독립적으로 작동하면서 scheduler가 따라야 할 서로 다른 명세를 검증한다.

구조를 단순하게 유지하기 위해 각 sched 명세는 nested monitor이고 `sched` 자체는 container이다. 인터페이스에서 `sched` 아래에 다른 monitor가 하위 디렉터리로 나타난다. `sched`를 enable 또는 disable하거나 reactor를 설정하면 모든 하위 monitor에 변경이 전파되지만, 개별 monitor도 독립적으로 사용할 수 있다.

향후 module은 container인 `sched`보다 뒤에 build해야 한다. 그렇지 않으면 linker가 순서를 지키지 않아 nesting이 예상대로 작동하지 않는다. Makefile에서 새 module을 `sched` 뒤에 추가하면 된다.

Scheduler monitors
==================

- Name: sched
- Type: container for multiple monitors
- Author: Gabriele Monaco <[email protected]>, Daniel Bristot de Oliveira <[email protected]>

Description
-----------

Monitors describing complex systems, such as the scheduler, can easily grow to
the point where they are just hard to understand because of the many possible
state transitions.
Often it is possible to break such descriptions into smaller monitors,
sharing some or all events. Enabling those smaller monitors concurrently is,
in fact, testing the system as if we had one single larger monitor.
Splitting models into multiple specification is not only easier to
understand, but gives some more clues when we see errors.

The sched monitor is a set of specifications to describe the scheduler behaviour.
It includes several per-cpu and per-task monitors that work independently to verify
different specifications the scheduler should follow.

To make this system as straightforward as possible, sched specifications are *nested*
monitors, whereas sched itself is a *container*.
From the interface perspective, sched includes other monitors as sub-directories,
enabling/disabling or setting reactors to sched, propagates the change to all monitors,
however single monitors can be used independently as well.

It is important that future modules are built after their container (sched, in
this case), otherwise the linker would not respect the order and the nesting
wouldn't work as expected.
To do so, simply add them after sched in the Makefile.

명세 개요

`sched`에 포함된 명세는 현재 진행 중인 작업이며, Daniel Bristot가 참고 문헌 [1]에서 정의한 모델을 적용하고 있다.

Specifications
--------------

The specifications included in sched are currently a work in progress, adapting the ones
defined in by Daniel Bristot in [1].

Currently we included the following:

sco monitor

scheduling context operations(`sco`) monitor는 task state 변경이 thread context에서만 일어나도록 보장한다.

`sched_set_state`는 `thread_context`에서만 허용된다. `schedule_entry` 이후 `scheduling_context`에 있는 동안에는 task state 변경을 허용하지 않고, `schedule_exit`으로 돌아와야 다시 허용한다.

Monitor sco
~~~~~~~~~~~

The scheduling context operations (sco) monitor ensures changes in a task state
happen only in thread context::


                        |
                        |
                        v
    sched_set_state   +------------------+
  +------------------ |                  |
  |                   |  thread_context  |
  +-----------------> |                  | <+
                      +------------------+  |
                        |                   |
                        | schedule_entry    | schedule_exit
                        v                   |
                                            |
                       scheduling_context  -+

snroc monitor

set non runnable on its own context(`snroc`) monitor는 task state 변경이 해당 task 자신의 context에서만 발생하도록 보장하는 per-task monitor이다.

`sched_switch_in` 뒤의 `own_context`에서만 `sched_set_state`를 허용한다. task가 `sched_switch_out`으로 나가 `other_context`가 되면 다른 task의 context에서는 그 상태를 바꿀 수 없다.

Monitor snroc
~~~~~~~~~~~~~

The set non runnable on its own context (snroc) monitor ensures changes in a
task state happens only in the respective task's context. This is a per-task
monitor::

                        |
                        |
                        v
                      +------------------+
                      |  other_context   | <+
                      +------------------+  |
                        |                   |
                        | sched_switch_in   | sched_switch_out
                        v                   |
    sched_set_state                         |
  +------------------                       |
  |                       own_context       |
  +----------------->                      -+

scpd monitor

schedule called with preemption disabled(`scpd`) monitor는 `schedule`이 preemption disabled 상태에서 호출되는지 확인한다.

초기 `cant_sched`에서는 schedule event를 허용하지 않는다. `preempt_disable` 뒤 `can_sched`에서 `schedule_entry`와 `schedule_exit`을 허용하고, `preempt_enable`이면 다시 `cant_sched`로 돌아간다.

Monitor scpd
~~~~~~~~~~~~

The schedule called with preemption disabled (scpd) monitor ensures schedule is
called with preemption disabled::

                       |
                       |
                       v
                     +------------------+
                     |    cant_sched    | <+
                     +------------------+  |
                       |                   |
                       | preempt_disable   | preempt_enable
                       v                   |
    schedule_entry                         |
    schedule_exit                          |
  +-----------------      can_sched        |
  |                                        |
  +---------------->                      -+

snep monitor

schedule does not enable preempt(`snep`) monitor는 한 번의 schedule 호출이 preemption을 활성화하지 않는지 보장한다.

`preempt_disable`과 `preempt_enable`은 schedule 밖의 `non_scheduling_context`에서만 관찰한다. `schedule_entry`부터 `schedule_exit`까지의 `scheduling_context`에서는 preemption을 켜는 전이가 없어야 한다.

Monitor snep
~~~~~~~~~~~~

The schedule does not enable preempt (snep) monitor ensures a schedule call
does not enable preemption::

                        |
                        |
                        v
    preempt_disable   +------------------------+
    preempt_enable    |                        |
  +------------------ | non_scheduling_context |
  |                   |                        |
  +-----------------> |                        | <+
                      +------------------------+  |
                        |                         |
                        | schedule_entry          | schedule_exit
                        v                         |
                                                  |
                          scheduling_contex      -+

sts monitor

schedule implies task switch(`sts`) monitor는 task switch가 scheduling context 안에서 최대 한 번만 일어나도록 보장한다. 또한 scheduling은 interrupt enabled 상태에서 시작하되 interrupt가 disabled되기 전에는 task switch가 일어날 수 없도록 검사한다.

scheduler가 다음 실행 task로 이전과 같은 task를 고르면 실제 task switch는 일어나지 않지만, 이 경우에도 interrupt는 비활성화된다.

`can_sched`에서는 `irq_disable` 또는 `irq_entry`로 `cant_sched`에 들어가고, `irq_enable`로 돌아온다. schedule 중 `irq_entry`가 발생하면 `in_irq`에서 중첩 interrupt를 처리한 뒤 원래 경로로 복귀한다.

`disable_to_switch`에서 `sched_switch`를 한 번 관찰하면 `switching`으로 이동하므로 두 번째 switch를 허용하지 않는다. 실제 switch가 없어도 `irq_enable` 경로를 통해 `enable_to_exit`으로 갈 수 있다.

Monitor sts
~~~~~~~~~~~

The schedule implies task switch (sts) monitor ensures a task switch happens
only in scheduling context and up to once, as well as scheduling occurs with
interrupts enabled but no task switch can happen before interrupts are
disabled. When the next task picked for execution is the same as the previously
running one, no real task switch occurs but interrupts are disabled nonetheless::

    irq_entry                      |
     +----+                        |
     v    |                        v
 +------------+ irq_enable    #===================#   irq_disable
 |            | ------------> H                   H   irq_entry
 | cant_sched | <------------ H                   H   irq_enable
 |            | irq_disable   H     can_sched     H --------------+
 +------------+               H                   H               |
                              H                   H               |
            +---------------> H                   H <-------------+
            |                 #===================#
            |                   |
      schedule_exit             | schedule_entry
            |                   v
            |   +-------------------+     irq_enable
            |   |    scheduling     | <---------------+
            |   +-------------------+                 |
            |     |                                   |
            |     | irq_disable                    +--------+  irq_entry
            |     v                                |        | --------+
            |   +-------------------+  irq_entry   | in_irq |         |
            |   |                   | -----------> |        | <-------+
            |   | disable_to_switch |              +--------+
            |   |                   | --+
            |   +-------------------+   |
            |     |                     |
            |     | sched_switch        |
            |     v                     |
            |   +-------------------+   |
            |   |     switching     |   | irq_enable
            |   +-------------------+   |
            |     |                     |
            |     | irq_enable          |
            |     v                     |
            |   +-------------------+   |
            +-- |  enable_to_exit   | <-+
                +-------------------+
                  ^               | irq_disable
                  |               | irq_entry
                  +---------------+ irq_enable

nrp monitor

need resched preempts(`nrp`) monitor는 preemption에 `need_resched`가 필요함을 보장한다. userspace로 복귀하는 동안의 preemption은 `sssw` monitor의 `sched_switch_yield`와 구분할 수 없으므로 kernel preemption만 고려한다.

kernel preemption은 `preempt_enable` 또는 interrupt 종료 같은 경로에서 preemption flag가 true인 채 `__schedule`이 호출되는 경우이다. 이런 preemption은 rescheduling 필요가 설정된 뒤 발생한다. userspace preemption만 일으키는 flag의 lazy 변형에는 이 규칙을 적용하지 않는다.

`schedule_entry_preempt`는 task switch를 일으킬 수도 있고 일으키지 않을 수도 있다. switch가 없으면 task가 preemption context에서 scheduler를 거쳤지만 다음 실행 task로 다시 선택된 것이다. scheduler가 실행되었으므로 reschedule 필요는 지워진다.

`any_thread_running` state는 monitored task가 실행 중이 아님을 뜻하지 않는다. 이 monitor는 scheduling 결과를 추적하지 않기 때문이다.

이론상 preemption은 `need_resched` flag가 설정된 뒤에만 가능하지만, 실제로는 flag가 없는 preemption을 볼 수 있는 특정 중첩 조건이 있다.

need_resched
                 preempt_schedule()
                                         preempt_schedule_irq()
                                                 __schedule()
!need_resched
                         __schedule()

flag가 설정된 상태에서 표준 preemption이 시작된 뒤 scheduling 전에 interrupt가 발생할 수 있다. interrupt 종료 경로가 먼저 schedule을 수행하면 `need_resched` flag가 지워진다. 이후 선점되었던 task가 다시 실행될 때 앞서 시작한 표준 preemption이 flag 없이 재개된다.

monitor는 이를 `nested_preemption`으로 간주해 flag를 다시 설정하지 않고도 한 번 더 preemption을 허용한다. 이 완화는 실제 `nested_preemption`이 아닌 경우를 놓치는 false negative를 만들 수 있지만, monitor를 더 견고하게 하고 다른 시나리오를 검증할 수 있게 한다.

이 상황의 정확한 시작점을 찾기 어려우므로 monitor는 실제 interrupt가 없었더라도 단순화를 위해 `preempt_irq`에서 시작한다.

arm64에서는 preemption count의 `need_resched` flag 동작 방식 때문에 이 monitor가 불안정하다. 위 우회가 있어도 flag가 설정되지 않은 preemption을 자주 기록하므로 현재 arm64에서는 기본적으로 비활성화되어 있다.

Monitor nrp
-----------

The need resched preempts (nrp) monitor ensures preemption requires
``need_resched``. Only kernel preemption is considered, since preemption
while returning to userspace, for this monitor, is indistinguishable from
``sched_switch_yield`` (described in the sssw monitor).
A kernel preemption is whenever ``__schedule`` is called with the preemption
flag set to true (e.g. from preempt_enable or exiting from interrupts). This
type of preemption occurs after the need for ``rescheduling`` has been set.
This is not valid for the *lazy* variant of the flag, which causes only
userspace preemption.
A ``schedule_entry_preempt`` may involve a task switch or not, in the latter
case, a task goes through the scheduler from a preemption context but it is
picked as the next task to run. Since the scheduler runs, this clears the need
to reschedule. The ``any_thread_running`` state does not imply the monitored
task is not running as this monitor does not track the outcome of scheduling.

In theory, a preemption can only occur after the ``need_resched`` flag is set. In
practice, however, it is possible to see a preemption where the flag is not
set. This can happen in one specific condition::

  need_resched
                   preempt_schedule()
                                           preempt_schedule_irq()
                                                   __schedule()
  !need_resched
                           __schedule()

In the situation above, standard preemption starts (e.g. from preempt_enable
when the flag is set), an interrupt occurs before scheduling and, on its exit
path, it schedules, which clears the ``need_resched`` flag.
When the preempted task runs again, the standard preemption started earlier
resumes, although the flag is no longer set. The monitor considers this a
``nested_preemption``, this allows another preemption without re-setting the
flag. This condition relaxes the monitor constraints and may catch false
negatives (i.e. no real ``nested_preemptions``) but makes the monitor more
robust and able to validate other scenarios.
For simplicity, the monitor starts in ``preempt_irq``, although no interrupt
occurred, as the situation above is hard to pinpoint::

    schedule_entry
    irq_entry                 #===========================================#
  +-------------------------- H                                           H
  |                           H                                           H
  +-------------------------> H             any_thread_running            H
                              H                                           H
  +-------------------------> H                                           H
  |                           #===========================================#
  | schedule_entry              |                       ^
  | schedule_entry_preempt      | sched_need_resched    | schedule_entry
  |                             |                      schedule_entry_preempt
  |                             v                       |
  |                           +----------------------+  |
  |                      +--- |                      |  |
  |   sched_need_resched |    |     rescheduling     | -+
  |                      +--> |                      |
  |                           +----------------------+
  |                             | irq_entry
  |                             v
  |                           +----------------------+
  |                           |                      | ---+
  |                      ---> |                      |    | sched_need_resched
  |                           |      preempt_irq     |    | irq_entry
  |                           |                      | <--+
  |                           |                      | <--+
  |                           +----------------------+    |
  |                             | schedule_entry          | sched_need_resched
  |                             | schedule_entry_preempt  |
  |                             v                         |
  |                           +-----------------------+   |
  +-------------------------- |    nested_preempt     | --+
                              +-----------------------+
                                ^ irq_entry         |
                                +-------------------+

Due to how the ``need_resched`` flag on the preemption count works on arm64,
this monitor is unstable on that architecture, as it often records preemption
when the flag is not set, even in presence of the workaround above.
For the time being, the monitor is disabled by default on arm64.

sssw monitor

set state sleep and wakeup(`sssw`) monitor는 `set_state`로 `sleepable`이 된 task가 실제로 잠들고, 잠든 task는 다시 실행되기 전에 wakeup이 필요함을 보장한다.

`switch_suspend`는 task가 명시적으로 `sleepable` state를 설정한 뒤 스스로 잠드는 전이다. suspend 뒤에는 다시 switch in되기 전에 `waking` state를 거쳐 깨워져야 한다. switch 전에 wakeup되거나 `runnable`로 설정되면 `sleepable` 설정을 되돌릴 수 있다.

`switch_blocking`은 task가 sleeping RT lock을 기다리는 `switch_suspend`의 특수 사례이며 `PREEMPT_RT`에서만 해당한다. wakeup event와 set state event의 race 때문에 실제로 task가 sleepable이 아닌데 모델이 이 switch로 인식할 수 있다. 이는 SMP model의 제한이며 우회책은 시스템을 느리게 할 수 있다.

`switch_preempt`는 kernel preemption으로 발생한 task switch이며 `nrp` model의 `schedule_entry_preempt`에 해당한다.

`switch_yield`는 task가 명시적으로 scheduler를 호출하거나 userspace 복귀 중 선점될 때 발생한다. `yield` syscall 뒤, idle task에서, 또는 `need_resched` flag가 설정되었을 때 가능하다. `sleepable` task의 양보는 정의상 suspension이므로 yield할 수 없다.

특수한 yield는 signal pending 상태에서 `TASK_INTERRUPTIBLE` task가 scheduler를 호출할 때 생긴다. task는 일반적인 blocking/waking을 거치지 않고 runnable로 돌아가며, switch가 있다면 `signal_wakeup` state로의 yield처럼 보이고 뒤이어 signal delivery가 온다.

`signal_wakeup`에서 monitor는 wakeup event를 보더라도 false negative를 배제하기 위해 signal을 기대한다. 실제로 signal이 반드시 필요한 것은 아니다.

이 monitor에는 running state가 없다. `sleepable`과 `runnable`은 task의 원하는 state만 가리키며, task는 preemption 등으로 schedule out될 수 있다. 다만 task가 running이 될 수 있는 시점을 나타내는 `sched_switch_in` event는 포함한다.

`sched_switch_in`은 preemption으로도 발생할 수 있지만, task가 `sleeping`에 도달한 뒤에는 `wakeup` 전까지 발생할 수 없다.

Monitor sssw
------------

The set state sleep and wakeup (sssw) monitor ensures ``set_state`` to
sleepable leads to sleeping and sleeping tasks require wakeup. It includes the
following types of switch:

* ``switch_suspend``:
  a task puts itself to sleep, this can happen only after explicitly setting
  the task to ``sleepable``. After a task is suspended, it needs to be woken up
  (``waking`` state) before being switched in again.
  Setting the task's state to ``sleepable`` can be reverted before switching if it
  is woken up or set to ``runnable``.
* ``switch_blocking``:
  a special case of a ``switch_suspend`` where the task is waiting on a
  sleeping RT lock (``PREEMPT_RT`` only), it is common to see wakeup and set
  state events racing with each other and this leads the model to perceive this
  type of switch when the task is not set to sleepable. This is a limitation of
  the model in SMP system and workarounds may slow down the system.
* ``switch_preempt``:
  a task switch as a result of kernel preemption (``schedule_entry_preempt`` in
  the nrp model).
* ``switch_yield``:
  a task explicitly calls the scheduler or is preempted while returning to
  userspace. It can happen after a ``yield`` system call, from the idle task or
  if the ``need_resched`` flag is set. By definition, a task cannot yield while
  ``sleepable`` as that would be a suspension. A special case of a yield occurs
  when a task in ``TASK_INTERRUPTIBLE`` calls the scheduler while a signal is
  pending. The task doesn't go through the usual blocking/waking and is set
  back to runnable, the resulting switch (if there) looks like a yield to the
  ``signal_wakeup`` state and is followed by the signal delivery. From this
  state, the monitor expects a signal even if it sees a wakeup event, although
  not necessary, to rule out false negatives.

This monitor doesn't include a running state, ``sleepable`` and ``runnable``
are only referring to the task's desired state, which could be scheduled out
(e.g. due to preemption). However, it does include the event
``sched_switch_in`` to represent when a task is allowed to become running. This
can be triggered also by preemption, but cannot occur after the task got to
``sleeping`` before a ``wakeup`` occurs::

   +--------------------------------------------------------------------------+
   |                                                                          |
   |                                                                          |
   | switch_suspend           |                                               |
   | switch_blocking          |                                               |
   v                          v                                               |
 +----------+              #==========================#   set_state_runnable  |
 |          |              H                          H   wakeup              |
 |          |              H                          H   switch_in           |
 |          |              H                          H   switch_yield        |
 | sleeping |              H                          H   switch_preempt      |
 |          |              H                          H   signal_deliver      |
 |          |  switch_     H                          H ------+               |
 |          |  _blocking   H         runnable         H       |               |
 |          | <----------- H                          H <-----+               |
 +----------+              H                          H                       |
   |   wakeup              H                          H                       |
   +---------------------> H                          H                       |
                           H                          H                       |
               +---------> H                          H                       |
               |           #==========================#                       |
               |             |                ^                               |
               |             |                | set_state_runnable            |
               |             |                | wakeup                        |
               |    set_state_sleepable       |      +------------------------+
               |             v                |      |
               |           +--------------------------+  set_state_sleepable
               |           |                          |  switch_in
               |           |                          |  switch_preempt
   signal_deliver          |        sleepable         |  signal_deliver
               |           |                          | ------+
               |           |                          |       |
               |           |                          | <-----+
               |           +--------------------------+
               |             |                ^
               |        switch_yield          | set_state_sleepable
               |             v                |
               |           +---------------+  |
               +---------- | signal_wakeup | -+
                           +---------------+
                             ^           | switch_in
                             |           | switch_preempt
                             |           | switch_yield
                             +-----------+ wakeup

opid monitor

operations with preemption and irq disabled(`opid`) monitor는 `wakeup`과 `need_resched` 같은 동작이 interrupt와 preemption이 모두 disabled인 상태 또는 interrupt context에서 발생하도록 보장한다. interrupt context에서는 preemption이 명시적으로 disabled되지 않았을 수도 있다.

일부 RCU 내부 함수도 `need_resched`를 설정할 수 있다. 이 경우 task wakeup과 대응하지 않으며 interrupt만 disabled인 상태에서 발생할 수 있다.

`disabled`에서는 `sched_need_resched`, `sched_waking`, `irq_entry`를 허용한다. `irq_disabled`는 RCU 내부 경로의 `sched_need_resched`를 허용하며, `in_irq`는 tracepoint가 보이지 않을 수 있는 interrupt context를 나타낸다.

이 monitor는 `PREEMPT_RT` kernel에서 작동하도록 설계되었다. interrupt 중에는 preemption이 항상 disabled이므로 interrupt context event는 preemption tracepoint가 보이지 않는 유효한 시나리오를 식별하는 지름길이다.

non-`PREEMPT_RT` kernel에서는 interrupt가 softirq를 호출해 `need_resched`를 설정하고 task를 깨울 수 있다. 이 특수 사례는 현재 monitor가 지원하지 않는다.

Monitor opid
------------

The operations with preemption and irq disabled (opid) monitor ensures
operations like ``wakeup`` and ``need_resched`` occur with interrupts and
preemption disabled or during interrupt context, in such case preemption may
not be disabled explicitly.
``need_resched`` can be set by some RCU internals functions, in which case it
doesn't match a task wakeup and might occur with only interrupts disabled::

                 |                     sched_need_resched
                 |                     sched_waking
                 |                     irq_entry
                 |                   +--------------------+
                 v                   v                    |
               +------------------------------------------------------+
  +----------- |                     disabled                         | <+
  |            +------------------------------------------------------+  |
  |              |                 ^                                     |
  |              |          preempt_disable      sched_need_resched      |
  |       preempt_enable           |           +--------------------+    |
  |              v                 |           v                    |    |
  |            +------------------------------------------------------+  |
  |            |                   irq_disabled                       |  |
  |            +------------------------------------------------------+  |
  |                              |             |        ^                |
  |     irq_entry            irq_entry         |        |                |
  |     sched_need_resched       v             |   irq_disable           |
  |     sched_waking +--------------+          |        |                |
  |           +----- |              |     irq_enable    |                |
  |           |      |    in_irq    |          |        |                |
  |           +----> |              |          |        |                |
  |                  +--------------+          |        |          irq_disable
  |                     |                      |        |                |
  | irq_enable          | irq_enable           |        |                |
  |                     v                      v        |                |
  |            #======================================================#  |
  |            H                     enabled                          H  |
  |            #======================================================#  |
  |              |                   ^         ^ preempt_enable     |    |
  |       preempt_disable     preempt_enable   +--------------------+    |
  |              v                   |                                   |
  |            +------------------+  |                                   |
  +----------> | preempt_disabled | -+                                   |
               +------------------+                                      |
                 |                                                       |
                 +-------------------------------------------------------+

This monitor is designed to work on ``PREEMPT_RT`` kernels, the special case of
events occurring in interrupt context is a shortcut to identify valid scenarios
where the preemption tracepoints might not be visible, during interrupts
preemption is always disabled. On non- ``PREEMPT_RT`` kernels, the interrupts
might invoke a softirq to set ``need_resched`` and wake up a task. This is
another special case that is currently not supported by the monitor.

참고 문헌

sched 명세가 적용 중인 Linux task model의 참고 자료는 [1] `https://bristot.me/linux-task-model`이다.

References
----------

[1] - https://bristot.me/linux-task-model