Monitor stall
=============

- Name: stall - stalled task monitor
- Type: per-task hybrid automaton
- Author: Gabriele Monaco <gmonaco@redhat.com>

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

The stalled task (stall) monitor is a sample per-task timed monitor that checks
if tasks are scheduled within a defined threshold after they are ready::

                        |
                        |
                        v
                      #==========================#
  +-----------------> H         dequeued         H
  |                   #==========================#
  |                     |
 sched_switch_wait      | sched_wakeup;reset(clk)
  |                     v
  |                   +--------------------------+ <+
  |                   |         enqueued         |  | sched_wakeup
  |                   | clk < threshold_jiffies  | -+
  |                   +--------------------------+
  |                     |                 ^
  |              sched_switch_in    sched_switch_preempt;reset(clk)
  |                     v                 |
  |                   +--------------------------+
  +------------------ |         running          |
                      +--------------------------+
                        ^ sched_switch_in      |
                        | sched_wakeup         |
                        +----------------------+

The threshold can be configured as a parameter by either booting with the
``stall.threshold_jiffies=<new value>`` argument or writing a new value to
``/sys/module/stall/parameters/threshold_jiffies``.

Specification
-------------
Graphviz Dot file in tools/verification/models/stall.dot