All of lore.kernel.org
 help / color / mirror / Atom feed
From: Daniel Bristot de Oliveira <bristot@kernel.org>
To: Steven Rostedt <rostedt@goodmis.org>, Guenter Roeck <linux@roeck-us.net>
Cc: Gabriele Paoloni <gpaoloni@redhat.com>,
	Wim Van Sebroeck <wim@linux-watchdog.org>,
	Jonathan Corbet <corbet@lwn.net>, Ingo Molnar <mingo@redhat.com>,
	Thomas Gleixner <tglx@linutronix.de>,
	Peter Zijlstra <peterz@infradead.org>,
	Will Deacon <will@kernel.org>,
	Catalin Marinas <catalin.marinas@arm.com>,
	Marco Elver <elver@google.com>,
	Dmitry Vyukov <dvyukov@google.com>,
	"Paul E. McKenney" <paulmck@kernel.org>,
	Shuah Khan <skhan@linuxfoundation.org>,
	Juri Lelli <juri.lelli@redhat.com>,
	Clark Williams <williams@redhat.com>,
	"open list:DOCUMENTATION" <linux-doc@vger.kernel.org>,
	Linux Kernel Mailing List <linux-kernel@vger.kernel.org>,
	linux-trace-devel@vger.kernel.org
Subject: Re: [PATCH V4 18/20] rv/monitor: Add safe watchdog monitor
Date: Mon, 4 Jul 2022 14:41:43 +0200	[thread overview]
Message-ID: <fe1c0bd0-303b-6758-a6fd-2eb5eeb5c0b8@kernel.org> (raw)
In-Reply-To: <20220701113851.3167403e@gandalf.local.home>

On 7/1/22 17:38, Steven Rostedt wrote:
> On Fri, 1 Jul 2022 07:45:50 -0700
> Guenter Roeck <linux@roeck-us.net> wrote:
> 
>>> Do not confuse this with static analyzers or other general purpose tooling
>>> to find bugs. This is not the purpose of the run time verify. It is just to
>>> prove that certain use cases will perform as expected, given a limited
>>> input.
>>>   
>>
>> ... this is, unfortunately, not explained in the patch. I would have much less
>> of a problem with the series if those details were included.
> 
> It's one of those cases where developers get so involved in their code that
> they leave out the things that are so obvious to them, but not obvious to
> others ;-)

I agree that the main point here is that the documentation [patch 20/20] needs
to be extended and correctly linked to the code.

The goal of the model is to specify the minimum but obligatory steps to set a
watchdog (start, set a safe timeout, ping...) so it can be used by
"safety/heath" monitors in safety-critical systems.

Another goal is to reduce the amount of code/dependencies that will require
deeper inspections to qualify the subsystem for usage in a given context via
monitoring (as steven mentioned - more about it here [1]), without having to
reduce the generic subsystem.

Although the method allows one to create a complete model of the watchdog device
layer, covering all use cases, that is not the idea of this monitor. Moreover, a
full model would not be the adequate model for this specific (but relevant) case
raised and discussed in the Elisa workgroup [2].

The goal of the monitor (that uses the model) is to verify that the interaction
between the watchdog device layer and the "safety/heath" monitors follows this
established model, at runtime.

> My new saying is: "We work in a field where the obvious seldom is".
> 
> Hmm, I think I'll go tweet that :-)

/me liked the tweet... and yep, you clarified well the context in which this is
being applied.

>>
>> Not that I would mind such a verifier, if it was possible to define one,
>> but it would have to be tested with a large number of watchdog drivers
>> to ensure that it addresses all use cases, or at least with a substantial
>> percentage of use cases. It would also require that the state machine is
>> readable to give people a chance to fix it if turns out to be broken.

The patch 20/20 has the automaton in the ASCII art format. Both C and ASCII
models were extracted from the same .dot file. I am not including the .dot file
because there was a previous discussion with the doc people that prefer the
ASCII format in the documentation. But I can add as well, not linked with the
rst file. By reading the model in the ASCII format, it is possible to see that
it is broad enough to cover many watchdogs as it uses simple/generic operations.

The model (the .h) and the instrumentation (the .c) can be updated at any time.
I am adding the tooling to facilitate that, like [patch 06/20].

