kernel/linux.git/include/rv/automata.h, branch linux-7.0.y

rv: Cleanup da_monitor after refactor

2026-01-12T06:43:49+00:00

Previous changes refactored the da_monitor header file to avoid using macros, however empty macros (e.g. DECLARE_DA_FUNCTION) were left to ease review with diff tools. Most macros also get the argument type which doesn't really have a purpose since states have their own enum and the storage in struct da_monitor is fixed to unsigned int. Remove empty and no longer required macros and substitute the type parameter with the appropriate enum. Additionally break long line and adjust the format overall. Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20251126104241.291258-3-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

rv: Refactor da_monitor to minimise macros

2026-01-12T06:43:49+00:00

The da_monitor helper functions are generated from macros of the type: DECLARE_DA_FUNCTION(name, type) \ static void da_func_x_##name(type arg) {} \ static void da_func_y_##name(type arg) {} \ This is good to minimise code duplication but the long macros made of skipped end of lines is rather hard to parse. Since functions are static, the advantage of naming them differently for each monitor is minimal. Refactor the da_monitor.h file to minimise macros, instead of declaring functions from macros, we simply declare them with the same name for all monitors (e.g. da_func_x) and for any remaining reference to the monitor name (e.g. tracepoints, enums, global variables) we use the CONCATENATE macro. In this way the file is much easier to maintain while keeping the same generality. Functions depending on the monitor types are now conditionally compiled according to the value of RV_MON_TYPE, which must be defined in the monitor source. The monitor type can be specified as in the original implementation, although it's best to keep the default implementation (unsigned char) as not all parts of code support larger data types, and likely there's no need. We keep the empty macro definitions to ease review of this change with diff tools, but cleanup is required. Also adapt existing monitors to keep the build working. Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20251126104241.291258-2-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

rv/include: Add helper functions for deterministic automata

2022-07-30T18:01:28+00:00

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 Cc: Guenter Roeck Cc: Jonathan Corbet Cc: Ingo Molnar Cc: Thomas Gleixner Cc: Peter Zijlstra Cc: Will Deacon Cc: Catalin Marinas Cc: Marco Elver Cc: Dmitry Vyukov Cc: "Paul E. McKenney" Cc: Shuah Khan Cc: Gabriele Paoloni Cc: Juri Lelli Cc: Clark Williams Cc: Tao Zhou Cc: Randy Dunlap 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 Signed-off-by: Steven Rostedt (Google)