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: <aKRAeOakjiwmgML_@jlelli-thinkpadt14gen4.remote.csb>
Date: Tue, 19 Aug 2025 11:14:32 +0200
From: Juri Lelli <juri.lelli@...hat.com>
To: Gabriele Monaco <gmonaco@...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 19/08/25 10:53, Juri Lelli wrote:
> Hi!
> 
> On 14/08/25 17:08, Gabriele Monaco wrote:

...

> > +  static bool verify_constraint(enum states curr_state, enum events event,
> > +				 enum states next_state)
> > +  {
> > +	bool res = true;
> > +
> > +	/* Validate guards as part of f */
> > +	if (curr_state == enqueued && event == sched_switch_in)
> > +		res = get_env(clk) < threshold;
> > +	else if (curr_state == dequeued && event == sched_wakeup)
> > +		reset_env(clk);
> > +
> > +	/* Validate invariants in i */
> > +	if (next_state == curr_state)
> > +		return res;
> > +	if (next_state == enqueued && res)
> > +		start_timer(clk, threshold);
> 
> So, then the timer callback checks the invariant and possibly reports
> failure?

Ah, OK. The 'standard' ha_monitor_timer_callback just reports failure
(react) in case the timer fires. Which makes sense as at that point the
invariant is broken. Maybe add some wording to highlight this?