lkml.org 
[lkml]   [2022]   [Jul]   [13]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    Patch in this message
    /
    From
    Subject[PATCH V5 13/16] rv/monitor: Add the wip monitor
    Date
    The wakeup in preemptive (wip) monitor verifies if the
    wakeup events always take place with preemption disabled:

    |
    |
    v
    #==================#
    H preemptive H <+
    #==================# |
    | |
    | preempt_disable | preempt_enable
    v |
    sched_waking +------------------+ |
    +--------------- | | |
    | | non_preemptive | |
    +--------------> | | -+
    +------------------+

    The wakeup event always takes place with preemption disabled because
    of the scheduler synchronization. However, because the preempt_count
    and its trace event are not atomic with regard to interrupts, some
    inconsistencies might happen.

    The documentation illustrates one of these cases.

    Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
    Cc: Guenter Roeck <linux@roeck-us.net>
    Cc: Jonathan Corbet <corbet@lwn.net>
    Cc: Steven Rostedt <rostedt@goodmis.org>
    Cc: Ingo Molnar <mingo@redhat.com>
    Cc: Thomas Gleixner <tglx@linutronix.de>
    Cc: Peter Zijlstra <peterz@infradead.org>
    Cc: Will Deacon <will@kernel.org>
    Cc: Catalin Marinas <catalin.marinas@arm.com>
    Cc: Marco Elver <elver@google.com>
    Cc: Dmitry Vyukov <dvyukov@google.com>
    Cc: "Paul E. McKenney" <paulmck@kernel.org>
    Cc: Shuah Khan <skhan@linuxfoundation.org>
    Cc: Gabriele Paoloni <gpaoloni@redhat.com>
    Cc: Juri Lelli <juri.lelli@redhat.com>
    Cc: Clark Williams <williams@redhat.com>
    Cc: Tao Zhou <tao.zhou@linux.dev>
    Cc: Randy Dunlap <rdunlap@infradead.org>
    Cc: linux-doc@vger.kernel.org
    Cc: linux-kernel@vger.kernel.org
    Cc: linux-trace-devel@vger.kernel.org
    Signed-off-by: Daniel Bristot de Oliveira <bristot@kernel.org>
    ---
    Documentation/trace/rv/index.rst | 1 +
    Documentation/trace/rv/monitor_wip.rst | 55 ++++++++++++++++++++++++++
    include/trace/events/rv.h | 10 +++++
    kernel/trace/rv/Kconfig | 13 ++++++
    kernel/trace/rv/Makefile | 1 +
    kernel/trace/rv/monitors/wip/wip.c | 51 +++++++-----------------
    tools/verification/models/wip.dot | 16 ++++++++
    7 files changed, 111 insertions(+), 36 deletions(-)
    create mode 100644 Documentation/trace/rv/monitor_wip.rst
    create mode 100644 tools/verification/models/wip.dot

    diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst
    index db2ae3f90b90..4cb71ed628b8 100644
    --- a/Documentation/trace/rv/index.rst
    +++ b/Documentation/trace/rv/index.rst
    @@ -10,3 +10,4 @@ Runtime Verification
    deterministic_automata.rst
    da_monitor_synthesis.rst
    da_monitor_instrumentation.rst
    + monitor_wip.rst
    diff --git a/Documentation/trace/rv/monitor_wip.rst b/Documentation/trace/rv/monitor_wip.rst
    new file mode 100644
    index 000000000000..0ea2d9388945
    --- /dev/null
    +++ b/Documentation/trace/rv/monitor_wip.rst
    @@ -0,0 +1,55 @@
    +Monitor wip
    +===========
    +
    + - Name: wip - wakeup in preemptive
    + - Type: per-cpu deterministic automaton
    + - Author: Daniel Bristot de Oliveira <bristot@kernel.org>
    +
    +Description
    +-----------
    +
    +The wakeup in preemptive (wip) monitor is a sample per-cpu monitor
    +that verifies if the wakeup events always take place with
    +preemption disabled::
    +
    + |
    + |
    + v
    + #==================#
    + H preemptive H <+
    + #==================# |
    + | |
    + | preempt_disable | preempt_enable
    + v |
    + sched_waking +------------------+ |
    + +--------------- | | |
    + | | non_preemptive | |
    + +--------------> | | -+
    + +------------------+
    +
    +The wakeup event always takes place with preemption disabled because
    +of the scheduler synchronization. However, because the preempt_count
    +and its trace event are not atomic with regard to interrupts, some
    +inconsistencies might happen. For example::
    +
    + preempt_disable() {
    + __preempt_count_add(1)
    + -------> smp_apic_timer_interrupt() {
    + preempt_disable()
    + do not trace (preempt count >= 1)
    +
    + wake up a thread
    +
    + preempt_enable()
    + do not trace (preempt count >= 1)
    + }
    + <------
    + trace_preempt_disable();
    + }
    +
    +This problem was reported and discussed here:
    + https://lore.kernel.org/r/cover.1559051152.git.bristot@redhat.com/
    +
    +Specification
    +-------------
    +Grapviz Dot file in tools/verification/models/wip.dot
    diff --git a/include/trace/events/rv.h b/include/trace/events/rv.h
    index 480aac18f403..90fa36cea517 100644
    --- a/include/trace/events/rv.h
    +++ b/include/trace/events/rv.h
    @@ -56,6 +56,16 @@ DECLARE_EVENT_CLASS(error_da_monitor,
    __entry->event,
    __entry->state)
    );
    +
    +#ifdef CONFIG_RV_MON_WIP
    +DEFINE_EVENT(event_da_monitor, event_wip,
    + TP_PROTO(char *state, char *event, char *next_state, bool final_state),
    + TP_ARGS(state, event, next_state, final_state));
    +
    +DEFINE_EVENT(error_da_monitor, error_wip,
    + TP_PROTO(char *state, char *event),
    + TP_ARGS(state, event));
    +#endif /* CONFIG_RV_MON_WIP */
    #endif /* CONFIG_DA_MON_EVENTS_IMPLICIT */

    #ifdef CONFIG_DA_MON_EVENTS_ID
    diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
    index 7ad6c93cda64..8755ad74ec22 100644
    --- a/kernel/trace/rv/Kconfig
    +++ b/kernel/trace/rv/Kconfig
    @@ -28,6 +28,19 @@ menuconfig RV
    For further information, see:
    Documentation/trace/rv/runtime-verification.rst

    +config RV_MON_WIP
    + depends on RV
    + depends on PREEMPT_TRACER
    + select DA_MON_EVENTS_IMPLICIT
    + bool "wip monitor"
    + help
    + Enable wip (wakeup in preemptive) sample monitor that illustrates
    + the usage of per-cpu monitors, and one limitation of the
    + preempt_disable/enable events.
    +
    + For further information, see:
    + Documentation/trace/rv/monitor_wip.rst
    +
    config RV_REACTORS
    bool "Runtime verification reactors"
    default y
    diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
    index 8944274d9b41..b41109d2750a 100644
    --- a/kernel/trace/rv/Makefile
    +++ b/kernel/trace/rv/Makefile
    @@ -2,3 +2,4 @@

    obj-$(CONFIG_RV) += rv.o
    obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
    +obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
    diff --git a/kernel/trace/rv/monitors/wip/wip.c b/kernel/trace/rv/monitors/wip/wip.c
    index 9ac5dc9618a3..cda13ac8f6c0 100644
    --- a/kernel/trace/rv/monitors/wip/wip.c
    +++ b/kernel/trace/rv/monitors/wip/wip.c
    @@ -10,44 +10,26 @@

    #define MODULE_NAME "wip"

    -/*
    - * XXX: include required tracepoint headers, e.g.,
    - * #include <linux/trace/events/sched.h>
    - */
    #include <trace/events/rv.h>
    +#include <trace/events/sched.h>
    +#include <trace/events/preemptirq.h>

    -/*
    - * This is the self-generated part of the monitor. Generally, there is no need
    - * to touch this section.
    - */
    #include "wip.h"

    -/*
    - * Declare the deterministic automata monitor.
    - *
    - * The rv monitor reference is needed for the monitor declaration.
    - */
    struct rv_monitor rv_wip;
    DECLARE_DA_MON_PER_CPU(wip, unsigned char);

    -/*
    - * This is the instrumentation part of the monitor.
    - *
    - * This is the section where manual work is required. Here the kernel events
    - * are translated into model's event.
    - *
    - */
    -static void handle_preempt_disable(void *data, /* XXX: fill header */)
    +static void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
    {
    da_handle_event_wip(preempt_disable_wip);
    }

    -static void handle_preempt_enable(void *data, /* XXX: fill header */)
    +static void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
    {
    - da_handle_event_wip(preempt_enable_wip);
    + da_handle_init_event_wip(preempt_enable_wip);
    }

    -static void handle_sched_waking(void *data, /* XXX: fill header */)
    +static void handle_sched_waking(void *data, struct task_struct *task)
    {
    da_handle_event_wip(sched_waking_wip);
    }
    @@ -60,9 +42,9 @@ static int start_wip(void)
    if (retval)
    return retval;

    - rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
    - rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
    - rv_attach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
    + rv_attach_trace_probe("wip", preempt_disable, handle_preempt_disable);
    + rv_attach_trace_probe("wip", preempt_enable, handle_preempt_enable);
    + rv_attach_trace_probe("wip", sched_waking, handle_sched_waking);

    return 0;
    }
    @@ -71,19 +53,16 @@ static void stop_wip(void)
    {
    rv_wip.enabled = 0;

    - rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_disable);
    - rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_preempt_enable);
    - rv_detach_trace_probe("wip", /* XXX: tracepoint */, handle_sched_waking);
    + rv_detach_trace_probe("wip", preempt_disable, handle_preempt_disable);
    + rv_detach_trace_probe("wip", preempt_enable, handle_preempt_enable);
    + rv_detach_trace_probe("wip", sched_waking, handle_sched_waking);

    da_monitor_destroy_wip();
    }

    -/*
    - * This is the monitor register section.
    - */
    struct rv_monitor rv_wip = {
    .name = "wip",
    - .description = "auto-generated wip",
    + .description = "wakeup in preemptive per-cpu testing monitor.",
    .start = start_wip,
    .stop = stop_wip,
    .reset = da_monitor_reset_all_wip,
    @@ -108,5 +87,5 @@ module_init(register_wip);
    module_exit(unregister_wip);

    MODULE_LICENSE("GPL");
    -MODULE_AUTHOR("dot2k: auto-generated");
    -MODULE_DESCRIPTION("wip");
    +MODULE_AUTHOR("Daniel Bristot de Oliveira <bristot@kernel.org>");
    +MODULE_DESCRIPTION("wip: wakeup in preemptive - per-cpu sample monitor.");
    diff --git a/tools/verification/models/wip.dot b/tools/verification/models/wip.dot
    new file mode 100644
    index 000000000000..2a53a9700a89
    --- /dev/null
    +++ b/tools/verification/models/wip.dot
    @@ -0,0 +1,16 @@
    +digraph state_automaton {
    + {node [shape = circle] "non_preemptive"};
    + {node [shape = plaintext, style=invis, label=""] "__init_preemptive"};
    + {node [shape = doublecircle] "preemptive"};
    + {node [shape = circle] "preemptive"};
    + "__init_preemptive" -> "preemptive";
    + "non_preemptive" [label = "non_preemptive"];
    + "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ];
    + "non_preemptive" -> "preemptive" [ label = "preempt_enable" ];
    + "preemptive" [label = "preemptive"];
    + "preemptive" -> "non_preemptive" [ label = "preempt_disable" ];
    + { rank = min ;
    + "__init_preemptive";
    + "preemptive";
    + }
    +}
    --
    2.35.1
    \
     
     \ /
      Last update: 2022-07-13 23:22    [W:4.338 / U:0.096 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site