Over the last years, I've been exploring the possibility of
verifying the Linux kernel behavior using Runtime Verification.
Runtime Verification (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 for complex
systems.
Instead of relying on a fine-grained model of a system (e.g., a
re-implementation a instruction level), RV works by analyzing the trace of the
system's actual execution, comparing it against a formal specification of
the system behavior.
The usage of deterministic automaton for RV is a well-established
approach. In the specific case of the Linux kernel, you can check how
to model complex behavior of the Linux kernel with 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.
And how efficient is this approach here:
DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread
synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
Architecture, 2020, 107: 101729.
tlrd: it is possible to model complex behaviors in a modular way, with
an acceptable overhead (even for production systems). See this
presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg
Here I am proposing a more practical approach for the usage of deterministic
automata for runtime verification, and it includes:
- An interface for controlling the verification;
- A tool and set of headers that enables the automatic code
generation of the RV monitor (Monitor Synthesis);
- Sample monitors to evaluate the interface;
- A sample monitor developed in the context of the Elisa Project
demonstrating how to use RV in the context of safety-critical
systems.
Given that RV is a tracing consumer, the code is being placed inside the
tracing subsystem (Steven and I have been talking about it for a while).
Changes from v3:
- Rebased on 5.19
(rostedt's request were made on 1x1 meetings)
- Moved monitors to monitors/$name/ (Rostedt)
- Consolidate the tracepoints into a single include file in the default
directory (trave/events/rv.h) (Rostedt)
- The tracepoints now record the entire string to the buffer.
- Change the enable_monitors to disable monitors with ! (instead of -).
(Rostedt)
- Add a suffix to the state/events enums, to avoid conflict in the
vmlinux.h used by eBPF.
- The models are now placed in the $name.h (it used to store the
tracepoints, but they are now consolidated in a single file)
- dot2c and dot2k updated to the changes
- models re-generated with these new standards.
- user-space tools moved to an directory outside of tools/tracing as
other methods of verification/log sources are planned.
Changes from v2:
- Tons of checkpatch and kernel test robot
- Moved files to better places
- Adjusted watchdog tracepoints patch (Guenter Roeck)
- Added pretimeout watchdog events (Peter Enderborg)
- Used task struct to store per-task monitors (Peter Zijlstra)
- Changed the instrumentation to use internal definition of tracepoint
and check the callback signature (Steven Rostedt)
- Used printk_deferred() and removed the comment about deadlocks
(Shuah Khan/John Ogness)
- Some simplifications:
- Removed the safe watchdog nowayout for now (myself)
- Removed export symbols for now (myself)
Changes from V1:
- rebased to the latest kernel;
- code cleanup;
- the watchdog dev monitor;
- safety app;
Things kept for a second moment (after this patchset):
- Add a reactor tha enables the visualization of the visited
states via KCOV (Marco Elver & Dmitry Vyukov)
- Add a CRC method to check from user-space if the values
exported by the monitor were not corrupted by any other
kernel task (Gabriele Paoloni)
- Export symbols for external modules
- dot2bpf
Daniel Bristot de Oliveira (20):
rv: Add Runtime Verification (RV) interface
rv: Add runtime reactors interface
rv/include: Add helper functions for deterministic automata
rv/include: Add deterministic automata monitor definition via C macros
rv/include: Add instrumentation helper functions
tools/rv: Add dot2c
tools/rv: Add dot2k
rv/monitor: Add the wip monitor skeleton created by dot2k
rv/monitor: wip instrumentation and Makefile/Kconfig entries
rv/monitor: Add the wwnr monitor skeleton created by dot2k
rv/monitor: wwnr instrumentation and Makefile/Kconfig entries
rv/reactor: Add the printk reactor
rv/reactor: Add the panic reactor
Documentation/rv: Add a basic documentation
Documentation/rv: Add deterministic automata monitor synthesis
documentation
Documentation/rv: Add deterministic automata instrumentation
documentation
watchdog/dev: Add tracepoints
rv/monitor: Add safe watchdog monitor
rv/safety_app: Add a safety_app sample
Documentation/rv: Add watchdog-monitor documentation
Documentation/trace/index.rst | 1 +
.../trace/rv/da_monitor_instrumentation.rst | 223 ++++++
.../trace/rv/da_monitor_synthesis.rst | 284 +++++++
Documentation/trace/rv/index.rst | 9 +
.../trace/rv/runtime-verification.rst | 233 ++++++
Documentation/trace/rv/watchdog-monitor.rst | 250 ++++++
drivers/watchdog/watchdog_dev.c | 43 +-
drivers/watchdog/watchdog_pretimeout.c | 2 +
include/linux/rv.h | 38 +
include/linux/sched.h | 11 +
include/linux/watchdog.h | 7 +-
include/rv/automata.h | 49 ++
include/rv/da_monitor.h | 419 ++++++++++
include/rv/instrumentation.h | 23 +
include/rv/rv.h | 32 +
include/trace/events/rv.h | 153 ++++
include/trace/events/watchdog.h | 101 +++
kernel/fork.c | 14 +
kernel/trace/Kconfig | 2 +
kernel/trace/Makefile | 2 +
kernel/trace/rv/Kconfig | 84 ++
kernel/trace/rv/Makefile | 9 +
kernel/trace/rv/monitors/safe_wtd/safe_wtd.c | 300 +++++++
kernel/trace/rv/monitors/safe_wtd/safe_wtd.h | 84 ++
kernel/trace/rv/monitors/wip/wip.c | 110 +++
kernel/trace/rv/monitors/wip/wip.h | 38 +
kernel/trace/rv/monitors/wwnr/wwnr.c | 109 +++
kernel/trace/rv/monitors/wwnr/wwnr.h | 38 +
kernel/trace/rv/reactor_panic.c | 44 +
kernel/trace/rv/reactor_printk.c | 43 +
kernel/trace/rv/rv.c | 757 ++++++++++++++++++
kernel/trace/rv/rv.h | 54 ++
kernel/trace/rv/rv_reactors.c | 476 +++++++++++
kernel/trace/trace.c | 4 +
kernel/trace/trace.h | 2 +
tools/verification/dot2/Makefile | 26 +
tools/verification/dot2/automata.py | 179 +++++
tools/verification/dot2/dot2c | 30 +
tools/verification/dot2/dot2c.py | 244 ++++++
tools/verification/dot2/dot2k | 50 ++
tools/verification/dot2/dot2k.py | 177 ++++
.../dot2/dot2k_templates/main_global.c | 94 +++
.../dot2/dot2k_templates/main_per_cpu.c | 94 +++
.../dot2/dot2k_templates/main_per_task.c | 94 +++
tools/verification/safety_app/Makefile | 51 ++
tools/verification/safety_app/safety_app.c | 614 ++++++++++++++
46 files changed, 5691 insertions(+), 10 deletions(-)
create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst
create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
create mode 100644 Documentation/trace/rv/index.rst
create mode 100644 Documentation/trace/rv/runtime-verification.rst
create mode 100644 Documentation/trace/rv/watchdog-monitor.rst
create mode 100644 include/linux/rv.h
create mode 100644 include/rv/automata.h
create mode 100644 include/rv/da_monitor.h
create mode 100644 include/rv/instrumentation.h
create mode 100644 include/rv/rv.h
create mode 100644 include/trace/events/rv.h
create mode 100644 include/trace/events/watchdog.h
create mode 100644 kernel/trace/rv/Kconfig
create mode 100644 kernel/trace/rv/Makefile
create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.c
create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.h
create mode 100644 kernel/trace/rv/monitors/wip/wip.c
create mode 100644 kernel/trace/rv/monitors/wip/wip.h
create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c
create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h
create mode 100644 kernel/trace/rv/reactor_panic.c
create mode 100644 kernel/trace/rv/reactor_printk.c
create mode 100644 kernel/trace/rv/rv.c
create mode 100644 kernel/trace/rv/rv.h
create mode 100644 kernel/trace/rv/rv_reactors.c
create mode 100644 tools/verification/dot2/Makefile
create mode 100644 tools/verification/dot2/automata.py
create mode 100644 tools/verification/dot2/dot2c
create mode 100644 tools/verification/dot2/dot2c.py
create mode 100644 tools/verification/dot2/dot2k
create mode 100644 tools/verification/dot2/dot2k.py
create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c
create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c
create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c
create mode 100644 tools/verification/safety_app/Makefile
create mode 100644 tools/verification/safety_app/safety_app.c
--
2.35.1
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
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
tools/verification/dot2/Makefile | 21 +++
tools/verification/dot2/automata.py | 179 ++++++++++++++++++++
tools/verification/dot2/dot2c | 30 ++++
tools/verification/dot2/dot2c.py | 244 ++++++++++++++++++++++++++++
4 files changed, 474 insertions(+)
create mode 100644 tools/verification/dot2/Makefile
create mode 100644 tools/verification/dot2/automata.py
create mode 100644 tools/verification/dot2/dot2c
create mode 100644 tools/verification/dot2/dot2c.py
diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile
new file mode 100644
index 000000000000..235d182f6b2c
--- /dev/null
+++ b/tools/verification/dot2/Makefile
@@ -0,0 +1,21 @@
+INSTALL=install
+
+prefix ?= /usr
+bindir ?= $(prefix)/bin
+mandir ?= $(prefix)/share/man
+miscdir ?= $(prefix)/share/dot2
+srcdir ?= $(prefix)/src
+
+PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))')
+
+.PHONY: all
+all:
+
+.PHONY: clean
+clean:
+
+.PHONY: install
+install:
+ $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py
+ $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py
+ $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/
diff --git a/tools/verification/dot2/automata.py b/tools/verification/dot2/automata.py
new file mode 100644
index 000000000000..171ad4497983
--- /dev/null
+++ b/tools/verification/dot2/automata.py
@@ -0,0 +1,179 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# automata object: parse a dot file into a python object
+# For more information, see:
+# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# This program was written in the development of this paper:
+# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+# "Efficient Formal Verification for the Linux Kernel." International
+# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# Copyright 2018-2020 Red Hat, Inc.
+#
+# Author:
+# Daniel Bristot de Oliveira <[email protected]>
+
+import ntpath
+
+class Automata:
+ """Automata class: Reads a dot file and part it as an automata.
+
+ Attributes:
+ dot_file: A dot file with an state_automaton definition.
+ """
+
+ def __init__(self, file_path):
+ self.__dot_path=file_path
+ self.name=self.__get_model_name()
+ self.__dot_lines = self.__open_dot()
+ self.states, self.initial_state, self.final_states = self.__get_state_variables()
+ self.events = self.__get_event_variables()
+ self.function = self.__create_matrix()
+
+ def __get_model_name(self):
+ basename=ntpath.basename(self.__dot_path)
+ if basename.endswith(".dot") == False:
+ print("not a dot file")
+ raise Exception("not a dot file: %s" % self.__dot_path)
+
+ model_name=basename[0:-4]
+ if model_name.__len__() == 0:
+ raise Exception("not a dot file: %s" % self.__dot_path)
+
+ return model_name
+
+ def __open_dot(self):
+ cursor = 0
+ dot_lines = []
+ try:
+ dot_file = open(self.__dot_path)
+ except:
+ raise Exception("Cannot open the file: %s" % self.__dot_path)
+
+ dot_lines = dot_file.read().splitlines()
+ dot_file.close()
+
+ # checking the first line:
+ line = dot_lines[cursor].split()
+
+ if (line[0] != "digraph") and (line[1] != "state_automaton"):
+ raise Exception("Not a valid .dot format: %s" % self.__dot_path)
+ else:
+ cursor = cursor + 1
+ return dot_lines
+
+ def __get_cursor_begin_states(self):
+ cursor = 0
+ while self.__dot_lines[cursor].split()[0] != "{node":
+ cursor += 1
+ return cursor
+
+ def __get_cursor_begin_events(self):
+ cursor = 0
+ while self.__dot_lines[cursor].split()[0] != "{node":
+ cursor += 1
+ while self.__dot_lines[cursor].split()[0] == "{node":
+ cursor += 1
+ # skip initial state transition
+ cursor += 1
+ return cursor
+
+ def __get_state_variables(self):
+ # wait for node declaration
+ states = []
+ final_states=[]
+
+ has_final_states = False
+ cursor = self.__get_cursor_begin_states()
+
+ # process nodes
+ while self.__dot_lines[cursor].split()[0] == "{node":
+ line = self.__dot_lines[cursor].split()
+ raw_state = line[-1]
+
+ # "enabled_fired"}; -> enabled_fired
+ state = raw_state.replace('"', '').replace('};', '').replace(',','_')
+ if state[0:7] == "__init_":
+ initial_state = state[7:]
+ else:
+ states.append(state)
+ if self.__dot_lines[cursor].__contains__("doublecircle") == True:
+ final_states.append(state)
+ has_final_states = True
+
+ if self.__dot_lines[cursor].__contains__("ellipse") == True:
+ final_states.append(state)
+ has_final_states = True
+
+ cursor = cursor + 1
+
+ states = sorted(set(states))
+ states.remove(initial_state)
+
+ # Insert the initial state at the bein og the states
+ states.insert(0, initial_state)
+
+ if has_final_states == False:
+ final_states.append(initial_state)
+
+ return states, initial_state, final_states
+
+ def __get_event_variables(self):
+ # here we are at the begin of transitions, take a note, we will return later.
+ cursor = self.__get_cursor_begin_events()
+
+ events = []
+ while self.__dot_lines[cursor][1] == '"':
+ # transitions have the format:
+ # "all_fired" -> "both_fired" [ label = "disable_irq" ];
+ # ------------ event is here ------------^^^^^
+ if self.__dot_lines[cursor].split()[1] == "->":
+ line = self.__dot_lines[cursor].split()
+ event = line[-2].replace('"','')
+
+ # when a transition has more than one lables, they are like this
+ # "local_irq_enable\nhw_local_irq_enable_n"
+ # so split them.
+
+ event = event.replace("\\n", " ")
+ for i in event.split():
+ events.append(i)
+ cursor = cursor + 1
+
+ return sorted(set(events))
+
+ def __create_matrix(self):
+ # transform the array into a dictionary
+ events = self.events
+ states = self.states
+ events_dict = {}
+ states_dict = {}
+ nr_event = 0
+ for event in events:
+ events_dict[event] = nr_event
+ nr_event += 1
+
+ nr_state = 0
+ for state in states:
+ states_dict[state] = nr_state
+ nr_state = nr_state + 1
+
+ # declare the matrix....
+ matrix = [['-1' for x in range(nr_event)] for y in range(nr_state)]
+
+ # and we are back! Let's fill the matrix
+ cursor = self.__get_cursor_begin_events()
+
+ while self.__dot_lines[cursor][1] == '"':
+ if self.__dot_lines[cursor].split()[1] == "->":
+ line = self.__dot_lines[cursor].split()
+ origin_state = line[0].replace('"','').replace(',','_')
+ dest_state = line[2].replace('"','').replace(',','_')
+ possible_events = line[-2].replace('"','').replace("\\n", " ")
+ for event in possible_events.split():
+ matrix[states_dict[origin_state]][events_dict[event]] = dest_state
+ cursor = cursor + 1
+
+ return matrix
diff --git a/tools/verification/dot2/dot2c b/tools/verification/dot2/dot2c
new file mode 100644
index 000000000000..0165f203dedc
--- /dev/null
+++ b/tools/verification/dot2/dot2c
@@ -0,0 +1,30 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# dot2m: transform dot files into C structures.
+# For more information, see:
+# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# This program was written in the development of this paper:
+# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+# "Efficient Formal Verification for the Linux Kernel." International
+# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# Copyright 2018-2020 Red Hat, Inc.
+#
+# Author:
+# Daniel Bristot de Oliveira <[email protected]>
+
+if __name__ == '__main__':
+ from dot2 import dot2c
+ import argparse
+ import ntpath
+ import sys
+
+ parser = argparse.ArgumentParser(description='dot2c: converts a .dot file into a C structure')
+ parser.add_argument('dot_file', help='The dot file to be converted')
+
+
+ args = parser.parse_args()
+ d=dot2c.Dot2c(args.dot_file)
+ d.print_model_classic()
diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/dot2/dot2c.py
new file mode 100644
index 000000000000..07f040ebf882
--- /dev/null
+++ b/tools/verification/dot2/dot2c.py
@@ -0,0 +1,244 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+#
+# dot2c: transform dot files into C structures.
+# For more information, see:
+# https://bristot.me/efficient-formal-verification-for-the-linux-kernel/
+#
+# This program was written in the development of this paper:
+# de Oliveira, D. B. and Cucinotta, T. and de Oliveira, R. S.
+# "Efficient Formal Verification for the Linux Kernel." International
+# Conference on Software Engineering and Formal Methods. Springer, Cham, 2019.
+#
+# Copyright 2018-2022 Red Hat, Inc.
+#
+# Author:
+# Daniel Bristot de Oliveira <[email protected]>
+
+from dot2.automata import Automata
+
+class Dot2c(Automata):
+ enum_suffix=""
+ enum_states_def="states"
+ enum_events_def="events"
+ struct_automaton_def="automaton"
+ var_automaton_def="aut"
+
+ def __init__(self, file_path):
+ super().__init__(file_path)
+ self.line_length=80
+
+ def __buff_to_string(self, buff):
+ string=""
+
+ for line in buff:
+ string=string + line + "\n"
+
+ # cut off the last \n
+ return string[:-1]
+
+ def __get_enum_states_content(self):
+ buff=[]
+ buff.append("\t%s%s = 0," % (self.initial_state, self.enum_suffix))
+ for state in self.states:
+ if state != self.initial_state:
+ buff.append("\t%s%s," % (state, self.enum_suffix))
+ buff.append("\tstate_max%s" % (self.enum_suffix))
+
+ return buff
+
+ def get_enum_states_string(self):
+ buff=self.__get_enum_states_content()
+ return self.__buff_to_string(buff)
+
+ def format_states_enum(self):
+ buff=[]
+ buff.append("enum %s {" % self.enum_states_def)
+ buff.append(self.get_enum_states_string())
+ buff.append("};\n")
+
+ return buff
+
+ def __get_enum_events_content(self):
+ buff=[]
+ first=True
+ for event in self.events:
+ if first:
+ buff.append("\t%s%s = 0," % (event, self.enum_suffix))
+ first=False
+ else:
+ buff.append("\t%s%s," % (event, self.enum_suffix))
+ buff.append("\tevent_max%s" % self.enum_suffix)
+
+ return buff
+
+ def get_enum_events_string(self):
+ buff=self.__get_enum_events_content()
+ return self.__buff_to_string(buff)
+
+ def format_events_enum(self):
+ buff=[]
+ buff.append("enum %s {" % self.enum_events_def)
+ buff.append(self.get_enum_events_string())
+ buff.append("};\n")
+
+ return buff
+
+ def get_minimun_type(self):
+ min_type="char"
+
+ if self.states.__len__() > 255:
+ min_type="short"
+
+ if self.states.__len__() > 65535:
+ min_type="int"
+
+ return min_type
+
+ def format_automaton_definition(self):
+ min_type = self.get_minimun_type()
+ buff=[]
+ buff.append("struct %s {" % self.struct_automaton_def)
+ buff.append("\tchar *state_names[state_max%s];" % (self.enum_suffix))
+ buff.append("\tchar *event_names[event_max%s];" % (self.enum_suffix))
+ buff.append("\t%s function[state_max%s][event_max%s];" % (min_type, self.enum_suffix, self.enum_suffix))
+ buff.append("\t%s initial_state;" % min_type)
+ buff.append("\tchar final_states[state_max%s];" % (self.enum_suffix))
+ buff.append("};\n")
+ return buff
+
+ def format_aut_init_header(self):
+ buff=[]
+ buff.append("struct %s %s = {" % (self.struct_automaton_def, self.var_automaton_def))
+ return buff
+
+ def __get_string_vector_per_line_content(self, buff):
+ first=True
+ string=""
+ for entry in buff:
+ if first:
+ string = string + "\t\t\"" + entry
+ first=False;
+ else:
+ string = string + "\",\n\t\t\"" + entry
+ string = string + "\""
+
+ return string
+
+ def get_aut_init_events_string(self):
+ return self.__get_string_vector_per_line_content(self.events)
+
+ def get_aut_init_states_string(self):
+ return self.__get_string_vector_per_line_content(self.states)
+
+ def format_aut_init_events_string(self):
+ buff=[]
+ buff.append("\t.event_names = {")
+ buff.append(self.get_aut_init_events_string())
+ buff.append("\t},")
+ return buff
+
+ def format_aut_init_states_string(self):
+ buff=[]
+ buff.append("\t.state_names = {")
+ buff.append(self.get_aut_init_states_string())
+ buff.append("\t},")
+
+ return buff
+
+ def __get_max_strlen_of_states(self):
+ return max(self.states, key=len).__len__()
+
+ def __get_state_string_length(self):
+ maxlen = self.__get_max_strlen_of_states() + self.enum_suffix.__len__()
+ return "%" + str(maxlen) + "s"
+
+ def get_aut_init_function(self):
+ nr_states=self.states.__len__()
+ nr_events=self.events.__len__()
+ buff=[]
+
+ strformat = self.__get_state_string_length()
+
+ for x in range(nr_states):
+ line="\t\t{ "
+ for y in range(nr_events):
+ next_state = self.function[x][y]
+ if next_state != '-1':
+ next_state = self.function[x][y] + self.enum_suffix
+
+ if y != nr_events-1:
+ line = line + strformat % next_state + ", "
+ else:
+ line = line + strformat % next_state + " },"
+ buff.append(line)
+
+ return self.__buff_to_string(buff)
+
+ def format_aut_init_function(self):
+ buff=[]
+ buff.append("\t.function = {")
+ buff.append(self.get_aut_init_function())
+ buff.append("\t},")
+
+ return buff
+
+ def get_aut_init_initial_state(self):
+ return self.initial_state
+
+ def format_aut_init_initial_state(self):
+ buff=[]
+ initial_state=self.get_aut_init_initial_state()
+ buff.append("\t.initial_state = " + initial_state + self.enum_suffix + ",")
+
+ return buff
+
+ def get_aut_init_final_states(self):
+ line=""
+ first=True
+ for state in self.states:
+ if first == False:
+ line = line + ', '
+ else:
+ first = False
+
+ if self.final_states.__contains__(state):
+ line = line + '1'
+ else:
+ line = line + '0'
+ return line
+
+ def format_aut_init_final_states(self):
+ buff=[]
+ buff.append("\t.final_states = { %s }," % self.get_aut_init_final_states())
+
+ return buff
+
+ def __get_automaton_initialization_footer_string(self):
+ footer="};\n"
+ return footer
+
+ def format_aut_init_footer(self):
+ buff=[]
+ buff.append(self.__get_automaton_initialization_footer_string())
+
+ return buff
+
+ def format_model(self):
+ buff=[]
+ buff += self.format_states_enum()
+ buff += self.format_events_enum()
+ buff += self.format_automaton_definition()
+ buff += self.format_aut_init_header()
+ buff += self.format_aut_init_states_string()
+ buff += self.format_aut_init_events_string()
+ buff += self.format_aut_init_function()
+ buff += self.format_aut_init_initial_state()
+ buff += self.format_aut_init_final_states()
+ buff += self.format_aut_init_footer()
+
+ return buff
+
+ def print_model_classic(self):
+ buff=self.format_model()
+ print(self.__buff_to_string(buff))
--
2.35.1
Add a set of tracepoints, enabling the observability of the watchdog
device interactions with user-space.
The events are:
watchdog:watchdog_open
watchdog:watchdog_close
watchdog:watchdog_start
watchdog:watchdog_stop
watchdog:watchdog_set_timeout
watchdog:watchdog_ping
watchdog:watchdog_nowayout
watchdog:watchdog_set_keep_alive
watchdog:watchdog_keep_alive
watchdog:watchdog_set_pretimeout
watchdog:watchdog_pretimeout
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
drivers/watchdog/watchdog_dev.c | 43 ++++++++++-
drivers/watchdog/watchdog_pretimeout.c | 2 +
include/linux/watchdog.h | 7 +-
include/trace/events/watchdog.h | 101 +++++++++++++++++++++++++
4 files changed, 143 insertions(+), 10 deletions(-)
create mode 100644 include/trace/events/watchdog.h
diff --git a/drivers/watchdog/watchdog_dev.c b/drivers/watchdog/watchdog_dev.c
index 54903f3c851e..2f28dc5ab763 100644
--- a/drivers/watchdog/watchdog_dev.c
+++ b/drivers/watchdog/watchdog_dev.c
@@ -44,6 +44,9 @@
#include <linux/watchdog.h> /* For watchdog specific items */
#include <linux/uaccess.h> /* For copy_to_user/put_user/... */
+#define CREATE_TRACE_POINTS
+#include <trace/events/watchdog.h>
+
#include "watchdog_core.h"
#include "watchdog_pretimeout.h"
@@ -130,9 +133,11 @@ static inline void watchdog_update_worker(struct watchdog_device *wdd)
if (watchdog_need_worker(wdd)) {
ktime_t t = watchdog_next_keepalive(wdd);
- if (t > 0)
+ if (t > 0) {
hrtimer_start(&wd_data->timer, t,
HRTIMER_MODE_REL_HARD);
+ trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
+ }
} else {
hrtimer_cancel(&wd_data->timer);
}
@@ -141,7 +146,7 @@ static inline void watchdog_update_worker(struct watchdog_device *wdd)
static int __watchdog_ping(struct watchdog_device *wdd)
{
struct watchdog_core_data *wd_data = wdd->wd_data;
- ktime_t earliest_keepalive, now;
+ ktime_t earliest_keepalive, now, next_keepalive;
int err;
earliest_keepalive = ktime_add(wd_data->last_hw_keepalive,
@@ -149,14 +154,16 @@ static int __watchdog_ping(struct watchdog_device *wdd)
now = ktime_get();
if (ktime_after(earliest_keepalive, now)) {
- hrtimer_start(&wd_data->timer,
- ktime_sub(earliest_keepalive, now),
+ next_keepalive = ktime_sub(earliest_keepalive, now);
+ hrtimer_start(&wd_data->timer, next_keepalive,
HRTIMER_MODE_REL_HARD);
+ trace_watchdog_set_keep_alive(wdd, ktime_to_ms(next_keepalive));
return 0;
}
wd_data->last_hw_keepalive = now;
+ trace_watchdog_ping(wdd);
if (wdd->ops->ping)
err = wdd->ops->ping(wdd); /* ping the watchdog */
else
@@ -215,6 +222,7 @@ static void watchdog_ping_work(struct kthread_work *work)
wd_data = container_of(work, struct watchdog_core_data, work);
mutex_lock(&wd_data->lock);
+ trace_watchdog_keep_alive(wd_data->wdd);
if (watchdog_worker_should_ping(wd_data))
__watchdog_ping(wd_data->wdd);
mutex_unlock(&wd_data->lock);
@@ -250,6 +258,8 @@ static int watchdog_start(struct watchdog_device *wdd)
set_bit(_WDOG_KEEPALIVE, &wd_data->status);
+ trace_watchdog_start(wdd);
+
started_at = ktime_get();
if (watchdog_hw_running(wdd) && wdd->ops->ping) {
err = __watchdog_ping(wdd);
@@ -294,6 +304,7 @@ static int watchdog_stop(struct watchdog_device *wdd)
return -EBUSY;
}
+ trace_watchdog_stop(wdd);
if (wdd->ops->stop) {
clear_bit(WDOG_HW_RUNNING, &wdd->status);
err = wdd->ops->stop(wdd);
@@ -367,6 +378,7 @@ static int watchdog_set_timeout(struct watchdog_device *wdd,
if (watchdog_timeout_invalid(wdd, timeout))
return -EINVAL;
+ trace_watchdog_set_timeout(wdd, timeout);
if (wdd->ops->set_timeout) {
err = wdd->ops->set_timeout(wdd, timeout);
} else {
@@ -399,6 +411,8 @@ static int watchdog_set_pretimeout(struct watchdog_device *wdd,
if (watchdog_pretimeout_invalid(wdd, timeout))
return -EINVAL;
+ trace_watchdog_set_pretimeout(wdd, timeout);
+
if (wdd->ops->set_pretimeout && (wdd->info->options & WDIOF_PRETIMEOUT))
err = wdd->ops->set_pretimeout(wdd, timeout);
else
@@ -430,6 +444,23 @@ static int watchdog_get_timeleft(struct watchdog_device *wdd,
return 0;
}
+/**
+ * watchdog_set_nowayout - set nowaout bit
+ * @wdd: The watchdog device to set nowayoutbit
+ * @nowayout A boolean on/off switcher
+ *
+ * If nowayout boolean is true, the nowayout option is set. No action is
+ * taken if nowayout is false.
+ */
+void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
+{
+ if (nowayout) {
+ set_bit(WDOG_NO_WAY_OUT, &wdd->status);
+ trace_watchdog_nowayout(wdd);
+ }
+}
+EXPORT_SYMBOL(watchdog_set_nowayout);
+
#ifdef CONFIG_WATCHDOG_SYSFS
static ssize_t nowayout_show(struct device *dev, struct device_attribute *attr,
char *buf)
@@ -861,6 +892,8 @@ static int watchdog_open(struct inode *inode, struct file *file)
goto out_clear;
}
+ trace_watchdog_open(wdd);
+
err = watchdog_start(wdd);
if (err < 0)
goto out_mod;
@@ -883,6 +916,7 @@ static int watchdog_open(struct inode *inode, struct file *file)
return stream_open(inode, file);
out_mod:
+ trace_watchdog_close(wdd);
module_put(wd_data->wdd->ops->owner);
out_clear:
clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
@@ -944,6 +978,7 @@ static int watchdog_release(struct inode *inode, struct file *file)
/* make sure that /dev/watchdog can be re-opened */
clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
+ trace_watchdog_close(wdd);
done:
running = wdd && watchdog_hw_running(wdd);
mutex_unlock(&wd_data->lock);
diff --git a/drivers/watchdog/watchdog_pretimeout.c b/drivers/watchdog/watchdog_pretimeout.c
index 376a495ab80c..58c391ed2205 100644
--- a/drivers/watchdog/watchdog_pretimeout.c
+++ b/drivers/watchdog/watchdog_pretimeout.c
@@ -8,6 +8,7 @@
#include <linux/spinlock.h>
#include <linux/string.h>
#include <linux/watchdog.h>
+#include <trace/events/watchdog.h>
#include "watchdog_core.h"
#include "watchdog_pretimeout.h"
@@ -107,6 +108,7 @@ void watchdog_notify_pretimeout(struct watchdog_device *wdd)
return;
}
+ trace_watchdog_pretimeout(wdd);
wdd->gov->pretimeout(wdd);
spin_unlock_irqrestore(&pretimeout_lock, flags);
}
diff --git a/include/linux/watchdog.h b/include/linux/watchdog.h
index 99660197a36c..11d93407e492 100644
--- a/include/linux/watchdog.h
+++ b/include/linux/watchdog.h
@@ -139,12 +139,7 @@ static inline bool watchdog_hw_running(struct watchdog_device *wdd)
return test_bit(WDOG_HW_RUNNING, &wdd->status);
}
-/* Use the following function to set the nowayout feature */
-static inline void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
-{
- if (nowayout)
- set_bit(WDOG_NO_WAY_OUT, &wdd->status);
-}
+void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout);
/* Use the following function to stop the watchdog on reboot */
static inline void watchdog_stop_on_reboot(struct watchdog_device *wdd)
diff --git a/include/trace/events/watchdog.h b/include/trace/events/watchdog.h
new file mode 100644
index 000000000000..145cd6cfaa02
--- /dev/null
+++ b/include/trace/events/watchdog.h
@@ -0,0 +1,101 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+#undef TRACE_SYSTEM
+#define TRACE_SYSTEM watchdog
+
+#if !defined(_TRACE_WATCHDOG_H) || defined(TRACE_HEADER_MULTI_READ)
+#define _TRACE_WATCHDOG_H
+
+#include <linux/tracepoint.h>
+
+/*
+ * These are all events whose sole argument is the watchdog id.
+ */
+DECLARE_EVENT_CLASS(dev_operations_template,
+
+ TP_PROTO(struct watchdog_device *wdd),
+
+ TP_ARGS(wdd),
+
+ TP_STRUCT__entry(
+ __field(__u32, id)
+ ),
+
+ TP_fast_assign(
+ __entry->id = wdd->id;
+ ),
+
+ TP_printk("id=%d",
+ __entry->id)
+);
+
+DEFINE_EVENT(dev_operations_template, watchdog_open,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_close,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_start,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_stop,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_ping,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_nowayout,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_keep_alive,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+DEFINE_EVENT(dev_operations_template, watchdog_pretimeout,
+ TP_PROTO(struct watchdog_device *wdd),
+ TP_ARGS(wdd));
+
+/*
+ * These are all events with a device ID and a given timeout.
+ */
+DECLARE_EVENT_CLASS(watchdog_timeout_template,
+
+ TP_PROTO(struct watchdog_device *wdd, u64 timeout),
+
+ TP_ARGS(wdd, timeout),
+
+ TP_STRUCT__entry(
+ __field(__u32, id)
+ __field(__u64, timeout)
+ ),
+
+ TP_fast_assign(
+ __entry->id = wdd->id;
+ __entry->timeout = timeout;
+ ),
+
+ TP_printk("id=%d timeout=%llus",
+ __entry->id, __entry->timeout)
+);
+
+DEFINE_EVENT(watchdog_timeout_template, watchdog_set_timeout,
+ TP_PROTO(struct watchdog_device *wdd, u64 timeout),
+ TP_ARGS(wdd, timeout));
+
+DEFINE_EVENT(watchdog_timeout_template, watchdog_set_pretimeout,
+ TP_PROTO(struct watchdog_device *wdd, u64 timeout),
+ TP_ARGS(wdd, timeout));
+
+DEFINE_EVENT(watchdog_timeout_template, watchdog_set_keep_alive,
+ TP_PROTO(struct watchdog_device *wdd, u64 timeout),
+ TP_ARGS(wdd, timeout));
+
+#endif /* _TRACE_WATCHDOG_H */
+
+/* This part must be outside protection */
+#include <trace/define_trace.h>
--
2.35.1
This is the direct output this command line:
$ dot2k -d ~/wip.dot -t per_cpu
with wip.dot as:
----- %< -----
digraph state_automaton {
center = true;
size = "7,11";
rankdir = LR;
{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";
}
}
----- >% -----
This model is broken because preempt_disable_notrace(). It is broken on
purpose to test the reactors.
It does not compile because it lacks the instrumentation, which will be
add next.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/monitors/wip/wip.c | 112 +++++++++++++++++++++++++++++
kernel/trace/rv/monitors/wip/wip.h | 38 ++++++++++
2 files changed, 150 insertions(+)
create mode 100644 kernel/trace/rv/monitors/wip/wip.c
create mode 100644 kernel/trace/rv/monitors/wip/wip.h
diff --git a/kernel/trace/rv/monitors/wip/wip.c b/kernel/trace/rv/monitors/wip/wip.c
new file mode 100644
index 000000000000..08950e09b823
--- /dev/null
+++ b/kernel/trace/rv/monitors/wip/wip.c
@@ -0,0 +1,112 @@
+// SPDX-License-Identifier: GPL-2.0
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <rv/da_monitor.h>
+
+#define MODULE_NAME "wip"
+
+/*
+ * XXX: include required tracepoint headers, e.g.,
+ * #include <linux/trace/events/sched.h>
+ */
+#include <trace/events/rv.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, 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 */)
+{
+ da_handle_event_wip(preempt_disable_wip);
+}
+
+static void handle_preempt_enable(void *data, /* XXX: fill header */)
+{
+ da_handle_event_wip(preempt_enable_wip);
+}
+
+static void handle_sched_waking(void *data, /* XXX: fill header */)
+{
+ da_handle_event_wip(sched_waking_wip);
+}
+
+static int start_wip(void)
+{
+ int retval;
+
+ retval = da_monitor_init_wip();
+ 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);
+
+ return 0;
+}
+
+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);
+
+ da_monitor_destroy_wip();
+}
+
+/*
+ * This is the monitor register section.
+ */
+struct rv_monitor rv_wip = {
+ .name = "wip",
+ .description = "auto-generated wip",
+ .start = start_wip,
+ .stop = stop_wip,
+ .reset = da_monitor_reset_all_wip,
+ .enabled = 0,
+};
+
+int register_wip(void)
+{
+ rv_register_monitor(&rv_wip);
+ return 0;
+}
+
+void unregister_wip(void)
+{
+ if (rv_wip.enabled)
+ stop_wip();
+
+ rv_unregister_monitor(&rv_wip);
+}
+
+module_init(register_wip);
+module_exit(unregister_wip);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("dot2k: auto-generated");
+MODULE_DESCRIPTION("wip");
diff --git a/kernel/trace/rv/monitors/wip/wip.h b/kernel/trace/rv/monitors/wip/wip.h
new file mode 100644
index 000000000000..3055ea331706
--- /dev/null
+++ b/kernel/trace/rv/monitors/wip/wip.h
@@ -0,0 +1,38 @@
+enum states_wip {
+ preemptive_wip = 0,
+ non_preemptive_wip,
+ state_max_wip
+};
+
+enum events_wip {
+ preempt_disable_wip = 0,
+ preempt_enable_wip,
+ sched_waking_wip,
+ event_max_wip
+};
+
+struct automaton_wip {
+ char *state_names[state_max_wip];
+ char *event_names[event_max_wip];
+ char function[state_max_wip][event_max_wip];
+ char initial_state;
+ char final_states[state_max_wip];
+};
+
+struct automaton_wip automaton_wip = {
+ .state_names = {
+ "preemptive",
+ "non_preemptive"
+ },
+ .event_names = {
+ "preempt_disable",
+ "preempt_enable",
+ "sched_waking"
+ },
+ .function = {
+ { non_preemptive_wip, -1, -1 },
+ { -1, preemptive_wip, non_preemptive_wip },
+ },
+ .initial_state = preemptive_wip,
+ .final_states = { 1, 0 },
+};
--
2.35.1
Sample reactor that printks the reaction message.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/Kconfig | 8 ++++++
kernel/trace/rv/Makefile | 3 ++-
kernel/trace/rv/reactor_printk.c | 43 ++++++++++++++++++++++++++++++++
3 files changed, 53 insertions(+), 1 deletion(-)
create mode 100644 kernel/trace/rv/reactor_printk.c
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index fba2ace2a22b..be8e3dab0a52 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -52,4 +52,12 @@ config RV_REACTORS
tracing reactions, printing the monitor output via tracepoints,
but other reactions can be added (on-demand) via this interface.
+config RV_REACT_PRINTK
+ bool "Printk reactor"
+ depends on RV_REACTORS
+ default y if RV_REACTORS
+ help
+ Enables the printk reactor. The printk reactor emmits a printk()
+ message if an exception is found.
+
endif # RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index af0ff9a46418..a13c750a35c1 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -1,6 +1,7 @@
# SPDX-License-Identifier: GPL-2.0
obj-$(CONFIG_RV) += rv.o
-obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o
+obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
+obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
diff --git a/kernel/trace/rv/reactor_printk.c b/kernel/trace/rv/reactor_printk.c
new file mode 100644
index 000000000000..6a7bbf3fc03f
--- /dev/null
+++ b/kernel/trace/rv/reactor_printk.c
@@ -0,0 +1,43 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Printk RV reactor:
+ * Prints the exception msg to the kernel message log.
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ *
+ */
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+
+static void rv_printk_reaction(char *msg)
+{
+ printk_deferred(msg);
+}
+
+struct rv_reactor rv_printk = {
+ .name = "printk",
+ .description = "prints the exception msg to the kernel message log",
+ .react = rv_printk_reaction
+};
+
+int register_react_printk(void)
+{
+ rv_register_reactor(&rv_printk);
+ return 0;
+}
+
+void unregister_react_printk(void)
+{
+ rv_unregister_reactor(&rv_printk);
+}
+
+module_init(register_react_printk);
+module_exit(unregister_react_printk);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Daniel Bristot de Oliveira");
+MODULE_DESCRIPTION("printk rv reactor: printk if an exception is hit");
--
2.35.1
Adds the instrumentation to the previously created wwnr monitor, as an
example of the developer work. It also adds a Makefile, Kconfig and
tracepoint entries.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
include/trace/events/rv.h | 12 +++++++++
kernel/trace/rv/Kconfig | 8 ++++++
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitors/wwnr/wwnr.c | 38 ++++++++++++----------------
4 files changed, 37 insertions(+), 22 deletions(-)
diff --git a/include/trace/events/rv.h b/include/trace/events/rv.h
index 4e0dabffcf29..00f11a8dac3b 100644
--- a/include/trace/events/rv.h
+++ b/include/trace/events/rv.h
@@ -122,6 +122,18 @@ DECLARE_EVENT_CLASS(error_da_monitor_id,
__entry->event,
__entry->state)
);
+
+#ifdef CONFIG_RV_MON_WWNR
+/* id is the pid of the task */
+DEFINE_EVENT(event_da_monitor_id, event_wwnr,
+ TP_PROTO(int id, char *state, char *event, char *next_state, bool safe),
+ TP_ARGS(id, state, event, next_state, safe));
+
+DEFINE_EVENT(error_da_monitor_id, error_wwnr,
+ TP_PROTO(int id, char *state, char *event),
+ TP_ARGS(id, state, event));
+#endif /* CONFIG_RV_MON_WWNR */
+
#endif /* CONFIG_DA_MON_EVENTS_ID */
#endif /* _TRACE_RV_H */
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index e9246b0bec9d..fba2ace2a22b 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -34,6 +34,14 @@ config RV_MON_WIP
Enable WIP sample monitor, this is a sample monitor that
illustrates the usage of per-cpu monitors.
+config RV_MON_WWNR
+ select DA_MON_EVENTS_ID
+ bool "WWNR monitor"
+ help
+ Enable WWNR sample monitor, this is a sample monitor that
+ illustrates the usage of per-task monitor. The model is
+ broken on purpose: it serves to test reactors.
+
config RV_REACTORS
bool "Runtime verification reactors"
default y if RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index b41109d2750a..af0ff9a46418 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -3,3 +3,4 @@
obj-$(CONFIG_RV) += rv.o
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
+obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o
diff --git a/kernel/trace/rv/monitors/wwnr/wwnr.c b/kernel/trace/rv/monitors/wwnr/wwnr.c
index 8ba01f0f0df8..3fe1ad9125d3 100644
--- a/kernel/trace/rv/monitors/wwnr/wwnr.c
+++ b/kernel/trace/rv/monitors/wwnr/wwnr.c
@@ -10,11 +10,8 @@
#define MODULE_NAME "wwnr"
-/*
- * XXX: include required tracepoint headers, e.g.,
- * #include <linux/trace/events/sched.h>
- */
#include <trace/events/rv.h>
+#include <trace/events/sched.h>
/*
* This is the self-generated part of the monitor. Generally, there is no need
@@ -37,21 +34,20 @@ DECLARE_DA_MON_PER_TASK(wwnr, char);
* are translated into model's event.
*
*/
-static void handle_switch_in(void *data, /* XXX: fill header */)
+static void handle_switch(void *data, bool preempt, struct task_struct *p,
+ struct task_struct *n, unsigned int prev_state)
{
- struct task_struct *p = /* XXX: how do I get p? */;
- da_handle_event_wwnr(p, switch_in_wwnr);
-}
+ /* start monitoring only after the first suspension */
+ if (prev_state == TASK_INTERRUPTIBLE)
+ da_handle_init_event_wwnr(p, switch_out_wwnr);
+ else
+ da_handle_event_wwnr(p, switch_out_wwnr);
-static void handle_switch_out(void *data, /* XXX: fill header */)
-{
- struct task_struct *p = /* XXX: how do I get p? */;
- da_handle_event_wwnr(p, switch_out_wwnr);
+ da_handle_event_wwnr(n, switch_in_wwnr);
}
-static void handle_wakeup(void *data, /* XXX: fill header */)
+static void handle_wakeup(void *data, struct task_struct *p)
{
- struct task_struct *p = /* XXX: how do I get p? */;
da_handle_event_wwnr(p, wakeup_wwnr);
}
@@ -63,9 +59,8 @@ static int start_wwnr(void)
if (retval)
return retval;
- rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_in);
- rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_out);
- rv_attach_trace_probe("wwnr", /* XXX: tracepoint */, handle_wakeup);
+ rv_attach_trace_probe("wwnr", sched_switch, handle_switch);
+ rv_attach_trace_probe("wwnr", sched_wakeup, handle_wakeup);
return 0;
}
@@ -74,9 +69,8 @@ static void stop_wwnr(void)
{
rv_wwnr.enabled = 0;
- rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_in);
- rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_switch_out);
- rv_detach_trace_probe("wwnr", /* XXX: tracepoint */, handle_wakeup);
+ rv_detach_trace_probe("wwnr", sched_switch, handle_switch);
+ rv_detach_trace_probe("wwnr", sched_wakeup, handle_wakeup);
da_monitor_destroy_wwnr();
}
@@ -111,5 +105,5 @@ module_init(register_wwnr);
module_exit(unregister_wwnr);
MODULE_LICENSE("GPL");
-MODULE_AUTHOR("dot2k: auto-generated");
-MODULE_DESCRIPTION("wwnr");
+MODULE_AUTHOR("Daniel Bristot de Oliveira <[email protected]>");
+MODULE_DESCRIPTION("wwnr: wakeup while not running monitor.");
--
2.35.1
Add the da_monitor_synthesis.rst introduces some concepts behind the
Deterministic Automata (DA) monitor synthesis and interface.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
.../trace/rv/da_monitor_synthesis.rst | 284 ++++++++++++++++++
1 file changed, 284 insertions(+)
create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst b/Documentation/trace/rv/da_monitor_synthesis.rst
new file mode 100644
index 000000000000..1e1c857d7bbd
--- /dev/null
+++ b/Documentation/trace/rv/da_monitor_synthesis.rst
@@ -0,0 +1,284 @@
+Deterministic Automata Monitor Synthesis
+========================================
+
+The starting point for the application of runtime verification (RV) technics is
+the *specification* or *modeling* of the desired (or undesired) behavior of the
+system under scrutiny.
+
+The formal representation needs to be then *synthesized* into a *monitor* that
+can then be used in the analysis of the trace of the system. The *monitor*
+conects to the system via an *instrumentation* layer, that converts the events
+from the *system* to the events of the *specification*.
+
+This document introduces some concepts behind the **Deterministic Automata
+(DA)** monitor synthesis.
+
+DA monitor synthesis in a nutshell
+------------------------------------------------------
+
+The synthesis of automata-based models into the Linux *RV monitor* abstraction
+is automated by a tool named "dot2k", and the "rv/da_monitor.h" provided
+by the RV interface.
+
+Given a file "wip.dot", representing a per-cpu monitor, with this content::
+
+ digraph state_automaton {
+ center = true;
+ size = "7,11";
+ rankdir = LR;
+ {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";
+ }
+ }
+
+Run the dot2k tool with the model, specifying that it is a "per-cpu"
+model::
+
+ $ dot2k -d ~/wip.dot -t per_cpu
+
+This will create a directory named "wip/" with the following files:
+
+- wip.h: the wip in C
+- wip.c: the RV monitor
+
+The following line in the "wip.c" file is responsible for the monitor
+synthesis::
+
+ DECLARE_DA_MON_PER_CPU(wip, char);
+
+With that in place, the work left to be done is the *instrumentation* of
+the monitor, which is already initialized by dot2k.
+
+DA: Introduction and representation formats
+---------------------------------------------------------------
+
+Formally, a deterministic automaton, denoted by G, is defined as a quintuple:
+
+ *G* = { *X*, *E*, *f*, x\ :subscript:`0`, X\ :subscript:`m` }
+
+where:
+
+- *X* is the set of states;
+- *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 states.
+- *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*.
+
+One of the most evident benefits for the practical application of the automata
+formalism is its *graphic representation*, represented using vertices (nodes)
+and edges, which is very intuitive for *operating system* practitioners.
+
+For example, given an automata wip, with a regular representation of:
+
+- *X* = { ``preemptive``, ``non_preemptive``}
+- *E* = { ``preempt_enable``, ``preempt_disable``, ``sched_waking``}
+- x\ :subscript:`0` = ``preemptive``
+- X\ :subscript:`m` = {``preemptive``}
+- *f* =
+ - *f*\ (``preemptive``, ``preempt_disable``) = ``non_preemptive``
+ - *f*\ (``non_preemptive``, ``sched_waking``) = ``non_preemptive``
+ - *f*\ (``non_preemptive``, ``preempt_enable``) = ``preemptive``
+
+
+It can also be represented in a graphic format, without any loss, using this
+format::
+
+ preempt_enable
+ +---------------------------------+
+ v |
+ #============# preempt_disable +------------------+
+ --> H preemptive H -----------------> | non_preemptive |
+ #============# +------------------+
+ ^ sched_waking |
+ +--------------+
+
+The Graphviz open-source tool can produce this graphic format using the
+(textual) DOT language as the source code. The DOT format is widely
+used and can be converted to many other formats, including the ASCII art above.
+
+The dot2c tool presented in:
+
+ 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. For instance, using the wip model as input for dot2c results in
+the following C representation::
+
+ enum states_wip {
+ preemptive_wip = 0,
+ non_preemptive_wip,
+ state_max_wip
+ };
+
+ enum events_wip {
+ preempt_disable_wip = 0,
+ preempt_enable_wip,
+ sched_waking_wip,
+ event_max_wip
+ };
+
+ struct automaton_wip {
+ char *state_names[state_max_wip];
+ char *event_names[event_max_wip];
+ char function[state_max_wip][event_max_wip];
+ char initial_state;
+ char final_states[state_max_wip];
+ };
+
+ struct automaton_wip automaton_wip = {
+ .state_names = {
+ "preemptive",
+ "non_preemptive"
+ },
+ .event_names = {
+ "preempt_disable",
+ "preempt_enable",
+ "sched_waking"
+ },
+ .function = {
+ { non_preemptive_wip, -1, -1 },
+ { -1, preemptive_wip, non_preemptive_wip },
+ },
+ .initial_state = preemptive_wip,
+ .final_states = { 1, 0 },
+ };
+
+DA monitor synthesis for Linux
+------------------------------
+
+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>
+
+
+The dot2c tool works connecting the *Reference Model* to the *RV Monitor*
+abstraction by translating the *formal notation* into *code*.
+
+The "rv/da_monitor.h" header goes beyond dot2c, extending the code
+generation to the verification stage, generating the code to the *Monitor
+Instance(s)* level using C macros. The trace event code inspires this
+approach.
+
+The benefits of the usage of macro for monitor synthesis is 3-fold:
+
+- 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 two different types of monitor instances:
+
+- ``#define DECLARE_DA_MON_PER_CPU(name, type)``
+- ``#define DECLARE_DA_MON_PER_TASK(name, type)``
+
+The first declares the functions for deterministic automata monitor with
+per-cpu instances, and the second with per-task instances.
+
+In both cases, the name is a string that identifies the monitor, and the type
+is the data type used by dot2c/k on the representation of the model.
+
+For example, the "wip" model with two states and three events can be
+stored in a "char" type. Considering that the preemption control is a
+per-cpu behavior, the monitor declaration will be::
+
+ DECLARE_DA_MON_PER_CPU(wip, char);
+
+The monitor is executed by sending events to be processed via the functions
+presented below::
+
+ da_handle_event_$(MONITOR_NAME)($(event from event enum));
+ da_handle_init_event_$(MONITOR_NAME)($(event from event enum));
+
+The function ``da_handle_event_$(MONITOR_NAME)()`` is the regular case,
+while the function ``da_handle_init_event_$(MONITOR_NAME)()`` is a special
+case used to synchronize the system with the model.
+
+When a monitor is enabled, it is placed in the initial state of the automata.
+However, the monitor does not know if the system is in the *initial state*.
+Hence, the monitor ignores events sent by sent by
+``da_handle_event_$(MONITOR_NAME)()`` until the function
+``da_handle_init_event_$(MONITOR_NAME)()`` is called.
+
+The function ``da_handle_init_event_$(MONITOR_NAME)()`` should be used for
+the case in which the system generates the event is the one that returns
+the automata to the initial state.
+
+After receiving a ``da_handle_init_event_$(MONITOR_NAME)()`` event, the
+monitor will know that it is in sync with the system and hence will
+start processing the next events.
+
+Using the wip model as example, the events "preempt_disable" and
+"sched_waking" should be sent to monitor, respectively, via::
+
+ da_handle_event_wip(preempt_disable);
+ da_handle_event_wip(sched_waking);
+
+While the event "preempt_enabled" will use::
+
+ da_handle_init_event_wip(preempt_enable);
+
+To notify the monitor that the system will be returning to the initial state,
+so the system and the monitor should be in sync.
+
+rv/da_monitor.h
+-------------------------------------------
+
+The "rv/da_monitor.h" is, mostly, a set of C macros that create function
+definitions based on the paremeters passed via ``DECLARE_DA_MON_*``.
+
+In fewer words, the declaration of a monitor generates:
+
+- Helper functions for getting information from the automata model generated
+ by dot2k.
+- Helper functions for the analysis of a deterministic automata model
+- Functions for the initialization of the monitor instances
+- The definition of the structure to store the monitor instances' data
+
+One important aspect is that the monitor does not call external functions
+for the handling of the events sent by the instrumentation, except for
+generating *tracing events* or *reactions*.
+
+Final remarks
+-------------
+
+With the monitor synthesis in place using, the "rv/da_monitor.h" and
+dot2k, the developer's work should be limited to the instrumentation
+of the system, increasing the confidence in the overall approach.
--
2.35.1
This is the sample code of a safety application that uses the
watchdog as a safety monitor and the RV monitors to monitor
this interaction/get feedback from kernel about the watchdog states.
This tool first creates a trace instance to follow the RV events
and then enables RV monitor. After that, the tool configures
the watchdog and starts running the main loop.
The main loop runs a use-case-specific function, like checking
the system. If the system is running as expected, it pings the
watchdog. After pinging the watchdog, the tool then collects
trace information to see if the RV monitor received the expected
events and is in a safe/safe_nwo state.
For further information, run safety_app --help
The safety-app specification was developed together with Gabriele Paoloni,
in the context of the Linux Foundation Elisa Project.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
tools/verification/safety_app/Makefile | 51 ++
tools/verification/safety_app/safety_app.c | 614 +++++++++++++++++++++
2 files changed, 665 insertions(+)
create mode 100644 tools/verification/safety_app/Makefile
create mode 100644 tools/verification/safety_app/safety_app.c
diff --git a/tools/verification/safety_app/Makefile b/tools/verification/safety_app/Makefile
new file mode 100644
index 000000000000..002531022e45
--- /dev/null
+++ b/tools/verification/safety_app/Makefile
@@ -0,0 +1,51 @@
+NAME := safety_app
+VERSION := 0.1
+
+# From libtracefs:
+# Makefiles suck: This macro sets a default value of $(2) for the
+# variable named by $(1), unless the variable has been set by
+# environment or command line. This is necessary for CC and AR
+# because make sets default values, so the simpler ?= approach
+# won't work as expected.
+define allow-override
+ $(if $(or $(findstring environment,$(origin $(1))),\
+ $(findstring command line,$(origin $(1)))),,\
+ $(eval $(1) = $(2)))
+endef
+
+# Allow setting CC and AR, or setting CROSS_COMPILE as a prefix.
+$(call allow-override,CC,$(CROSS_COMPILE)gcc)
+$(call allow-override,AR,$(CROSS_COMPILE)ar)
+$(call allow-override,STRIP,$(CROSS_COMPILE)strip)
+$(call allow-override,PKG_CONFIG,pkg-config)
+$(call allow-override,LD_SO_CONF_PATH,/etc/ld.so.conf.d/)
+$(call allow-override,LDCONFIG,ldconfig)
+
+INSTALL = install
+FOPTS := -flto=auto -ffat-lto-objects -fexceptions -fstack-protector-strong \
+ -fasynchronous-unwind-tables -fstack-clash-protection
+WOPTS := -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -Wno-maybe-uninitialized
+
+TRACEFS_HEADERS := $$($(PKG_CONFIG) --cflags libtracefs)
+
+CFLAGS := -O -g -DVERSION=\"$(VERSION)\" $(FOPTS) $(WOPTS) $(TRACEFS_HEADERS)
+LDFLAGS := -ggdb
+LIBS := $$($(PKG_CONFIG) --libs libtracefs)
+FILES := Makefile
+BINDIR := /usr/bin
+
+OBJ := $(NAME).o
+
+.PHONY: all
+all: $(OBJ)
+ $(CC) -o $(NAME) $(LDFLAGS) $(OBJ) $(LIBS)
+
+.PHONY: install
+install:
+ $(INSTALL) -d -m 755 $(DESTDIR)$(BINDIR)
+ $(INSTALL) $(NAME) -m 755 $(DESTDIR)$(BINDIR)
+ $(STRIP) $(DESTDIR)$(BINDIR)/$(NAME)
+
+.PHONY: clean
+clean:
+ @rm -rf *~ $(OBJ) $(NAME)
diff --git a/tools/verification/safety_app/safety_app.c b/tools/verification/safety_app/safety_app.c
new file mode 100644
index 000000000000..143ebe17dfc9
--- /dev/null
+++ b/tools/verification/safety_app/safety_app.c
@@ -0,0 +1,614 @@
+// SPDX-License-Identifier: LGPL-2.1
+/*
+ * This is the starting point for a safety monitor.
+ *
+ * The safety_check() function is where you need to add your own code.
+ *
+ * Copyright: Red Hat, Inc. Daniel Bristot de Oliveira <[email protected]>
+ */
+#define _GNU_SOURCE
+#include <errno.h>
+#include <fcntl.h>
+#include <stdio.h>
+#include <getopt.h>
+#include <stdlib.h>
+#include <string.h>
+#include <unistd.h>
+#include <sys/ioctl.h>
+#include <linux/watchdog.h>
+#include <tracefs/tracefs.h>
+
+#define MAX_PATH 1024
+
+static int config_watchdog_id;
+static char config_watchdog_path[MAX_PATH];
+static int config_nowayout;
+static char config_nowayout_path[MAX_PATH];
+static long long config_timeout = 10;
+static long config_cycles;
+static long config_monitor_period = 1;
+static char *config_rv_monitor = "safe_wtd";
+static char *config_rv_reactor = "panic";
+static int config_stop_monitor = 0;
+static int config_restart_monitor = 0;
+
+/*
+ * print_msg - print a message to stdout
+ */
+void print_msg(const char *fmt, ...)
+{
+ char message[1024];
+ va_list ap;
+
+ va_start(ap, fmt);
+ vsnprintf(message, sizeof(message), fmt, ap);
+ va_end(ap);
+
+ fprintf(stdout, "%s", message);
+ fflush(NULL);
+}
+
+/*
+ * ==================================================================
+ * The code section bellow is responsible for enabling the RV monitor.
+ * ==================================================================
+ */
+
+/*
+ * __disable_rv_monitor - disables the RV monitor
+ *
+ * Unconditionally disables the RV monitor and set the reactor to nop.
+ */
+static void __disable_rv_monitor(char *monitor)
+{
+ char path[MAX_PATH];
+ int retval;
+
+ snprintf(path, MAX_PATH, "rv/monitors/%s/enable", monitor);
+ retval = tracefs_instance_file_write(NULL, path, "0\n");
+ if (retval < 0) {
+ perror("Error disabling the RV monitor");
+ return;
+ }
+
+ snprintf(path, MAX_PATH, "rv/monitors/%s/reactors", monitor);
+ retval = tracefs_instance_file_write(NULL, path, "nop\n");
+ if (retval < 0) {
+ perror("Error disabling the RV reactor");
+ return;
+ }
+}
+
+/*
+ * disable_rv_monitor - conditionally disables the RV monitor
+ */
+static void disable_rv_monitor(char *monitor)
+{
+ if (!config_stop_monitor)
+ return;
+
+ __disable_rv_monitor(monitor);
+}
+
+/*
+ * enable_rv_monitor - sets the 'reactor' and enable RV 'monitor'
+ */
+static int enable_rv_monitor(char *monitor, char *reactor)
+{
+ char buffer[MAX_PATH];
+ char path[MAX_PATH];
+ int size = 2;
+ int retval;
+ char *on;
+
+ snprintf(path, MAX_PATH, "rv/monitors/%s/enable", monitor);
+ on = tracefs_instance_file_read(NULL, path, &size);
+ if (on && on[0] == '1') {
+ if (!config_restart_monitor)
+ return 0;
+ __disable_rv_monitor(monitor);
+ }
+
+ snprintf(path, MAX_PATH, "rv/monitors/%s/reactors", monitor);
+ snprintf(buffer, MAX_PATH, "%s\n", reactor);
+ retval = tracefs_instance_file_write(NULL, path, buffer);
+ if (retval < 0) {
+ perror("Error enabling the RV reactor");
+ return -1;
+ }
+
+ snprintf(path, MAX_PATH, "rv/monitors/%s/enable", monitor);
+ retval = tracefs_instance_file_write(NULL, path, "1\n");
+ if (retval < 0) {
+ perror("Error enabling the RV monitor");
+ return -1;
+ }
+
+ return 0;
+}
+
+/*
+ * ==================================================================
+ * The code section bellow is responsible for parsing the RV monitor output.
+ * ==================================================================
+ */
+struct trace_instance {
+ struct tracefs_instance *inst;
+ struct tep_handle *tep;
+ struct trace_seq *seq;
+};
+
+int ping_counter = 0;
+int last_state_running = 0;
+
+/*
+ * handle_safe_wtd_rv_event - parse events from the safe_wtd RV monitor
+ */
+static int
+handle_safe_wtd_rv_event(struct trace_seq *s, struct tep_record *record,
+ struct tep_event *event, void *context)
+{
+ char *event_name;
+ char *state;
+ int len;
+
+ event_name = tep_get_field_raw(s, event, "event", record, &len, 1);
+ if (event_name && !strcmp(event_name, "ping"))
+ ping_counter++;
+
+ state = tep_get_field_raw(s, event, "next_state", record, &len, 0);
+ if (state && !strncmp(state, "safe", 4))
+ last_state_running = 1;
+ else
+ last_state_running = 0;
+
+ return 0;
+}
+
+/*
+ * collect_registered_events - call the existing callback function for the event
+ *
+ * If an event has a registered callback function, call it.
+ * Otherwise, ignore the event.
+ */
+static int
+collect_registered_events(struct tep_event *event, struct tep_record *record,
+ int cpu, void *context)
+{
+ struct trace_instance *trace = context;
+ struct trace_seq *s = trace->seq;
+
+ if (!event->handler)
+ return 0;
+
+ event->handler(s, record, event, context);
+
+ return 0;
+}
+
+/*
+ * check_rv_events - parse trace events and check for the desired states
+ *
+ * Return 0 if success, 1 otherwise.
+ */
+static int check_rv_events(struct trace_instance *trace)
+{
+ int prev_ping_counter = ping_counter;
+ int retval;
+ int pings;
+
+ retval = tracefs_iterate_raw_events(trace->tep, trace->inst, NULL, 0,
+ collect_registered_events, trace);
+ if (retval < 0) {
+ print_msg("Error iterating on events\n");
+ return 1;
+ }
+
+ pings = ping_counter - prev_ping_counter;
+ print_msg("RV read %d ping(s) and is %s the watchdog\n", pings,
+ last_state_running ? "running" : "not running");
+
+ /*
+ * If there is exactly one ping and the last state is running,
+ * it is safe.
+ */
+ if (pings == 1 && last_state_running) {
+ /* reset the variable */
+ last_state_running = 0;
+ return 0;
+ } else {
+ return 1;
+ }
+}
+
+/*
+ * trace_instance_destroy - destroy and free a trace instance
+ */
+static void trace_instance_destroy(struct trace_instance *trace)
+{
+ if (!trace)
+ return;
+
+ if (trace->inst) {
+ tracefs_instance_destroy(trace->inst);
+ tracefs_instance_free(trace->inst);
+ }
+
+ if (trace->seq)
+ free(trace->seq);
+
+ if (trace->tep)
+ tep_free(trace->tep);
+
+ free(trace);
+}
+
+/*
+ * trace_instance_init - create a trace instance to read monitor's event
+ *
+ * It is more than the tracefs instance, as it contains other
+ * things required for the tracing, such as the local events and
+ * a seq file.
+ */
+static struct trace_instance *trace_instance_init(void)
+{
+ struct trace_instance *trace;
+
+ trace = calloc(1, sizeof(*trace));
+ if (!trace)
+ return NULL;
+
+ trace->seq = calloc(1, sizeof(*trace->seq));
+ if (!trace->seq)
+ goto destroy_instance;
+
+ trace_seq_init(trace->seq);
+
+ trace->inst = tracefs_instance_create("safety_app");
+ if (!trace->inst)
+ goto destroy_instance;
+
+ trace->tep = tracefs_local_events(NULL);
+ if (!trace->tep)
+ goto destroy_instance;
+
+ /*
+ * register for both monitors, it is free.
+ */
+ tep_register_event_handler(trace->tep, -1, "rv", "event_safe_wtd",
+ handle_safe_wtd_rv_event, trace);
+ tracefs_event_enable(trace->inst, "rv", "event_safe_wtd");
+
+ return trace;
+
+destroy_instance:
+ trace_instance_destroy(trace);
+ return NULL;
+}
+
+/*
+ * ==================================================================
+ * The code section bellow are helper functions to use a watchdog device.
+ * ==================================================================
+ */
+
+/*
+ * set_nowayout - set the watchdog's nowayout option
+ */
+static int set_nowayout(char *nowayout_path)
+{
+ int nowayout_fd;
+ int retval;
+
+ print_msg("nowayout\n");
+
+ nowayout_fd = open(nowayout_path, O_WRONLY);
+ if (nowayout_path < 0) {
+ perror("Error opening nowayout fd");
+ return -1;
+ }
+
+ retval = write(nowayout_fd, "1", 1);
+ if (retval != 1) {
+ perror("Error setting nowayout");
+ close(nowayout_fd);
+ return -1;
+ }
+
+ close(nowayout_fd);
+ return 0;
+}
+
+/*
+ * open_watchdog - open watchdog at the watchdog_path
+ */
+static int open_watchdog(char *watchdog_path)
+{
+ int watchdog_fd;
+
+ print_msg("open %s\n", watchdog_path);
+
+ watchdog_fd = open(watchdog_path, O_WRONLY);
+ if (watchdog_fd < 0) {
+ perror("Error opening watchdog");
+ return -1;
+ }
+
+ return watchdog_fd;
+}
+
+/*
+ * set_timeout - set the timeout in seconds for the previously opened watchdog_fd
+ */
+static int set_timeout(int watchdog_fd, int timeout)
+{
+ int retval;
+
+ print_msg("set_timeout %d\n", timeout);
+
+ retval = ioctl(watchdog_fd, WDIOC_SETTIMEOUT, &timeout);
+ if (retval) {
+ perror("Error set_timeout");
+ return -1;
+ }
+
+ return 0;
+}
+
+/*
+ * ping - ping (or pet) the watchdog
+ */
+static int ping(int watchdog_fd)
+{
+ int retval;
+
+ print_msg("ping\n");
+
+ retval = write(watchdog_fd, "1", 1);
+ if (retval != 1) {
+ perror("Error resseting watchdog");
+ return -1;
+ }
+
+ return 0;
+}
+
+/*
+ * stop - try to the watchdog
+ *
+ * Writing "V" to the watchdog is a special case. Unless nowayout is set,
+ * it will stop the watchdog device.
+ */
+static void stop(int watchdog_fd)
+{
+ int retval;
+
+ print_msg("stop\n");
+
+ retval = write(watchdog_fd, "V", 1);
+ if (retval != 1)
+ perror("Error disabling the watchdog");
+}
+
+/*
+ * usage - print usage message
+ */
+static void usage(char *usage, int exitval)
+{
+ int i;
+
+ static const char * const msg[] = {
+ " usage: safety_app [-i id] [-t timeout in seconds ] [-n nowayout_path] \\",
+ " [-c cycles] [-p period] [-N] \\",
+ " [-N] [-r reactor] [-s] [-R] \\",
+ " [-h] \\",
+ "",
+ "Watchdog options",
+ " -i/--id: watchdog id",
+ " -t/--timeout: watchdog timeout",
+ " -n/--nowayout: set nowayout",
+ "",
+ "Safety monitor options",
+ " -c/--cycles: run cycle nr ping, 0 means forever (default)",
+ " -p/--period: monitor loop period",
+ "",
+ "RV monitor options",
+ " -r/--reactor set the reactor (panic is automatically set if no other reactor is passed)",
+ " -s/--stop-mon stop the rv monitor at the end of the execution",
+ " -R/--restart-mon restart the monitor if already started",
+ "",
+ "Generic options",
+ " -h/--help: print help message",
+ NULL,
+ };
+
+ if (usage)
+ fprintf(stderr, "%s\n", usage);
+
+ fprintf(stderr, "sample safety monitor (version %s)\n", VERSION);
+
+ for (i = 0; msg[i]; i++)
+ fprintf(stderr, "%s\n", msg[i]);
+ exit(exitval);
+}
+
+static long long get_long_from_str(char *start)
+{
+ long value;
+ char *end;
+
+ errno = 0;
+ value = strtoll(start, &end, 10);
+ if (errno || start == end) {
+ fprintf(stderr, "Invalid value '%s'", start);
+ return -1;
+ }
+
+ return value;
+}
+
+static int parse_args(int argc, char **argv)
+{
+ int c;
+
+ while (1) {
+ static struct option long_options[] = {
+ {"help", no_argument, 0, 'h'},
+ {"id", required_argument, 0, 'i'},
+ {"timeout", required_argument, 0, 't'},
+ {"nowayout", optional_argument, 0, 'n'},
+ {"cycles", required_argument, 0, 'c'},
+ {"period", required_argument, 0, 'p'},
+ {"reactor", required_argument, 0, 'r'},
+ {"stop-mon", no_argument, 0, 's'},
+ {"restart-mon", no_argument, 0, 'R'},
+ {0, 0, 0, 0}
+ };
+
+ /* getopt_long stores the option index here. */
+ int option_index = 0;
+
+ c = getopt_long(argc, argv, "hi:t:n::c:p:r:sR",
+ long_options, &option_index);
+
+ /* Detect the end of the options. */
+ if (c == -1)
+ break;
+
+ switch (c) {
+ case 'i':
+ config_watchdog_id = get_long_from_str(optarg);
+ break;
+ case 't':
+ config_timeout = get_long_from_str(optarg);
+ break;
+ case 'n':
+ config_nowayout = 1;
+ if (optarg)
+ strncpy(config_nowayout_path, optarg, MAX_PATH);
+ break;
+ case 'c':
+ config_cycles = get_long_from_str(optarg);
+ break;
+ case 'p':
+ config_monitor_period = get_long_from_str(optarg);
+ break;
+ case 'r':
+ config_rv_reactor = optarg;
+ break;
+ case 's':
+ config_stop_monitor = 1;
+ break;
+ case 'R':
+ config_restart_monitor = 1;
+ break;
+ case 'h':
+ usage("Help message", 0);
+ break;
+ default:
+ usage("Invalid option", 1);
+ }
+ }
+
+ if (!strlen(config_nowayout_path)) {
+ snprintf(config_nowayout_path, MAX_PATH,
+ "/sys/devices/virtual/watchdog/watchdog%i/nowayout",
+ config_watchdog_id);
+ }
+
+ if (config_monitor_period > config_timeout)
+ usage("Monitor period higher than the watchdog timeout.\n", 1);
+
+ snprintf(config_watchdog_path, MAX_PATH, "/dev/watchdog%d", config_watchdog_id);
+
+ return 0;
+}
+
+/*
+ * safety_check - check if the system is working properly
+ *
+ * This is the function where the system check will be actually done.
+ * It will be periodically called by the safety_app. If it returns
+ * true, the watchdog will be pinged and the system will continue running.
+ * If this function returns false, the safety_app will not ping the
+ * watchdog and will exit with an error.
+ */
+static int safety_check(void)
+{
+ /*
+ * Add your code here.
+ *
+ * Return 0 to make the safety monitor to skip the watchdog ping and
+ * exit with error, or just kill the system yourself.
+ */
+ return 1;
+}
+
+int main(int argc, char *argv[])
+{
+ struct trace_instance *trace;
+ int exit_val = 1;
+ int watchdog_fd;
+ long cycles = 0;
+ int retval;
+
+ parse_args(argc, argv);
+
+ trace = trace_instance_init();
+
+ retval = enable_rv_monitor(config_rv_monitor, config_rv_reactor);
+ if (retval) {
+ perror("Cannot proceed without the RV monitor");
+ goto out_destroy_trace;
+ }
+
+ if (config_nowayout)
+ set_nowayout(config_nowayout_path);
+
+ watchdog_fd = open_watchdog(config_watchdog_path);
+ if (watchdog_fd < 0) {
+ perror("Error opening watchdog");
+ exit(1);
+ }
+
+ if (config_timeout) {
+ retval = set_timeout(watchdog_fd, config_timeout);
+ if (retval)
+ goto out_close_watchdog;
+ }
+
+ retval = check_rv_events(trace);
+ if (retval) {
+ print_msg("RV monitor returned a failure, it is not safe to continue\n");
+ goto out_close_watchdog;
+ }
+
+ do {
+ retval = safety_check();
+ if (!retval)
+ goto out_close_watchdog;
+
+ retval = ping(watchdog_fd);
+ if (retval)
+ goto out_close_watchdog;
+
+ retval = check_rv_events(trace);
+ if (retval) {
+ print_msg("RV monitor returned a failure, it is not safe to continue\n");
+ goto out_close_watchdog;
+ }
+
+ sleep(config_monitor_period);
+ } while (!config_cycles || ++cycles < config_cycles);
+
+ stop(watchdog_fd);
+
+ exit_val = 0;
+
+out_close_watchdog:
+ close(watchdog_fd);
+ disable_rv_monitor(config_rv_monitor);
+out_destroy_trace:
+ trace_instance_destroy(trace);
+ return exit_val;
+}
--
2.35.1
Sample reactor that panics the system when an exception is found. This
is useful both to capture a vmcore, or to fail-safe a critical system.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
kernel/trace/rv/Kconfig | 8 ++++++
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/reactor_panic.c | 44 +++++++++++++++++++++++++++++++++
3 files changed, 53 insertions(+)
create mode 100644 kernel/trace/rv/reactor_panic.c
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index be8e3dab0a52..91a17b13a080 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -60,4 +60,12 @@ config RV_REACT_PRINTK
Enables the printk reactor. The printk reactor emmits a printk()
message if an exception is found.
+config RV_REACT_PANIC
+ bool "Panic reactor"
+ depends on RV_REACTORS
+ default y if RV_REACTORS
+ help
+ Enables the panic reactor. The panic reactor emmits a printk()
+ message if an exception is found and panic()s the system.
+
endif # RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index a13c750a35c1..963d14875b45 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -5,3 +5,4 @@ obj-$(CONFIG_RV_MON_WIP) += monitors/wip/wip.o
obj-$(CONFIG_RV_MON_WWNR) += monitors/wwnr/wwnr.o
obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
obj-$(CONFIG_RV_REACT_PRINTK) += reactor_printk.o
+obj-$(CONFIG_RV_REACT_PANIC) += reactor_panic.o
diff --git a/kernel/trace/rv/reactor_panic.c b/kernel/trace/rv/reactor_panic.c
new file mode 100644
index 000000000000..9d8d78a337a3
--- /dev/null
+++ b/kernel/trace/rv/reactor_panic.c
@@ -0,0 +1,44 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Panic RV reactor:
+ * Prints the exception msg to the kernel message log and panic().
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ *
+ */
+
+#include <linux/ftrace.h>
+#include <linux/tracepoint.h>
+#include <linux/kernel.h>
+#include <linux/module.h>
+#include <linux/init.h>
+#include <linux/rv.h>
+
+static void rv_panic_reaction(char *msg)
+{
+ panic(msg);
+}
+
+struct rv_reactor rv_panic = {
+ .name = "panic",
+ .description = "panic the system if an exception is found.",
+ .react = rv_panic_reaction
+};
+
+int register_react_panic(void)
+{
+ rv_register_reactor(&rv_panic);
+ return 0;
+}
+
+void unregister_react_panic(void)
+{
+ rv_unregister_reactor(&rv_panic);
+}
+
+module_init(register_react_panic);
+module_exit(unregister_react_panic);
+
+MODULE_LICENSE("GPL");
+MODULE_AUTHOR("Daniel Bristot de Oliveira");
+MODULE_DESCRIPTION("panic rv reactor: panic if an exception is found");
--
2.35.1
Adds documentation about the safe_wtd and safe_wtd_nwo RV monitors,
and their usage via a safety application.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
Documentation/trace/rv/watchdog-monitor.rst | 250 ++++++++++++++++++++
1 file changed, 250 insertions(+)
create mode 100644 Documentation/trace/rv/watchdog-monitor.rst
diff --git a/Documentation/trace/rv/watchdog-monitor.rst b/Documentation/trace/rv/watchdog-monitor.rst
new file mode 100644
index 000000000000..2b142fb31572
--- /dev/null
+++ b/Documentation/trace/rv/watchdog-monitor.rst
@@ -0,0 +1,250 @@
+Watchdog monitor
+----------------
+
+The watchdog is an essential building block for the usage of Linux in
+safety-critical systems because it allows the system to be monitored from
+an external element - the watchdog hardware, acting as a safety-monitor.
+
+A user-space application controls the watchdog device via the watchdog
+interface. This application, hereafter safety_app, enables the watchdog
+and periodically pets the watchdog upon correct completion of the safety
+related processing.
+
+If the safety_app, for any reason, stops pinging the watchdog,
+the watchdog hardware can set the system in a fail-safe state. For
+example, shutting the system down.
+
+Given the importance of the safety_app / watchdog hardware couple,
+the interaction between these software pieces also needs some
+sort of monitoring. In other words, "who monitors the monitor?"
+
+The safe watchdog (safe_wtd) RV monitor monitors the interaction between
+the safety_app and the watchdog device, enforcing the correct sequence of
+events that leads the system to a safe state.
+
+Furthermore, the safety_app can monitor the RV monitor by collecting the
+events generated by the RV monitor itself via tracing interface. In this way,
+closing the monitoring loop with the safety_app.
+
+A diagram of the components and their interactions is::
+
+ user-space:
+ +--------------------------------+
+ | safety_app |-----------+
+ +--------------------------------+ |
+ | ^ |
+ | Configure | Enable and |
+ | | check data |
+ ===================+====================+=============== |
+ kernel-space: | | |
+ v v |
+ +----------+ instr. +-------------+ |
+ | watchdog | ----------->| RV Monitor |----+ |
+ | device | +-------------+ | |
+ +----------+ | |
+ | | |
+ | | |
+ ================+====================================== | |
+ hardware: | | |
+ v | +-> Bring the system
+ +--------------------+ +----> to a safe state,
+ | watchdog hardware |---------------------------> e.g., halt.
+ +--------------------+
+
+Sample safety_app
+-----------------
+
+The user-space safety_app sample code in ``tools/verification/safety_app/``
+serves to illustrate the usage of the RV monitors for this use-case, as
+well as the starting point to the development of a user-specific safety_app.
+
+Watchdog events
+---------------
+
+The RV monitor observes the watchdog by using instrumentation to
+process the events generated by the interaction between the
+safety_app and the watchdog device layer in kernel.
+
+The monitored events are:
+
+ - watchdog:watchdog_open: open the watchdog device;
+ - watchdog:watchdog_close: close the watchdog device;
+ - watchdog:watchdog_start: start the watchdog;
+ - watchdog:watchdog_stop: stop the watchdog;
+ - watchdog:watchdog_set_timeout: set the watchdog timeout;
+ - watchdog:watchdog_ping: reprogram the watchdog with the previously set
+ timeout;
+ - watchdog:watchdog_nowayout: prevents the watchdog from stopping;
+ - watchdog:watchdog_set_keep_alive: set an intermediary ping to overcome
+ the limitation of a hardware watchdog maximum timeout being shorter than
+ the timeout set by the user-space tool;
+ - watchdog:watchdog_keep_alive: the execution of the function that runs the
+ intermediary keep alive ping;
+
+RV monitor events
+-----------------
+
+The RV monitor monitors the relevant events as an outside observer,
+interpreting all the components (the hardware; the watchdog device
+interface; and the safety monitor) as an integrated component.
+
+The events selected for the monitor are:
+
+ - other_threads: an event generated by any thread other than the
+ one that set nowayout or open the watchdog the last time.
+ - open: a thread opens the watchdog to manipulate it;
+ - close: a thread closes the watchdog;
+ - start: starts the watchdog countdown;
+ - stop: stops the watchdog;
+ - set_safe_timeout: configures the watchdog with a given timeout;
+ - ping: resets the watchdog countdown with the previously configured timeout;
+ - nowayout: prevents the watchdog to be stopped until the system's shutdown;
+ - sched_keep_alive: schedules a kernel worker to ping the watchdog if the
+ timeout is longer than the watchdog hardware can handle.
+ - keep_alive: executes the previously scheduled watchdog ping;
+
+Noting that the events that does not appear in the automata models are
+considered blocked events, and their execution will always cause the
+RV monitor to react to an unexpected event.
+
+RV monitor specification
+------------------------
+
+The monitor's goal is to assess a set of specifications that conducts the
+system to a safe state.
+
+These specifications are:
+
+ - 1: Once open, only one process manipulates the watchdog;
+ - 2: Following 1, the keep-alive mechanisms will not be used;
+ - 3: If required, nowayout will be set before opening the watchdog;
+ - 4: A safe timeout must be set;
+ - 5: At least one ping must be made before entering the safe/safe_nwo states
+ - 6: The RV monitor does not react if the watchdog is closed without stopping.
+ But the hardware watchdog is expected to react.
+
+Deterministic automata monitors
+-------------------------------
+
+Following the specifications, a deterministic automata monitor
+was developed. The monitor is modeled as Deterministic Automata model.
+
+The deterministic automata model for safe_wtd is::
+
+ #==================================# other_threads
+ H H ----------------+
+ -----------> H init H |
+ H H <---------------+
+ #==================================#
+ | | ^
+ | | | close
+ | | +----------------------------------------------------+
+ | | |
+ | | open |
+ | +------------------------------------------------------+ |
+ | | |
+ | nowayout | |
+ v | |
+ nowayout +-------------------+ | |
+ other_threads | | nowayout | |
+ +---------------- | nwo |<-------------------------------------+ | |
+ | | | | | |
+ +---------------> | | <+ | | |
+ +-------------------+ | | | |
+ | | | | |
+ | open | close | | |
+ v | | | |
+ +-------------------+ | | | |
+ | opened_nwo | -+ | | |
+ +-------------------+ | | |
+ | | | |
+ | start | | |
+ v | | |
+ +-------------------+ | | |
+ +---------------> | started_nwo | -+ | | |
+ | +-------------------+ | | | |
+ | | | | | |
+ | open | set_safe_timeout | | | |
+ | v | | | |
+ | +-------------------+ | | | |
+ | | set_nwo | | | | |
+ | +-------------------+ | | | |
+ | | | | | |
+ | +-------------+ | ping | | | |
+ | | | | | | | |
+ | | ping v v | | | |
+ | | +-------------------+ | | | |
+ | +-----------| safe_nwo | | | | |
+ | +-------------------+ | | | |
+ | | | | | |
+ | | close | close | | |
+ | v v | | |
+ | +----------------------------------+ nowayout | | |
+ | | | other_threads | | |
+ | | closed_running_nwo | ----------------+ | | |
+ | | | | | | |
+ +---------------- | | <---------------+ | | |
+ +----------------------------------+ | | |
+ | nowayout ^ | | |
+ +-----------------------------+ | | |
+ | | |
+ | | |
+ +-------------------+ +--------+ | | |
+ | | | |------+---+ |
+ | started | start | opened | | |
+ +---------------- | | <-------- | |>-----+-------+
+ | +-------------------+ +--------+ | ^
+ | | | |
+ | | set_safe_timeout +-------------+-------+
+ | v | |
+ | +-------------------+ | |
+ | | | | |
+ | | set | | |
+ +----------+---------------> | | | |
+ | | +-------------------+ | |
+ | | | | |
+ | | | ping | |
+ | | v | |
+ | | +-------------------+ ping | |
+ | | | | -------+ | |
+ | | +---- | safe | | | |
+ | | | | | <------+ | |
+ | | | +-------------------+ | |
+ | | | | | |
+ | | stop | | stop | |
+ | | | v | |
+ | | | +-------------------+ close | |
+ | +-----------+---> | stopped |-------------+ |
+ | | +-------------------+ |
+ | +---+ |
+ | | close |
+ | v |
+ | other_threads +----------------------------------------+ |
+ | +--------------> | | |
+ | | | closed_running | |
+ | +--------------- | |--------------+
+ | +----------------------------------------+
+ | | ^
+ | open | | close
+ | v |
+ | set_safe_timeout +-------------------+
+ +-------------------------> | reopened |
+ +-------------------+
+
+It is important to note that the events sched_keep_alive and keep_alive
+are not allowed in the monitor (they are said to be blocked events).
+The execution of any blocked events leads the RV monitor to react.
+
+Additional options
+------------------
+
+The RV monitor also has a set of options enabled via kernel command
+line/module options. They are:
+
+ - watchdog_id: the device id to monitor (default 0);
+ - dont_stop: once enabled, do not allow the RV monitor to be stopped (default off);
+ - safe_timeout: define a maximum safe value that a user-space application can
+ set as the watchdog timeout (default unlimited);
+ - check_timeout: After every ping, check if the time left in the watchdog is less
+ than or equal to the last timeout set for the watchdog. It only works for watchdog
+ devices that provide the get_timeleft() function (default off);
--
2.35.1
Adds the instrumentation to the previously created wip monitor, as an
example of the developer work. It also adds a Makefile, Kconfig and
tracepoint entries.
This is a good example of the manual work that is left for the
developer to do.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
include/trace/events/rv.h | 10 ++++++++++
kernel/trace/rv/Kconfig | 7 +++++++
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/monitors/wip/wip.c | 30 ++++++++++++++----------------
4 files changed, 32 insertions(+), 16 deletions(-)
diff --git a/include/trace/events/rv.h b/include/trace/events/rv.h
index 9f40f2a49f84..4e0dabffcf29 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 safe),
+ TP_ARGS(state, event, next_state, safe));
+
+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 1eafb5adcfcb..e9246b0bec9d 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -26,6 +26,13 @@ menuconfig RV
the system behavior.
if RV
+config RV_MON_WIP
+ depends on PREEMPTIRQ_TRACEPOINTS
+ select DA_MON_EVENTS_IMPLICIT
+ bool "WIP monitor"
+ help
+ Enable WIP sample monitor, this is a sample monitor that
+ illustrates the usage of per-cpu monitors.
config RV_REACTORS
bool "Runtime verification reactors"
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 08950e09b823..123827db0a03 100644
--- a/kernel/trace/rv/monitors/wip/wip.c
+++ b/kernel/trace/rv/monitors/wip/wip.c
@@ -10,11 +10,9 @@
#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
@@ -37,17 +35,17 @@ DECLARE_DA_MON_PER_CPU(wip, char);
* 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 +58,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,9 +69,9 @@ 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();
}
@@ -108,5 +106,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 <[email protected]>");
+MODULE_DESCRIPTION("wip: wakeup in preemptive - per-cpu sample monitor.");
--
2.35.1
Add the da_monitor_instrumentation.rst. It describes the basics
of RV monitor instrumentation.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
.../trace/rv/da_monitor_instrumentation.rst | 223 ++++++++++++++++++
1 file changed, 223 insertions(+)
create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst
diff --git a/Documentation/trace/rv/da_monitor_instrumentation.rst b/Documentation/trace/rv/da_monitor_instrumentation.rst
new file mode 100644
index 000000000000..994110050d93
--- /dev/null
+++ b/Documentation/trace/rv/da_monitor_instrumentation.rst
@@ -0,0 +1,223 @@
+Deterministic Automata Instrumentation
+========================================
+
+This document introduces some concepts behind the **Deterministic Automata
+(DA)** monitor instrumentation.
+
+The synthesis of automata-based models into the Linux *RV monitor* abstraction
+is automated by a tool named dot2k, and the "rv/da_monitor.h" provided
+by the RV interface.
+
+For example, given a file "wip.dot", representing a per-cpu monitor, with
+this content::
+
+ digraph state_automaton {
+ center = true;
+ size = "7,11";
+ rankdir = LR;
+ {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";
+ }
+ }
+
+That is the "DOT" representation of this automata model::
+
+ preempt_enable
+ +---------------------------------+
+ v |
+ #============# preempt_disable +------------------+
+ --> H preemptive H -----------------> | non_preemptive |
+ #============# +------------------+
+ ^ sched_waking |
+ +--------------+
+
+
+Run the dot2k tool with the model, specifying that it is a "per-cpu"
+model::
+
+ $ dot2k -d ~/wip.dot -t per_cpu
+
+This will create a directory named "wip/" with the following files:
+
+- model.h: the wip in C
+- wip.h: tracepoints that report the execution of the events by the
+ monitor
+- wip.c: the RV monitor
+
+The monitor instrumentation should be done entirely in the RV monitor,
+in the example above, in the wip.c file.
+
+The RV monitor instrumentation section
+--------------------------------------
+
+The RV monitor file created by dot2k, with the name "$MODEL_NAME.c"
+will include a section dedicated to instrumentation.
+
+In the example of the wip.dot above, it will look like::
+
+ /*
+ * 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 */)
+ {
+ da_handle_event_wip(preempt_disable_wip);
+ }
+
+ static void handle_preempt_enable(void *data, /* XXX: fill header */)
+ {
+ da_handle_event_wip(preempt_enable_wip);
+ }
+
+ static void handle_sched_waking(void *data, /* XXX: fill header */)
+ {
+ da_handle_event_wip(sched_waking_wip);
+ }
+
+ static int start_wip(void)
+ {
+ int retval;
+
+ retval = da_monitor_init_wip();
+ 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);
+
+ return 0;
+ }
+
+The comment at the top of the section explains the general idea: the
+instrumentation section translates *kernel events* into the *events
+accepted by the model*.
+
+Tracing callback functions
+-----------------------------
+
+The first three functions are skeletons for callback *handler functions* for
+each of the three events from the wip model. The developer does not
+necessarily need to use them: they are just starting points.
+
+Using the example of::
+
+ void handle_preempt_disable(void *data, /* XXX: fill header */)
+ {
+ da_handle_event_wip(preempt_disable_wip);
+ }
+
+The "preempt_disable" event from the model conects directly to the
+"preemptirq:preempt_disable". The "preemptirq:preempt_disable" event
+has the following signature, from "include/trace/events/preemptirq.h"::
+
+ TP_PROTO(unsigned long ip, unsigned long parent_ip)
+
+Hence, the "handle_preempt_disable()" function will look like::
+
+ void handle_preempt_disable(void *data, unsigned long ip, unsigned long parent_ip)
+
+In this case, the kernel even translates one to one with the automata event,
+and indeed, no other change is needed for this function.
+
+The next handler function, "handle_preempt_enable()" has the same argument
+list from the "handle_preempt_disable()". The difference is that the
+"preempt_enable" event will be used to synchronize the system to the model.
+
+Initially, the *model* is placed in the initial state. However, the *system*
+might, or might not be in the initial state. The monitor cannot start
+processing events until it knows that the system reached the initial state.
+Otherwise the monitor and the system could be out-of-sync.
+
+Looking at the automata definition, it is possible to see that the system
+and the model are expected to return to the initial state after the
+"preempt_enable" execution. Hence, it can be used to synchronize the
+system and the model at the initialization of the monitoring section.
+
+The initialization is informed via an special handle function, the
+"da_handle_init_event_$(MONITOR)(event)", in this case::
+
+ da_handle_event_wip(preempt_disable_wip);
+
+So, the callback function will look like::
+
+ void handle_preempt_enable(void *data, unsigned long ip, unsigned long parent_ip)
+ {
+ da_handle_init_event_wip(preempt_enable_wip);
+ }
+
+Finally, the "handle_sched_waking()" will look like::
+
+ void handle_sched_waking(void *data, struct task_struct *task)
+ {
+ da_handle_event_wip(sched_waking_wip);
+ }
+
+And the explanation is left for the reader as an exercise.
+
+Start and Stop functions
+------------------------
+
+dot2k automatically creates two special functions::
+
+ start_$MODELNAME()
+ stop_$MODELNAME()
+
+These functions are called when the monitor is enabled and disabled,
+respectivelly.
+
+They should be used to *attach* and *detach* the instrumentation to the running
+system. The developer must add to the relative function all that is needed to
+*attach* and *detach* its monitor to the system.
+
+For the wip case, these functions were named::
+
+ start_wip()
+ stop_wip()
+
+But no change was required because: by default, these functions *attach* and
+*detach* the tracepoints_to_attach, which was enough for this case.
+
+Instrumentation helpers
+--------------------------
+
+To complete the instrumentation, the *handler functions* need to be attached to a
+kernel event, at the monitoring start phase.
+
+The RV interface also facilitates this step. For example, the macro "rv_attach_trace_probe()"
+is used to connect the wip model events to the relative kernel event. dot2k automatically
+adds "rv_attach_trace_probe()" function call for each model event in the start phase, as
+a suggestion.
+
+For example, from the wip sample model::
+
+ static int start_wip(void)
+ {
+ int retval;
+
+ retval = da_monitor_init_wip();
+ 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);
+
+ return 0;
+ }
+
+The probes then need to be detached at the stop phase.
--
2.35.1
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:
[root@f32 rv]# 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:
[root@f32 rv]# cat monitors/wip/reactors
[nop]
panic
printk
[root@f32 rv]# echo panic > monitors/wip/reactors
[root@f32 rv]# cat monitors/wip/reactors
nop
[panic]
printk
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
include/linux/rv.h | 13 +
kernel/trace/rv/Kconfig | 14 +
kernel/trace/rv/Makefile | 1 +
kernel/trace/rv/rv.c | 18 +-
kernel/trace/rv/rv.h | 20 ++
kernel/trace/rv/rv_reactors.c | 476 ++++++++++++++++++++++++++++++++++
6 files changed, 540 insertions(+), 2 deletions(-)
create mode 100644 kernel/trace/rv/rv_reactors.c
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 205e65f57637..1e48c6bb74bf 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -8,6 +8,13 @@
*/
#ifndef _LINUX_RV_H
#define _LINUX_RV_H
+
+struct rv_reactor {
+ char *name;
+ char *description;
+ void (*react)(char *msg);
+};
+
struct rv_monitor {
const char *name;
const char *description;
@@ -15,9 +22,15 @@ struct rv_monitor {
int (*start)(void);
void (*stop)(void);
void (*reset)(void);
+ void (*react)(char *msg);
+
};
extern bool monitoring_on;
int rv_unregister_monitor(struct rv_monitor *monitor);
int rv_register_monitor(struct rv_monitor *monitor);
+
+extern bool reacting_on;
+int rv_unregister_reactor(struct rv_reactor *reactor);
+int rv_register_reactor(struct rv_reactor *reactor);
#endif /* _LINUX_RV_H */
diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
index 6d127cdb00dd..560408fec0c8 100644
--- a/kernel/trace/rv/Kconfig
+++ b/kernel/trace/rv/Kconfig
@@ -10,3 +10,17 @@ menuconfig RV
theorem proving). RV works by analyzing the trace of the system's
actual execution, comparing it against a formal specification of
the system behavior.
+
+if RV
+
+config RV_REACTORS
+ bool "Runtime verification reactors"
+ default y if RV
+ help
+ Enables the online runtime verification reactors. 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.
+
+endif # RV
diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
index fd995379df67..8944274d9b41 100644
--- a/kernel/trace/rv/Makefile
+++ b/kernel/trace/rv/Makefile
@@ -1,3 +1,4 @@
# SPDX-License-Identifier: GPL-2.0
obj-$(CONFIG_RV) += rv.o
+obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
index 43af7b13187e..7576d492a974 100644
--- a/kernel/trace/rv/rv.c
+++ b/kernel/trace/rv/rv.c
@@ -362,8 +362,13 @@ static int create_monitor_dir(struct rv_monitor_def *mdef)
retval = -ENOMEM;
goto out_remove_root;
}
+#ifdef CONFIG_RV_REACTORS
+ retval = reactor_create_monitor_files(mdef);
+ if (retval)
+ goto out_remove_root;
+#endif
- return retval;
+ return 0;
out_remove_root:
rv_remove(mdef->root_d);
@@ -674,7 +679,11 @@ int rv_register_monitor(struct rv_monitor *monitor)
r->monitor = monitor;
- create_monitor_dir(r);
+ retval = create_monitor_dir(r);
+ if (retval) {
+ kfree(r);
+ goto out_unlock;
+ }
list_add_tail(&r->list, &rv_monitors_list);
@@ -732,6 +741,11 @@ int __init rv_init_interface(void)
rv_create_file("monitoring_on", 0600, rv_root.root_dir, NULL,
&monitoring_on_fops);
+#ifdef CONFIG_RV_REACTORS
+ init_rv_reactors(rv_root.root_dir);
+ reacting_on = true;
+#endif
+
monitoring_on = true;
return 0;
diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h
index 0796867a7b1e..6d43f52d72a9 100644
--- a/kernel/trace/rv/rv.h
+++ b/kernel/trace/rv/rv.h
@@ -15,14 +15,28 @@ struct rv_interface {
#define rv_remove tracefs_remove
#define MAX_RV_MONITOR_NAME_SIZE 32
+#define MAX_RV_REACTOR_NAME_SIZE 32
extern struct mutex rv_interface_lock;
+#ifdef CONFIG_RV_REACTORS
+struct rv_reactor_def {
+ struct list_head list;
+ struct rv_reactor *reactor;
+ /* protected by the monitor interface lock */
+ int counter;
+};
+#endif
+
struct rv_monitor_def {
struct list_head list;
struct rv_monitor *monitor;
+#ifdef CONFIG_RV_REACTORS
+ struct rv_reactor_def *rdef;
+#endif
struct dentry *root_d;
bool enabled;
+ bool reacting;
bool task_monitor;
};
@@ -32,3 +46,9 @@ void reset_all_monitors(void);
int init_rv_monitors(struct dentry *root_dir);
int get_task_monitor_slot(void);
void put_task_monitor_slot(int slot);
+
+#ifdef CONFIG_RV_REACTORS
+extern bool reacting_on;
+int reactor_create_monitor_files(struct rv_monitor_def *mdef);
+int init_rv_reactors(struct dentry *root_dir);
+#endif
diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c
new file mode 100644
index 000000000000..bfe54d6996cc
--- /dev/null
+++ b/kernel/trace/rv/rv_reactors.c
@@ -0,0 +1,476 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Runtime reactor interface.
+ *
+ * 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.
+ *
+ * == Registering reactors ==
+ *
+ * The struct rv_reactor defines a callback function to be executed
+ * in case of a model exception happens. The callback function
+ * receives a message to be (optionally) printed before executing
+ * the reaction.
+ *
+ * A RV reactor is registered via:
+ * int rv_register_reactor(struct rv_reactor *reactor)
+ * And unregistered via:
+ * int rv_unregister_reactor(struct rv_reactor *reactor)
+ *
+ * These functions are exported to modules, enabling reactors to be
+ * dynamically loaded.
+ *
+ * == User interface ==
+ *
+ * The user interface resembles the kernel tracing interface and
+ * presents these files:
+ *
+ * "available_reactors"
+ * - List the available reactors, one per line.
+ *
+ * For example:
+ * [root@f32 rv]# 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 defaul one is the nop (no operation)
+ * reactor.
+ * - Writing the name of an reactor enables it to the given
+ * MONITOR.
+ *
+ * For example:
+ * [root@f32 rv]# cat monitors/wip/reactors
+ * [nop]
+ * panic
+ * printk
+ * [root@f32 rv]# echo panic > monitors/wip/reactors
+ * [root@f32 rv]# cat monitors/wip/reactors
+ * nop
+ * [panic]
+ * printk
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+#include <linux/slab.h>
+
+#include "rv.h"
+
+bool __read_mostly reacting_on;
+
+/*
+ * Interface for the reactor register.
+ */
+LIST_HEAD(rv_reactors_list);
+
+static struct rv_reactor_def *get_reactor_rdef_by_name(char *name)
+{
+ struct rv_reactor_def *r;
+
+ list_for_each_entry(r, &rv_reactors_list, list) {
+ if (strcmp(name, r->reactor->name) == 0)
+ return r;
+ }
+ return NULL;
+}
+
+/*
+ * Available reactors seq functions.
+ */
+static int reactors_show(struct seq_file *m, void *p)
+{
+ struct rv_reactor_def *rea_def = p;
+
+ seq_printf(m, "%s\n", rea_def->reactor->name);
+ return 0;
+}
+
+static void reactors_stop(struct seq_file *m, void *p)
+{
+ mutex_unlock(&rv_interface_lock);
+}
+
+static void *reactors_start(struct seq_file *m, loff_t *pos)
+{
+ mutex_lock(&rv_interface_lock);
+ return seq_list_start(&rv_reactors_list, *pos);
+}
+
+static void *reactors_next(struct seq_file *m, void *p, loff_t *pos)
+{
+ return seq_list_next(p, &rv_reactors_list, pos);
+}
+
+/*
+ * available reactors seq definition.
+ */
+static const struct seq_operations available_reactors_seq_ops = {
+ .start = reactors_start,
+ .next = reactors_next,
+ .stop = reactors_stop,
+ .show = reactors_show
+};
+
+/*
+ * available_reactors interface.
+ */
+static int available_reactors_open(struct inode *inode, struct file *file)
+{
+ return seq_open(file, &available_reactors_seq_ops);
+};
+
+static const struct file_operations available_reactors_ops = {
+ .open = available_reactors_open,
+ .read = seq_read,
+ .llseek = seq_lseek,
+ .release = seq_release
+};
+
+/*
+ * Monitor reactor file.
+ */
+static int monitor_reactor_show(struct seq_file *m, void *p)
+{
+ struct rv_monitor_def *mdef = m->private;
+ struct rv_reactor_def *rdef = p;
+
+ if (mdef->rdef == rdef)
+ seq_printf(m, "[%s]\n", rdef->reactor->name);
+ else
+ seq_printf(m, "%s\n", rdef->reactor->name);
+ return 0;
+}
+
+/*
+ * available reactors seq definition.
+ */
+static const struct seq_operations monitor_reactors_seq_ops = {
+ .start = reactors_start,
+ .next = reactors_next,
+ .stop = reactors_stop,
+ .show = monitor_reactor_show
+};
+
+static ssize_t
+monitor_reactors_write(struct file *file, const char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ char buff[MAX_RV_REACTOR_NAME_SIZE+1];
+ struct rv_monitor_def *mdef;
+ struct rv_reactor_def *rdef;
+ struct seq_file *seq_f;
+ int retval = -EINVAL;
+ char *ptr = buff;
+ int len;
+
+ if (count < 1 || count > MAX_RV_REACTOR_NAME_SIZE+1)
+ return -EINVAL;
+
+ memset(buff, 0, sizeof(buff));
+
+ retval = simple_write_to_buffer(buff, sizeof(buff)-1, ppos, user_buf,
+ count);
+ if (!retval)
+ return -EFAULT;
+
+ len = strlen(ptr);
+ if (!len)
+ return count;
+ /*
+ * remove the \n
+ */
+ ptr[len-1] = '\0';
+
+ /*
+ * See monitor_reactors_open()
+ */
+ seq_f = file->private_data;
+ mdef = seq_f->private;
+
+ mutex_lock(&rv_interface_lock);
+
+ retval = -EINVAL;
+
+ /*
+ * nop special case: disable reacting.
+ */
+ if (strcmp(ptr, "nop") == 0) {
+
+ if (mdef->monitor->enabled)
+ mdef->monitor->stop();
+
+ mdef->rdef = get_reactor_rdef_by_name("nop");
+ mdef->reacting = false;
+ mdef->monitor->react = NULL;
+
+ if (mdef->monitor->enabled)
+ mdef->monitor->start();
+
+ retval = count;
+ goto unlock;
+ }
+
+ list_for_each_entry(rdef, &rv_reactors_list, list) {
+ if (strcmp(ptr, rdef->reactor->name) == 0) {
+ /*
+ * found!
+ */
+ if (mdef->monitor->enabled)
+ mdef->monitor->stop();
+
+ mdef->rdef = rdef;
+ mdef->reacting = true;
+ mdef->monitor->react = rdef->reactor->react;
+
+ if (mdef->monitor->enabled)
+ mdef->monitor->start();
+
+ retval = count;
+ break;
+ }
+ }
+
+unlock:
+ mutex_unlock(&rv_interface_lock);
+
+ return retval;
+}
+
+/*
+ * available_reactors interface.
+ */
+static int monitor_reactors_open(struct inode *inode, struct file *file)
+{
+ /*
+ * create file "private" info is stored in the inode->i_private
+ */
+ struct rv_monitor_def *mdef = inode->i_private;
+ struct seq_file *seq_f;
+ int ret;
+
+
+ ret = seq_open(file, &monitor_reactors_seq_ops);
+ if (ret < 0)
+ return ret;
+
+ /*
+ * seq_open stores the seq_file on the file->private data.
+ */
+ seq_f = file->private_data;
+ /*
+ * Copy the create file "private" data to the seq_file
+ * private data.
+ */
+ seq_f->private = mdef;
+
+ return 0;
+};
+
+static const struct file_operations monitor_reactors_ops = {
+ .open = monitor_reactors_open,
+ .read = seq_read,
+ .llseek = seq_lseek,
+ .release = seq_release,
+ .write = monitor_reactors_write
+};
+
+static int __rv_register_reactor(struct rv_reactor *reactor)
+{
+ struct rv_reactor_def *r;
+
+ list_for_each_entry(r, &rv_reactors_list, list) {
+ if (strcmp(reactor->name, r->reactor->name) == 0) {
+ pr_info("Reactor %s is already registered\n",
+ reactor->name);
+ return -EINVAL;
+ }
+ }
+
+ r = kzalloc(sizeof(struct rv_reactor_def), GFP_KERNEL);
+ if (!r)
+ return -ENOMEM;
+
+ r->reactor = reactor;
+ r->counter = 0;
+
+ list_add_tail(&r->list, &rv_reactors_list);
+
+ return 0;
+}
+
+/**
+ * rv_register_reactor - register a rv reactor.
+ * @reactor: The rv_reactor to be registered.
+ *
+ * Returns 0 if successful, error otherwise.
+ */
+int rv_register_reactor(struct rv_reactor *reactor)
+{
+ int retval = 0;
+
+ if (strlen(reactor->name) >= MAX_RV_REACTOR_NAME_SIZE) {
+ pr_info("Reactor %s has a name longer than %d\n",
+ reactor->name, MAX_RV_MONITOR_NAME_SIZE);
+ return -EINVAL;
+ }
+
+ mutex_lock(&rv_interface_lock);
+ retval = __rv_register_reactor(reactor);
+ mutex_unlock(&rv_interface_lock);
+ return retval;
+}
+
+/**
+ * rv_unregister_reactor - unregister a rv reactor.
+ * @reactor: The rv_reactor to be unregistered.
+ *
+ * Returns 0 if successful, error otherwise.
+ */
+int rv_unregister_reactor(struct rv_reactor *reactor)
+{
+ struct rv_reactor_def *ptr, *next;
+
+ mutex_lock(&rv_interface_lock);
+
+ list_for_each_entry_safe(ptr, next, &rv_reactors_list, list) {
+ if (strcmp(reactor->name, ptr->reactor->name) == 0) {
+
+ if (!ptr->counter) {
+ list_del(&ptr->list);
+ } else {
+ printk(KERN_WARNING
+ "rv: the rv_reactor %s is in use by %d monitor(s)\n",
+ ptr->reactor->name, ptr->counter);
+ printk(KERN_WARNING "rv: the rv_reactor %s cannot be removed\n",
+ ptr->reactor->name);
+ return -EBUSY;
+ }
+
+ }
+ }
+
+ mutex_unlock(&rv_interface_lock);
+ return 0;
+}
+
+/*
+ * reacting_on interface.
+ */
+static ssize_t reacting_on_read_data(struct file *filp,
+ char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ char buff[4];
+
+ memset(buff, 0, sizeof(buff));
+
+ mutex_lock(&rv_interface_lock);
+ sprintf(buff, "%d\n", reacting_on);
+ mutex_unlock(&rv_interface_lock);
+
+ return simple_read_from_buffer(user_buf, count, ppos,
+ buff, strlen(buff)+1);
+}
+
+static void turn_reacting_off(void)
+{
+ reacting_on = false;
+}
+
+static void turn_reacting_on(void)
+{
+ reacting_on = true;
+}
+
+static ssize_t
+reacting_on_write_data(struct file *filp, const char __user *user_buf,
+ size_t count, loff_t *ppos)
+{
+ int retval;
+ u64 val;
+
+ retval = kstrtoull_from_user(user_buf, count, 10, &val);
+ if (retval)
+ return retval;
+
+ retval = count;
+
+ mutex_lock(&rv_interface_lock);
+
+ switch (val) {
+ case 0:
+ turn_reacting_off();
+ break;
+ case 1:
+ turn_reacting_on();
+ break;
+ default:
+ retval = -EINVAL;
+ }
+
+ mutex_unlock(&rv_interface_lock);
+
+ return retval;
+}
+
+static const struct file_operations reacting_on_fops = {
+ .open = simple_open,
+ .llseek = no_llseek,
+ .write = reacting_on_write_data,
+ .read = reacting_on_read_data,
+};
+
+
+int reactor_create_monitor_files(struct rv_monitor_def *mdef)
+{
+ struct dentry *tmp;
+
+ tmp = rv_create_file("reactors", 0400, mdef->root_d, mdef,
+ &monitor_reactors_ops);
+ if (!tmp)
+ return -ENOMEM;
+
+ /*
+ * Configure as the rv_nop reactor.
+ */
+ mdef->rdef = get_reactor_rdef_by_name("nop");
+ mdef->reacting = false;
+
+ return 0;
+}
+
+/*
+ * None reactor register
+ */
+static void rv_nop_reaction(char *msg)
+{
+}
+
+struct rv_reactor rv_nop = {
+ .name = "nop",
+ .description = "no-operation reactor: do nothing.",
+ .react = rv_nop_reaction
+};
+
+/*
+ * This section collects the rv/ root dir files and folders.
+ */
+int init_rv_reactors(struct dentry *root_dir)
+{
+ rv_create_file("available_reactors", 0400, root_dir, NULL,
+ &available_reactors_ops);
+ rv_create_file("reacting_on", 0600, root_dir, NULL, &reacting_on_fops);
+
+ __rv_register_reactor(&rv_nop);
+
+ return 0;
+}
--
2.35.1
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 for monitoring.
Cc: Wim Van Sebroeck <[email protected]>
Cc: Guenter Roeck <[email protected]>
Cc: Jonathan Corbet <[email protected]>
Cc: Steven Rostedt <[email protected]>
Cc: Ingo Molnar <[email protected]>
Cc: Thomas Gleixner <[email protected]>
Cc: Peter Zijlstra <[email protected]>
Cc: Will Deacon <[email protected]>
Cc: Catalin Marinas <[email protected]>
Cc: Marco Elver <[email protected]>
Cc: Dmitry Vyukov <[email protected]>
Cc: "Paul E. McKenney" <[email protected]>
Cc: Shuah Khan <[email protected]>
Cc: Gabriele Paoloni <[email protected]>
Cc: Juri Lelli <[email protected]>
Cc: Clark Williams <[email protected]>
Cc: [email protected]
Cc: [email protected]
Cc: [email protected]
Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
---
include/rv/automata.h | 49 +++++++++++++++++++++++++++++++++++++++++++
1 file changed, 49 insertions(+)
create mode 100644 include/rv/automata.h
diff --git a/include/rv/automata.h b/include/rv/automata.h
new file mode 100644
index 000000000000..0c0aa54bd820
--- /dev/null
+++ b/include/rv/automata.h
@@ -0,0 +1,49 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Deterministic automata helper functions, to be used with the automata
+ * models in C generated by the dot2k tool.
+ *
+ * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
+ */
+
+#define DECLARE_AUTOMATA_HELPERS(name, type) \
+ \
+static inline void *model_get_model_##name(void) \
+{ \
+ return (void *) &automaton_##name; \
+} \
+ \
+static char *model_get_state_name_##name(enum states_##name state) \
+{ \
+ return automaton_##name.state_names[state]; \
+} \
+ \
+static char *model_get_event_name_##name(enum events_##name event) \
+{ \
+ return automaton_##name.event_names[event]; \
+} \
+ \
+static inline type model_get_init_state_##name(void) \
+{ \
+ return automaton_##name.initial_state; \
+} \
+ \
+static inline type model_get_next_state_##name(enum states_##name curr_state, \
+ enum events_##name event) \
+{ \
+ if ((curr_state < 0) || (curr_state > state_max_##name)) \
+ return -1; \
+ \
+ if ((event < 0) || (event > event_max_##name)) \
+ return -1; \
+ \
+ return automaton_##name.function[curr_state][event]; \
+} \
+ \
+static inline bool model_is_final_state_##name(enum states_##name state) \
+{ \
+ if ((state < 0) || (state > state_max_##name)) \
+ return 0; \
+ \
+ return !!automaton_##name.final_states[state]; \
+}
--
2.35.1
Hi Daniel,
I love your patch! Perhaps something to improve:
[auto build test WARNING on rostedt-trace/for-next]
[also build test WARNING on tip/sched/core]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch]
url: https://github.com/intel-lab-lkp/linux/commits/Daniel-Bristot-de-Oliveira/The-Runtime-Verification-RV-interface/20220616-164837
base: https://git.kernel.org/pub/scm/linux/kernel/git/rostedt/linux-trace.git for-next
config: riscv-randconfig-r004-20220616 (https://download.01.org/0day-ci/archive/20220616/[email protected]/config)
compiler: riscv64-linux-gcc (GCC) 11.3.0
reproduce (this is a W=1 build):
wget https://raw.githubusercontent.com/intel/lkp-tests/master/sbin/make.cross -O ~/bin/make.cross
chmod +x ~/bin/make.cross
# https://github.com/intel-lab-lkp/linux/commit/a76032130de277ff6f39fc08277a70823fd85bf3
git remote add linux-review https://github.com/intel-lab-lkp/linux
git fetch --no-tags linux-review Daniel-Bristot-de-Oliveira/The-Runtime-Verification-RV-interface/20220616-164837
git checkout a76032130de277ff6f39fc08277a70823fd85bf3
# save the config file
mkdir build_dir && cp config build_dir/.config
COMPILER_INSTALL_PATH=$HOME/0day COMPILER=gcc-11.3.0 make.cross W=1 O=build_dir ARCH=riscv SHELL=/bin/bash kernel/trace/rv/
If you fix the issue, kindly add following tag where applicable
Reported-by: kernel test robot <[email protected]>
All warnings (new ones prefixed by >>):
In file included from kernel/trace/rv/monitors/wip/wip.c:8:
kernel/trace/rv/monitors/wip/wip.c: In function 'start_wip':
include/rv/instrumentation.h:15:17: error: implicit declaration of function 'check_trace_callback_type_preempt_disable'; did you mean 'check_trace_callback_type_irq_disable'? [-Werror=implicit-function-declaration]
15 | check_trace_callback_type_##tp(rv_handler); \
| ^~~~~~~~~~~~~~~~~~~~~~~~~~
kernel/trace/rv/monitors/wip/wip.c:61:9: note: in expansion of macro 'rv_attach_trace_probe'
61 | rv_attach_trace_probe("wip", preempt_disable, handle_preempt_disable);
| ^~~~~~~~~~~~~~~~~~~~~
In file included from include/linux/printk.h:11,
from include/linux/kernel.h:29,
from include/linux/interrupt.h:6,
from include/linux/trace_recursion.h:5,
from include/linux/ftrace.h:10,
from kernel/trace/rv/monitors/wip/wip.c:2:
include/rv/instrumentation.h:16:27: error: implicit declaration of function 'register_trace_preempt_disable'; did you mean 'register_trace_prio_irq_disable'? [-Werror=implicit-function-declaration]
16 | WARN_ONCE(register_trace_##tp(rv_handler, NULL), \
| ^~~~~~~~~~~~~~~
include/linux/once_lite.h:15:41: note: in definition of macro 'DO_ONCE_LITE_IF'
15 | bool __ret_do_once = !!(condition); \
| ^~~~~~~~~
include/rv/instrumentation.h:16:17: note: in expansion of macro 'WARN_ONCE'
16 | WARN_ONCE(register_trace_##tp(rv_handler, NULL), \
| ^~~~~~~~~
kernel/trace/rv/monitors/wip/wip.c:61:9: note: in expansion of macro 'rv_attach_trace_probe'
61 | rv_attach_trace_probe("wip", preempt_disable, handle_preempt_disable);
| ^~~~~~~~~~~~~~~~~~~~~
In file included from kernel/trace/rv/monitors/wip/wip.c:8:
include/rv/instrumentation.h:15:17: error: implicit declaration of function 'check_trace_callback_type_preempt_enable'; did you mean 'check_trace_callback_type_irq_enable'? [-Werror=implicit-function-declaration]
15 | check_trace_callback_type_##tp(rv_handler); \
| ^~~~~~~~~~~~~~~~~~~~~~~~~~
kernel/trace/rv/monitors/wip/wip.c:62:9: note: in expansion of macro 'rv_attach_trace_probe'
62 | rv_attach_trace_probe("wip", preempt_enable, handle_preempt_enable);
| ^~~~~~~~~~~~~~~~~~~~~
In file included from include/linux/printk.h:11,
from include/linux/kernel.h:29,
from include/linux/interrupt.h:6,
from include/linux/trace_recursion.h:5,
from include/linux/ftrace.h:10,
from kernel/trace/rv/monitors/wip/wip.c:2:
include/rv/instrumentation.h:16:27: error: implicit declaration of function 'register_trace_preempt_enable'; did you mean 'register_trace_prio_irq_enable'? [-Werror=implicit-function-declaration]
16 | WARN_ONCE(register_trace_##tp(rv_handler, NULL), \
| ^~~~~~~~~~~~~~~
include/linux/once_lite.h:15:41: note: in definition of macro 'DO_ONCE_LITE_IF'
15 | bool __ret_do_once = !!(condition); \
| ^~~~~~~~~
include/rv/instrumentation.h:16:17: note: in expansion of macro 'WARN_ONCE'
16 | WARN_ONCE(register_trace_##tp(rv_handler, NULL), \
| ^~~~~~~~~
kernel/trace/rv/monitors/wip/wip.c:62:9: note: in expansion of macro 'rv_attach_trace_probe'
62 | rv_attach_trace_probe("wip", preempt_enable, handle_preempt_enable);
| ^~~~~~~~~~~~~~~~~~~~~
In file included from kernel/trace/rv/monitors/wip/wip.c:8:
kernel/trace/rv/monitors/wip/wip.c: In function 'stop_wip':
include/rv/instrumentation.h:22:17: error: implicit declaration of function 'unregister_trace_preempt_disable'; did you mean 'unregister_trace_irq_disable'? [-Werror=implicit-function-declaration]
22 | unregister_trace_##tp(rv_handler, NULL); \
| ^~~~~~~~~~~~~~~~~
kernel/trace/rv/monitors/wip/wip.c:72:9: note: in expansion of macro 'rv_detach_trace_probe'
72 | rv_detach_trace_probe("wip", preempt_disable, handle_preempt_disable);
| ^~~~~~~~~~~~~~~~~~~~~
include/rv/instrumentation.h:22:17: error: implicit declaration of function 'unregister_trace_preempt_enable'; did you mean 'unregister_trace_irq_enable'? [-Werror=implicit-function-declaration]
22 | unregister_trace_##tp(rv_handler, NULL); \
| ^~~~~~~~~~~~~~~~~
kernel/trace/rv/monitors/wip/wip.c:73:9: note: in expansion of macro 'rv_detach_trace_probe'
73 | rv_detach_trace_probe("wip", preempt_enable, handle_preempt_enable);
| ^~~~~~~~~~~~~~~~~~~~~
kernel/trace/rv/monitors/wip/wip.c: At top level:
>> kernel/trace/rv/monitors/wip/wip.c:91:5: warning: no previous prototype for 'register_wip' [-Wmissing-prototypes]
91 | int register_wip(void)
| ^~~~~~~~~~~~
>> kernel/trace/rv/monitors/wip/wip.c:97:6: warning: no previous prototype for 'unregister_wip' [-Wmissing-prototypes]
97 | void unregister_wip(void)
| ^~~~~~~~~~~~~~
cc1: some warnings being treated as errors
vim +/register_wip +91 kernel/trace/rv/monitors/wip/wip.c
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 90
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 @91 int register_wip(void)
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 92 {
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 93 rv_register_monitor(&rv_wip);
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 94 return 0;
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 95 }
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 96
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 @97 void unregister_wip(void)
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 98 {
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 99 if (rv_wip.enabled)
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 100 stop_wip();
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 101
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 102 rv_unregister_monitor(&rv_wip);
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 103 }
15679ffb99664f Daniel Bristot de Oliveira 2022-06-16 104
--
0-DAY CI Kernel Test Service
https://01.org/lkp
On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
> Add a set of tracepoints, enabling the observability of the watchdog
> device interactions with user-space.
>
> The events are:
> watchdog:watchdog_open
> watchdog:watchdog_close
> watchdog:watchdog_start
> watchdog:watchdog_stop
> watchdog:watchdog_set_timeout
> watchdog:watchdog_ping
> watchdog:watchdog_nowayout
> watchdog:watchdog_set_keep_alive
> watchdog:watchdog_keep_alive
> watchdog:watchdog_set_pretimeout
> watchdog:watchdog_pretimeout
>
> Cc: Wim Van Sebroeck <[email protected]>
> Cc: Guenter Roeck <[email protected]>
> Cc: Jonathan Corbet <[email protected]>
> Cc: Steven Rostedt <[email protected]>
> Cc: Ingo Molnar <[email protected]>
> Cc: Thomas Gleixner <[email protected]>
> Cc: Peter Zijlstra <[email protected]>
> Cc: Will Deacon <[email protected]>
> Cc: Catalin Marinas <[email protected]>
> Cc: Marco Elver <[email protected]>
> Cc: Dmitry Vyukov <[email protected]>
> Cc: "Paul E. McKenney" <[email protected]>
> Cc: Shuah Khan <[email protected]>
> Cc: Gabriele Paoloni <[email protected]>
> Cc: Juri Lelli <[email protected]>
> Cc: Clark Williams <[email protected]>
> Cc: [email protected]
> Cc: [email protected]
> Cc: [email protected]
> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
> ---
> drivers/watchdog/watchdog_dev.c | 43 ++++++++++-
> drivers/watchdog/watchdog_pretimeout.c | 2 +
> include/linux/watchdog.h | 7 +-
> include/trace/events/watchdog.h | 101 +++++++++++++++++++++++++
> 4 files changed, 143 insertions(+), 10 deletions(-)
> create mode 100644 include/trace/events/watchdog.h
>
> diff --git a/drivers/watchdog/watchdog_dev.c b/drivers/watchdog/watchdog_dev.c
> index 54903f3c851e..2f28dc5ab763 100644
> --- a/drivers/watchdog/watchdog_dev.c
> +++ b/drivers/watchdog/watchdog_dev.c
> @@ -44,6 +44,9 @@
> #include <linux/watchdog.h> /* For watchdog specific items */
> #include <linux/uaccess.h> /* For copy_to_user/put_user/... */
>
> +#define CREATE_TRACE_POINTS
> +#include <trace/events/watchdog.h>
> +
> #include "watchdog_core.h"
> #include "watchdog_pretimeout.h"
>
> @@ -130,9 +133,11 @@ static inline void watchdog_update_worker(struct watchdog_device *wdd)
> if (watchdog_need_worker(wdd)) {
> ktime_t t = watchdog_next_keepalive(wdd);
>
> - if (t > 0)
> + if (t > 0) {
> hrtimer_start(&wd_data->timer, t,
> HRTIMER_MODE_REL_HARD);
> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
> + }
> } else {
> hrtimer_cancel(&wd_data->timer);
> }
> @@ -141,7 +146,7 @@ static inline void watchdog_update_worker(struct watchdog_device *wdd)
> static int __watchdog_ping(struct watchdog_device *wdd)
> {
> struct watchdog_core_data *wd_data = wdd->wd_data;
> - ktime_t earliest_keepalive, now;
> + ktime_t earliest_keepalive, now, next_keepalive;
> int err;
>
> earliest_keepalive = ktime_add(wd_data->last_hw_keepalive,
> @@ -149,14 +154,16 @@ static int __watchdog_ping(struct watchdog_device *wdd)
> now = ktime_get();
>
> if (ktime_after(earliest_keepalive, now)) {
> - hrtimer_start(&wd_data->timer,
> - ktime_sub(earliest_keepalive, now),
> + next_keepalive = ktime_sub(earliest_keepalive, now);
> + hrtimer_start(&wd_data->timer, next_keepalive,
> HRTIMER_MODE_REL_HARD);
> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(next_keepalive));
> return 0;
> }
>
> wd_data->last_hw_keepalive = now;
>
> + trace_watchdog_ping(wdd);
> if (wdd->ops->ping)
> err = wdd->ops->ping(wdd); /* ping the watchdog */
> else
> @@ -215,6 +222,7 @@ static void watchdog_ping_work(struct kthread_work *work)
> wd_data = container_of(work, struct watchdog_core_data, work);
>
> mutex_lock(&wd_data->lock);
> + trace_watchdog_keep_alive(wd_data->wdd);
> if (watchdog_worker_should_ping(wd_data))
> __watchdog_ping(wd_data->wdd);
> mutex_unlock(&wd_data->lock);
> @@ -250,6 +258,8 @@ static int watchdog_start(struct watchdog_device *wdd)
>
> set_bit(_WDOG_KEEPALIVE, &wd_data->status);
>
> + trace_watchdog_start(wdd);
> +
> started_at = ktime_get();
> if (watchdog_hw_running(wdd) && wdd->ops->ping) {
> err = __watchdog_ping(wdd);
> @@ -294,6 +304,7 @@ static int watchdog_stop(struct watchdog_device *wdd)
> return -EBUSY;
> }
>
> + trace_watchdog_stop(wdd);
> if (wdd->ops->stop) {
> clear_bit(WDOG_HW_RUNNING, &wdd->status);
> err = wdd->ops->stop(wdd);
> @@ -367,6 +378,7 @@ static int watchdog_set_timeout(struct watchdog_device *wdd,
> if (watchdog_timeout_invalid(wdd, timeout))
> return -EINVAL;
>
> + trace_watchdog_set_timeout(wdd, timeout);
The driver has no obligation to set the timeout to the
requested value. It might be more valuable to report both
the requested and the actual values.
> if (wdd->ops->set_timeout) {
> err = wdd->ops->set_timeout(wdd, timeout);
> } else {
> @@ -399,6 +411,8 @@ static int watchdog_set_pretimeout(struct watchdog_device *wdd,
> if (watchdog_pretimeout_invalid(wdd, timeout))
> return -EINVAL;
>
> + trace_watchdog_set_pretimeout(wdd, timeout);
> +
Again, the driver has no obligation to set the timeout to the
requested value.
> if (wdd->ops->set_pretimeout && (wdd->info->options & WDIOF_PRETIMEOUT))
> err = wdd->ops->set_pretimeout(wdd, timeout);
> else
> @@ -430,6 +444,23 @@ static int watchdog_get_timeleft(struct watchdog_device *wdd,
> return 0;
> }
>
> +/**
> + * watchdog_set_nowayout - set nowaout bit
> + * @wdd: The watchdog device to set nowayoutbit
> + * @nowayout A boolean on/off switcher
> + *
> + * If nowayout boolean is true, the nowayout option is set. No action is
> + * taken if nowayout is false.
> + */
> +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
> +{
> + if (nowayout) {
> + set_bit(WDOG_NO_WAY_OUT, &wdd->status);
> + trace_watchdog_nowayout(wdd);
> + }
> +}
> +EXPORT_SYMBOL(watchdog_set_nowayout);
> +
> #ifdef CONFIG_WATCHDOG_SYSFS
> static ssize_t nowayout_show(struct device *dev, struct device_attribute *attr,
> char *buf)
> @@ -861,6 +892,8 @@ static int watchdog_open(struct inode *inode, struct file *file)
> goto out_clear;
> }
>
> + trace_watchdog_open(wdd);
> +
> err = watchdog_start(wdd);
> if (err < 0)
> goto out_mod;
> @@ -883,6 +916,7 @@ static int watchdog_open(struct inode *inode, struct file *file)
> return stream_open(inode, file);
>
> out_mod:
> + trace_watchdog_close(wdd);
> module_put(wd_data->wdd->ops->owner);
> out_clear:
> clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
> @@ -944,6 +978,7 @@ static int watchdog_release(struct inode *inode, struct file *file)
> /* make sure that /dev/watchdog can be re-opened */
> clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
>
> + trace_watchdog_close(wdd);
> done:
> running = wdd && watchdog_hw_running(wdd);
> mutex_unlock(&wd_data->lock);
> diff --git a/drivers/watchdog/watchdog_pretimeout.c b/drivers/watchdog/watchdog_pretimeout.c
> index 376a495ab80c..58c391ed2205 100644
> --- a/drivers/watchdog/watchdog_pretimeout.c
> +++ b/drivers/watchdog/watchdog_pretimeout.c
> @@ -8,6 +8,7 @@
> #include <linux/spinlock.h>
> #include <linux/string.h>
> #include <linux/watchdog.h>
> +#include <trace/events/watchdog.h>
>
> #include "watchdog_core.h"
> #include "watchdog_pretimeout.h"
> @@ -107,6 +108,7 @@ void watchdog_notify_pretimeout(struct watchdog_device *wdd)
> return;
> }
>
> + trace_watchdog_pretimeout(wdd);
> wdd->gov->pretimeout(wdd);
> spin_unlock_irqrestore(&pretimeout_lock, flags);
> }
> diff --git a/include/linux/watchdog.h b/include/linux/watchdog.h
> index 99660197a36c..11d93407e492 100644
> --- a/include/linux/watchdog.h
> +++ b/include/linux/watchdog.h
> @@ -139,12 +139,7 @@ static inline bool watchdog_hw_running(struct watchdog_device *wdd)
> return test_bit(WDOG_HW_RUNNING, &wdd->status);
> }
>
> -/* Use the following function to set the nowayout feature */
> -static inline void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
> -{
> - if (nowayout)
> - set_bit(WDOG_NO_WAY_OUT, &wdd->status);
> -}
> +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout);
>
> /* Use the following function to stop the watchdog on reboot */
> static inline void watchdog_stop_on_reboot(struct watchdog_device *wdd)
> diff --git a/include/trace/events/watchdog.h b/include/trace/events/watchdog.h
> new file mode 100644
> index 000000000000..145cd6cfaa02
> --- /dev/null
> +++ b/include/trace/events/watchdog.h
> @@ -0,0 +1,101 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +#undef TRACE_SYSTEM
> +#define TRACE_SYSTEM watchdog
> +
> +#if !defined(_TRACE_WATCHDOG_H) || defined(TRACE_HEADER_MULTI_READ)
> +#define _TRACE_WATCHDOG_H
> +
> +#include <linux/tracepoint.h>
> +
> +/*
> + * These are all events whose sole argument is the watchdog id.
> + */
> +DECLARE_EVENT_CLASS(dev_operations_template,
> +
> + TP_PROTO(struct watchdog_device *wdd),
> +
> + TP_ARGS(wdd),
> +
> + TP_STRUCT__entry(
> + __field(__u32, id)
> + ),
> +
> + TP_fast_assign(
> + __entry->id = wdd->id;
> + ),
> +
> + TP_printk("id=%d",
> + __entry->id)
> +);
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_open,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_close,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_start,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_stop,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_ping,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_nowayout,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_keep_alive,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +DEFINE_EVENT(dev_operations_template, watchdog_pretimeout,
> + TP_PROTO(struct watchdog_device *wdd),
> + TP_ARGS(wdd));
> +
> +/*
> + * These are all events with a device ID and a given timeout.
> + */
> +DECLARE_EVENT_CLASS(watchdog_timeout_template,
> +
> + TP_PROTO(struct watchdog_device *wdd, u64 timeout),
> +
> + TP_ARGS(wdd, timeout),
> +
> + TP_STRUCT__entry(
> + __field(__u32, id)
> + __field(__u64, timeout)
Why u64 ? timeout is unsigned long.
> + ),
> +
> + TP_fast_assign(
> + __entry->id = wdd->id;
> + __entry->timeout = timeout;
> + ),
> +
> + TP_printk("id=%d timeout=%llus",
> + __entry->id, __entry->timeout)
> +);
> +
> +DEFINE_EVENT(watchdog_timeout_template, watchdog_set_timeout,
> + TP_PROTO(struct watchdog_device *wdd, u64 timeout),
> + TP_ARGS(wdd, timeout));
> +
> +DEFINE_EVENT(watchdog_timeout_template, watchdog_set_pretimeout,
> + TP_PROTO(struct watchdog_device *wdd, u64 timeout),
> + TP_ARGS(wdd, timeout));
> +
> +DEFINE_EVENT(watchdog_timeout_template, watchdog_set_keep_alive,
> + TP_PROTO(struct watchdog_device *wdd, u64 timeout),
> + TP_ARGS(wdd, timeout));
> +
> +#endif /* _TRACE_WATCHDOG_H */
> +
> +/* This part must be outside protection */
> +#include <trace/define_trace.h>
Hi Daniel,
I love your patch! Perhaps something to improve:
[auto build test WARNING on rostedt-trace/for-next]
[also build test WARNING on tip/sched/core]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch]
url: https://github.com/intel-lab-lkp/linux/commits/Daniel-Bristot-de-Oliveira/The-Runtime-Verification-RV-interface/20220616-164837
base: https://git.kernel.org/pub/scm/linux/kernel/git/rostedt/linux-trace.git for-next
config: x86_64-allyesconfig (https://download.01.org/0day-ci/archive/20220616/[email protected]/config)
compiler: gcc-11 (Debian 11.3.0-3) 11.3.0
reproduce (this is a W=1 build):
# https://github.com/intel-lab-lkp/linux/commit/31dad6685057c10f6301fbc4018b6586fce0757e
git remote add linux-review https://github.com/intel-lab-lkp/linux
git fetch --no-tags linux-review Daniel-Bristot-de-Oliveira/The-Runtime-Verification-RV-interface/20220616-164837
git checkout 31dad6685057c10f6301fbc4018b6586fce0757e
# save the config file
mkdir build_dir && cp config build_dir/.config
make W=1 O=build_dir ARCH=x86_64 SHELL=/bin/bash kernel/trace/rv/
If you fix the issue, kindly add following tag where applicable
Reported-by: kernel test robot <[email protected]>
All warnings (new ones prefixed by >>):
In file included from kernel/trace/rv/monitors/wwnr/wwnr.c:8:
kernel/trace/rv/monitors/wwnr/wwnr.c: In function 'start_wwnr':
kernel/trace/rv/monitors/wwnr/wwnr.c:62:53: error: passing argument 1 of 'check_trace_callback_type_sched_switch' from incompatible pointer type [-Werror=incompatible-pointer-types]
62 | rv_attach_trace_probe("wwnr", sched_switch, handle_switch);
| ^~~~~~~~~~~~~
| |
| void (*)(void *, bool, struct task_struct *, struct task_struct *, unsigned int) {aka void (*)(void *, _Bool, struct task_struct *, struct task_struct *, unsigned int)}
include/rv/instrumentation.h:15:48: note: in definition of macro 'rv_attach_trace_probe'
15 | check_trace_callback_type_##tp(rv_handler); \
| ^~~~~~~~~~
In file included from kernel/trace/rv/monitors/wwnr/wwnr.c:3:
include/linux/tracepoint.h:279:49: note: expected 'void (*)(void *, bool, unsigned int, struct task_struct *, struct task_struct *)' {aka 'void (*)(void *, _Bool, unsigned int, struct task_struct *, struct task_struct *)'} but argument is of type 'void (*)(void *, bool, struct task_struct *, struct task_struct *, unsigned int)' {aka 'void (*)(void *, _Bool, struct task_struct *, struct task_struct *, unsigned int)'}
279 | check_trace_callback_type_##name(void (*cb)(data_proto)) \
| ~~~~~~~^~~~~~~~~~~~~~~
include/linux/tracepoint.h:419:9: note: in expansion of macro '__DECLARE_TRACE'
419 | __DECLARE_TRACE(name, PARAMS(proto), PARAMS(args), \
| ^~~~~~~~~~~~~~~
include/linux/tracepoint.h:553:9: note: in expansion of macro 'DECLARE_TRACE'
553 | DECLARE_TRACE(name, PARAMS(proto), PARAMS(args))
| ^~~~~~~~~~~~~
include/trace/events/sched.h:222:1: note: in expansion of macro 'TRACE_EVENT'
222 | TRACE_EVENT(sched_switch,
| ^~~~~~~~~~~
In file included from include/linux/printk.h:11,
from include/linux/kernel.h:29,
from include/linux/interrupt.h:6,
from include/linux/trace_recursion.h:5,
from include/linux/ftrace.h:10,
from kernel/trace/rv/monitors/wwnr/wwnr.c:2:
kernel/trace/rv/monitors/wwnr/wwnr.c:62:53: error: passing argument 1 of 'register_trace_sched_switch' from incompatible pointer type [-Werror=incompatible-pointer-types]
62 | rv_attach_trace_probe("wwnr", sched_switch, handle_switch);
| ^~~~~~~~~~~~~
| |
| void (*)(void *, bool, struct task_struct *, struct task_struct *, unsigned int) {aka void (*)(void *, _Bool, struct task_struct *, struct task_struct *, unsigned int)}
include/linux/once_lite.h:15:41: note: in definition of macro 'DO_ONCE_LITE_IF'
15 | bool __ret_do_once = !!(condition); \
| ^~~~~~~~~
include/rv/instrumentation.h:16:17: note: in expansion of macro 'WARN_ONCE'
16 | WARN_ONCE(register_trace_##tp(rv_handler, NULL), \
| ^~~~~~~~~
kernel/trace/rv/monitors/wwnr/wwnr.c:62:9: note: in expansion of macro 'rv_attach_trace_probe'
62 | rv_attach_trace_probe("wwnr", sched_switch, handle_switch);
| ^~~~~~~~~~~~~~~~~~~~~
In file included from kernel/trace/rv/monitors/wwnr/wwnr.c:3:
include/linux/tracepoint.h:260:38: note: expected 'void (*)(void *, bool, unsigned int, struct task_struct *, struct task_struct *)' {aka 'void (*)(void *, _Bool, unsigned int, struct task_struct *, struct task_struct *)'} but argument is of type 'void (*)(void *, bool, struct task_struct *, struct task_struct *, unsigned int)' {aka 'void (*)(void *, _Bool, struct task_struct *, struct task_struct *, unsigned int)'}
260 | register_trace_##name(void (*probe)(data_proto), void *data) \
| ~~~~~~~^~~~~~~~~~~~~~~~~~
include/linux/tracepoint.h:419:9: note: in expansion of macro '__DECLARE_TRACE'
419 | __DECLARE_TRACE(name, PARAMS(proto), PARAMS(args), \
| ^~~~~~~~~~~~~~~
include/linux/tracepoint.h:553:9: note: in expansion of macro 'DECLARE_TRACE'
553 | DECLARE_TRACE(name, PARAMS(proto), PARAMS(args))
| ^~~~~~~~~~~~~
include/trace/events/sched.h:222:1: note: in expansion of macro 'TRACE_EVENT'
222 | TRACE_EVENT(sched_switch,
| ^~~~~~~~~~~
In file included from kernel/trace/rv/monitors/wwnr/wwnr.c:8:
kernel/trace/rv/monitors/wwnr/wwnr.c: In function 'stop_wwnr':
kernel/trace/rv/monitors/wwnr/wwnr.c:72:53: error: passing argument 1 of 'unregister_trace_sched_switch' from incompatible pointer type [-Werror=incompatible-pointer-types]
72 | rv_detach_trace_probe("wwnr", sched_switch, handle_switch);
| ^~~~~~~~~~~~~
| |
| void (*)(void *, bool, struct task_struct *, struct task_struct *, unsigned int) {aka void (*)(void *, _Bool, struct task_struct *, struct task_struct *, unsigned int)}
include/rv/instrumentation.h:22:39: note: in definition of macro 'rv_detach_trace_probe'
22 | unregister_trace_##tp(rv_handler, NULL); \
| ^~~~~~~~~~
In file included from kernel/trace/rv/monitors/wwnr/wwnr.c:3:
include/linux/tracepoint.h:273:40: note: expected 'void (*)(void *, bool, unsigned int, struct task_struct *, struct task_struct *)' {aka 'void (*)(void *, _Bool, unsigned int, struct task_struct *, struct task_struct *)'} but argument is of type 'void (*)(void *, bool, struct task_struct *, struct task_struct *, unsigned int)' {aka 'void (*)(void *, _Bool, struct task_struct *, struct task_struct *, unsigned int)'}
273 | unregister_trace_##name(void (*probe)(data_proto), void *data) \
| ~~~~~~~^~~~~~~~~~~~~~~~~~
include/linux/tracepoint.h:419:9: note: in expansion of macro '__DECLARE_TRACE'
419 | __DECLARE_TRACE(name, PARAMS(proto), PARAMS(args), \
| ^~~~~~~~~~~~~~~
include/linux/tracepoint.h:553:9: note: in expansion of macro 'DECLARE_TRACE'
553 | DECLARE_TRACE(name, PARAMS(proto), PARAMS(args))
| ^~~~~~~~~~~~~
include/trace/events/sched.h:222:1: note: in expansion of macro 'TRACE_EVENT'
222 | TRACE_EVENT(sched_switch,
| ^~~~~~~~~~~
kernel/trace/rv/monitors/wwnr/wwnr.c: At top level:
>> kernel/trace/rv/monitors/wwnr/wwnr.c:90:5: warning: no previous prototype for 'register_wwnr' [-Wmissing-prototypes]
90 | int register_wwnr(void)
| ^~~~~~~~~~~~~
>> kernel/trace/rv/monitors/wwnr/wwnr.c:96:6: warning: no previous prototype for 'unregister_wwnr' [-Wmissing-prototypes]
96 | void unregister_wwnr(void)
| ^~~~~~~~~~~~~~~
cc1: some warnings being treated as errors
vim +/register_wwnr +90 kernel/trace/rv/monitors/wwnr/wwnr.c
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 89
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 @90 int register_wwnr(void)
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 91 {
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 92 rv_register_monitor(&rv_wwnr);
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 93 return 0;
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 94 }
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 95
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 @96 void unregister_wwnr(void)
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 97 {
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 98 if (rv_wwnr.enabled)
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 99 stop_wwnr();
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 100
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 101 rv_unregister_monitor(&rv_wwnr);
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 102 }
13d11b21732323 Daniel Bristot de Oliveira 2022-06-16 103
--
0-DAY CI Kernel Test Service
https://01.org/lkp
Hi Daniel,
I love your patch! Perhaps something to improve:
[auto build test WARNING on rostedt-trace/for-next]
[also build test WARNING on tip/sched/core]
[If your patch is applied to the wrong git tree, kindly drop us a note.
And when submitting patch, we suggest to use '--base' as documented in
https://git-scm.com/docs/git-format-patch]
url: https://github.com/intel-lab-lkp/linux/commits/Daniel-Bristot-de-Oliveira/The-Runtime-Verification-RV-interface/20220616-164837
base: https://git.kernel.org/pub/scm/linux/kernel/git/rostedt/linux-trace.git for-next
config: x86_64-allyesconfig (https://download.01.org/0day-ci/archive/20220616/[email protected]/config)
compiler: gcc-11 (Debian 11.3.0-3) 11.3.0
reproduce (this is a W=1 build):
# https://github.com/intel-lab-lkp/linux/commit/c32f84c1978c0e0b8526da45a2ab87e191246f68
git remote add linux-review https://github.com/intel-lab-lkp/linux
git fetch --no-tags linux-review Daniel-Bristot-de-Oliveira/The-Runtime-Verification-RV-interface/20220616-164837
git checkout c32f84c1978c0e0b8526da45a2ab87e191246f68
# save the config file
mkdir build_dir && cp config build_dir/.config
make W=1 O=build_dir ARCH=x86_64 SHELL=/bin/bash kernel/trace/rv/
If you fix the issue, kindly add following tag where applicable
Reported-by: kernel test robot <[email protected]>
All warnings (new ones prefixed by >>):
>> kernel/trace/rv/reactor_panic.c:28:5: warning: no previous prototype for 'register_react_panic' [-Wmissing-prototypes]
28 | int register_react_panic(void)
| ^~~~~~~~~~~~~~~~~~~~
>> kernel/trace/rv/reactor_panic.c:34:6: warning: no previous prototype for 'unregister_react_panic' [-Wmissing-prototypes]
34 | void unregister_react_panic(void)
| ^~~~~~~~~~~~~~~~~~~~~~
vim +/register_react_panic +28 kernel/trace/rv/reactor_panic.c
27
> 28 int register_react_panic(void)
29 {
30 rv_register_reactor(&rv_panic);
31 return 0;
32 }
33
> 34 void unregister_react_panic(void)
35 {
36 rv_unregister_reactor(&rv_panic);
37 }
38
--
0-DAY CI Kernel Test Service
https://01.org/lkp
On 6/16/22 15:44, Guenter Roeck wrote:
> On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
>> Add a set of tracepoints, enabling the observability of the watchdog
>> device interactions with user-space.
>>
>> The events are:
>> watchdog:watchdog_open
>> watchdog:watchdog_close
>> watchdog:watchdog_start
>> watchdog:watchdog_stop
>> watchdog:watchdog_set_timeout
>> watchdog:watchdog_ping
>> watchdog:watchdog_nowayout
>> watchdog:watchdog_set_keep_alive
>> watchdog:watchdog_keep_alive
>> watchdog:watchdog_set_pretimeout
>> watchdog:watchdog_pretimeout
>>
>> Cc: Wim Van Sebroeck <[email protected]>
>> Cc: Guenter Roeck <[email protected]>
>> Cc: Jonathan Corbet <[email protected]>
>> Cc: Steven Rostedt <[email protected]>
>> Cc: Ingo Molnar <[email protected]>
>> Cc: Thomas Gleixner <[email protected]>
>> Cc: Peter Zijlstra <[email protected]>
>> Cc: Will Deacon <[email protected]>
>> Cc: Catalin Marinas <[email protected]>
>> Cc: Marco Elver <[email protected]>
>> Cc: Dmitry Vyukov <[email protected]>
>> Cc: "Paul E. McKenney" <[email protected]>
>> Cc: Shuah Khan <[email protected]>
>> Cc: Gabriele Paoloni <[email protected]>
>> Cc: Juri Lelli <[email protected]>
>> Cc: Clark Williams <[email protected]>
>> Cc: [email protected]
>> Cc: [email protected]
>> Cc: [email protected]
>> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
>> ---
>> drivers/watchdog/watchdog_dev.c | 43 ++++++++++-
>> drivers/watchdog/watchdog_pretimeout.c | 2 +
>> include/linux/watchdog.h | 7 +-
>> include/trace/events/watchdog.h | 101 +++++++++++++++++++++++++
>> 4 files changed, 143 insertions(+), 10 deletions(-)
>> create mode 100644 include/trace/events/watchdog.h
>>
>> diff --git a/drivers/watchdog/watchdog_dev.c b/drivers/watchdog/watchdog_dev.c
>> index 54903f3c851e..2f28dc5ab763 100644
>> --- a/drivers/watchdog/watchdog_dev.c
>> +++ b/drivers/watchdog/watchdog_dev.c
>> @@ -44,6 +44,9 @@
>> #include <linux/watchdog.h> /* For watchdog specific items */
>> #include <linux/uaccess.h> /* For copy_to_user/put_user/... */
>> +#define CREATE_TRACE_POINTS
>> +#include <trace/events/watchdog.h>
>> +
>> #include "watchdog_core.h"
>> #include "watchdog_pretimeout.h"
>> @@ -130,9 +133,11 @@ static inline void watchdog_update_worker(struct
>> watchdog_device *wdd)
>> if (watchdog_need_worker(wdd)) {
>> ktime_t t = watchdog_next_keepalive(wdd);
>> - if (t > 0)
>> + if (t > 0) {
>> hrtimer_start(&wd_data->timer, t,
>> HRTIMER_MODE_REL_HARD);
>> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
>> + }
>> } else {
>> hrtimer_cancel(&wd_data->timer);
>> }
>> @@ -141,7 +146,7 @@ static inline void watchdog_update_worker(struct
>> watchdog_device *wdd)
>> static int __watchdog_ping(struct watchdog_device *wdd)
>> {
>> struct watchdog_core_data *wd_data = wdd->wd_data;
>> - ktime_t earliest_keepalive, now;
>> + ktime_t earliest_keepalive, now, next_keepalive;
>> int err;
>> earliest_keepalive = ktime_add(wd_data->last_hw_keepalive,
>> @@ -149,14 +154,16 @@ static int __watchdog_ping(struct watchdog_device *wdd)
>> now = ktime_get();
>> if (ktime_after(earliest_keepalive, now)) {
>> - hrtimer_start(&wd_data->timer,
>> - ktime_sub(earliest_keepalive, now),
>> + next_keepalive = ktime_sub(earliest_keepalive, now);
>> + hrtimer_start(&wd_data->timer, next_keepalive,
>> HRTIMER_MODE_REL_HARD);
>> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(next_keepalive));
>> return 0;
>> }
>> wd_data->last_hw_keepalive = now;
>> + trace_watchdog_ping(wdd);
>> if (wdd->ops->ping)
>> err = wdd->ops->ping(wdd); /* ping the watchdog */
>> else
>> @@ -215,6 +222,7 @@ static void watchdog_ping_work(struct kthread_work *work)
>> wd_data = container_of(work, struct watchdog_core_data, work);
>> mutex_lock(&wd_data->lock);
>> + trace_watchdog_keep_alive(wd_data->wdd);
>> if (watchdog_worker_should_ping(wd_data))
>> __watchdog_ping(wd_data->wdd);
>> mutex_unlock(&wd_data->lock);
>> @@ -250,6 +258,8 @@ static int watchdog_start(struct watchdog_device *wdd)
>> set_bit(_WDOG_KEEPALIVE, &wd_data->status);
>> + trace_watchdog_start(wdd);
>> +
>> started_at = ktime_get();
>> if (watchdog_hw_running(wdd) && wdd->ops->ping) {
>> err = __watchdog_ping(wdd);
>> @@ -294,6 +304,7 @@ static int watchdog_stop(struct watchdog_device *wdd)
>> return -EBUSY;
>> }
>> + trace_watchdog_stop(wdd);
>> if (wdd->ops->stop) {
>> clear_bit(WDOG_HW_RUNNING, &wdd->status);
>> err = wdd->ops->stop(wdd);
>> @@ -367,6 +378,7 @@ static int watchdog_set_timeout(struct watchdog_device *wdd,
>> if (watchdog_timeout_invalid(wdd, timeout))
>> return -EINVAL;
>> + trace_watchdog_set_timeout(wdd, timeout);
>
> The driver has no obligation to set the timeout to the
> requested value. It might be more valuable to report both
> the requested and the actual values.
>
>
Ack! how do I get the actual value?
>> if (wdd->ops->set_timeout) {
>> err = wdd->ops->set_timeout(wdd, timeout);
>> } else {
>> @@ -399,6 +411,8 @@ static int watchdog_set_pretimeout(struct watchdog_device
>> *wdd,
>> if (watchdog_pretimeout_invalid(wdd, timeout))
>> return -EINVAL;
>> + trace_watchdog_set_pretimeout(wdd, timeout);
>> +
>
> Again, the driver has no obligation to set the timeout to the
> requested value.
/me takes note.
>
>> if (wdd->ops->set_pretimeout && (wdd->info->options & WDIOF_PRETIMEOUT))
>> err = wdd->ops->set_pretimeout(wdd, timeout);
>> else
>> @@ -430,6 +444,23 @@ static int watchdog_get_timeleft(struct watchdog_device
>> *wdd,
>> return 0;
>> }
>> +/**
>> + * watchdog_set_nowayout - set nowaout bit
>> + * @wdd: The watchdog device to set nowayoutbit
>> + * @nowayout A boolean on/off switcher
>> + *
>> + * If nowayout boolean is true, the nowayout option is set. No action is
>> + * taken if nowayout is false.
>> + */
>> +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
>> +{
>> + if (nowayout) {
>> + set_bit(WDOG_NO_WAY_OUT, &wdd->status);
>> + trace_watchdog_nowayout(wdd);
>> + }
>> +}
>> +EXPORT_SYMBOL(watchdog_set_nowayout);
>> +
>> #ifdef CONFIG_WATCHDOG_SYSFS
>> static ssize_t nowayout_show(struct device *dev, struct device_attribute *attr,
>> char *buf)
>> @@ -861,6 +892,8 @@ static int watchdog_open(struct inode *inode, struct file
>> *file)
>> goto out_clear;
>> }
>> + trace_watchdog_open(wdd);
>> +
>> err = watchdog_start(wdd);
>> if (err < 0)
>> goto out_mod;
>> @@ -883,6 +916,7 @@ static int watchdog_open(struct inode *inode, struct file
>> *file)
>> return stream_open(inode, file);
>> out_mod:
>> + trace_watchdog_close(wdd);
>> module_put(wd_data->wdd->ops->owner);
>> out_clear:
>> clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
>> @@ -944,6 +978,7 @@ static int watchdog_release(struct inode *inode, struct
>> file *file)
>> /* make sure that /dev/watchdog can be re-opened */
>> clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
>> + trace_watchdog_close(wdd);
>> done:
>> running = wdd && watchdog_hw_running(wdd);
>> mutex_unlock(&wd_data->lock);
>> diff --git a/drivers/watchdog/watchdog_pretimeout.c
>> b/drivers/watchdog/watchdog_pretimeout.c
>> index 376a495ab80c..58c391ed2205 100644
>> --- a/drivers/watchdog/watchdog_pretimeout.c
>> +++ b/drivers/watchdog/watchdog_pretimeout.c
>> @@ -8,6 +8,7 @@
>> #include <linux/spinlock.h>
>> #include <linux/string.h>
>> #include <linux/watchdog.h>
>> +#include <trace/events/watchdog.h>
>> #include "watchdog_core.h"
>> #include "watchdog_pretimeout.h"
>> @@ -107,6 +108,7 @@ void watchdog_notify_pretimeout(struct watchdog_device *wdd)
>> return;
>> }
>> + trace_watchdog_pretimeout(wdd);
>> wdd->gov->pretimeout(wdd);
>> spin_unlock_irqrestore(&pretimeout_lock, flags);
>> }
>> diff --git a/include/linux/watchdog.h b/include/linux/watchdog.h
>> index 99660197a36c..11d93407e492 100644
>> --- a/include/linux/watchdog.h
>> +++ b/include/linux/watchdog.h
>> @@ -139,12 +139,7 @@ static inline bool watchdog_hw_running(struct
>> watchdog_device *wdd)
>> return test_bit(WDOG_HW_RUNNING, &wdd->status);
>> }
>> -/* Use the following function to set the nowayout feature */
>> -static inline void watchdog_set_nowayout(struct watchdog_device *wdd, bool
>> nowayout)
>> -{
>> - if (nowayout)
>> - set_bit(WDOG_NO_WAY_OUT, &wdd->status);
>> -}
>> +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout);
>> /* Use the following function to stop the watchdog on reboot */
>> static inline void watchdog_stop_on_reboot(struct watchdog_device *wdd)
>> diff --git a/include/trace/events/watchdog.h b/include/trace/events/watchdog.h
>> new file mode 100644
>> index 000000000000..145cd6cfaa02
>> --- /dev/null
>> +++ b/include/trace/events/watchdog.h
>> @@ -0,0 +1,101 @@
>> +/* SPDX-License-Identifier: GPL-2.0 */
>> +#undef TRACE_SYSTEM
>> +#define TRACE_SYSTEM watchdog
>> +
>> +#if !defined(_TRACE_WATCHDOG_H) || defined(TRACE_HEADER_MULTI_READ)
>> +#define _TRACE_WATCHDOG_H
>> +
>> +#include <linux/tracepoint.h>
>> +
>> +/*
>> + * These are all events whose sole argument is the watchdog id.
>> + */
>> +DECLARE_EVENT_CLASS(dev_operations_template,
>> +
>> + TP_PROTO(struct watchdog_device *wdd),
>> +
>> + TP_ARGS(wdd),
>> +
>> + TP_STRUCT__entry(
>> + __field(__u32, id)
>> + ),
>> +
>> + TP_fast_assign(
>> + __entry->id = wdd->id;
>> + ),
>> +
>> + TP_printk("id=%d",
>> + __entry->id)
>> +);
>> +
>> +DEFINE_EVENT(dev_operations_template, watchdog_open,
>> + TP_PROTO(struct watchdog_device *wdd),
>> + TP_ARGS(wdd));
>> +
>> +DEFINE_EVENT(dev_operations_template, watchdog_close,
>> + TP_PROTO(struct watchdog_device *wdd),
>> + TP_ARGS(wdd));
>> +
>> +DEFINE_EVENT(dev_operations_template, watchdog_start,
>> + TP_PROTO(struct watchdog_device *wdd),
>> + TP_ARGS(wdd));
>> +
>> +DEFINE_EVENT(dev_operations_template, watchdog_stop,
>> + TP_PROTO(struct watchdog_device *wdd),
>> + TP_ARGS(wdd));
>> +
>> +DEFINE_EVENT(dev_operations_template, watchdog_ping,
>> + TP_PROTO(struct watchdog_device *wdd),
>> + TP_ARGS(wdd));
>> +
>> +DEFINE_EVENT(dev_operations_template, watchdog_nowayout,
>> + TP_PROTO(struct watchdog_device *wdd),
>> + TP_ARGS(wdd));
>> +
>> +DEFINE_EVENT(dev_operations_template, watchdog_keep_alive,
>> + TP_PROTO(struct watchdog_device *wdd),
>> + TP_ARGS(wdd));
>> +
>> +DEFINE_EVENT(dev_operations_template, watchdog_pretimeout,
>> + TP_PROTO(struct watchdog_device *wdd),
>> + TP_ARGS(wdd));
>> +
>> +/*
>> + * These are all events with a device ID and a given timeout.
>> + */
>> +DECLARE_EVENT_CLASS(watchdog_timeout_template,
>> +
>> + TP_PROTO(struct watchdog_device *wdd, u64 timeout),
>> +
>> + TP_ARGS(wdd, timeout),
>> +
>> + TP_STRUCT__entry(
>> + __field(__u32, id)
>> + __field(__u64, timeout)
>
>
> Why u64 ? timeout is unsigned long.
ack! I will change it. (I am seeing unsigned int, am I missing something?).
Thanks!
-- Daniel
On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index 1eafb5adcfcb..e9246b0bec9d 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -26,6 +26,13 @@ menuconfig RV
> the system behavior.
>
> if RV
> +config RV_MON_WIP
> + depends on PREEMPTIRQ_TRACEPOINTS
> + select DA_MON_EVENTS_IMPLICIT
> + bool "WIP monitor"
Does WIP mean work-in-progress? (It does to me.)
If not, please explain what it means in the help text.
> + help
> + Enable WIP sample monitor, this is a sample monitor that
> + illustrates the usage of per-cpu monitors.
thanks.
--
~Randy
On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index be8e3dab0a52..91a17b13a080 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -60,4 +60,12 @@ config RV_REACT_PRINTK
> Enables the printk reactor. The printk reactor emmits a printk()
emits
> message if an exception is found.
>
> +config RV_REACT_PANIC
> + bool "Panic reactor"
> + depends on RV_REACTORS
> + default y if RV_REACTORS
> + help
> + Enables the panic reactor. The panic reactor emmits a printk()
emits
> + message if an exception is found and panic()s the system.
--
~Randy
On 6/16/22 08:47, Daniel Bristot de Oliveira wrote:
> On 6/16/22 15:44, Guenter Roeck wrote:
>> On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
>>> Add a set of tracepoints, enabling the observability of the watchdog
>>> device interactions with user-space.
>>>
>>> The events are:
>>> watchdog:watchdog_open
>>> watchdog:watchdog_close
>>> watchdog:watchdog_start
>>> watchdog:watchdog_stop
>>> watchdog:watchdog_set_timeout
>>> watchdog:watchdog_ping
>>> watchdog:watchdog_nowayout
>>> watchdog:watchdog_set_keep_alive
>>> watchdog:watchdog_keep_alive
>>> watchdog:watchdog_set_pretimeout
>>> watchdog:watchdog_pretimeout
>>>
>>> Cc: Wim Van Sebroeck <[email protected]>
>>> Cc: Guenter Roeck <[email protected]>
>>> Cc: Jonathan Corbet <[email protected]>
>>> Cc: Steven Rostedt <[email protected]>
>>> Cc: Ingo Molnar <[email protected]>
>>> Cc: Thomas Gleixner <[email protected]>
>>> Cc: Peter Zijlstra <[email protected]>
>>> Cc: Will Deacon <[email protected]>
>>> Cc: Catalin Marinas <[email protected]>
>>> Cc: Marco Elver <[email protected]>
>>> Cc: Dmitry Vyukov <[email protected]>
>>> Cc: "Paul E. McKenney" <[email protected]>
>>> Cc: Shuah Khan <[email protected]>
>>> Cc: Gabriele Paoloni <[email protected]>
>>> Cc: Juri Lelli <[email protected]>
>>> Cc: Clark Williams <[email protected]>
>>> Cc: [email protected]
>>> Cc: [email protected]
>>> Cc: [email protected]
>>> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
>>> ---
>>> drivers/watchdog/watchdog_dev.c | 43 ++++++++++-
>>> drivers/watchdog/watchdog_pretimeout.c | 2 +
>>> include/linux/watchdog.h | 7 +-
>>> include/trace/events/watchdog.h | 101 +++++++++++++++++++++++++
>>> 4 files changed, 143 insertions(+), 10 deletions(-)
>>> create mode 100644 include/trace/events/watchdog.h
>>>
>>> diff --git a/drivers/watchdog/watchdog_dev.c b/drivers/watchdog/watchdog_dev.c
>>> index 54903f3c851e..2f28dc5ab763 100644
>>> --- a/drivers/watchdog/watchdog_dev.c
>>> +++ b/drivers/watchdog/watchdog_dev.c
>>> @@ -44,6 +44,9 @@
>>> #include <linux/watchdog.h> /* For watchdog specific items */
>>> #include <linux/uaccess.h> /* For copy_to_user/put_user/... */
>>> +#define CREATE_TRACE_POINTS
>>> +#include <trace/events/watchdog.h>
>>> +
>>> #include "watchdog_core.h"
>>> #include "watchdog_pretimeout.h"
>>> @@ -130,9 +133,11 @@ static inline void watchdog_update_worker(struct
>>> watchdog_device *wdd)
>>> if (watchdog_need_worker(wdd)) {
>>> ktime_t t = watchdog_next_keepalive(wdd);
>>> - if (t > 0)
>>> + if (t > 0) {
>>> hrtimer_start(&wd_data->timer, t,
>>> HRTIMER_MODE_REL_HARD);
>>> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
>>> + }
>>> } else {
>>> hrtimer_cancel(&wd_data->timer);
>>> }
>>> @@ -141,7 +146,7 @@ static inline void watchdog_update_worker(struct
>>> watchdog_device *wdd)
>>> static int __watchdog_ping(struct watchdog_device *wdd)
>>> {
>>> struct watchdog_core_data *wd_data = wdd->wd_data;
>>> - ktime_t earliest_keepalive, now;
>>> + ktime_t earliest_keepalive, now, next_keepalive;
>>> int err;
>>> earliest_keepalive = ktime_add(wd_data->last_hw_keepalive,
>>> @@ -149,14 +154,16 @@ static int __watchdog_ping(struct watchdog_device *wdd)
>>> now = ktime_get();
>>> if (ktime_after(earliest_keepalive, now)) {
>>> - hrtimer_start(&wd_data->timer,
>>> - ktime_sub(earliest_keepalive, now),
>>> + next_keepalive = ktime_sub(earliest_keepalive, now);
>>> + hrtimer_start(&wd_data->timer, next_keepalive,
>>> HRTIMER_MODE_REL_HARD);
>>> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(next_keepalive));
>>> return 0;
>>> }
>>> wd_data->last_hw_keepalive = now;
>>> + trace_watchdog_ping(wdd);
>>> if (wdd->ops->ping)
>>> err = wdd->ops->ping(wdd); /* ping the watchdog */
>>> else
>>> @@ -215,6 +222,7 @@ static void watchdog_ping_work(struct kthread_work *work)
>>> wd_data = container_of(work, struct watchdog_core_data, work);
>>> mutex_lock(&wd_data->lock);
>>> + trace_watchdog_keep_alive(wd_data->wdd);
>>> if (watchdog_worker_should_ping(wd_data))
>>> __watchdog_ping(wd_data->wdd);
>>> mutex_unlock(&wd_data->lock);
>>> @@ -250,6 +258,8 @@ static int watchdog_start(struct watchdog_device *wdd)
>>> set_bit(_WDOG_KEEPALIVE, &wd_data->status);
>>> + trace_watchdog_start(wdd);
>>> +
>>> started_at = ktime_get();
>>> if (watchdog_hw_running(wdd) && wdd->ops->ping) {
>>> err = __watchdog_ping(wdd);
>>> @@ -294,6 +304,7 @@ static int watchdog_stop(struct watchdog_device *wdd)
>>> return -EBUSY;
>>> }
>>> + trace_watchdog_stop(wdd);
>>> if (wdd->ops->stop) {
>>> clear_bit(WDOG_HW_RUNNING, &wdd->status);
>>> err = wdd->ops->stop(wdd);
>>> @@ -367,6 +378,7 @@ static int watchdog_set_timeout(struct watchdog_device *wdd,
>>> if (watchdog_timeout_invalid(wdd, timeout))
>>> return -EINVAL;
>>> + trace_watchdog_set_timeout(wdd, timeout);
>>
>> The driver has no obligation to set the timeout to the
>> requested value. It might be more valuable to report both
>> the requested and the actual values.
>>
>>
>
> Ack! how do I get the actual value?
>
Read it from the data structure after the driver function returned.
>>> if (wdd->ops->set_timeout) {
>>> err = wdd->ops->set_timeout(wdd, timeout);
>>> } else {
>>> @@ -399,6 +411,8 @@ static int watchdog_set_pretimeout(struct watchdog_device
>>> *wdd,
>>> if (watchdog_pretimeout_invalid(wdd, timeout))
>>> return -EINVAL;
>>> + trace_watchdog_set_pretimeout(wdd, timeout);
>>> +
>>
>> Again, the driver has no obligation to set the timeout to the
>> requested value.
>
> /me takes note.
>
>>
>>> if (wdd->ops->set_pretimeout && (wdd->info->options & WDIOF_PRETIMEOUT))
>>> err = wdd->ops->set_pretimeout(wdd, timeout);
>>> else
>>> @@ -430,6 +444,23 @@ static int watchdog_get_timeleft(struct watchdog_device
>>> *wdd,
>>> return 0;
>>> }
>>> +/**
>>> + * watchdog_set_nowayout - set nowaout bit
>>> + * @wdd: The watchdog device to set nowayoutbit
>>> + * @nowayout A boolean on/off switcher
>>> + *
>>> + * If nowayout boolean is true, the nowayout option is set. No action is
>>> + * taken if nowayout is false.
>>> + */
>>> +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout)
>>> +{
>>> + if (nowayout) {
>>> + set_bit(WDOG_NO_WAY_OUT, &wdd->status);
>>> + trace_watchdog_nowayout(wdd);
>>> + }
>>> +}
>>> +EXPORT_SYMBOL(watchdog_set_nowayout);
>>> +
>>> #ifdef CONFIG_WATCHDOG_SYSFS
>>> static ssize_t nowayout_show(struct device *dev, struct device_attribute *attr,
>>> char *buf)
>>> @@ -861,6 +892,8 @@ static int watchdog_open(struct inode *inode, struct file
>>> *file)
>>> goto out_clear;
>>> }
>>> + trace_watchdog_open(wdd);
>>> +
>>> err = watchdog_start(wdd);
>>> if (err < 0)
>>> goto out_mod;
>>> @@ -883,6 +916,7 @@ static int watchdog_open(struct inode *inode, struct file
>>> *file)
>>> return stream_open(inode, file);
>>> out_mod:
>>> + trace_watchdog_close(wdd);
>>> module_put(wd_data->wdd->ops->owner);
>>> out_clear:
>>> clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
>>> @@ -944,6 +978,7 @@ static int watchdog_release(struct inode *inode, struct
>>> file *file)
>>> /* make sure that /dev/watchdog can be re-opened */
>>> clear_bit(_WDOG_DEV_OPEN, &wd_data->status);
>>> + trace_watchdog_close(wdd);
>>> done:
>>> running = wdd && watchdog_hw_running(wdd);
>>> mutex_unlock(&wd_data->lock);
>>> diff --git a/drivers/watchdog/watchdog_pretimeout.c
>>> b/drivers/watchdog/watchdog_pretimeout.c
>>> index 376a495ab80c..58c391ed2205 100644
>>> --- a/drivers/watchdog/watchdog_pretimeout.c
>>> +++ b/drivers/watchdog/watchdog_pretimeout.c
>>> @@ -8,6 +8,7 @@
>>> #include <linux/spinlock.h>
>>> #include <linux/string.h>
>>> #include <linux/watchdog.h>
>>> +#include <trace/events/watchdog.h>
>>> #include "watchdog_core.h"
>>> #include "watchdog_pretimeout.h"
>>> @@ -107,6 +108,7 @@ void watchdog_notify_pretimeout(struct watchdog_device *wdd)
>>> return;
>>> }
>>> + trace_watchdog_pretimeout(wdd);
>>> wdd->gov->pretimeout(wdd);
>>> spin_unlock_irqrestore(&pretimeout_lock, flags);
>>> }
>>> diff --git a/include/linux/watchdog.h b/include/linux/watchdog.h
>>> index 99660197a36c..11d93407e492 100644
>>> --- a/include/linux/watchdog.h
>>> +++ b/include/linux/watchdog.h
>>> @@ -139,12 +139,7 @@ static inline bool watchdog_hw_running(struct
>>> watchdog_device *wdd)
>>> return test_bit(WDOG_HW_RUNNING, &wdd->status);
>>> }
>>> -/* Use the following function to set the nowayout feature */
>>> -static inline void watchdog_set_nowayout(struct watchdog_device *wdd, bool
>>> nowayout)
>>> -{
>>> - if (nowayout)
>>> - set_bit(WDOG_NO_WAY_OUT, &wdd->status);
>>> -}
>>> +void watchdog_set_nowayout(struct watchdog_device *wdd, bool nowayout);
>>> /* Use the following function to stop the watchdog on reboot */
>>> static inline void watchdog_stop_on_reboot(struct watchdog_device *wdd)
>>> diff --git a/include/trace/events/watchdog.h b/include/trace/events/watchdog.h
>>> new file mode 100644
>>> index 000000000000..145cd6cfaa02
>>> --- /dev/null
>>> +++ b/include/trace/events/watchdog.h
>>> @@ -0,0 +1,101 @@
>>> +/* SPDX-License-Identifier: GPL-2.0 */
>>> +#undef TRACE_SYSTEM
>>> +#define TRACE_SYSTEM watchdog
>>> +
>>> +#if !defined(_TRACE_WATCHDOG_H) || defined(TRACE_HEADER_MULTI_READ)
>>> +#define _TRACE_WATCHDOG_H
>>> +
>>> +#include <linux/tracepoint.h>
>>> +
>>> +/*
>>> + * These are all events whose sole argument is the watchdog id.
>>> + */
>>> +DECLARE_EVENT_CLASS(dev_operations_template,
>>> +
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> +
>>> + TP_ARGS(wdd),
>>> +
>>> + TP_STRUCT__entry(
>>> + __field(__u32, id)
>>> + ),
>>> +
>>> + TP_fast_assign(
>>> + __entry->id = wdd->id;
>>> + ),
>>> +
>>> + TP_printk("id=%d",
>>> + __entry->id)
>>> +);
>>> +
>>> +DEFINE_EVENT(dev_operations_template, watchdog_open,
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> + TP_ARGS(wdd));
>>> +
>>> +DEFINE_EVENT(dev_operations_template, watchdog_close,
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> + TP_ARGS(wdd));
>>> +
>>> +DEFINE_EVENT(dev_operations_template, watchdog_start,
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> + TP_ARGS(wdd));
>>> +
>>> +DEFINE_EVENT(dev_operations_template, watchdog_stop,
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> + TP_ARGS(wdd));
>>> +
>>> +DEFINE_EVENT(dev_operations_template, watchdog_ping,
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> + TP_ARGS(wdd));
>>> +
>>> +DEFINE_EVENT(dev_operations_template, watchdog_nowayout,
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> + TP_ARGS(wdd));
>>> +
>>> +DEFINE_EVENT(dev_operations_template, watchdog_keep_alive,
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> + TP_ARGS(wdd));
>>> +
>>> +DEFINE_EVENT(dev_operations_template, watchdog_pretimeout,
>>> + TP_PROTO(struct watchdog_device *wdd),
>>> + TP_ARGS(wdd));
>>> +
>>> +/*
>>> + * These are all events with a device ID and a given timeout.
>>> + */
>>> +DECLARE_EVENT_CLASS(watchdog_timeout_template,
>>> +
>>> + TP_PROTO(struct watchdog_device *wdd, u64 timeout),
>>> +
>>> + TP_ARGS(wdd, timeout),
>>> +
>>> + TP_STRUCT__entry(
>>> + __field(__u32, id)
>>> + __field(__u64, timeout)
>>
>>
>> Why u64 ? timeout is unsigned long.
>
> ack! I will change it. (I am seeing unsigned int, am I missing something?).
Yes, you are correct.
Guenter
On 6/16/22 23:03, Randy Dunlap wrote:
>
>
> On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
>> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
>> index be8e3dab0a52..91a17b13a080 100644
>> --- a/kernel/trace/rv/Kconfig
>> +++ b/kernel/trace/rv/Kconfig
>> @@ -60,4 +60,12 @@ config RV_REACT_PRINTK
>> Enables the printk reactor. The printk reactor emmits a printk()
>
> emits
oops!
>> message if an exception is found.
>>
>> +config RV_REACT_PANIC
>> + bool "Panic reactor"
>> + depends on RV_REACTORS
>> + default y if RV_REACTORS
>> + help
>> + Enables the panic reactor. The panic reactor emmits a printk()
>
> emits
and Oops again.
>> + message if an exception is found and panic()s the system.
>
I will fix that, thanks Randy!
-- Daniel
On 6/17/22 01:55, Guenter Roeck wrote:
> On 6/16/22 08:47, Daniel Bristot de Oliveira wrote:
>> On 6/16/22 15:44, Guenter Roeck wrote:
>>> On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
>>>> Add a set of tracepoints, enabling the observability of the watchdog
>>>> device interactions with user-space.
>>>>
>>>> The events are:
>>>> watchdog:watchdog_open
>>>> watchdog:watchdog_close
>>>> watchdog:watchdog_start
>>>> watchdog:watchdog_stop
>>>> watchdog:watchdog_set_timeout
>>>> watchdog:watchdog_ping
>>>> watchdog:watchdog_nowayout
>>>> watchdog:watchdog_set_keep_alive
>>>> watchdog:watchdog_keep_alive
>>>> watchdog:watchdog_set_pretimeout
>>>> watchdog:watchdog_pretimeout
>>>>
>>>> Cc: Wim Van Sebroeck <[email protected]>
>>>> Cc: Guenter Roeck <[email protected]>
>>>> Cc: Jonathan Corbet <[email protected]>
>>>> Cc: Steven Rostedt <[email protected]>
>>>> Cc: Ingo Molnar <[email protected]>
>>>> Cc: Thomas Gleixner <[email protected]>
>>>> Cc: Peter Zijlstra <[email protected]>
>>>> Cc: Will Deacon <[email protected]>
>>>> Cc: Catalin Marinas <[email protected]>
>>>> Cc: Marco Elver <[email protected]>
>>>> Cc: Dmitry Vyukov <[email protected]>
>>>> Cc: "Paul E. McKenney" <[email protected]>
>>>> Cc: Shuah Khan <[email protected]>
>>>> Cc: Gabriele Paoloni <[email protected]>
>>>> Cc: Juri Lelli <[email protected]>
>>>> Cc: Clark Williams <[email protected]>
>>>> Cc: [email protected]
>>>> Cc: [email protected]
>>>> Cc: [email protected]
>>>> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
>>>> ---
>>>> drivers/watchdog/watchdog_dev.c | 43 ++++++++++-
>>>> drivers/watchdog/watchdog_pretimeout.c | 2 +
>>>> include/linux/watchdog.h | 7 +-
>>>> include/trace/events/watchdog.h | 101 +++++++++++++++++++++++++
>>>> 4 files changed, 143 insertions(+), 10 deletions(-)
>>>> create mode 100644 include/trace/events/watchdog.h
>>>>
>>>> diff --git a/drivers/watchdog/watchdog_dev.c b/drivers/watchdog/watchdog_dev.c
>>>> index 54903f3c851e..2f28dc5ab763 100644
>>>> --- a/drivers/watchdog/watchdog_dev.c
>>>> +++ b/drivers/watchdog/watchdog_dev.c
>>>> @@ -44,6 +44,9 @@
>>>> #include <linux/watchdog.h> /* For watchdog specific items */
>>>> #include <linux/uaccess.h> /* For copy_to_user/put_user/... */
>>>> +#define CREATE_TRACE_POINTS
>>>> +#include <trace/events/watchdog.h>
>>>> +
>>>> #include "watchdog_core.h"
>>>> #include "watchdog_pretimeout.h"
>>>> @@ -130,9 +133,11 @@ static inline void watchdog_update_worker(struct
>>>> watchdog_device *wdd)
>>>> if (watchdog_need_worker(wdd)) {
>>>> ktime_t t = watchdog_next_keepalive(wdd);
>>>> - if (t > 0)
>>>> + if (t > 0) {
>>>> hrtimer_start(&wd_data->timer, t,
>>>> HRTIMER_MODE_REL_HARD);
>>>> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(t));
>>>> + }
>>>> } else {
>>>> hrtimer_cancel(&wd_data->timer);
>>>> }
>>>> @@ -141,7 +146,7 @@ static inline void watchdog_update_worker(struct
>>>> watchdog_device *wdd)
>>>> static int __watchdog_ping(struct watchdog_device *wdd)
>>>> {
>>>> struct watchdog_core_data *wd_data = wdd->wd_data;
>>>> - ktime_t earliest_keepalive, now;
>>>> + ktime_t earliest_keepalive, now, next_keepalive;
>>>> int err;
>>>> earliest_keepalive = ktime_add(wd_data->last_hw_keepalive,
>>>> @@ -149,14 +154,16 @@ static int __watchdog_ping(struct watchdog_device *wdd)
>>>> now = ktime_get();
>>>> if (ktime_after(earliest_keepalive, now)) {
>>>> - hrtimer_start(&wd_data->timer,
>>>> - ktime_sub(earliest_keepalive, now),
>>>> + next_keepalive = ktime_sub(earliest_keepalive, now);
>>>> + hrtimer_start(&wd_data->timer, next_keepalive,
>>>> HRTIMER_MODE_REL_HARD);
>>>> + trace_watchdog_set_keep_alive(wdd, ktime_to_ms(next_keepalive));
>>>> return 0;
>>>> }
>>>> wd_data->last_hw_keepalive = now;
>>>> + trace_watchdog_ping(wdd);
>>>> if (wdd->ops->ping)
>>>> err = wdd->ops->ping(wdd); /* ping the watchdog */
>>>> else
>>>> @@ -215,6 +222,7 @@ static void watchdog_ping_work(struct kthread_work *work)
>>>> wd_data = container_of(work, struct watchdog_core_data, work);
>>>> mutex_lock(&wd_data->lock);
>>>> + trace_watchdog_keep_alive(wd_data->wdd);
>>>> if (watchdog_worker_should_ping(wd_data))
>>>> __watchdog_ping(wd_data->wdd);
>>>> mutex_unlock(&wd_data->lock);
>>>> @@ -250,6 +258,8 @@ static int watchdog_start(struct watchdog_device *wdd)
>>>> set_bit(_WDOG_KEEPALIVE, &wd_data->status);
>>>> + trace_watchdog_start(wdd);
>>>> +
>>>> started_at = ktime_get();
>>>> if (watchdog_hw_running(wdd) && wdd->ops->ping) {
>>>> err = __watchdog_ping(wdd);
>>>> @@ -294,6 +304,7 @@ static int watchdog_stop(struct watchdog_device *wdd)
>>>> return -EBUSY;
>>>> }
>>>> + trace_watchdog_stop(wdd);
>>>> if (wdd->ops->stop) {
>>>> clear_bit(WDOG_HW_RUNNING, &wdd->status);
>>>> err = wdd->ops->stop(wdd);
>>>> @@ -367,6 +378,7 @@ static int watchdog_set_timeout(struct watchdog_device *wdd,
>>>>
>>>> if (watchdog_timeout_invalid(wdd, timeout))
>>>> return -EINVAL;
>>>> + trace_watchdog_set_timeout(wdd, timeout);
>>>
>>> The driver has no obligation to set the timeout to the
>>> requested value. It might be more valuable to report both
>>> the requested and the actual values.
>>>
>>>
>>
>> Ack! how do I get the actual value?
>>
> Read it from the data structure after the driver function returned.
Got it! I will add this field too.
-- Daniel
On 6/16/22 23:00, Randy Dunlap wrote:
>
> On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
>> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
>> index 1eafb5adcfcb..e9246b0bec9d 100644
>> --- a/kernel/trace/rv/Kconfig
>> +++ b/kernel/trace/rv/Kconfig
>> @@ -26,6 +26,13 @@ menuconfig RV
>> the system behavior.
>>
>> if RV
>> +config RV_MON_WIP
>> + depends on PREEMPTIRQ_TRACEPOINTS
>> + select DA_MON_EVENTS_IMPLICIT
>> + bool "WIP monitor"
> Does WIP mean work-in-progress? (It does to me.)
>
> If not, please explain what it means in the help text.
>
Wakeup in preemptive. I will add it to the description.
Thanks Randy!
-- Daniel
Hi Daniel,
On Thu, Jun 16, 2022 at 1:45 AM Daniel Bristot de Oliveira
<[email protected]> wrote:
>
> Over the last years, I've been exploring the possibility of
> verifying the Linux kernel behavior using Runtime Verification.
>
> Runtime Verification (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 for complex
> systems.
>
> Instead of relying on a fine-grained model of a system (e.g., a
> re-implementation a instruction level), RV works by analyzing the trace of the
> system's actual execution, comparing it against a formal specification of
> the system behavior.
>
> The usage of deterministic automaton for RV is a well-established
> approach. In the specific case of the Linux kernel, you can check how
> to model complex behavior of the Linux kernel with 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.
>
> And how efficient is this approach here:
>
> DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread
> synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
> Architecture, 2020, 107: 101729.
>
> tlrd: it is possible to model complex behaviors in a modular way, with
> an acceptable overhead (even for production systems). See this
> presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg
>
> Here I am proposing a more practical approach for the usage of deterministic
> automata for runtime verification, and it includes:
>
> - An interface for controlling the verification;
> - A tool and set of headers that enables the automatic code
> generation of the RV monitor (Monitor Synthesis);
> - Sample monitors to evaluate the interface;
> - A sample monitor developed in the context of the Elisa Project
> demonstrating how to use RV in the context of safety-critical
> systems.
>
> Given that RV is a tracing consumer, the code is being placed inside the
> tracing subsystem (Steven and I have been talking about it for a while).
This is interesting work!
I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d
in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and
CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two
configs disabled. However, I hit the some issue with monitors/wwnr/enabled :
[root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/
[root@eth50-1 rv]# cat available_monitors
wwnr
[root@eth50-1 rv]# echo wwnr > enabled_monitors
[root@eth50-1 rv]# cd monitors/
[root@eth50-1 monitors]# cd wwnr/
[root@eth50-1 wwnr]# ls
desc enable reactors
[root@eth50-1 wwnr]# cat enable
1
[root@eth50-1 wwnr]# echo 0 > enable <<< hangs
The last echo command hangs forever on a qemu vm. I haven't figured out why
this happens though.
I also have a more general question: can we do RV with BPF and simplify the
work? AFAICT, the idea of RV is to maintain a state machine based on events.
If something unexpected happens, call the reactor.
IIUC, BPF has most of these building blocks ready for use. With BPF, we
can ship many RV monitors without much kernel changes.
Here is my toy wwnr in bpftrace. The reactor is "print to console".
It runs on most systems with BPF and tracepoint enabled. I probably
missed some events, as a result, the script triggers the "reactor" a lot.
=============== 8< ======================
[root@ ~]# cat wwnr.bt
/*
* task_state[pid]
* not_running = 1
* running = 2
*/
tracepoint:sched:sched_switch
{
if (args->prev_state == 0x0001 /* TASK_INTERRUPTIBLE */) {
/* after first suspension */
@task_state[args->prev_pid] = 1;
} else {
if (@task_state[args->prev_pid] == 1) {
printf("Something wrong, call reactor\n");
}
@task_state[args->prev_pid] = 1;
}
@task_state[args->next_pid] = 2;
}
tracepoint:sched:sched_wakeup
{
if (@task_state[args->pid] == 2) {
printf("Something wrong, call reactor\n");
}
@task_state[args->pid] = 2;
}
[root@ ~]# bpftrace wwnr.bt
<<<< some print >>>>
=============== 8< ======================
Does this (BPF for RV) make any sense?
Thanks,
Song
On 6/22/22 09:24, Song Liu wrote:
> This is interesting work!
>
> I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d
> in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and
> CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two
> configs disabled.
I rebased the code and... it compiled. Maybe it was missing some
config options that I forgot to set as "depends on" in the Kconfig.
Can you check if it was the same problem automatically reported?
Any further information here would help. I will revisit this.
However, I hit the some issue with monitors/wwnr/enabled :
>
> [root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/
> [root@eth50-1 rv]# cat available_monitors
> wwnr
> [root@eth50-1 rv]# echo wwnr > enabled_monitors
> [root@eth50-1 rv]# cd monitors/
> [root@eth50-1 monitors]# cd wwnr/
> [root@eth50-1 wwnr]# ls
> desc enable reactors
> [root@eth50-1 wwnr]# cat enable
> 1
> [root@eth50-1 wwnr]# echo 0 > enable <<< hangs
>
> The last echo command hangs forever on a qemu vm. I haven't figured out why
> this happens though.
I could reproduce it. It is an error in the return code of monitor_enable_write_data(),
I fixed it locally (return retval ? retval : count; // needs more test), and
will add it to the next version. Thanks!
> I also have a more general question: can we do RV with BPF and simplify the
> work? AFAICT, the idea of RV is to maintain a state machine based on events.
> If something unexpected happens, call the reactor.
>
> IIUC, BPF has most of these building blocks ready for use. With BPF, we
> can ship many RV monitors without much kernel changes.
I am aware of bpftrace and bpf + libbpf, and I have a PoC tool doing most of the
work I do in C/kernel in C/bpf.
From the cover letter:
"Things kept for a second moment (after this patchset):
[...]
- dot2bpf"
The point is that there are use-cases in which the users need the code in
C. One of those is the work being done in the Linux Foundation Elisa group.
There will be more formalism, like timed automata... which will require
infra-structure that is easily accessible in C... including synchronization,
and reactors that are available only in C on "per use-cases" basis - for
example on embedded devices.
On the other hand, there is ongoing research on asynchronous RV in which
I am only using BPF on the instrumentation side, for more complex formalism
running the processing in user-space (but for a different use-case,
with different timing and logical properties).
I see C and BPF (and rust?...) as complementary tools that I can use, and
we will have them all :-).
In this first series, I am adding the DA monitor in the kernel (motivated
by Elisa), and the basic kernel interface. After that, I will add the dot2bpf
for the cases in which BPF is a viable option... other formalism... other
extensions from Elisa... and so on... collecting these methods in a single
place.
-- Daniel
> Thanks,
> Song
On Thu, Jun 23, 2022 at 9:42 AM Daniel Bristot de Oliveira
<[email protected]> wrote:
>
> On 6/22/22 09:24, Song Liu wrote:
> > This is interesting work!
> >
> > I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d
> > in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and
> > CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two
> > configs disabled.
>
> I rebased the code and... it compiled. Maybe it was missing some
> config options that I forgot to set as "depends on" in the Kconfig.
>
> Can you check if it was the same problem automatically reported?
>
> Any further information here would help. I will revisit this.
Here are the error messages I got: https://pastebin.com/zJxMA6RK , and
attached is the config file I used.
>
> However, I hit the some issue with monitors/wwnr/enabled :
> >
> > [root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/
> > [root@eth50-1 rv]# cat available_monitors
> > wwnr
> > [root@eth50-1 rv]# echo wwnr > enabled_monitors
> > [root@eth50-1 rv]# cd monitors/
> > [root@eth50-1 monitors]# cd wwnr/
> > [root@eth50-1 wwnr]# ls
> > desc enable reactors
> > [root@eth50-1 wwnr]# cat enable
> > 1
> > [root@eth50-1 wwnr]# echo 0 > enable <<< hangs
> >
> > The last echo command hangs forever on a qemu vm. I haven't figured out why
> > this happens though.
>
> I could reproduce it. It is an error in the return code of monitor_enable_write_data(),
> I fixed it locally (return retval ? retval : count; // needs more test), and
> will add it to the next version. Thanks!
>
> > I also have a more general question: can we do RV with BPF and simplify the
> > work? AFAICT, the idea of RV is to maintain a state machine based on events.
> > If something unexpected happens, call the reactor.
> >
> > IIUC, BPF has most of these building blocks ready for use. With BPF, we
> > can ship many RV monitors without much kernel changes.
>
> I am aware of bpftrace and bpf + libbpf, and I have a PoC tool doing most of the
> work I do in C/kernel in C/bpf.
>
> From the cover letter:
>
> "Things kept for a second moment (after this patchset):
> [...]
> - dot2bpf"
>
> The point is that there are use-cases in which the users need the code in
> C. One of those is the work being done in the Linux Foundation Elisa group.
> There will be more formalism, like timed automata... which will require
> infra-structure that is easily accessible in C... including synchronization,
> and reactors that are available only in C on "per use-cases" basis - for
> example on embedded devices.
Where can I find more information about the constraints of these use cases?
I am asking because there are multiple ways to load a BPF program to the
system. If the constraint is that we cannot have bpftrace or bcc in the system,
maybe it is ok to run a standalone binary (written in C, compiled on a different
system). Or maybe we can load BPF programs in a kernel module, or compile
the BPF programs into the kernel? (Yes, we can do it now, check
kernel/bpf/preload). If any of these works, we can benefit from the good
properties of BPF. For example, we can update the RV models without
rebooting the system; and we can reuse various BPF maps, so we don't
need to add union rv_task_monitor to task_struct.
Of course, we are out of luck if these systems cannot enable CONFIG_BPF
at all. But I guess this is not common for modern embedded systems?
Thanks,
Song
On 6/23/22 12:52, Song Liu wrote:
> On Thu, Jun 23, 2022 at 9:42 AM Daniel Bristot de Oliveira
> <[email protected]> wrote:
>>
>> On 6/22/22 09:24, Song Liu wrote:
>>> This is interesting work!
>>>
>>> I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d
>>> in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and
>>> CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two
>>> configs disabled.
>>
>> I rebased the code and... it compiled. Maybe it was missing some
>> config options that I forgot to set as "depends on" in the Kconfig.
>>
>> Can you check if it was the same problem automatically reported?
>>
>> Any further information here would help. I will revisit this.
>
> Here are the error messages I got: https://pastebin.com/zJxMA6RK , and
> attached is the config file I used.
>
>>
>> However, I hit the some issue with monitors/wwnr/enabled :
>>>
>>> [root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/
>>> [root@eth50-1 rv]# cat available_monitors
>>> wwnr
>>> [root@eth50-1 rv]# echo wwnr > enabled_monitors
>>> [root@eth50-1 rv]# cd monitors/
>>> [root@eth50-1 monitors]# cd wwnr/
>>> [root@eth50-1 wwnr]# ls
>>> desc enable reactors
>>> [root@eth50-1 wwnr]# cat enable
>>> 1
>>> [root@eth50-1 wwnr]# echo 0 > enable <<< hangs
>>>
>>> The last echo command hangs forever on a qemu vm. I haven't figured out why
>>> this happens though.
>>
>> I could reproduce it. It is an error in the return code of monitor_enable_write_data(),
>> I fixed it locally (return retval ? retval : count; // needs more test), and
>> will add it to the next version. Thanks!
>>
>>> I also have a more general question: can we do RV with BPF and simplify the
>>> work? AFAICT, the idea of RV is to maintain a state machine based on events.
>>> If something unexpected happens, call the reactor.
>>>
>>> IIUC, BPF has most of these building blocks ready for use. With BPF, we
>>> can ship many RV monitors without much kernel changes.
>>
>> I am aware of bpftrace and bpf + libbpf, and I have a PoC tool doing most of the
>> work I do in C/kernel in C/bpf.
>>
>> From the cover letter:
>>
>> "Things kept for a second moment (after this patchset):
>> [...]
>> - dot2bpf"
>>
>> The point is that there are use-cases in which the users need the code in
>> C. One of those is the work being done in the Linux Foundation Elisa group.
>> There will be more formalism, like timed automata... which will require
>> infra-structure that is easily accessible in C... including synchronization,
>> and reactors that are available only in C on "per use-cases" basis - for
>> example on embedded devices.
>
> Where can I find more information about the constraints of these use cases?
Check the LF elisa workgroup.
> I am asking because there are multiple ways to load a BPF program to the
> system. If the constraint is that we cannot have bpftrace or bcc in the system,
> maybe it is ok to run a standalone binary (written in C, compiled on a different
> system).
as I said... *I am aware of that*. I do like BPF! I was already convinced I will having
things in BPF :-)
dot2bpf does stand alone application, C + libbpf (and I did it this way to
have the most of flexibility), it works (for the things that are possible in BPF).
It shares most of the work in C/kernel, I will add it in the second patch series.
Or maybe we can load BPF programs in a kernel module, or compile
> the BPF programs into the kernel? (Yes, we can do it now, check
> kernel/bpf/preload). If any of these works, we can benefit from the good
> properties of BPF.
RV will take all these benefits, it is in the todo list as I said in this thread.
But the in kernel version also has its facilities.
For example, we can update the RV models without
> rebooting the system; and we can reuse various BPF maps, so we don't
> need to add union rv_task_monitor to task_struct.
>
> Of course, we are out of luck if these systems cannot enable CONFIG_BPF
> at all. But I guess this is not common for modern embedded systems?
I understand your motivations, and I agree with the benefits of BPF, but I also
see benefits of having it in kernel as well.
So, RV will go with both, they are not mutually exclusive.
Thanks!
-- Daniel
> Thanks,
> Song
On Thu, 16 Jun 2022 10:44:44 +0200
Daniel Bristot de Oliveira <[email protected]> wrote:
> diff --git a/include/linux/rv.h b/include/linux/rv.h
> index 205e65f57637..1e48c6bb74bf 100644
> --- a/include/linux/rv.h
> +++ b/include/linux/rv.h
> @@ -8,6 +8,13 @@
> */
> #ifndef _LINUX_RV_H
> #define _LINUX_RV_H
> +
> +struct rv_reactor {
> + char *name;
> + char *description;
> + void (*react)(char *msg);
> +};
> +
> struct rv_monitor {
> const char *name;
> const char *description;
> @@ -15,9 +22,15 @@ struct rv_monitor {
> int (*start)(void);
> void (*stop)(void);
> void (*reset)(void);
> + void (*react)(char *msg);
> +
> };
>
> extern bool monitoring_on;
> int rv_unregister_monitor(struct rv_monitor *monitor);
> int rv_register_monitor(struct rv_monitor *monitor);
> +
> +extern bool reacting_on;
> +int rv_unregister_reactor(struct rv_reactor *reactor);
> +int rv_register_reactor(struct rv_reactor *reactor);
> #endif /* _LINUX_RV_H */
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index 6d127cdb00dd..560408fec0c8 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -10,3 +10,17 @@ menuconfig RV
> theorem proving). RV works by analyzing the trace of the system's
> actual execution, comparing it against a formal specification of
> the system behavior.
> +
> +if RV
Remove the above.
> +
> +config RV_REACTORS
> + bool "Runtime verification reactors"
> + default y if RV
default y
DEPENDS ON RV
> + help
> + Enables the online runtime verification reactors. 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.
> +
> +endif # RV
> diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
> index fd995379df67..8944274d9b41 100644
> --- a/kernel/trace/rv/Makefile
> +++ b/kernel/trace/rv/Makefile
> @@ -1,3 +1,4 @@
> # SPDX-License-Identifier: GPL-2.0
>
> obj-$(CONFIG_RV) += rv.o
> +obj-$(CONFIG_RV_REACTORS) += rv_reactors.o
> diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c
> index 43af7b13187e..7576d492a974 100644
> --- a/kernel/trace/rv/rv.c
> +++ b/kernel/trace/rv/rv.c
> @@ -362,8 +362,13 @@ static int create_monitor_dir(struct rv_monitor_def *mdef)
> retval = -ENOMEM;
> goto out_remove_root;
> }
> +#ifdef CONFIG_RV_REACTORS
Could you move the ifdefs to a header or above, and then just make
theses functions into nops when not defined. Keeps the actual code
cleaner.
> + retval = reactor_create_monitor_files(mdef);
> + if (retval)
> + goto out_remove_root;
> +#endif
>
> - return retval;
> + return 0;
>
> out_remove_root:
> rv_remove(mdef->root_d);
> @@ -674,7 +679,11 @@ int rv_register_monitor(struct rv_monitor *monitor)
>
> r->monitor = monitor;
>
> - create_monitor_dir(r);
> + retval = create_monitor_dir(r);
> + if (retval) {
> + kfree(r);
> + goto out_unlock;
> + }
>
> list_add_tail(&r->list, &rv_monitors_list);
>
> @@ -732,6 +741,11 @@ int __init rv_init_interface(void)
> rv_create_file("monitoring_on", 0600, rv_root.root_dir, NULL,
> &monitoring_on_fops);
>
> +#ifdef CONFIG_RV_REACTORS
> + init_rv_reactors(rv_root.root_dir);
> + reacting_on = true;
Same here.
Could have init_rv_reactors() return a value and then:
if (init_rv_reactors(...))
reacting_on = true;
> +#endif
> +
> monitoring_on = true;
>
> return 0;
> diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h
> index 0796867a7b1e..6d43f52d72a9 100644
> --- a/kernel/trace/rv/rv.h
> +++ b/kernel/trace/rv/rv.h
> @@ -15,14 +15,28 @@ struct rv_interface {
> #define rv_remove tracefs_remove
>
> #define MAX_RV_MONITOR_NAME_SIZE 32
> +#define MAX_RV_REACTOR_NAME_SIZE 32
>
> extern struct mutex rv_interface_lock;
>
> +#ifdef CONFIG_RV_REACTORS
> +struct rv_reactor_def {
> + struct list_head list;
> + struct rv_reactor *reactor;
> + /* protected by the monitor interface lock */
> + int counter;
> +};
> +#endif
> +
> struct rv_monitor_def {
> struct list_head list;
> struct rv_monitor *monitor;
> +#ifdef CONFIG_RV_REACTORS
> + struct rv_reactor_def *rdef;
> +#endif
> struct dentry *root_d;
> bool enabled;
> + bool reacting;
> bool task_monitor;
> };
>
> @@ -32,3 +46,9 @@ void reset_all_monitors(void);
> int init_rv_monitors(struct dentry *root_dir);
> int get_task_monitor_slot(void);
> void put_task_monitor_slot(int slot);
> +
> +#ifdef CONFIG_RV_REACTORS
> +extern bool reacting_on;
> +int reactor_create_monitor_files(struct rv_monitor_def *mdef);
> +int init_rv_reactors(struct dentry *root_dir);
> +#endif
> diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c
> new file mode 100644
> index 000000000000..bfe54d6996cc
> --- /dev/null
> +++ b/kernel/trace/rv/rv_reactors.c
> @@ -0,0 +1,476 @@
> +// SPDX-License-Identifier: GPL-2.0
> +/*
> + * Runtime reactor interface.
> + *
> + * 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.
> + *
> + * == Registering reactors ==
> + *
> + * The struct rv_reactor defines a callback function to be executed
> + * in case of a model exception happens. The callback function
> + * receives a message to be (optionally) printed before executing
> + * the reaction.
> + *
> + * A RV reactor is registered via:
> + * int rv_register_reactor(struct rv_reactor *reactor)
> + * And unregistered via:
> + * int rv_unregister_reactor(struct rv_reactor *reactor)
> + *
> + * These functions are exported to modules, enabling reactors to be
> + * dynamically loaded.
> + *
> + * == User interface ==
> + *
> + * The user interface resembles the kernel tracing interface and
> + * presents these files:
> + *
> + * "available_reactors"
> + * - List the available reactors, one per line.
> + *
> + * For example:
> + * [root@f32 rv]# 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 defaul one is the nop (no operation)
> + * reactor.
> + * - Writing the name of an reactor enables it to the given
> + * MONITOR.
> + *
> + * For example:
> + * [root@f32 rv]# cat monitors/wip/reactors
> + * [nop]
> + * panic
> + * printk
> + * [root@f32 rv]# echo panic > monitors/wip/reactors
> + * [root@f32 rv]# cat monitors/wip/reactors
> + * nop
> + * [panic]
> + * printk
> + *
> + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
> + */
> +
> +#include <linux/slab.h>
> +
> +#include "rv.h"
> +
> +bool __read_mostly reacting_on;
> +
> +/*
> + * Interface for the reactor register.
> + */
> +LIST_HEAD(rv_reactors_list);
> +
> +static struct rv_reactor_def *get_reactor_rdef_by_name(char *name)
> +{
> + struct rv_reactor_def *r;
> +
> + list_for_each_entry(r, &rv_reactors_list, list) {
> + if (strcmp(name, r->reactor->name) == 0)
> + return r;
> + }
> + return NULL;
> +}
> +
> +/*
> + * Available reactors seq functions.
> + */
> +static int reactors_show(struct seq_file *m, void *p)
> +{
> + struct rv_reactor_def *rea_def = p;
> +
> + seq_printf(m, "%s\n", rea_def->reactor->name);
> + return 0;
> +}
> +
> +static void reactors_stop(struct seq_file *m, void *p)
> +{
> + mutex_unlock(&rv_interface_lock);
> +}
> +
> +static void *reactors_start(struct seq_file *m, loff_t *pos)
> +{
> + mutex_lock(&rv_interface_lock);
> + return seq_list_start(&rv_reactors_list, *pos);
> +}
> +
> +static void *reactors_next(struct seq_file *m, void *p, loff_t *pos)
> +{
> + return seq_list_next(p, &rv_reactors_list, pos);
> +}
> +
> +/*
> + * available reactors seq definition.
> + */
> +static const struct seq_operations available_reactors_seq_ops = {
> + .start = reactors_start,
> + .next = reactors_next,
> + .stop = reactors_stop,
> + .show = reactors_show
> +};
> +
> +/*
> + * available_reactors interface.
> + */
> +static int available_reactors_open(struct inode *inode, struct file *file)
> +{
> + return seq_open(file, &available_reactors_seq_ops);
> +};
> +
> +static const struct file_operations available_reactors_ops = {
> + .open = available_reactors_open,
> + .read = seq_read,
> + .llseek = seq_lseek,
> + .release = seq_release
> +};
> +
> +/*
> + * Monitor reactor file.
> + */
> +static int monitor_reactor_show(struct seq_file *m, void *p)
> +{
> + struct rv_monitor_def *mdef = m->private;
> + struct rv_reactor_def *rdef = p;
> +
> + if (mdef->rdef == rdef)
> + seq_printf(m, "[%s]\n", rdef->reactor->name);
> + else
> + seq_printf(m, "%s\n", rdef->reactor->name);
> + return 0;
> +}
> +
> +/*
> + * available reactors seq definition.
> + */
> +static const struct seq_operations monitor_reactors_seq_ops = {
> + .start = reactors_start,
> + .next = reactors_next,
> + .stop = reactors_stop,
> + .show = monitor_reactor_show
> +};
> +
> +static ssize_t
> +monitor_reactors_write(struct file *file, const char __user *user_buf,
> + size_t count, loff_t *ppos)
> +{
> + char buff[MAX_RV_REACTOR_NAME_SIZE+1];
> + struct rv_monitor_def *mdef;
> + struct rv_reactor_def *rdef;
> + struct seq_file *seq_f;
> + int retval = -EINVAL;
> + char *ptr = buff;
> + int len;
> +
> + if (count < 1 || count > MAX_RV_REACTOR_NAME_SIZE+1)
> + return -EINVAL;
> +
> + memset(buff, 0, sizeof(buff));
> +
> + retval = simple_write_to_buffer(buff, sizeof(buff)-1, ppos, user_buf,
> + count);
> + if (!retval)
> + return -EFAULT;
> +
> + len = strlen(ptr);
> + if (!len)
> + return count;
> + /*
> + * remove the \n
> + */
> + ptr[len-1] = '\0';
Again, use strim().
> +
> + /*
> + * See monitor_reactors_open()
> + */
> + seq_f = file->private_data;
> + mdef = seq_f->private;
> +
> + mutex_lock(&rv_interface_lock);
> +
> + retval = -EINVAL;
> +
> + /*
> + * nop special case: disable reacting.
> + */
> + if (strcmp(ptr, "nop") == 0) {
> +
> + if (mdef->monitor->enabled)
> + mdef->monitor->stop();
> +
> + mdef->rdef = get_reactor_rdef_by_name("nop");
> + mdef->reacting = false;
> + mdef->monitor->react = NULL;
> +
> + if (mdef->monitor->enabled)
> + mdef->monitor->start();
> +
> + retval = count;
> + goto unlock;
> + }
> +
> + list_for_each_entry(rdef, &rv_reactors_list, list) {
> + if (strcmp(ptr, rdef->reactor->name) == 0) {
Again,
if (strcmp(ptr, rdef->reactor->name) != 0)
continue;
Then we can remove the extra indent.
-- Steve
> + /*
> + * found!
> + */
> + if (mdef->monitor->enabled)
> + mdef->monitor->stop();
> +
> + mdef->rdef = rdef;
> + mdef->reacting = true;
> + mdef->monitor->react = rdef->reactor->react;
> +
> + if (mdef->monitor->enabled)
> + mdef->monitor->start();
> +
> + retval = count;
> + break;
> + }
> + }
> +
> +unlock:
> + mutex_unlock(&rv_interface_lock);
> +
> + return retval;
> +}
> +
> +/*
On Thu, Jun 23, 2022 at 1:29 PM Daniel Bristot de Oliveira
<[email protected]> wrote:
>
[...]
> >>
> >> The point is that there are use-cases in which the users need the code in
> >> C. One of those is the work being done in the Linux Foundation Elisa group.
> >> There will be more formalism, like timed automata... which will require
> >> infra-structure that is easily accessible in C... including synchronization,
> >> and reactors that are available only in C on "per use-cases" basis - for
> >> example on embedded devices.
> >
> > Where can I find more information about the constraints of these use cases?
>
> Check the LF elisa workgroup.
Thanks for the information. It looks interesting.
>
> > I am asking because there are multiple ways to load a BPF program to the
> > system. If the constraint is that we cannot have bpftrace or bcc in the system,
> > maybe it is ok to run a standalone binary (written in C, compiled on a different
> > system).
>
> as I said... *I am aware of that*. I do like BPF! I was already convinced I will having
> things in BPF :-)
>
> dot2bpf does stand alone application, C + libbpf (and I did it this way to
> have the most of flexibility), it works (for the things that are possible in BPF).
> It shares most of the work in C/kernel, I will add it in the second patch series.
This is great! Looking forward to trying it out. :)
Thanks,
Song
On Thu, 16 Jun 2022 10:44:48 +0200
Daniel Bristot de Oliveira <[email protected]> wrote:
> + def __create_matrix(self):
> + # transform the array into a dictionary
> + events = self.events
> + states = self.states
> + events_dict = {}
> + states_dict = {}
> + nr_event = 0
> + for event in events:
> + events_dict[event] = nr_event
> + nr_event += 1
> +
> + nr_state = 0
> + for state in states:
> + states_dict[state] = nr_state
> + nr_state = nr_state + 1
> +
Hmm, do you just like inconsistency?
nr_event += 1
nr_state = nr_state + 1
??
-- Steve
On Thu, 16 Jun 2022 10:44:45 +0200
Daniel Bristot de Oliveira <[email protected]> wrote:
> 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 for monitoring.
>
> Cc: Wim Van Sebroeck <[email protected]>
> Cc: Guenter Roeck <[email protected]>
> Cc: Jonathan Corbet <[email protected]>
> Cc: Steven Rostedt <[email protected]>
> Cc: Ingo Molnar <[email protected]>
> Cc: Thomas Gleixner <[email protected]>
> Cc: Peter Zijlstra <[email protected]>
> Cc: Will Deacon <[email protected]>
> Cc: Catalin Marinas <[email protected]>
> Cc: Marco Elver <[email protected]>
> Cc: Dmitry Vyukov <[email protected]>
> Cc: "Paul E. McKenney" <[email protected]>
> Cc: Shuah Khan <[email protected]>
> Cc: Gabriele Paoloni <[email protected]>
> Cc: Juri Lelli <[email protected]>
> Cc: Clark Williams <[email protected]>
> Cc: [email protected]
> Cc: [email protected]
> Cc: [email protected]
> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
> ---
> include/rv/automata.h | 49 +++++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 49 insertions(+)
> create mode 100644 include/rv/automata.h
>
> diff --git a/include/rv/automata.h b/include/rv/automata.h
> new file mode 100644
> index 000000000000..0c0aa54bd820
> --- /dev/null
> +++ b/include/rv/automata.h
> @@ -0,0 +1,49 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Deterministic automata helper functions, to be used with the automata
> + * models in C generated by the dot2k tool.
> + *
> + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
Copyright before the description.
> + */
> +
There should be comments here describing how the helper functions are used.
-- Steve
> +#define DECLARE_AUTOMATA_HELPERS(name, type) \
> + \
> +static inline void *model_get_model_##name(void) \
> +{ \
> + return (void *) &automaton_##name; \
> +} \
> + \
> +static char *model_get_state_name_##name(enum states_##name state) \
> +{ \
> + return automaton_##name.state_names[state]; \
> +} \
> + \
> +static char *model_get_event_name_##name(enum events_##name event) \
> +{ \
> + return automaton_##name.event_names[event]; \
> +} \
> + \
> +static inline type model_get_init_state_##name(void) \
> +{ \
> + return automaton_##name.initial_state; \
> +} \
> + \
> +static inline type model_get_next_state_##name(enum states_##name curr_state, \
> + enum events_##name event) \
> +{ \
> + if ((curr_state < 0) || (curr_state > state_max_##name)) \
> + return -1; \
> + \
> + if ((event < 0) || (event > event_max_##name)) \
> + return -1; \
> + \
> + return automaton_##name.function[curr_state][event]; \
> +} \
> + \
> +static inline bool model_is_final_state_##name(enum states_##name state) \
> +{ \
> + if ((state < 0) || (state > state_max_##name)) \
> + return 0; \
> + \
> + return !!automaton_##name.final_states[state]; \
> +}
On Thu, 16 Jun 2022 10:44:48 +0200
Daniel Bristot de Oliveira <[email protected]> wrote:
> + def get_minimun_type(self):
> + min_type="char"
> +
> + if self.states.__len__() > 255:
> + min_type="short"
> +
> + if self.states.__len__() > 65535:
> + min_type="int"
Should these be "unsigned"? As char goes from -128 <-> 127
and short goes from -32768 <-> 32767
And are you sure you're not going to have more than 2,147,483,647 states ;-)
(or 4,294,967,296 if it's unsigned).
-- Steve
> +
> + return min_type
> +
On Thu, 16 Jun 2022 14:00:10 -0700
Randy Dunlap <[email protected]> wrote:
> On 6/16/22 01:44, Daniel Bristot de Oliveira wrote:
> > diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> > index 1eafb5adcfcb..e9246b0bec9d 100644
> > --- a/kernel/trace/rv/Kconfig
> > +++ b/kernel/trace/rv/Kconfig
> > @@ -26,6 +26,13 @@ menuconfig RV
> > the system behavior.
> >
> > if RV
> > +config RV_MON_WIP
> > + depends on PREEMPTIRQ_TRACEPOINTS
> > + select DA_MON_EVENTS_IMPLICIT
> > + bool "WIP monitor"
>
> Does WIP mean work-in-progress? (It does to me.)
>
> If not, please explain what it means in the help text.
Yeah, that's exactly what I thought too ;-)
-- Steve
>
> > + help
> > + Enable WIP sample monitor, this is a sample monitor that
> > + illustrates the usage of per-cpu monitors.
>
> thanks.
On Thu, 16 Jun 2022 10:44:57 +0200
Daniel Bristot de Oliveira <[email protected]> wrote:
> +DA monitor synthesis in a nutshell
> +------------------------------------------------------
> +
> +The synthesis of automata-based models into the Linux *RV monitor* abstraction
> +is automated by a tool named "dot2k", and the "rv/da_monitor.h" provided
> +by the RV interface.
> +
> +Given a file "wip.dot", representing a per-cpu monitor, with this content::
Specify what "wip" is here too.
-- Steve
> +
> + digraph state_automaton {
> + center = true;
> + size = "7,11";
> + rankdir = LR;
> + {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";
> + }
> + }
> +
On Thu, 16 Jun 2022 10:44:55 +0200
Daniel Bristot de Oliveira <[email protected]> wrote:
> Sample reactor that panics the system when an exception is found. This
> is useful both to capture a vmcore, or to fail-safe a critical system.
>
> Cc: Wim Van Sebroeck <[email protected]>
> Cc: Guenter Roeck <[email protected]>
> Cc: Jonathan Corbet <[email protected]>
> Cc: Steven Rostedt <[email protected]>
> Cc: Ingo Molnar <[email protected]>
> Cc: Thomas Gleixner <[email protected]>
> Cc: Peter Zijlstra <[email protected]>
> Cc: Will Deacon <[email protected]>
> Cc: Catalin Marinas <[email protected]>
> Cc: Marco Elver <[email protected]>
> Cc: Dmitry Vyukov <[email protected]>
> Cc: "Paul E. McKenney" <[email protected]>
> Cc: Shuah Khan <[email protected]>
> Cc: Gabriele Paoloni <[email protected]>
> Cc: Juri Lelli <[email protected]>
> Cc: Clark Williams <[email protected]>
> Cc: [email protected]
> Cc: [email protected]
> Cc: [email protected]
> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
> ---
> kernel/trace/rv/Kconfig | 8 ++++++
> kernel/trace/rv/Makefile | 1 +
> kernel/trace/rv/reactor_panic.c | 44 +++++++++++++++++++++++++++++++++
> 3 files changed, 53 insertions(+)
> create mode 100644 kernel/trace/rv/reactor_panic.c
>
> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig
> index be8e3dab0a52..91a17b13a080 100644
> --- a/kernel/trace/rv/Kconfig
> +++ b/kernel/trace/rv/Kconfig
> @@ -60,4 +60,12 @@ config RV_REACT_PRINTK
> Enables the printk reactor. The printk reactor emmits a printk()
> message if an exception is found.
>
> +config RV_REACT_PANIC
> + bool "Panic reactor"
> + depends on RV_REACTORS
> + default y if RV_REACTORS
Just put default y if it already depends on RV_REACTORS.
-- Steve
> + help
> + Enables the panic reactor. The panic reactor emmits a printk()
> + message if an exception is found and panic()s the system.
> +
> endif # RV
> diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile
On Thu, 16 Jun 2022 10:44:53 +0200
Daniel Bristot de Oliveira <[email protected]> wrote:
> diff --git a/kernel/trace/rv/monitors/wwnr/wwnr.c b/kernel/trace/rv/monitors/wwnr/wwnr.c
> index 8ba01f0f0df8..3fe1ad9125d3 100644
> --- a/kernel/trace/rv/monitors/wwnr/wwnr.c
> +++ b/kernel/trace/rv/monitors/wwnr/wwnr.c
> @@ -10,11 +10,8 @@
>
> #define MODULE_NAME "wwnr"
>
> -/*
> - * XXX: include required tracepoint headers, e.g.,
> - * #include <linux/trace/events/sched.h>
> - */
> #include <trace/events/rv.h>
> +#include <trace/events/sched.h>
>
> /*
> * This is the self-generated part of the monitor. Generally, there is no need
> @@ -37,21 +34,20 @@ DECLARE_DA_MON_PER_TASK(wwnr, char);
> * are translated into model's event.
> *
> */
> -static void handle_switch_in(void *data, /* XXX: fill header */)
> +static void handle_switch(void *data, bool preempt, struct task_struct *p,
> + struct task_struct *n, unsigned int prev_state)
> {
Patch 8 was the "educational" patch. There's no reason to split 10 and 11
up too.
-- Steve
> - struct task_struct *p = /* XXX: how do I get p? */;
> - da_handle_event_wwnr(p, switch_in_wwnr);
> -}
> + /* start monitoring only after the first suspension */
> + if (prev_state == TASK_INTERRUPTIBLE)
> + da_handle_init_event_wwnr(p, switch_out_wwnr);
> + else
> + da_handle_event_wwnr(p, switch_out_wwnr);
>
> -static void handle_switch_out(void *data, /* XXX: fill header */)
> -{
> - struct task_struct *p = /* XXX: how do I get p? */;
> - da_handle_event_wwnr(p, switch_out_wwnr);
> + da_handle_event_wwnr(n, switch_in_wwnr);
> }
>
> -static void handle_wakeup(void *data, /* XXX: fill header */)
> +static void handle_wakeup(void *data, struct task_struct *p)
> {
> - struct task_struct *p = /* XXX: how do I get p? */;
> da_handle_event_wwnr(p, wakeup_wwnr);
> }
On Thu, 16 Jun 2022 10:44:50 +0200
Daniel Bristot de Oliveira <[email protected]> wrote:
> This is the direct output this command line:
> $ dot2k -d ~/wip.dot -t per_cpu
>
> with wip.dot as:
So you created the "Work In Progress" monitor?
Is that what wip stands for?
-- Steve
Hi Daniel,
After reading things in paper and the previous versions these days slowly
from me, I choose to join the thread this time not because I understand
them clearly. Sorry for not saving your email bandwidth..
On Thu, Jun 16, 2022 at 10:44:42AM +0200, Daniel Bristot de Oliveira wrote:
> Over the last years, I've been exploring the possibility of
> verifying the Linux kernel behavior using Runtime Verification.
>
> Runtime Verification (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 for complex
> systems.
>
> Instead of relying on a fine-grained model of a system (e.g., a
> re-implementation a instruction level), RV works by analyzing the trace of the
> system's actual execution, comparing it against a formal specification of
> the system behavior.
>
> The usage of deterministic automaton for RV is a well-established
> approach. In the specific case of the Linux kernel, you can check how
> to model complex behavior of the Linux kernel with 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.
>
> And how efficient is this approach here:
>
> DE OLIVEIRA, Daniel B.; DE OLIVEIRA, Romulo S.; CUCINOTTA, Tommaso. *A thread
> synchronization model for the PREEMPT_RT Linux kernel.* Journal of Systems
> Architecture, 2020, 107: 101729.
>
> tlrd: it is possible to model complex behaviors in a modular way, with
> an acceptable overhead (even for production systems). See this
> presentation at 2019's ELCE: https://www.youtube.com/watch?v=BfTuEHafNgg
>
> Here I am proposing a more practical approach for the usage of deterministic
> automata for runtime verification, and it includes:
>
> - An interface for controlling the verification;
> - A tool and set of headers that enables the automatic code
> generation of the RV monitor (Monitor Synthesis);
> - Sample monitors to evaluate the interface;
> - A sample monitor developed in the context of the Elisa Project
> demonstrating how to use RV in the context of safety-critical
> systems.
>
> Given that RV is a tracing consumer, the code is being placed inside the
> tracing subsystem (Steven and I have been talking about it for a while).
>
> Changes from v3:
> - Rebased on 5.19
> (rostedt's request were made on 1x1 meetings)
> - Moved monitors to monitors/$name/ (Rostedt)
> - Consolidate the tracepoints into a single include file in the default
> directory (trave/events/rv.h) (Rostedt)
s/trave\(\/events\/rv.h\)/trace\1/
> - The tracepoints now record the entire string to the buffer.
> - Change the enable_monitors to disable monitors with ! (instead of -).
> (Rostedt)
> - Add a suffix to the state/events enums, to avoid conflict in the
> vmlinux.h used by eBPF.
> - The models are now placed in the $name.h (it used to store the
> tracepoints, but they are now consolidated in a single file)
> - dot2c and dot2k updated to the changes
> - models re-generated with these new standards.
> - user-space tools moved to an directory outside of tools/tracing as
> other methods of verification/log sources are planned.
> Changes from v2:
> - Tons of checkpatch and kernel test robot
> - Moved files to better places
> - Adjusted watchdog tracepoints patch (Guenter Roeck)
> - Added pretimeout watchdog events (Peter Enderborg)
> - Used task struct to store per-task monitors (Peter Zijlstra)
> - Changed the instrumentation to use internal definition of tracepoint
> and check the callback signature (Steven Rostedt)
> - Used printk_deferred() and removed the comment about deadlocks
> (Shuah Khan/John Ogness)
> - Some simplifications:
> - Removed the safe watchdog nowayout for now (myself)
> - Removed export symbols for now (myself)
> Changes from V1:
> - rebased to the latest kernel;
> - code cleanup;
> - the watchdog dev monitor;
> - safety app;
>
> Things kept for a second moment (after this patchset):
> - Add a reactor tha enables the visualization of the visited
> states via KCOV (Marco Elver & Dmitry Vyukov)
> - Add a CRC method to check from user-space if the values
> exported by the monitor were not corrupted by any other
> kernel task (Gabriele Paoloni)
> - Export symbols for external modules
> - dot2bpf
>
> Daniel Bristot de Oliveira (20):
> rv: Add Runtime Verification (RV) interface
> rv: Add runtime reactors interface
> rv/include: Add helper functions for deterministic automata
> rv/include: Add deterministic automata monitor definition via C macros
> rv/include: Add instrumentation helper functions
> tools/rv: Add dot2c
> tools/rv: Add dot2k
> rv/monitor: Add the wip monitor skeleton created by dot2k
> rv/monitor: wip instrumentation and Makefile/Kconfig entries
> rv/monitor: Add the wwnr monitor skeleton created by dot2k
> rv/monitor: wwnr instrumentation and Makefile/Kconfig entries
> rv/reactor: Add the printk reactor
> rv/reactor: Add the panic reactor
> Documentation/rv: Add a basic documentation
> Documentation/rv: Add deterministic automata monitor synthesis
> documentation
> Documentation/rv: Add deterministic automata instrumentation
> documentation
> watchdog/dev: Add tracepoints
> rv/monitor: Add safe watchdog monitor
> rv/safety_app: Add a safety_app sample
> Documentation/rv: Add watchdog-monitor documentation
>
> Documentation/trace/index.rst | 1 +
> .../trace/rv/da_monitor_instrumentation.rst | 223 ++++++
> .../trace/rv/da_monitor_synthesis.rst | 284 +++++++
> Documentation/trace/rv/index.rst | 9 +
> .../trace/rv/runtime-verification.rst | 233 ++++++
> Documentation/trace/rv/watchdog-monitor.rst | 250 ++++++
> drivers/watchdog/watchdog_dev.c | 43 +-
> drivers/watchdog/watchdog_pretimeout.c | 2 +
> include/linux/rv.h | 38 +
> include/linux/sched.h | 11 +
> include/linux/watchdog.h | 7 +-
> include/rv/automata.h | 49 ++
> include/rv/da_monitor.h | 419 ++++++++++
> include/rv/instrumentation.h | 23 +
> include/rv/rv.h | 32 +
> include/trace/events/rv.h | 153 ++++
> include/trace/events/watchdog.h | 101 +++
> kernel/fork.c | 14 +
> kernel/trace/Kconfig | 2 +
> kernel/trace/Makefile | 2 +
> kernel/trace/rv/Kconfig | 84 ++
> kernel/trace/rv/Makefile | 9 +
> kernel/trace/rv/monitors/safe_wtd/safe_wtd.c | 300 +++++++
> kernel/trace/rv/monitors/safe_wtd/safe_wtd.h | 84 ++
> kernel/trace/rv/monitors/wip/wip.c | 110 +++
> kernel/trace/rv/monitors/wip/wip.h | 38 +
> kernel/trace/rv/monitors/wwnr/wwnr.c | 109 +++
> kernel/trace/rv/monitors/wwnr/wwnr.h | 38 +
> kernel/trace/rv/reactor_panic.c | 44 +
> kernel/trace/rv/reactor_printk.c | 43 +
> kernel/trace/rv/rv.c | 757 ++++++++++++++++++
> kernel/trace/rv/rv.h | 54 ++
> kernel/trace/rv/rv_reactors.c | 476 +++++++++++
> kernel/trace/trace.c | 4 +
> kernel/trace/trace.h | 2 +
> tools/verification/dot2/Makefile | 26 +
> tools/verification/dot2/automata.py | 179 +++++
> tools/verification/dot2/dot2c | 30 +
> tools/verification/dot2/dot2c.py | 244 ++++++
> tools/verification/dot2/dot2k | 50 ++
> tools/verification/dot2/dot2k.py | 177 ++++
> .../dot2/dot2k_templates/main_global.c | 94 +++
> .../dot2/dot2k_templates/main_per_cpu.c | 94 +++
> .../dot2/dot2k_templates/main_per_task.c | 94 +++
> tools/verification/safety_app/Makefile | 51 ++
> tools/verification/safety_app/safety_app.c | 614 ++++++++++++++
> 46 files changed, 5691 insertions(+), 10 deletions(-)
> create mode 100644 Documentation/trace/rv/da_monitor_instrumentation.rst
> create mode 100644 Documentation/trace/rv/da_monitor_synthesis.rst
> create mode 100644 Documentation/trace/rv/index.rst
> create mode 100644 Documentation/trace/rv/runtime-verification.rst
> create mode 100644 Documentation/trace/rv/watchdog-monitor.rst
> create mode 100644 include/linux/rv.h
> create mode 100644 include/rv/automata.h
> create mode 100644 include/rv/da_monitor.h
> create mode 100644 include/rv/instrumentation.h
> create mode 100644 include/rv/rv.h
> create mode 100644 include/trace/events/rv.h
> create mode 100644 include/trace/events/watchdog.h
> create mode 100644 kernel/trace/rv/Kconfig
> create mode 100644 kernel/trace/rv/Makefile
> create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.c
> create mode 100644 kernel/trace/rv/monitors/safe_wtd/safe_wtd.h
> create mode 100644 kernel/trace/rv/monitors/wip/wip.c
> create mode 100644 kernel/trace/rv/monitors/wip/wip.h
> create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.c
> create mode 100644 kernel/trace/rv/monitors/wwnr/wwnr.h
> create mode 100644 kernel/trace/rv/reactor_panic.c
> create mode 100644 kernel/trace/rv/reactor_printk.c
> create mode 100644 kernel/trace/rv/rv.c
> create mode 100644 kernel/trace/rv/rv.h
> create mode 100644 kernel/trace/rv/rv_reactors.c
> create mode 100644 tools/verification/dot2/Makefile
> create mode 100644 tools/verification/dot2/automata.py
> create mode 100644 tools/verification/dot2/dot2c
> create mode 100644 tools/verification/dot2/dot2c.py
> create mode 100644 tools/verification/dot2/dot2k
> create mode 100644 tools/verification/dot2/dot2k.py
> create mode 100644 tools/verification/dot2/dot2k_templates/main_global.c
> create mode 100644 tools/verification/dot2/dot2k_templates/main_per_cpu.c
> create mode 100644 tools/verification/dot2/dot2k_templates/main_per_task.c
> create mode 100644 tools/verification/safety_app/Makefile
> create mode 100644 tools/verification/safety_app/safety_app.c
>
> --
> 2.35.1
>
On Thu, Jun 16, 2022 at 10:44:45AM +0200, Daniel Bristot de Oliveira wrote:
> 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
> surce code representation that to be used for monitoring.
>
> This header file implements helper functions to facilitate the usage
> of the C output from dot2c for monitoring.
>
> Cc: Wim Van Sebroeck <[email protected]>
> Cc: Guenter Roeck <[email protected]>
> Cc: Jonathan Corbet <[email protected]>
> Cc: Steven Rostedt <[email protected]>
> Cc: Ingo Molnar <[email protected]>
> Cc: Thomas Gleixner <[email protected]>
> Cc: Peter Zijlstra <[email protected]>
> Cc: Will Deacon <[email protected]>
> Cc: Catalin Marinas <[email protected]>
> Cc: Marco Elver <[email protected]>
> Cc: Dmitry Vyukov <[email protected]>
> Cc: "Paul E. McKenney" <[email protected]>
> Cc: Shuah Khan <[email protected]>
> Cc: Gabriele Paoloni <[email protected]>
> Cc: Juri Lelli <[email protected]>
> Cc: Clark Williams <[email protected]>
> Cc: [email protected]
> Cc: [email protected]
> Cc: [email protected]
> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
> ---
> include/rv/automata.h | 49 +++++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 49 insertions(+)
> create mode 100644 include/rv/automata.h
>
> diff --git a/include/rv/automata.h b/include/rv/automata.h
> new file mode 100644
> index 000000000000..0c0aa54bd820
> --- /dev/null
> +++ b/include/rv/automata.h
> @@ -0,0 +1,49 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Deterministic automata helper functions, to be used with the automata
> + * models in C generated by the dot2k tool.
> + *
> + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
> + */
> +
> +#define DECLARE_AUTOMATA_HELPERS(name, type) \
> + \
> +static inline void *model_get_model_##name(void) \
> +{ \
> + return (void *) &automaton_##name; \
> +} \
> + \
> +static char *model_get_state_name_##name(enum states_##name state) \
> +{ \
> + return automaton_##name.state_names[state]; \
> +} \
> + \
> +static char *model_get_event_name_##name(enum events_##name event) \
> +{ \
> + return automaton_##name.event_names[event]; \
> +} \
> + \
> +static inline type model_get_init_state_##name(void) \
> +{ \
> + return automaton_##name.initial_state; \
> +} \
> + \
> +static inline type model_get_next_state_##name(enum states_##name curr_state, \
> + enum events_##name event) \
> +{ \
> + if ((curr_state < 0) || (curr_state > state_max_##name)) \
> + return -1; \
curr_state can not be state_max_xxx. curr_state must be not bigger
than state_max_xxx. Or am I miss something?
> + if ((event < 0) || (event > event_max_##name)) \
> + return -1; \
> + \
Same here for the event boundary check.
> + return automaton_##name.function[curr_state][event]; \
> +} \
> + \
> +static inline bool model_is_final_state_##name(enum states_##name state) \
> +{ \
> + if ((state < 0) || (state > state_max_##name)) \
> + return 0; \
> + \
Same here.
> + return !!automaton_##name.final_states[state]; \
If the value of .final_states[state] is 0 or 1, can the type of
.final_states[state] be befined to bool. Or not need to use !! to
explicitly transfer the type to bool. I remember that you define
this as char array and the matrix model value of this array is 0 or 1
see from the next patche. 1 delegate the state it is the initial state.
0 for others.
> +}
> --
> 2.35.1
>
On Thu, Jun 16, 2022 at 10:45:02AM +0200,
Daniel Bristot de Oliveira wrote:
> Adds documentation about the safe_wtd and safe_wtd_nwo RV monitors,
> and their usage via a safety application.
>
> Cc: Wim Van Sebroeck <[email protected]>
> Cc: Guenter Roeck <[email protected]>
> Cc: Jonathan Corbet <[email protected]>
> Cc: Steven Rostedt <[email protected]>
> Cc: Ingo Molnar <[email protected]>
> Cc: Thomas Gleixner <[email protected]>
> Cc: Peter Zijlstra <[email protected]>
> Cc: Will Deacon <[email protected]>
> Cc: Catalin Marinas <[email protected]>
> Cc: Marco Elver <[email protected]>
> Cc: Dmitry Vyukov <[email protected]>
> Cc: "Paul E. McKenney" <[email protected]>
> Cc: Shuah Khan <[email protected]>
> Cc: Gabriele Paoloni <[email protected]>
> Cc: Juri Lelli <[email protected]>
> Cc: Clark Williams <[email protected]>
> Cc: [email protected]
> Cc: [email protected]
> Cc: [email protected]
> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
> ---
> Documentation/trace/rv/watchdog-monitor.rst | 250 ++++++++++++++++++++
> 1 file changed, 250 insertions(+)
> create mode 100644 Documentation/trace/rv/watchdog-monitor.rst
>
> diff --git a/Documentation/trace/rv/watchdog-monitor.rst b/Documentation/trace/rv/watchdog-monitor.rst
> new file mode 100644
> index 000000000000..2b142fb31572
> --- /dev/null
> +++ b/Documentation/trace/rv/watchdog-monitor.rst
> @@ -0,0 +1,250 @@
> +Watchdog monitor
> +----------------
> +
> +The watchdog is an essential building block for the usage of Linux in
> +safety-critical systems because it allows the system to be monitored from
> +an external element - the watchdog hardware, acting as a safety-monitor.
> +
> +A user-space application controls the watchdog device via the watchdog
> +interface. This application, hereafter safety_app, enables the watchdog
> +and periodically pets the watchdog upon correct completion of the safety
> +related processing.
> +
> +If the safety_app, for any reason, stops pinging the watchdog,
> +the watchdog hardware can set the system in a fail-safe state. For
> +example, shutting the system down.
> +
> +Given the importance of the safety_app / watchdog hardware couple,
> +the interaction between these software pieces also needs some
> +sort of monitoring. In other words, "who monitors the monitor?"
> +
> +The safe watchdog (safe_wtd) RV monitor monitors the interaction between
> +the safety_app and the watchdog device, enforcing the correct sequence of
> +events that leads the system to a safe state.
> +
> +Furthermore, the safety_app can monitor the RV monitor by collecting the
> +events generated by the RV monitor itself via tracing interface. In this way,
> +closing the monitoring loop with the safety_app.
> +
> +A diagram of the components and their interactions is::
> +
> + user-space:
> + +--------------------------------+
> + | safety_app |-----------+
> + +--------------------------------+ |
> + | ^ |
> + | Configure | Enable and |
> + | | check data |
> + ===================+====================+=============== |
> + kernel-space: | | |
> + v v |
> + +----------+ instr. +-------------+ |
> + | watchdog | ----------->| RV Monitor |----+ |
> + | device | +-------------+ | |
> + +----------+ | |
> + | | |
> + | | |
> + ================+====================================== | |
> + hardware: | | |
> + v | +-> Bring the system
> + +--------------------+ +----> to a safe state,
> + | watchdog hardware |---------------------------> e.g., halt.
> + +--------------------+
> +
> +Sample safety_app
> +-----------------
> +
> +The user-space safety_app sample code in ``tools/verification/safety_app/``
> +serves to illustrate the usage of the RV monitors for this use-case, as
> +well as the starting point to the development of a user-specific safety_app.
> +
> +Watchdog events
> +---------------
> +
> +The RV monitor observes the watchdog by using instrumentation to
> +process the events generated by the interaction between the
> +safety_app and the watchdog device layer in kernel.
> +
> +The monitored events are:
> +
> + - watchdog:watchdog_open: open the watchdog device;
> + - watchdog:watchdog_close: close the watchdog device;
> + - watchdog:watchdog_start: start the watchdog;
> + - watchdog:watchdog_stop: stop the watchdog;
> + - watchdog:watchdog_set_timeout: set the watchdog timeout;
> + - watchdog:watchdog_ping: reprogram the watchdog with the previously set
> + timeout;
> + - watchdog:watchdog_nowayout: prevents the watchdog from stopping;
> + - watchdog:watchdog_set_keep_alive: set an intermediary ping to overcome
> + the limitation of a hardware watchdog maximum timeout being shorter than
> + the timeout set by the user-space tool;
> + - watchdog:watchdog_keep_alive: the execution of the function that runs the
> + intermediary keep alive ping;
> +
> +RV monitor events
> +-----------------
> +
> +The RV monitor monitors the relevant events as an outside observer,
> +interpreting all the components (the hardware; the watchdog device
> +interface; and the safety monitor) as an integrated component.
> +
> +The events selected for the monitor are:
> +
> + - other_threads: an event generated by any thread other than the
> + one that set nowayout or open the watchdog the last time.
> + - open: a thread opens the watchdog to manipulate it;
> + - close: a thread closes the watchdog;
> + - start: starts the watchdog countdown;
> + - stop: stops the watchdog;
> + - set_safe_timeout: configures the watchdog with a given timeout;
> + - ping: resets the watchdog countdown with the previously configured timeout;
> + - nowayout: prevents the watchdog to be stopped until the system's shutdown;
> + - sched_keep_alive: schedules a kernel worker to ping the watchdog if the
> + timeout is longer than the watchdog hardware can handle.
> + - keep_alive: executes the previously scheduled watchdog ping;
> +
> +Noting that the events that does not appear in the automata models are
> +considered blocked events, and their execution will always cause the
> +RV monitor to react to an unexpected event.
> +
> +RV monitor specification
> +------------------------
> +
> +The monitor's goal is to assess a set of specifications that conducts the
> +system to a safe state.
> +
> +These specifications are:
> +
> + - 1: Once open, only one process manipulates the watchdog;
> + - 2: Following 1, the keep-alive mechanisms will not be used;
> + - 3: If required, nowayout will be set before opening the watchdog;
> + - 4: A safe timeout must be set;
> + - 5: At least one ping must be made before entering the safe/safe_nwo states
> + - 6: The RV monitor does not react if the watchdog is closed without stopping.
> + But the hardware watchdog is expected to react.
> +
> +Deterministic automata monitors
> +-------------------------------
> +
> +Following the specifications, a deterministic automata monitor
> +was developed. The monitor is modeled as Deterministic Automata model.
> +
> +The deterministic automata model for safe_wtd is::
> +
> + #==================================# other_threads
> + H H ----------------+
> + -----------> H init H |
> + H H <---------------+
> + #==================================#
> + | | ^
> + | | | close
> + | | +----------------------------------------------------+
> + | | |
> + | | open |
> + | +------------------------------------------------------+ |
> + | | |
> + | nowayout | |
> + v | |
> + nowayout +-------------------+ | |
> + other_threads | | nowayout | |
> + +---------------- | nwo |<-------------------------------------+ | |
> + | | | | | |
> + +---------------> | | <+ | | |
> + +-------------------+ | | | |
> + | | | | |
> + | open | close | | |
> + v | | | |
> + +-------------------+ | | | |
> + | opened_nwo | -+ | | |
> + +-------------------+ | | |
> + | | | |
> + | start | | |
> + v | | |
> + +-------------------+ | | |
> + +---------------> | started_nwo | -+ | | |
> + | +-------------------+ | | | |
> + | | | | | |
> + | open | set_safe_timeout | | | |
> + | v | | | |
> + | +-------------------+ | | | |
> + | | set_nwo | | | | |
> + | +-------------------+ | | | |
> + | | | | | |
> + | +-------------+ | ping | | | |
> + | | | | | | | |
> + | | ping v v | | | |
> + | | +-------------------+ | | | |
> + | +-----------| safe_nwo | | | | |
> + | +-------------------+ | | | |
> + | | | | | |
> + | | close | close | | |
> + | v v | | |
> + | +----------------------------------+ nowayout | | |
> + | | | other_threads | | |
> + | | closed_running_nwo | ----------------+ | | |
> + | | | | | | |
> + +---------------- | | <---------------+ | | |
> + +----------------------------------+ | | |
> + | nowayout ^ | | |
> + +-----------------------------+ | | |
> + | | |
> + | | |
> + +-------------------+ +--------+ | | |
> + | | | |------+---+ |
> + | started | start | opened | | |
> + +---------------- | | <-------- | |>-----+-------+
> + | +-------------------+ +--------+ | ^
> + | | | |
> + | | set_safe_timeout +-------------+-------+
> + | v | |
> + | +-------------------+ | |
> + | | | | |
> + | | set | | |
> + +----------+---------------> | | | |
> + | | +-------------------+ | |
> + | | | | |
> + | | | ping | |
> + | | v | |
> + | | +-------------------+ ping | |
> + | | | | -------+ | |
> + | | +---- | safe | | | |
> + | | | | | <------+ | |
> + | | | +-------------------+ | |
> + | | | | | |
> + | | stop | | stop | |
> + | | | v | |
> + | | | +-------------------+ close | |
> + | +-----------+---> | stopped |-------------+ |
> + | | +-------------------+ |
> + | +---+ |
> + | | close |
> + | v |
> + | other_threads +----------------------------------------+ |
> + | +--------------> | | |
> + | | | closed_running | |
> + | +--------------- | |--------------+
> + | +----------------------------------------+
> + | | ^
> + | open | | close
> + | v |
> + | set_safe_timeout +-------------------+
> + +-------------------------> | reopened |
> + +-------------------+
So I must check the model matrix in patch18 and the above graph to
check if the matrix have the not right value or something in this
graph go wrong.
open
o init state ------> opened state: there lack a direction arrow.
nwo
o closed_running state -------> closed_running_nwo state: this
is the state trasfer indicated from matrix, but the above
graph is not consistent with it. In graph:
nwo
closed_running state -------> nwo state. I prefer the state
closed_running_nwo.
nwo
other_thread
o closed_running_nwo state ---------------> closed_running_nwo state.
The graph above have a duplicate nwo event leading to state transfer.
open
closed_running_nwo state ---------------> started_nwo state. I think
it should transfer to opened_nwo state.
set_safe_timeout
o reopened state ------------------> set state: the direction is from
reopened state to set state. The graph above have two direction arrow.
stop
reopenped state ------------------> opened state. why stop event trigger
it to opened state not stoped state. I think it should transfer to stoped
state like the started state do.
o started state do not have link to closed_running state by close event in
graph. Like started_nwo state do, it should have a direct close event to
link to closed_running state.
Modified the above graph like this:
+
+ #==================================# other_threads
+ H H ----------------+
+ -----------> H init H |
+ H H <---------------+
+ #==================================#
+ | | ^
+ | | | close
+ | | +----------------------------------------------------+
+ | | |
+ | | open |
+ | +------------------------------------------------------+ |
+ | | |
+ | nowayout | |
+ v | |
+ nowayout +-------------------+ | |
+ other_threads | | | |
+ +---------------- | nwo | | |
+ | | | | |
+ +---------------> | | <+ | |
+ +-------------------+ | | |
+ | | | |
+ | open | close | |
+ v | | |
+ +-------------------+ | | |
+ +---------------> | opened_nwo | -+ | |
+ | +-------------------+ | |
+ | | | |
+ | | start | |
+ | v | |
+ | +-------------------+ | |
+ | | started_nwo | -+ | |
+ | +-------------------+ | | |
+ | | | | |
+ | open | set_safe_timeout | | |
+ | v | | |
+ | +-------------------+ | | |
+ | | set_nwo | | | |
+ | +-------------------+ | | |
+ | | | | |
+ | +-------------+ | ping | | |
+ | | | | | | |
+ | | ping v v | | |
+ | | +-------------------+ | | |
+ | +-----------| safe_nwo | | | |
+ | +-------------------+ | | |
+ | | | | |
+ | | close | close | |
+ | v v | |
+ | +----------------------------------+ nowayout | |
+ | | | other_threads | |
+ | | closed_running_nwo | ----------------+ | |
+ | | | | | |
+ +---------------- | | <---------------+ | |
+ +----------------------------------+ | |
+ ^ | |
+ | nowayout | |
+ +--------------------------------------+ | |
+ | | |
+ +-------------------+ +--------+ | | |
+ | | start | |<----+---+ |
+ | started | <--------- | opened | | |
+ +---------------- | | ---------+ | |>----+-------+
+ | +-------------------+ close | +--------+ | ^
+ | | | | |
+ | | set_safe_timeout | +-----------+-------+
+ | v | | |
+ | +-------------------+ | | |
+ | | | | | |
+ | | set | | | |
+ +----------+---------------> | | | | |
+ | | +-------------------+ | | |
+ | | | | | |
+ | | | ping | | |
+ | | v | | |
+ | | +-------------------+ ping | | |
+ | | | | -------+ | | |
+ | | +---- | safe | | | | |
+ | | | | | <------+ | | |
+ | | | +-------------------+ | | |
+ | | | | | | |
+ | | stop | | stop | | |
+ | | | v | | |
+ | | | +-------------------+ close | | |
+ | +-----------+---> | stopped |----------+----+ |
+ | | +-------------------+ | |
+ | +---+ ^ | |
+ | | close | | |
+ | | +------------------+------+ |
| v v | |
+ | other_threads +----------------------------------------+ | |
+ | +--------------> | | | |
+ | | | closed_running | | |
+ | +--------------- | |----+---------+
+ | +----------------------------------------+ |
+ | | ^ |
+ | open | | close |stop
+ | v | |
+ | set_safe_timeout +-------------------+ |
+ +-------------------------- | reopened |------------------+
+ +-------------------+
Thanks
> +It is important to note that the events sched_keep_alive and keep_alive
> +are not allowed in the monitor (they are said to be blocked events).
> +The execution of any blocked events leads the RV monitor to react.
> +
> +Additional options
> +------------------
> +
> +The RV monitor also has a set of options enabled via kernel command
> +line/module options. They are:
> +
> + - watchdog_id: the device id to monitor (default 0);
> + - dont_stop: once enabled, do not allow the RV monitor to be stopped (default off);
> + - safe_timeout: define a maximum safe value that a user-space application can
> + set as the watchdog timeout (default unlimited);
> + - check_timeout: After every ping, check if the time left in the watchdog is less
> + than or equal to the last timeout set for the watchdog. It only works for watchdog
> + devices that provide the get_timeleft() function (default off);
> --
> 2.35.1
>
On 6/28/22 20:16, Steven Rostedt wrote:
> On Thu, 16 Jun 2022 10:44:48 +0200
> Daniel Bristot de Oliveira <[email protected]> wrote:
>
>> + def get_minimun_type(self):
>> + min_type="char"
>> +
>> + if self.states.__len__() > 255:
>> + min_type="short"
>> +
>> + if self.states.__len__() > 65535:
>> + min_type="int"
> Should these be "unsigned"? As char goes from -128 <-> 127
> and short goes from -32768 <-> 32767
>
> And are you sure you're not going to have more than 2,147,483,647 states ;-)
> (or 4,294,967,296 if it's unsigned).
Fixed! now I am using the "state_max" as the invalid state, so I can use unsigned.
I also revisited all python code for consistency.
-- Daniel
On 6/17/22 01:55, Guenter Roeck wrote:
>>
>> ack! I will change it. (I am seeing unsigned int, am I missing something?).
>
> Yes, you are correct.
Fixed!
-- Daniel
On 7/7/22 14:41, Tao Zhou wrote:
> So I must check the model matrix in patch18 and the above graph to
> check if the matrix have the not right value or something in this
> graph go wrong.
It was my fault, the ASCII art generated by graph-easy was too wide, so I had to manually
change it... and so I broke it.
At least this validates that it is better to have it automatically generated :-)
Thanks for reviewing it Tao, I do appreciate these kind of reviews!!!!
-- Daniel
On 7/6/22 20:35, Tao Zhou wrote:
> On Thu, Jun 16, 2022 at 10:44:45AM +0200, Daniel Bristot de Oliveira wrote:
>
>> 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
>> surce code representation that to be used for monitoring.
>>
>> This header file implements helper functions to facilitate the usage
>> of the C output from dot2c for monitoring.
>>
>> Cc: Wim Van Sebroeck <[email protected]>
>> Cc: Guenter Roeck <[email protected]>
>> Cc: Jonathan Corbet <[email protected]>
>> Cc: Steven Rostedt <[email protected]>
>> Cc: Ingo Molnar <[email protected]>
>> Cc: Thomas Gleixner <[email protected]>
>> Cc: Peter Zijlstra <[email protected]>
>> Cc: Will Deacon <[email protected]>
>> Cc: Catalin Marinas <[email protected]>
>> Cc: Marco Elver <[email protected]>
>> Cc: Dmitry Vyukov <[email protected]>
>> Cc: "Paul E. McKenney" <[email protected]>
>> Cc: Shuah Khan <[email protected]>
>> Cc: Gabriele Paoloni <[email protected]>
>> Cc: Juri Lelli <[email protected]>
>> Cc: Clark Williams <[email protected]>
>> Cc: [email protected]
>> Cc: [email protected]
>> Cc: [email protected]
>> Signed-off-by: Daniel Bristot de Oliveira <[email protected]>
>> ---
>> include/rv/automata.h | 49 +++++++++++++++++++++++++++++++++++++++++++
>> 1 file changed, 49 insertions(+)
>> create mode 100644 include/rv/automata.h
>>
>> diff --git a/include/rv/automata.h b/include/rv/automata.h
>> new file mode 100644
>> index 000000000000..0c0aa54bd820
>> --- /dev/null
>> +++ b/include/rv/automata.h
>> @@ -0,0 +1,49 @@
>> +/* SPDX-License-Identifier: GPL-2.0 */
>> +/*
>> + * Deterministic automata helper functions, to be used with the automata
>> + * models in C generated by the dot2k tool.
>> + *
>> + * Copyright (C) 2019-2022 Daniel Bristot de Oliveira <[email protected]>
>> + */
>> +
>> +#define DECLARE_AUTOMATA_HELPERS(name, type) \
>> + \
>> +static inline void *model_get_model_##name(void) \
>> +{ \
>> + return (void *) &automaton_##name; \
>> +} \
>> + \
>> +static char *model_get_state_name_##name(enum states_##name state) \
>> +{ \
>> + return automaton_##name.state_names[state]; \
>> +} \
>> + \
>> +static char *model_get_event_name_##name(enum events_##name event) \
>> +{ \
>> + return automaton_##name.event_names[event]; \
>> +} \
>> + \
>> +static inline type model_get_init_state_##name(void) \
>> +{ \
>> + return automaton_##name.initial_state; \
>> +} \
>> + \
>> +static inline type model_get_next_state_##name(enum states_##name curr_state, \
>> + enum events_##name event) \
>> +{ \
>> + if ((curr_state < 0) || (curr_state > state_max_##name)) \
>> + return -1; \
>
> curr_state can not be state_max_xxx. curr_state must be not bigger
> than state_max_xxx. Or am I miss something?
>
>> + if ((event < 0) || (event > event_max_##name)) \
>> + return -1; \
>> + \
>
> Same here for the event boundary check.
>
>> + return automaton_##name.function[curr_state][event]; \
>> +} \
>> + \
>> +static inline bool model_is_final_state_##name(enum states_##name state) \
>> +{ \
>> + if ((state < 0) || (state > state_max_##name)) \
>> + return 0; \
>> + \
>
> Same here.
>
>> + return !!automaton_##name.final_states[state]; \
>
> If the value of .final_states[state] is 0 or 1, can the type of
> .final_states[state] be befined to bool. Or not need to use !! to
> explicitly transfer the type to bool. I remember that you define
> this as char array and the matrix model value of this array is 0 or 1
> see from the next patche. 1 delegate the state it is the initial state.
> 0 for others.
All points addressed!
-- Daniel
On 6/16/22 23:03, Randy Dunlap wrote:
>> Enables the printk reactor. The printk reactor emmits a printk()
> emits
>
Fixed all the cases!
-- Daniel