diff options
Diffstat (limited to 'Documentation/trace')
| -rw-r--r-- | Documentation/trace/coresight/coresight.rst | 16 | ||||
| -rw-r--r-- | Documentation/trace/debugging.rst | 19 | ||||
| -rw-r--r-- | Documentation/trace/events-pci-controller.rst | 42 | ||||
| -rw-r--r-- | Documentation/trace/events-pci.rst | 74 | ||||
| -rw-r--r-- | Documentation/trace/fprobe.rst | 2 | ||||
| -rw-r--r-- | Documentation/trace/ftrace-uses.rst | 2 | ||||
| -rw-r--r-- | Documentation/trace/ftrace.rst | 25 | ||||
| -rw-r--r-- | Documentation/trace/histogram-design.rst | 20 | ||||
| -rw-r--r-- | Documentation/trace/index.rst | 20 | ||||
| -rw-r--r-- | Documentation/trace/remotes.rst | 66 | ||||
| -rw-r--r-- | Documentation/trace/rv/da_monitor_instrumentation.rst | 6 | ||||
| -rw-r--r-- | Documentation/trace/rv/deterministic_automata.rst | 2 | ||||
| -rw-r--r-- | Documentation/trace/rv/hybrid_automata.rst | 341 | ||||
| -rw-r--r-- | Documentation/trace/rv/index.rst | 3 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_deadline.rst | 84 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_sched.rst | 62 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_stall.rst | 43 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_synthesis.rst | 161 |
18 files changed, 893 insertions, 95 deletions
diff --git a/Documentation/trace/coresight/coresight.rst b/Documentation/trace/coresight/coresight.rst index 806699871b80..d461de4e067e 100644 --- a/Documentation/trace/coresight/coresight.rst +++ b/Documentation/trace/coresight/coresight.rst @@ -613,8 +613,20 @@ They are also listed in the folder /sys/bus/event_source/devices/cs_etm/format/ - Session local version of the system wide setting: :ref:`ETM_MODE_RETURNSTACK <coresight-return-stack>` * - timestamp - - Session local version of the system wide setting: :ref:`ETMv4_MODE_TIMESTAMP - <coresight-timestamp>` + - Controls generation and interval of timestamps. + + 0 = off, 1 = minimum interval .. 15 = maximum interval. + + Values 1 - 14 use a counter that decrements every cycle to generate a + timestamp on underflow. The reload value for the counter is 2 ^ (interval + - 1). If the value is 1 then the reload value is 1, if the value is 11 + then the reload value is 1024 etc. + + Setting the maximum interval (15) will disable the counter generated + timestamps, freeing the counter resource, leaving only ones emitted when + a SYNC packet is generated. The sync interval is controlled with + TRCSYNCPR.PERIOD which is every 4096 bytes of trace by default. + * - cc_threshold - Cycle count threshold value. If nothing is provided here or the provided value is 0, then the default value i.e 0x100 will be used. If provided value is less than minimum cycles threshold diff --git a/Documentation/trace/debugging.rst b/Documentation/trace/debugging.rst index 4d88c346fc38..bca1710d92bf 100644 --- a/Documentation/trace/debugging.rst +++ b/Documentation/trace/debugging.rst @@ -159,3 +159,22 @@ If setting it from the kernel command line, it is recommended to also disable tracing with the "traceoff" flag, and enable tracing after boot up. Otherwise the trace from the most recent boot will be mixed with the trace from the previous boot, and may make it confusing to read. + +Using a backup instance for keeping previous boot data +------------------------------------------------------ + +It is also possible to record trace data at system boot time by specifying +events with the persistent ring buffer, but in this case the data before the +reboot will be lost before it can be read. This problem can be solved by a +backup instance. From the kernel command line:: + + reserve_mem=12M:4096:trace trace_instance=boot_map@trace,sched,irq trace_instance=backup=boot_map + +On boot up, the previous data in the "boot_map" is copied to the "backup" +instance, and the "sched:*" and "irq:*" events for the current boot are traced +in the "boot_map". Thus the user can read the previous boot data from the "backup" +instance without stopping the trace. + +Note that this "backup" instance is readonly, and will be removed automatically +if you clear the trace data or read out all trace data from the "trace_pipe" +or the "trace_pipe_raw" files. diff --git a/Documentation/trace/events-pci-controller.rst b/Documentation/trace/events-pci-controller.rst new file mode 100644 index 000000000000..cb9f71592973 --- /dev/null +++ b/Documentation/trace/events-pci-controller.rst @@ -0,0 +1,42 @@ +.. SPDX-License-Identifier: GPL-2.0 + +====================================== +Subsystem Trace Points: PCI Controller +====================================== + +Overview +======== +The PCI controller tracing system provides tracepoints to monitor controller +level information for debugging purpose. The events normally show up here: + + /sys/kernel/tracing/events/pci_controller + +Cf. include/trace/events/pci_controller.h for the events definitions. + +Available Tracepoints +===================== + +pcie_ltssm_state_transition +--------------------------- + +Monitors PCIe LTSSM state transition including state and rate information +:: + + pcie_ltssm_state_transition "dev: %s state: %s rate: %s\n" + +**Parameters**: + +* ``dev`` - PCIe controller instance +* ``state`` - PCIe LTSSM state +* ``rate`` - PCIe date rate + +**Example Usage**: + +.. code-block:: shell + + # Enable the tracepoint + echo 1 > /sys/kernel/debug/tracing/events/pci_controller/pcie_ltssm_state_transition/enable + + # Monitor events (the following output is generated when a device is linking) + cat /sys/kernel/debug/tracing/trace_pipe + kworker/0:0-9 [000] ..... 5.600221: pcie_ltssm_state_transition: dev: a40000000.pcie state: RCVRY_EQ2 rate: 8.0 GT/s diff --git a/Documentation/trace/events-pci.rst b/Documentation/trace/events-pci.rst new file mode 100644 index 000000000000..03ff4ad30ddf --- /dev/null +++ b/Documentation/trace/events-pci.rst @@ -0,0 +1,74 @@ +.. SPDX-License-Identifier: GPL-2.0 + +=========================== +Subsystem Trace Points: PCI +=========================== + +Overview +======== +The PCI tracing system provides tracepoints to monitor critical hardware events +that can impact system performance and reliability. These events normally show +up here: + + /sys/kernel/tracing/events/pci + +Cf. include/trace/events/pci.h for the events definitions. + +Available Tracepoints +===================== + +pci_hp_event +------------ + +Monitors PCI hotplug events including card insertion/removal and link +state changes. +:: + + pci_hp_event "%s slot:%s, event:%s\n" + +**Event Types**: + +* ``LINK_UP`` - PCIe link established +* ``LINK_DOWN`` - PCIe link lost +* ``CARD_PRESENT`` - Card detected in slot +* ``CARD_NOT_PRESENT`` - Card removed from slot + +**Example Usage**:: + + # Enable the tracepoint + echo 1 > /sys/kernel/debug/tracing/events/pci/pci_hp_event/enable + + # Monitor events (the following output is generated when a device is hotplugged) + cat /sys/kernel/debug/tracing/trace_pipe + irq/51-pciehp-88 [001] ..... 1311.177459: pci_hp_event: 0000:00:02.0 slot:10, event:CARD_PRESENT + + irq/51-pciehp-88 [001] ..... 1311.177566: pci_hp_event: 0000:00:02.0 slot:10, event:LINK_UP + +pcie_link_event +--------------- + +Monitors PCIe link speed changes and provides detailed link status information. +:: + + pcie_link_event "%s type:%d, reason:%d, cur_bus_speed:%d, max_bus_speed:%d, width:%u, flit_mode:%u, status:%s\n" + +**Parameters**: + +* ``type`` - PCIe device type (4=Root Port, etc.) +* ``reason`` - Reason for link change: + + - ``0`` - Link retrain + - ``1`` - Bus enumeration + - ``2`` - Bandwidth notification enable + - ``3`` - Bandwidth notification IRQ + - ``4`` - Hotplug event + + +**Example Usage**:: + + # Enable the tracepoint + echo 1 > /sys/kernel/debug/tracing/events/pci/pcie_link_event/enable + + # Monitor events (the following output is generated when a device is hotplugged) + cat /sys/kernel/debug/tracing/trace_pipe + irq/51-pciehp-88 [001] ..... 381.545386: pcie_link_event: 0000:00:02.0 type:4, reason:4, cur_bus_speed:20, max_bus_speed:23, width:1, flit_mode:0, status:DLLLA diff --git a/Documentation/trace/fprobe.rst b/Documentation/trace/fprobe.rst index 06b0edad0179..95998b189ae3 100644 --- a/Documentation/trace/fprobe.rst +++ b/Documentation/trace/fprobe.rst @@ -79,7 +79,7 @@ The above is defined by including the header:: Same as ftrace, the registered callbacks will start being called some time after the register_fprobe() is called and before it returns. See -:file:`Documentation/trace/ftrace.rst`. +Documentation/trace/ftrace.rst. Also, the unregister_fprobe() will guarantee that both enter and exit handlers are no longer being called by functions after unregister_fprobe() diff --git a/Documentation/trace/ftrace-uses.rst b/Documentation/trace/ftrace-uses.rst index e225cc46b71e..a9701add27c5 100644 --- a/Documentation/trace/ftrace-uses.rst +++ b/Documentation/trace/ftrace-uses.rst @@ -253,7 +253,7 @@ If @buf is NULL and reset is set, all functions will be enabled for tracing. The @buf can also be a glob expression to enable all functions that match a specific pattern. -See Filter Commands in :file:`Documentation/trace/ftrace.rst`. +See Filter Commands in Documentation/trace/ftrace.rst. To just trace the schedule function: diff --git a/Documentation/trace/ftrace.rst b/Documentation/trace/ftrace.rst index d1f313a5f4ad..b9efb148a5c2 100644 --- a/Documentation/trace/ftrace.rst +++ b/Documentation/trace/ftrace.rst @@ -684,6 +684,22 @@ of ftrace. Here is a list of some of the key files: See events.rst for more information. + show_event_filters: + + A list of events that have filters. This shows the + system/event pair along with the filter that is attached to + the event. + + See events.rst for more information. + + show_event_triggers: + + A list of events that have triggers. This shows the + system/event pair along with the trigger that is attached to + the event. + + See events.rst for more information. + available_events: A list of events that can be enabled in tracing. @@ -1290,6 +1306,15 @@ Here are the available options: This will be useful if you want to find out which hashed value is corresponding to the real value in trace log. + bitmask-list + When enabled, bitmasks are displayed as a human-readable list of + ranges (e.g., 0,2-5,7) using the printk "%*pbl" format specifier. + When disabled (the default), bitmasks are displayed in the + traditional hexadecimal bitmap representation. The list format is + particularly useful for tracing CPU masks and other large bitmasks + where individual bit positions are more meaningful than their + hexadecimal encoding. + record-cmd When any event or tracer is enabled, a hook is enabled in the sched_switch trace point to fill comm cache diff --git a/Documentation/trace/histogram-design.rst b/Documentation/trace/histogram-design.rst index ae71b5bf97c6..e92f56ebd0b5 100644 --- a/Documentation/trace/histogram-design.rst +++ b/Documentation/trace/histogram-design.rst @@ -69,7 +69,8 @@ So in this histogram, there's a separate bucket for each pid, and each bucket contains a value for that bucket, counting the number of times sched_waking was called for that pid. -Each histogram is represented by a hist_data struct. +Each histogram is represented by a hist_data struct +(struct hist_trigger_data). To keep track of each key and value field in the histogram, hist_data keeps an array of these fields named fields[]. The fields[] array is @@ -82,7 +83,7 @@ value or not, which the above histogram does not. Each struct hist_field contains a pointer to the ftrace_event_field from the event's trace_event_file along with various bits related to -that such as the size, offset, type, and a hist_field_fn_t function, +that such as the size, offset, type, and a hist field function, which is used to grab the field's data from the ftrace event buffer (in most cases - some hist_fields such as hitcount don't directly map to an event field in the trace buffer - in these cases the function @@ -241,28 +242,33 @@ it, event_hist_trigger() is called. event_hist_trigger() first deals with the key: for each subkey in the key (in the above example, there is just one subkey corresponding to pid), the hist_field that represents that subkey is retrieved from hist_data.fields[] and the -hist_field_fn_t fn() associated with that field, along with the +hist field function associated with that field, along with the field's size and offset, is used to grab that subkey's data from the current trace record. +Note, the hist field function use to be a function pointer in the +hist_field stucture. Due to spectre mitigation, it was converted into +a fn_num and hist_fn_call() is used to call the associated hist field +function that corresponds to the fn_num of the hist_field structure. + Once the complete key has been retrieved, it's used to look that key up in the tracing_map. If there's no tracing_map_elt associated with that key, an empty one is claimed and inserted in the map for the new key. In either case, the tracing_map_elt associated with that key is returned. -Once a tracing_map_elt available, hist_trigger_elt_update() is called. +Once a tracing_map_elt is available, hist_trigger_elt_update() is called. As the name implies, this updates the element, which basically means updating the element's fields. There's a tracing_map_field associated with each key and value in the histogram, and each of these correspond to the key and value hist_fields created when the histogram was created. hist_trigger_elt_update() goes through each value hist_field -and, as for the keys, uses the hist_field's fn() and size and offset +and, as for the keys, uses the hist_field's function and size and offset to grab the field's value from the current trace record. Once it has that value, it simply adds that value to that field's continually-updated tracing_map_field.sum member. Some hist_field -fn()s, such as for the hitcount, don't actually grab anything from the -trace record (the hitcount fn() just increments the counter sum by 1), +functions, such as for the hitcount, don't actually grab anything from the +trace record (the hitcount function just increments the counter sum by 1), but the idea is the same. Once all the values have been updated, hist_trigger_elt_update() is diff --git a/Documentation/trace/index.rst b/Documentation/trace/index.rst index b4a429dc4f7a..5d9bf4694d5d 100644 --- a/Documentation/trace/index.rst +++ b/Documentation/trace/index.rst @@ -54,6 +54,8 @@ applications. events-power events-nmi events-msr + events-pci + events-pci-controller boottime-trace histogram histogram-design @@ -90,15 +92,19 @@ interactions. user_events uprobetracer +Remote Tracing +-------------- + +This section covers the framework to read compatible ring-buffers, written by +entities outside of the kernel (most likely firmware or hypervisor) + +.. toctree:: + :maxdepth: 1 + + remotes + Additional Resources -------------------- For more details, refer to the respective documentation of each tracing tool and framework. - -.. only:: subproject and html - - Indices - ======= - - * :ref:`genindex` diff --git a/Documentation/trace/remotes.rst b/Documentation/trace/remotes.rst new file mode 100644 index 000000000000..1f9d764f69aa --- /dev/null +++ b/Documentation/trace/remotes.rst @@ -0,0 +1,66 @@ +.. SPDX-License-Identifier: GPL-2.0 + +=============== +Tracing Remotes +=============== + +:Author: Vincent Donnefort <vdonnefort@google.com> + +Overview +======== +Firmware and hypervisors are black boxes to the kernel. Having a way to see what +they are doing can be useful to debug both. This is where remote tracing buffers +come in. A remote tracing buffer is a ring buffer executed by the firmware or +hypervisor into memory that is memory mapped to the host kernel. This is similar +to how user space memory maps the kernel ring buffer but in this case the kernel +is acting like user space and the firmware or hypervisor is the "kernel" side. +With a trace remote ring buffer, the firmware and hypervisor can record events +for which the host kernel can see and expose to user space. + +Register a remote +================= +A remote must provide a set of callbacks `struct trace_remote_callbacks` whom +description can be found below. Those callbacks allows Tracefs to enable and +disable tracing and events, to load and unload a tracing buffer (a set of +ring-buffers) and to swap a reader page with the head page, which enables +consuming reading. + +.. kernel-doc:: include/linux/trace_remote.h + +Once registered, an instance will appear for this remote in the Tracefs +directory **remotes/**. Buffers can then be read using the usual Tracefs files +**trace_pipe** and **trace**. + +Declare a remote event +====================== +Macros are provided to ease the declaration of remote events, in a similar +fashion to in-kernel events. A declaration must provide an ID, a description of +the event arguments and how to print the event: + +.. code-block:: c + + REMOTE_EVENT(foo, EVENT_FOO_ID, + RE_STRUCT( + re_field(u64, bar) + ), + RE_PRINTK("bar=%lld", __entry->bar) + ); + +Then those events must be declared in a C file with the following: + +.. code-block:: c + + #define REMOTE_EVENT_INCLUDE_FILE foo_events.h + #include <trace/define_remote_events.h> + +This will provide a `struct remote_event remote_event_foo` that can be given to +`trace_remote_register`. + +Registered events appear in the remote directory under **events/**. + +Simple ring-buffer +================== +A simple implementation for a ring-buffer writer can be found in +kernel/trace/simple_ring_buffer.c. + +.. kernel-doc:: include/linux/simple_ring_buffer.h diff --git a/Documentation/trace/rv/da_monitor_instrumentation.rst b/Documentation/trace/rv/da_monitor_instrumentation.rst index 6c67c7b57811..9eff38a4ad1f 100644 --- a/Documentation/trace/rv/da_monitor_instrumentation.rst +++ b/Documentation/trace/rv/da_monitor_instrumentation.rst @@ -162,10 +162,10 @@ For example, from the wip sample model:: The probes then need to be detached at the disable phase. -[1] The wip model is presented in:: +[1] The wip model is presented in: Documentation/trace/rv/deterministic_automata.rst -The wip monitor is presented in:: +The wip monitor is presented in: - Documentation/trace/rv/da_monitor_synthesis.rst + Documentation/trace/rv/monitor_synthesis.rst diff --git a/Documentation/trace/rv/deterministic_automata.rst b/Documentation/trace/rv/deterministic_automata.rst index d0638f95a455..7a1c2b20ec72 100644 --- a/Documentation/trace/rv/deterministic_automata.rst +++ b/Documentation/trace/rv/deterministic_automata.rst @@ -11,7 +11,7 @@ where: - *E* is the finite set of events; - x\ :subscript:`0` is the initial state; - X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states. -- *f* : *X* x *E* -> *X* $ is the transition function. It defines the state +- *f* : *X* x *E* -> *X* is the transition function. It defines the state transition in the occurrence of an event from *E* in the state *X*. In the special case of deterministic automata, the occurrence of the event in *E* in a state in *X* has a deterministic next state from *X*. diff --git a/Documentation/trace/rv/hybrid_automata.rst b/Documentation/trace/rv/hybrid_automata.rst new file mode 100644 index 000000000000..f20d489f18c1 --- /dev/null +++ b/Documentation/trace/rv/hybrid_automata.rst @@ -0,0 +1,341 @@ +Hybrid Automata +=============== + +Hybrid automata are an extension of deterministic automata, there are several +definitions of hybrid automata in the literature. The adaptation implemented +here is formally denoted by G and defined as a 7-tuple: + + *G* = { *X*, *E*, *V*, *f*, x\ :subscript:`0`, X\ :subscript:`m`, *i* } + +- *X* is the set of states; +- *E* is the finite set of events; +- *V* is the finite set of environment variables; +- x\ :subscript:`0` is the initial state; +- X\ :subscript:`m` (subset of *X*) is the set of marked (or final) states. +- *f* : *X* x *E* x *C(V)* -> *X* is the transition function. + It defines the state transition in the occurrence of an event from *E* in the + state *X*. Unlike deterministic automata, the transition function also + includes guards from the set of all possible constraints (defined as *C(V)*). + Guards can be true or false with the valuation of *V* when the event occurs, + and the transition is possible only when constraints are true. Similarly to + deterministic automata, the occurrence of the event in *E* in a state in *X* + has a deterministic next state from *X*, if the guard is true. +- *i* : *X* -> *C'(V)* is the invariant assignment function, this is a + constraint assigned to each state in *X*, every state in *X* must be left + before the invariant turns to false. We can omit the representation of + invariants whose value is true regardless of the valuation of *V*. + +The set of all possible constraints *C(V)* is defined according to the +following grammar: + + g = v < c | v > c | v <= c | v >= c | v == c | v != c | g && g | true + +With v a variable in *V* and c a numerical value. + +We define the special case of hybrid automata whose variables grow with uniform +rates as timed automata. In this case, the variables are called clocks. +As the name implies, timed automata can be used to describe real time. +Additionally, clocks support another type of guard which always evaluates to true: + + reset(v) + +The reset constraint is used to set the value of a clock to 0. + +The set of invariant constraints *C'(V)* is a subset of *C(V)* including only +constraint of the form: + + g = v < c | true + +This simplifies the implementation as a clock expiration is a necessary and +sufficient condition for the violation of invariants while still allowing more +complex constraints to be specified as guards. + +It is important to note that any hybrid automaton is a valid deterministic +automaton with additional guards and invariants. Those can only further +constrain what transitions are valid but it is not possible to define +transition functions starting from the same state in *X* and the same event in +*E* but ending up in different states in *X* based on the valuation of *V*. + +Examples +-------- + +Wip as hybrid automaton +~~~~~~~~~~~~~~~~~~~~~~~ + +The 'wip' (wakeup in preemptive) example introduced as a deterministic automaton +can also be described as: + +- *X* = { ``any_thread_running`` } +- *E* = { ``sched_waking`` } +- *V* = { ``preemptive`` } +- x\ :subscript:`0` = ``any_thread_running`` +- X\ :subscript:`m` = {``any_thread_running``} +- *f* = + - *f*\ (``any_thread_running``, ``sched_waking``, ``preemptive==0``) = ``any_thread_running`` +- *i* = + - *i*\ (``any_thread_running``) = ``true`` + +Which can be represented graphically as:: + + | + | + v + #====================# sched_waking;preemptive==0 + H H ------------------------------+ + H any_thread_running H | + H H <-----------------------------+ + #====================# + +In this example, by using the preemptive state of the system as an environment +variable, we can assert this constraint on ``sched_waking`` without requiring +preemption events (as we would in a deterministic automaton), which can be +useful in case those events are not available or not reliable on the system. + +Since all the invariants in *i* are true, we can omit them from the representation. + +Stall model with guards (iteration 1) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +As a sample timed automaton we can define 'stall' as: + +- *X* = { ``dequeued``, ``enqueued``, ``running``} +- *E* = { ``enqueue``, ``dequeue``, ``switch_in``} +- *V* = { ``clk`` } +- x\ :subscript:`0` = ``dequeue`` +- X\ :subscript:`m` = {``dequeue``} +- *f* = + - *f*\ (``enqueued``, ``switch_in``, ``clk < threshold``) = ``running`` + - *f*\ (``running``, ``dequeue``) = ``dequeued`` + - *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued`` +- *i* = *omitted as all true* + +Graphically represented as:: + + | + | + v + #============================# + H dequeued H <+ + #============================# | + | | + | enqueue; reset(clk) | + v | + +----------------------------+ | + | enqueued | | dequeue + +----------------------------+ | + | | + | switch_in; clk < threshold | + v | + +----------------------------+ | + | running | -+ + +----------------------------+ + +This model imposes that the time between when a task is enqueued (it becomes +runnable) and when the task gets to run must be lower than a certain threshold. +A failure in this model means that the task is starving. +One problem in using guards on the edges in this case is that the model will +not report a failure until the ``switch_in`` event occurs. This means that, +according to the model, it is valid for the task never to run. + +Stall model with invariants (iteration 2) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The first iteration isn't exactly what was intended, we can change the model as: + +- *X* = { ``dequeued``, ``enqueued``, ``running``} +- *E* = { ``enqueue``, ``dequeue``, ``switch_in``} +- *V* = { ``clk`` } +- x\ :subscript:`0` = ``dequeue`` +- X\ :subscript:`m` = {``dequeue``} +- *f* = + - *f*\ (``enqueued``, ``switch_in``) = ``running`` + - *f*\ (``running``, ``dequeue``) = ``dequeued`` + - *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued`` +- *i* = + - *i*\ (``enqueued``) = ``clk < threshold`` + +Graphically:: + + | + | + v + #=========================# + H dequeued H <+ + #=========================# | + | | + | enqueue; reset(clk) | + v | + +-------------------------+ | + | enqueued | | + | clk < threshold | | dequeue + +-------------------------+ | + | | + | switch_in | + v | + +-------------------------+ | + | running | -+ + +-------------------------+ + +In this case, we moved the guard as an invariant to the ``enqueued`` state, +this means we not only forbid the occurrence of ``switch_in`` when ``clk`` is +past the threshold but also mark as invalid in case we are *still* in +``enqueued`` after the threshold. This model is effectively in an invalid state +as soon as a task is starving, rather than when the starving task finally runs. + +Hybrid Automaton in C +--------------------- + +The definition of hybrid automata in C is heavily based on the deterministic +automata one. Specifically, we add the set of environment variables and the +constraints (both guards on transitions and invariants on states) as follows. +This is a combination of both iterations of the stall example:: + + /* enum representation of X (set of states) to be used as index */ + enum states { + dequeued, + enqueued, + running, + state_max, + }; + + #define INVALID_STATE state_max + + /* enum representation of E (set of events) to be used as index */ + enum events { + dequeue, + enqueue, + switch_in, + event_max, + }; + + /* enum representation of V (set of environment variables) to be used as index */ + enum envs { + clk, + env_max, + env_max_stored = env_max, + }; + + struct automaton { + char *state_names[state_max]; // X: the set of states + char *event_names[event_max]; // E: the finite set of events + char *env_names[env_max]; // V: the finite set of env vars + unsigned char function[state_max][event_max]; // f: transition function + unsigned char initial_state; // x_0: the initial state + bool final_states[state_max]; // X_m: the set of marked states + }; + + struct automaton aut = { + .state_names = { + "dequeued", + "enqueued", + "running", + }, + .event_names = { + "dequeue", + "enqueue", + "switch_in", + }, + .env_names = { + "clk", + }, + .function = { + { INVALID_STATE, enqueued, INVALID_STATE }, + { INVALID_STATE, INVALID_STATE, running }, + { dequeued, INVALID_STATE, INVALID_STATE }, + }, + .initial_state = dequeued, + .final_states = { 1, 0, 0 }, + }; + + static bool verify_constraint(enum states curr_state, enum events event, + enum states next_state) + { + bool res = true; + + /* Validate guards as part of f */ + if (curr_state == enqueued && event == switch_in) + res = get_env(clk) < threshold; + else if (curr_state == dequeued && event == enqueue) + reset_env(clk); + + /* Validate invariants in i */ + if (next_state == curr_state || !res) + return res; + if (next_state == enqueued) + ha_start_timer_jiffy(ha_mon, clk, threshold_jiffies); + else if (curr_state == enqueued) + res = !ha_cancel_timer(ha_mon); + return res; + } + +The function ``verify_constraint``, here reported as simplified, checks guards, +performs resets and starts timers to validate invariants according to +specification, those cannot easily be represented in the automaton struct. +Due to the complex nature of environment variables, the user needs to provide +functions to get and reset environment variables that are not common clocks +(e.g. clocks with ns or jiffy granularity). +Since invariants are only defined as clock expirations (e.g. *clk < +threshold*), reaching the expiration of a timer armed when entering the state +is in fact a failure in the model and triggers a reaction. Leaving the state +stops the timer. + +It is important to note that timers implemented with hrtimers introduce +overhead, if the monitor has several instances (e.g. all tasks) this can become +an issue. The impact can be decreased using the timer wheel (``HA_TIMER_TYPE`` +set to ``HA_TIMER_WHEEL``), this lowers the responsiveness of the timer without +damaging the accuracy of the model, since the invariant condition is checked +before disabling the timer in case the callback is late. +Alternatively, if the monitor is guaranteed to *eventually* leave the state and +the incurred delay to wait for the next event is acceptable, guards can be used +in place of invariants, as seen in the stall example. + +Graphviz .dot format +-------------------- + +Also the Graphviz representation of hybrid automata is an extension of the +deterministic automata one. Specifically, guards can be provided in the event +name separated by ``;``:: + + "state_start" -> "state_dest" [ label = "sched_waking;preemptible==0;reset(clk)" ]; + +Invariant can be specified in the state label (not the node name!) separated by ``\n``:: + + "enqueued" [label = "enqueued\nclk < threshold_jiffies"]; + +Constraints can be specified as valid C comparisons and allow spaces, the first +element of the comparison must be the clock while the second is a numerical or +parametrised value. Guards allow comparisons to be combined with boolean +operations (``&&`` and ``||``), resets must be separated from other constraints. + +This is the full example of the last version of the 'stall' model in DOT:: + + digraph state_automaton { + {node [shape = circle] "enqueued"}; + {node [shape = plaintext, style=invis, label=""] "__init_dequeued"}; + {node [shape = doublecircle] "dequeued"}; + {node [shape = circle] "running"}; + "__init_dequeued" -> "dequeued"; + "enqueued" [label = "enqueued\nclk < threshold_jiffies"]; + "running" [label = "running"]; + "dequeued" [label = "dequeued"]; + "enqueued" -> "running" [ label = "switch_in" ]; + "running" -> "dequeued" [ label = "dequeue" ]; + "dequeued" -> "enqueued" [ label = "enqueue;reset(clk)" ]; + { rank = min ; + "__init_dequeued"; + "dequeued"; + } + } + +References +---------- + +One book covering model checking and timed automata is:: + + Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, + The MIT Press, 2008. + +Hybrid automata are described in detail in:: + + Thomas Henzinger: The theory of hybrid automata, + Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 1996. diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst index a2812ac5cfeb..29769f06bb0f 100644 --- a/Documentation/trace/rv/index.rst +++ b/Documentation/trace/rv/index.rst @@ -9,9 +9,12 @@ Runtime Verification runtime-verification.rst deterministic_automata.rst |