1. 30 Jul, 2022 15 commits
    • Daniel Bristot de Oliveira's avatar
      rv/monitor: Add the wip monitor skeleton created by dot2k · 8812d212
      Daniel Bristot de Oliveira authored
      THIS CODE IS NOT LINKED TO THE MAKEFILE.
      
      This model does not compile because it lacks the instrumentation
      part, which will be added next. In the typical case, there will be
      only one patch, but it was split into two patches for educational
      purposes.
      
      This is the direct output this command line:
        $ dot2k -d tools/verification/models/wip.dot -t per_cpu
      
      Link: https://lkml.kernel.org/r/5eb7a9118917e8a814c5e49853a72fc62be0a101.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      8812d212
    • Daniel Bristot de Oliveira's avatar
      Documentation/rv: Add deterministic automata instrumentation documentation · b6172b51
      Daniel Bristot de Oliveira authored
      Add the da_monitor_instrumentation.rst. It describes the basics
      of RV monitor instrumentation.
      
      Link: https://lkml.kernel.org/r/0557d5c68e2fc252f2643c2cc5295a67e2b73277.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      b6172b51
    • Daniel Bristot de Oliveira's avatar
      Documentation/rv: Add deterministic automata monitor synthesis documentation · d57aff24
      Daniel Bristot de Oliveira authored
      Add the da_monitor_synthesis.rst introduces some concepts behind the
      Deterministic Automata (DA) monitor synthesis and interface.
      
      Link: https://lkml.kernel.org/r/7873bdb7b2e5d2bc0b2eb6ca0b324af9a0ba27a0.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      d57aff24
    • Daniel Bristot de Oliveira's avatar
      tools/rv: Add dot2k · 24bce201
      Daniel Bristot de Oliveira authored
      transform .dot file into kernel rv monitor
      
      usage: dot2k [-h] -d DOT_FILE -t MONITOR_TYPE [-n MODEL_NAME] [-D DESCRIPTION]
      
      optional arguments:
        -h, --help            show this help message and exit
        -d DOT_FILE, --dot DOT_FILE
        -t MONITOR_TYPE, --monitor_type MONITOR_TYPE
        -n MODEL_NAME, --model_name MODEL_NAME
        -D DESCRIPTION, --description DESCRIPTION
      
      Link: https://lkml.kernel.org/r/083b3ae61e5a62c1e2e5d08009baa91f82181618.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      24bce201
    • Daniel Bristot de Oliveira's avatar
      Documentation/rv: Add deterministic automaton documentation · 4041b9bb
      Daniel Bristot de Oliveira authored
      Add documentation about deterministic automaton and its possible
      representations (formal, graphic, .dot and C).
      
      Link: https://lkml.kernel.org/r/387edaed87630bd5eb37c4275045dfd229700aa6.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      4041b9bb
    • Daniel Bristot de Oliveira's avatar
      tools/rv: Add dot2c · e3c9fc78
      Daniel Bristot de Oliveira authored
      dot2c is a tool that transforms an automata in the graphiviz .dot file
      into an C representation of the automata.
      
      usage: dot2c [-h] dot_file
      
      dot2c: converts a .dot file into a C structure
      
      positional arguments:
        dot_file    The dot file to be converted
      
      optional arguments:
        -h, --help  show this help message and exit
      
      Link: https://lkml.kernel.org/r/b26204ba9509c80bcda31b76cdea31ddb188cd24.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      e3c9fc78
    • Daniel Bristot de Oliveira's avatar
      Documentation/rv: Add a basic documentation · ff0aaf67
      Daniel Bristot de Oliveira authored
      Add the runtime-verification.rst document, explaining the basics of RV
      and how to use the interface.
      
      Link: https://lkml.kernel.org/r/4be7d1a88ab1e2eb0767521e1ab52a149a154bc4.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      ff0aaf67
    • Daniel Bristot de Oliveira's avatar
      rv/include: Add instrumentation helper functions · cc8e71c8
      Daniel Bristot de Oliveira authored
      Instrumentation helper functions to facilitate the instrumentation of
      auto-generated RV monitors create by dot2k.
      
      Link: https://lkml.kernel.org/r/3b36c9435f9d9299beb84e5c7c46920e205bedec.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      cc8e71c8
    • Daniel Bristot de Oliveira's avatar
      rv/include: Add deterministic automata monitor definition via C macros · 79257534
      Daniel Bristot de Oliveira authored
      In Linux terms, the runtime verification monitors are encapsulated
      inside the "RV monitor" abstraction. The "RV monitor" includes a set
      of instances of the monitor (per-cpu monitor, per-task monitor, and
      so on), the helper functions that glue the monitor to the system
      reference model, and the trace output as a reaction for event parsing
      and exceptions, as depicted below:
      
      Linux  +----- RV Monitor ----------------------------------+ Formal
       Realm |                                                   |  Realm
       +-------------------+     +----------------+     +-----------------+
       |   Linux kernel    |     |     Monitor    |     |     Reference   |
       |     Tracing       |  -> |   Instance(s)  | <-  |       Model     |
       | (instrumentation) |     | (verification) |     | (specification) |
       +-------------------+     +----------------+     +-----------------+
              |                          |                       |
              |                          V                       |
              |                     +----------+                 |
              |                     | Reaction |                 |
              |                     +--+--+--+-+                 |
              |                        |  |  |                   |
              |                        |  |  +-> trace output ?  |
              +------------------------|--|----------------------+
                                       |  +----> panic ?
                                       +-------> <user-specified>
      
      Add the rv/da_monitor.h, enabling automatic code generation for the
      *Monitor Instance(s)* using C macros, and code to support it.
      
      The benefits of the usage of macro for monitor synthesis are 3-fold as it:
      
      - Reduces the code duplication;
      - Facilitates the bug fix/improvement;
      - Avoids the case of developers changing the core of the monitor code
        to manipulate the model in a (let's say) non-standard way.
      
      This initial implementation presents three different types of monitor
      instances:
      
      - DECLARE_DA_MON_GLOBAL(name, type)
      - DECLARE_DA_MON_PER_CPU(name, type)
      - DECLARE_DA_MON_PER_TASK(name, type)
      
      The first declares the functions for a global deterministic automata monitor,
      the second for monitors with per-cpu instances, and the third with per-task
      instances.
      
      Link: https://lkml.kernel.org/r/51b0bf425a281e226dfeba7401d2115d6091f84e.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      79257534
    • Daniel Bristot de Oliveira's avatar
      rv/include: Add helper functions for deterministic automata · 09ecd8b8
      Daniel Bristot de Oliveira authored
      Formally, a deterministic automaton, denoted by G, is defined as a
      quintuple:
      
        G = { X, E, f, x_0, X_m }
      
      where:
      	- X is the set of states;
      	- E is the finite set of events;
      	- x_0 is the initial state;
      	- X_m (subset of X) is the set of marked states.
      	- f : X x E -> X $ is the transition function. It defines the
      	  state transition in the occurrence of a 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.
      
      An automaton can also be represented using a graphical format of
      vertices (nodes) and edges. The open-source tool Graphviz can produce
      this graphic format using the (textual) DOT language as the source code.
      
      The dot2c tool presented in this paper:
      
      De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
      Silva. Efficient formal verification for the Linux kernel. In:
      International Conference on Software Engineering and Formal Methods.
      Springer, Cham, 2019. p. 315-332.
      
      Translates a deterministic automaton in the DOT format into a C
      source code representation that to be used for monitoring.
      
      This header file implements helper functions to facilitate the usage
      of the C output from dot2c/k for monitoring.
      
      Link: https://lkml.kernel.org/r/563234f2bfa84b540f60cf9e39c2d9f0eea95a55.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      09ecd8b8
    • Daniel Bristot de Oliveira's avatar
      rv: Add runtime reactors interface · 04acadcb
      Daniel Bristot de Oliveira authored
      A runtime monitor can cause a reaction to the detection of an
      exception on the model's execution. By default, the monitors have
      tracing reactions, printing the monitor output via tracepoints.
      But other reactions can be added (on-demand) via this interface.
      
      The user interface resembles the kernel tracing interface and
      presents these files:
      
      "available_reactors"
        - Reading shows the available reactors, one per line.
      
         For example:
           # cat available_reactors
           nop
           panic
           printk
      
       "reacting_on"
         - It is an on/off general switch for reactors, disabling
         all reactions.
      
       "monitors/MONITOR/reactors"
         - List available reactors, with the select reaction for the given
         MONITOR inside []. The default one is the nop (no operation)
         reactor.
         - Writing the name of a reactor enables it to the given
         MONITOR.
      
         For example:
           # cat monitors/wip/reactors
           [nop]
           panic
           printk
           # echo panic > monitors/wip/reactors
           # cat monitors/wip/reactors
           nop
           [panic]
           printk
      
      Link: https://lkml.kernel.org/r/1794eb994637457bdeaa6bad0b8263d2f7eece0c.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      04acadcb
    • Daniel Bristot de Oliveira's avatar
      rv: Add Runtime Verification (RV) interface · 102227b9
      Daniel Bristot de Oliveira authored
      RV is a lightweight (yet rigorous) method that complements classical
      exhaustive verification techniques (such as model checking and
      theorem proving) with a more practical approach to complex systems.
      
      RV works by analyzing the trace of the system's actual execution,
      comparing it against a formal specification of the system behavior.
      RV can give precise information on the runtime behavior of the
      monitored system while enabling the reaction for unexpected
      events, avoiding, for example, the propagation of a failure on
      safety-critical systems.
      
      The development of this interface roots in the development of the
      paper:
      
      De Oliveira, Daniel Bristot; Cucinotta, Tommaso; De Oliveira, Romulo
      Silva. Efficient formal verification for the Linux kernel. In:
      International Conference on Software Engineering and Formal Methods.
      Springer, Cham, 2019. p. 315-332.
      
      And:
      
      De Oliveira, Daniel Bristot. Automata-based formal analysis
      and verification of the real-time Linux kernel. PhD Thesis, 2020.
      
      The RV interface resembles the tracing/ interface on purpose. The current
      path for the RV interface is /sys/kernel/tracing/rv/.
      
      It presents these files:
      
       "available_monitors"
         - List the available monitors, one per line.
      
         For example:
           # cat available_monitors
           wip
           wwnr
      
       "enabled_monitors"
         - Lists the enabled monitors, one per line;
         - Writing to it enables a given monitor;
         - Writing a monitor name with a '!' prefix disables it;
         - Truncating the file disables all enabled monitors.
      
         For example:
           # cat enabled_monitors
           # echo wip > enabled_monitors
           # echo wwnr >> enabled_monitors
           # cat enabled_monitors
           wip
           wwnr
           # echo '!wip' >> enabled_monitors
           # cat enabled_monitors
           wwnr
           # echo > enabled_monitors
           # cat enabled_monitors
           #
      
         Note that more than one monitor can be enabled concurrently.
      
       "monitoring_on"
         - It is an on/off general switcher for monitoring. Note
         that it does not disable enabled monitors or detach events,
         but stop the per-entity monitors of monitoring the events
         received from the system. It resembles the "tracing_on" switcher.
      
       "monitors/"
         Each monitor will have its one directory inside "monitors/". There
         the monitor specific files will be presented.
         The "monitors/" directory resembles the "events" directory on
         tracefs.
      
         For example:
           # cd monitors/wip/
           # ls
           desc  enable
           # cat desc
           wakeup in preemptive per-cpu testing monitor.
           # cat enable
           0
      
      For further information, see the comments in the header of
      kernel/trace/rv/rv.c from this patch.
      
      Link: https://lkml.kernel.org/r/a4bfe038f50cb047bfb343ad0e12b0e646ab308b.1659052063.git.bristot@kernel.org
      
      Cc: Wim Van Sebroeck <wim@linux-watchdog.org>
      Cc: Guenter Roeck <linux@roeck-us.net>
      Cc: Jonathan Corbet <corbet@lwn.net>
      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: default avatarDaniel Bristot de Oliveira <bristot@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      102227b9
    • Steven Rostedt (Google)'s avatar
      ftrace/x86: Add back ftrace_expected assignment · ac6c1b2c
      Steven Rostedt (Google) authored
      When a ftrace_bug happens (where ftrace fails to modify a location) it is
      helpful to have what was at that location as well as what was expected to
      be there.
      
      But with the conversion to text_poke() the variable that assigns the
      expected for debugging was dropped. Unfortunately, I noticed this when I
      needed it. Add it back.
      
      Link: https://lkml.kernel.org/r/20220726101851.069d2e70@gandalf.local.home
      
      Cc: "x86@kernel.org" <x86@kernel.org>
      Cc: Peter Zijlstra <peterz@infradead.org>
      Cc: Thomas Gleixner <tglx@linutronix.de>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Borislav Petkov <bp@alien8.de>
      Cc: "H. Peter Anvin" <hpa@zytor.com>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: stable@vger.kernel.org
      Fixes: 768ae440 ("x86/ftrace: Use text_poke()")
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      ac6c1b2c
    • Steven Rostedt (Google)'s avatar
      tracing: Use a copy of the va_list for __assign_vstr() · 3a2dcbaf
      Steven Rostedt (Google) authored
      If an instance of tracing enables the same trace event as another
      instance, or the top level instance, or even perf, then the va_list passed
      into some tracepoints can be used more than once.
      
      As va_list can only be traversed once, this can cause issues:
      
       # cat /sys/kernel/tracing/instances/qla2xxx/trace
                   cat-56106   [012] ..... 2419873.470098: ql_dbg_log: qla2xxx [0000:05:00.0]-1054:14:  Entered (null).
                   cat-56106   [012] ..... 2419873.470101: ql_dbg_log: qla2xxx [0000:05:00.0]-1000:14:  Entered ×+<96>²Ü<98>^H.
                   cat-56106   [012] ..... 2419873.470102: ql_dbg_log: qla2xxx [0000:05:00.0]-1006:14:  Prepare to issue mbox cmd=0xde589000.
      
       # cat /sys/kernel/tracing/trace
                   cat-56106   [012] ..... 2419873.470097: ql_dbg_log: qla2xxx [0000:05:00.0]-1054:14:  Entered qla2x00_get_firmware_state.
                   cat-56106   [012] ..... 2419873.470100: ql_dbg_log: qla2xxx [0000:05:00.0]-1000:14:  Entered qla2x00_mailbox_command.
                   cat-56106   [012] ..... 2419873.470102: ql_dbg_log: qla2xxx [0000:05:00.0]-1006:14:  Prepare to issue mbox cmd=0x69.
      
      The instance version is corrupted because the top level instance iterated
      the va_list first.
      
      Use va_copy() in the __assign_vstr() macro to make sure that each trace
      event for each use case gets a fresh va_list.
      
      Link: https://lore.kernel.org/all/259d53a5-958e-6508-4e45-74dba2821242@marvell.com/
      Link: https://lkml.kernel.org/r/20220719182004.21daa83e@gandalf.local.home
      
      Fixes: 0563231f ("tracing/events: Add __vstring() and __assign_vstr() helper macros")
      Reported-by: default avatarArun Easi <aeasi@marvell.com>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      3a2dcbaf
    • Steven Rostedt (Google)'s avatar
      batman-adv: tracing: Use the new __vstring() helper · 9abc2918
      Steven Rostedt (Google) authored
      Instead of open coding a __dynamic_array() with a fixed length (which
      defeats the purpose of the dynamic array in the first place). Use the new
      __vstring() helper that will use a va_list and only write enough of the
      string into the ring buffer that is needed.
      
      Link: https://lkml.kernel.org/r/20220724191650.236b1355@rorschach.local.home
      
      Cc: Marek Lindner <mareklindner@neomailbox.ch>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: Simon Wunderlich <sw@simonwunderlich.de>
      Cc: Antonio Quartulli <a@unstable.cc>
      Cc: "David S. Miller" <davem@davemloft.net>
      Cc: Eric Dumazet <edumazet@google.com>
      Cc: Jakub Kicinski <kuba@kernel.org>
      Cc: Paolo Abeni <pabeni@redhat.com>
      Cc: b.a.t.m.a.n@lists.open-mesh.org
      Cc: netdev@vger.kernel.org
      Acked-by: default avatarSven Eckelmann <sven@narfation.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      9abc2918
  2. 24 Jul, 2022 9 commits
  3. 19 Jul, 2022 3 commits
  4. 15 Jul, 2022 9 commits
    • Steven Rostedt (Google)'s avatar
      xhci: tracing: Use the new __vstring() helper · 0ba4c9de
      Steven Rostedt (Google) authored
      Instead of open coding a __dynamic_array() with a fixed length (which
      defeats the purpose of the dynamic array in the first place). Use the new
      __vstring() helper that will use a va_list and only write enough of the
      string into the ring buffer that is needed.
      
      Link: https://lkml.kernel.org/r/20220705224750.172301548@goodmis.org
      
      Cc: Mathias Nyman <mathias.nyman@intel.com>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: Greg Kroah-Hartman <gregkh@linuxfoundation.org>
      Cc: linux-usb@vger.kernel.org
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      0ba4c9de
    • Steven Rostedt (Google)'s avatar
      usb: chipidea: tracing: Use the new __vstring() helper · 1b756b37
      Steven Rostedt (Google) authored
      Instead of open coding a __dynamic_array() with a fixed length (which
      defeats the purpose of the dynamic array in the first place). Use the new
      __vstring() helper that will use a va_list and only write enough of the
      string into the ring buffer that is needed.
      
      Link: https://lkml.kernel.org/r/20220705224749.991587733@goodmis.org
      
      Cc: Peter Chen <peter.chen@kernel.org>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: Greg Kroah-Hartman <gregkh@linuxfoundation.org>
      Cc: linux-usb@vger.kernel.org
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      1b756b37
    • Steven Rostedt (Google)'s avatar
      tracing/iwlwifi: Use the new __vstring() helper · c7c37bb8
      Steven Rostedt (Google) authored
      Instead of open coding a __dynamic_array() with a fixed length (which
      defeats the purpose of the dynamic array in the first place). Use the new
      __vstring() helper that will use a va_list and only write enough of the
      string into the ring buffer that is needed.
      
      Link: https://lkml.kernel.org/r/20220705224749.806599472@goodmis.org
      
      Cc: Gregory Greenman <gregory.greenman@intel.com>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: Kalle Valo <kvalo@kernel.org>
      Cc: "David S. Miller" <davem@davemloft.net>
      Cc: Eric Dumazet <edumazet@google.com>
      Cc: Jakub Kicinski <kuba@kernel.org>
      Cc: Paolo Abeni <pabeni@redhat.com>
      Cc: linux-wireless@vger.kernel.org
      Cc: netdev@vger.kernel.org
      Acked-by: default avatarKalle Valo <kvalo@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      c7c37bb8
    • Steven Rostedt (Google)'s avatar
      tracing/brcm: Use the new __vstring() helper · b6d18ab3
      Steven Rostedt (Google) authored
      Instead of open coding a __dynamic_array() with a fixed length (which
      defeats the purpose of the dynamic array in the first place). Use the new
      __vstring() helper that will use a va_list and only write enough of the
      string into the ring buffer that is needed.
      
      Link: https://lkml.kernel.org/r/20220705224749.622796175@goodmis.org
      
      Cc: Arend van Spriel <aspriel@gmail.com>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: Franky Lin <franky.lin@broadcom.com>
      Cc: Hante Meuleman <hante.meuleman@broadcom.com>
      Cc: Kalle Valo <kvalo@kernel.org>
      Cc: "David S. Miller" <davem@davemloft.net>
      Cc: Eric Dumazet <edumazet@google.com>
      Cc: Jakub Kicinski <kuba@kernel.org>
      Cc: Paolo Abeni <pabeni@redhat.com>
      Cc: linux-wireless@vger.kernel.org
      Cc: brcm80211-dev-list.pdl@broadcom.com
      Cc: SHA-cyfmac-dev-list@infineon.com
      Cc: netdev@vger.kernel.org
      Acked-by: default avatarKalle Valo <kvalo@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      b6d18ab3
    • Steven Rostedt (Google)'s avatar
      tracing/ath: Use the new __vstring() helper · c01406f8
      Steven Rostedt (Google) authored
      Instead of open coding a __dynamic_array() with a fixed length (which
      defeats the purpose of the dynamic array in the first place). Use the new
      __vstring() helper that will use a va_list and only write enough of the
      string into the ring buffer that is needed.
      
      Link: https://lkml.kernel.org/r/20220705224749.430339634@goodmis.org
      
      Cc: Kalle Valo <kvalo@kernel.org>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: "David S. Miller" <davem@davemloft.net>
      Cc: Eric Dumazet <edumazet@google.com>
      Cc: Jakub Kicinski <kuba@kernel.org>
      Cc: Paolo Abeni <pabeni@redhat.com>
      Cc: ath10k@lists.infradead.org
      Cc: linux-wireless@vger.kernel.org
      Cc: netdev@vger.kernel.org
      Cc: ath11k@lists.infradead.org
      Acked-by: default avatarKalle Valo <kvalo@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      c01406f8
    • Steven Rostedt (Google)'s avatar
      tracing/IB/hfi1: Use the new __vstring() helper · 8d7f5df0
      Steven Rostedt (Google) authored
      Instead of open coding a __dynamic_array() with a fixed length (which
      defeats the purpose of the dynamic array in the first place). Use the new
      __vstring() helper that will use a va_list and only write enough of the
      string into the ring buffer that is needed.
      
      Link: https://lkml.kernel.org/r/20220705224749.239494531@goodmis.org
      
      Cc: Dennis Dalessandro <dennis.dalessandro@cornelisnetworks.com>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: Jason Gunthorpe <jgg@ziepe.ca>
      Cc: Leon Romanovsky <leon@kernel.org>
      Cc: linux-rdma@vger.kernel.org
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      8d7f5df0
    • Steven Rostedt (Google)'s avatar
      tracing/events: Add __vstring() and __assign_vstr() helper macros · 0563231f
      Steven Rostedt (Google) authored
      There's several places that open code the following logic:
      
        TP_STRUCT__entry(__dynamic_array(char, msg, MSG_MAX)),
        TP_fast_assign(vsnprintf(__get_str(msg), MSG_MAX, vaf->fmt, *vaf->va);)
      
      To load a string created by variable array va_list.
      
      The main issue with this approach is that "MSG_MAX" usage in the
      __dynamic_array() portion. That actually just reserves the MSG_MAX in the
      event, and even wastes space because there's dynamic meta data also saved
      in the event to denote the offset and size of the dynamic array. It would
      have been better to just use a static __array() field.
      
      Instead, create __vstring() and __assign_vstr() that work like __string
      and __assign_str() but instead of taking a destination string to copy,
      take a format string and a va_list pointer and fill in the values.
      
      It uses the helper:
      
       #define __trace_event_vstr_len(fmt, va)		\
       ({							\
      	va_list __ap;					\
      	int __ret;					\
      							\
      	va_copy(__ap, *(va));				\
      	__ret = vsnprintf(NULL, 0, fmt, __ap) + 1;	\
      	va_end(__ap);					\
      							\
      	min(__ret, TRACE_EVENT_STR_MAX);		\
       })
      
      To figure out the length to store the string. It may be slightly slower as
      it needs to run the vsnprintf() twice, but it now saves space on the ring
      buffer.
      
      Link: https://lkml.kernel.org/r/20220705224749.053570613@goodmis.org
      
      Cc: Dennis Dalessandro <dennis.dalessandro@cornelisnetworks.com>
      Cc: Ingo Molnar <mingo@kernel.org>
      Cc: Andrew Morton <akpm@linux-foundation.org>
      Cc: Jason Gunthorpe <jgg@ziepe.ca>
      Cc: Leon Romanovsky <leon@kernel.org>
      Cc: Kalle Valo <kvalo@kernel.org>
      Cc: "David S. Miller" <davem@davemloft.net>
      Cc: Eric Dumazet <edumazet@google.com>
      Cc: Jakub Kicinski <kuba@kernel.org>
      Cc: Paolo Abeni <pabeni@redhat.com>
      Cc: Arend van Spriel <aspriel@gmail.com>
      Cc: Franky Lin <franky.lin@broadcom.com>
      Cc: Hante Meuleman <hante.meuleman@broadcom.com>
      Cc: Gregory Greenman <gregory.greenman@intel.com>
      Cc: Peter Chen <peter.chen@kernel.org>
      Cc: Greg Kroah-Hartman <gregkh@linuxfoundation.org>
      Cc: Mathias Nyman <mathias.nyman@intel.com>
      Cc: Chunfeng Yun <chunfeng.yun@mediatek.com>
      Cc: Bin Liu <b-liu@ti.com>
      Cc: Marek Lindner <mareklindner@neomailbox.ch>
      Cc: Simon Wunderlich <sw@simonwunderlich.de>
      Cc: Antonio Quartulli <a@unstable.cc>
      Cc: Sven Eckelmann <sven@narfation.org>
      Cc: Johannes Berg <johannes@sipsolutions.net>
      Cc: Jim Cromie <jim.cromie@gmail.com>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      0563231f
    • Steven Rostedt (Google)'s avatar
      neighbor: tracing: Have neigh_create event use __string() · 43b2aef3
      Steven Rostedt (Google) authored
      The dev field of the neigh_create event uses __dynamic_array() with a
      fixed size, which defeats the purpose of __dynamic_array(). Looking at the
      logic, as it already uses __assign_str(), just use the same logic in
      __string to create the size needed. It appears that because "dev" can be
      NULL, it needs the check. But __string() can have the same checks as
      __assign_str() so use them there too.
      
      Link: https://lkml.kernel.org/r/20220705183741.35387e3f@rorschach.local.home
      
      Cc: David Ahern <dsahern@gmail.com>
      Cc: David S. Miller <davem@davemloft.net>
      Cc: netdev@vger.kernel.org
      Acked-by: default avatarJakub Kicinski <kuba@kernel.org>
      Reviewed-by: default avatarDavid Ahern <dsahern@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      43b2aef3
    • Steven Rostedt (Google)'s avatar
      tracing/ipv4/ipv6: Use static array for name field in fib*_lookup_table event · fca8300f
      Steven Rostedt (Google) authored
      The fib_lookup_table and fib6_lookup_table events declare name as a
      dynamic_array, but also give it a fixed size, which defeats the purpose of
      the dynamic array, especially since the dynamic array also includes meta
      data in the event to specify its size.
      
      Since the size of the name is at most 16 bytes (defined by IFNAMSIZ),
      it is not worth spending the effort to determine the size of the string.
      
      Just use a fixed size array and copy into it. This will save 4 bytes that
      are used for the meta data that saves the size and position of a dynamic
      array, and even slightly speed up the event processing.
      
      Link: https://lkml.kernel.org/r/20220704091436.3705edbf@rorschach.local.home
      
      Cc: David S. Miller <davem@davemloft.net>
      Cc: netdev@vger.kernel.org
      Acked-by: default avatarJakub Kicinski <kuba@kernel.org>
      Reviewed-by: default avatarDavid Ahern <dsahern@kernel.org>
      Signed-off-by: default avatarSteven Rostedt (Google) <rostedt@goodmis.org>
      fca8300f
  5. 14 Jul, 2022 1 commit
  6. 12 Jul, 2022 3 commits