linux-kernel - Re: [RFC PATCH 11/17] Documentation/rv: Add documentation about hybrid automata

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <cdf1912c57cc49d203aec31c645c1c38e863a0ab.camel@redhat.com>
Date: Tue, 19 Aug 2025 12:40:06 +0200
From: Gabriele Monaco <gmonaco@...hat.com>
To: Juri Lelli <juri.lelli@...hat.com>
Cc: linux-kernel@...r.kernel.org, Steven Rostedt <rostedt@...dmis.org>, 
 Jonathan Corbet	 <corbet@....net>, linux-trace-kernel@...r.kernel.org,
 linux-doc@...r.kernel.org,  Nam Cao <namcao@...utronix.de>, Tomas Glozar
 <tglozar@...hat.com>, Juri Lelli <jlelli@...hat.com>,  Clark Williams
 <williams@...hat.com>, John Kacur <jkacur@...hat.com>
Subject: Re: [RFC PATCH 11/17] Documentation/rv: Add documentation about
 hybrid automata

On Tue, 2025-08-19 at 10:53 +0200, Juri Lelli wrote:
> Hi!
> 
> On 14/08/25 17:08, Gabriele Monaco wrote:
> > 
> > +
> > +Examples
> > +--------
> 
> Maybe add subsection titles to better mark separation between
> different examples?

Sure, makes sense.

> 
> > +The 'wip' (wakeup in preemptive) example introduced as a
> > deterministic automaton
> > +can also be described as:
> > +
> > +- *X* = { ``any_thread_running`` }
> > +- *E* = { ``sched_waking`` }
> > +- *V* = { ``preemptive`` }
> > +- x\ :subscript:`0` = ``any_thread_running``
> > +- X\ :subscript:`m` = {``any_thread_running``}
> > +- *f* =
> > +   - *f*\ (``any_thread_running``, ``sched_waking``,
> > ``preemptive==0``) = ``any_thread_running``
> > +- *i* =
> > +   - *i*\ (``any_thread_running``) = ``true``
> > +
> > +Which can be represented graphically as::
> > +
> > +     |
> > +     |
> > +     v
> > +   #====================#   sched_waking;preemptive==0
> > +   H                    H ------------------------------+
> > +   H any_thread_running H                               |
> > +   H                    H <-----------------------------+
> > +   #====================#
> > +
> > +In this example, by using the preemptive state of the system as an
> > environment
> > +variable, we can assert this constraint on ``sched_waking``
> > without requiring
> > +preemption events (as we would in a deterministic automaton),
> > which can be
> > +useful in case those events are not available or not reliable on
> > the system.
> > +
> > +Since all the invariants in *i* are true, we can omit them from
> > the representation.
> > +
> > +As a sample timed automaton we can define 'stall' as:
> 
> Maybe indicate this first one is a not properly correct example
> (correct version follows)?

Yeah I should definitely be clearer about it. As you've guessed, this
example is to show things can be done differently as a tradeoff with
responsiveness, I should make that explicitly.

Thanks for the comments,
Gabriele