Patch 19/20 adds a safety application that enables the RV monitor, uses the
watchdog, and collects feedback from the monitor to see if the requested actions
are occurring in the model - and it can be used to test the RV monitor with
any watchdog.

The goal is the one I described above, so an exception generated by this monitor
needs to be read accordingly: it does not imply that a watchdog driver is
broken. It means the interaction between the safety/health monitor and the
watchdog is not following specifications and must be checked at the development
phase, or that something went really wrong at runtime phase.

I will add that to the documentation and emphasize the context of this monitor.

>> It would also have to be robust, meaning it would have to reject invalid
>> (unsupported) settings from the start and not only during runtime.
> 
> I would agree than any module would need to state up front exactly what it
> is modeling. In safety critical systems, all the components that are used
> are defined up front. Not sure if we can have the model not load if the
> required drivers to test are not loaded or ones not part of the model are
> (Daniel?).

I can add a check in the time in which the model is being enabled. But for this
specific case, removing that part might be better and adding it later if it
becomes fundamental.

In practice, selecting a watchdog device can assume that the get_timeleft
implementation is a requirement - so that option was just an additional check.

[1] This is one use case for the broader goal of the strategy discussed here:
https://www.youtube.com/watch?v=DkiwkAKOXNs

[2] https://www.youtube.com/watch?v=qFSYlCbHCYk
> Anyway, thanks for the feedback.
> 
> -- Steve


  reply	other threads:[~2022-07-04 12:41 UTC|newest]

Thread overview: 82+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-06-16  8:44 [PATCH V4 00/20] The Runtime Verification (RV) interface Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 01/20] rv: Add " Daniel Bristot de Oliveira
2022-06-23 17:21   ` Punit Agrawal
2022-07-01 13:24     ` Daniel Bristot de Oliveira
2022-06-23 20:26   ` Steven Rostedt
2022-07-04 19:49     ` Daniel Bristot de Oliveira
2022-07-06 17:49   ` Tao Zhou
2022-07-06 17:53     ` Matthew Wilcox
2022-07-08 15:36       ` Tao Zhou
2022-07-08 15:55         ` Matthew Wilcox
2022-07-08 14:39     ` Daniel Bristot de Oliveira
2022-07-10 15:11       ` Tao Zhou
2022-07-10 15:42         ` Steven Rostedt
2022-07-10 22:28           ` Tao Zhou
2022-06-16  8:44 ` [PATCH V4 02/20] rv: Add runtime reactors interface Daniel Bristot de Oliveira
2022-06-23 20:40   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 03/20] rv/include: Add helper functions for deterministic automata Daniel Bristot de Oliveira
2022-06-28 17:48   ` Steven Rostedt
2022-07-06 18:35   ` Tao Zhou
2022-07-13 18:38     ` Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 04/20] rv/include: Add deterministic automata monitor definition via C macros Daniel Bristot de Oliveira
2022-07-06 18:56   ` Tao Zhou
2022-07-13 18:39     ` Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 05/20] rv/include: Add instrumentation helper functions Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 06/20] tools/rv: Add dot2c Daniel Bristot de Oliveira
2022-06-28 18:10   ` Steven Rostedt
2022-06-28 18:16   ` Steven Rostedt
2022-07-13 18:41     ` Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 07/20] tools/rv: Add dot2k Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 08/20] rv/monitor: Add the wip monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-06-28 19:02   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 09/20] rv/monitor: wip instrumentation and Makefile/Kconfig entries Daniel Bristot de Oliveira
2022-06-16 11:21   ` kernel test robot
2022-06-16 21:00   ` Randy Dunlap
2022-06-17 16:07     ` Daniel Bristot de Oliveira
2022-06-28 19:02     ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 10/20] rv/monitor: Add the wwnr monitor skeleton created by dot2k Daniel Bristot de Oliveira
2022-07-06 20:08   ` Tao Zhou
2022-06-16  8:44 ` [PATCH V4 11/20] rv/monitor: wwnr instrumentation and Makefile/Kconfig entries Daniel Bristot de Oliveira
2022-06-16 13:47   ` kernel test robot
2022-06-28 19:05   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 12/20] rv/reactor: Add the printk reactor Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 13/20] rv/reactor: Add the panic reactor Daniel Bristot de Oliveira
2022-06-16 15:20   ` kernel test robot
2022-06-16 21:03   ` Randy Dunlap
2022-06-17 16:09     ` Daniel Bristot de Oliveira
2022-07-13 18:47     ` Daniel Bristot de Oliveira
2022-06-28 19:06   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 14/20] Documentation/rv: Add a basic documentation Daniel Bristot de Oliveira
2022-06-29  3:35   ` Bagas Sanjaya
2022-07-13 19:30     ` Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 15/20] Documentation/rv: Add deterministic automata monitor synthesis documentation Daniel Bristot de Oliveira
2022-06-28 19:09   ` Steven Rostedt
2022-06-16  8:44 ` [PATCH V4 16/20] Documentation/rv: Add deterministic automata instrumentation documentation Daniel Bristot de Oliveira
2022-06-16  8:44 ` [PATCH V4 17/20] watchdog/dev: Add tracepoints Daniel Bristot de Oliveira
2022-06-16 13:44   ` Guenter Roeck
2022-06-16 15:47     ` Daniel Bristot de Oliveira
2022-06-16 23:55       ` Guenter Roeck
2022-06-17 16:16         ` Daniel Bristot de Oliveira
2022-07-13 18:49         ` Daniel Bristot de Oliveira
2022-06-16  8:45 ` [PATCH V4 18/20] rv/monitor: Add safe watchdog monitor Daniel Bristot de Oliveira
2022-06-16 13:36   ` Guenter Roeck
2022-06-16 15:29     ` Daniel Bristot de Oliveira
     [not found]       ` <CA+wEVJbvcMZbCroO2_rdVxLvYkUo-ePxCwsp5vbDpoqys4HGWQ@mail.gmail.com>
2022-06-16 23:53         ` Guenter Roeck
2022-06-17 17:06           ` Daniel Bristot de Oliveira
2022-06-28 19:32           ` Steven Rostedt
2022-07-01 14:45             ` Guenter Roeck
2022-07-01 15:38               ` Steven Rostedt
2022-07-04 12:41                 ` Daniel Bristot de Oliveira [this message]
2022-06-16 20:57   ` Randy Dunlap
2022-06-17 16:17     ` Daniel Bristot de Oliveira
2022-07-13 19:13   ` Daniel Bristot de Oliveira
2022-06-16  8:45 ` [PATCH V4 19/20] rv/safety_app: Add a safety_app sample Daniel Bristot de Oliveira
2022-06-16  8:45 ` [PATCH V4 20/20] Documentation/rv: Add watchdog-monitor documentation Daniel Bristot de Oliveira
2022-07-07 12:41   ` Tao Zhou
2022-07-13 18:51     ` Daniel Bristot de Oliveira
2022-06-22  7:24 ` [PATCH V4 00/20] The Runtime Verification (RV) interface Song Liu
2022-06-23 16:41   ` Daniel Bristot de Oliveira
2022-06-23 17:52     ` Song Liu
2022-06-23 20:29       ` Daniel Bristot de Oliveira
2022-06-23 21:10         ` Song Liu
2022-07-06 16:18 ` Tao Zhou

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=fe1c0bd0-303b-6758-a6fd-2eb5eeb5c0b8@kernel.org \
    --to=bristot@kernel.org \
    --cc=catalin.marinas@arm.com \
    --cc=corbet@lwn.net \
    --cc=dvyukov@google.com \
    --cc=elver@google.com \
    --cc=gpaoloni@redhat.com \
    --cc=juri.lelli@redhat.com \
    --cc=linux-doc@vger.kernel.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=linux-trace-devel@vger.kernel.org \
    --cc=linux@roeck-us.net \
    --cc=mingo@redhat.com \
    --cc=paulmck@kernel.org \
    --cc=peterz@infradead.org \
    --cc=rostedt@goodmis.org \
    --cc=skhan@linuxfoundation.org \
    --cc=tglx@linutronix.de \
    --cc=will@kernel.org \
    --cc=williams@redhat.com \
    --cc=wim@linux-watchdog.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.