From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.133.124]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id A457F3218B3 for ; Mon, 2 Mar 2026 13:58:56 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1772459937; cv=none; b=mpDKa/i9OpDdej011cquwbygC+UBGs4enM5Gj+QHSdMS1rDP1BCzW374kWEiYq3UBHOgutl0HqiawK3McdzQp7/RMiPS5K74+lm14GVMIjh34Pyalma29u+d+Dhfat0pqsmrEmO4FMNQQ9LSB6eMxCeUlZ5GoBckQEX49oOoXt4= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1772459937; c=relaxed/simple; bh=Vup7WS03UeljBKAxRmSAsILBwKizCecVYLzL7awCpkM=; h=Date:From:To:Cc:Subject:Message-ID:References:MIME-Version: Content-Type:Content-Disposition:In-Reply-To; b=r+yquPSB/0T0Spi3PSY8s5A/7T2BKFlZOV/EMSwt+V1l43FCuO+ycB899ZpCdrj0BZ+lwZ49cdoqrpZyT3i4RKo/ylrAsTjcu+vUko8+TnlI5F+MHV0el4yzFNa0eBp8Xmex0/yUzHBPzHDXi2e1leI134VewZ+XWb43fXMJ1Go= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=eEiotC7w; dkim=pass (2048-bit key) header.d=redhat.com header.i=@redhat.com header.b=MXyCYiJu; arc=none smtp.client-ip=170.10.133.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="eEiotC7w"; dkim=pass (2048-bit key) header.d=redhat.com header.i=@redhat.com header.b="MXyCYiJu" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1772459935; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: in-reply-to:in-reply-to:references:references; bh=CeiEMsIq1M19XQRSyjWmM83RqV4mUxb0zPC+IH30st0=; b=eEiotC7wfFzjJbW1Y5TBOdB33O4nFfgUnCYxjFkEZlOGuep/LAEa1olVZeHfprsoJC+Xy7 t2pCUeE0YOH2WE5gxhfqkyeMs63eWRQvWcbQ9BexPnrAO7hpwkzxqHsEbba3YI9a6akQQq y+hOhZHBad9TfiWYcbiG8+IkrJ0rhBI= Received: from mail-wm1-f72.google.com (mail-wm1-f72.google.com [209.85.128.72]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-696-cV12520HON6TmykPKwGa-g-1; Mon, 02 Mar 2026 08:58:52 -0500 X-MC-Unique: cV12520HON6TmykPKwGa-g-1 X-Mimecast-MFC-AGG-ID: cV12520HON6TmykPKwGa-g_1772459931 Received: by mail-wm1-f72.google.com with SMTP id 5b1f17b1804b1-483a2db68caso37312105e9.0 for ; Mon, 02 Mar 2026 05:58:52 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=google; t=1772459931; x=1773064731; darn=vger.kernel.org; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:cc:to:from:date:from:to:cc:subject:date:message-id:reply-to; bh=CeiEMsIq1M19XQRSyjWmM83RqV4mUxb0zPC+IH30st0=; b=MXyCYiJuisC0xm0wWSBdSxiNqio3QlV3ikuoGDtUoDqzmJSlRGmeDC5nrljnccLDR1 OCwS/iyKX93qfIHMCM5ev1GJXd7YJ/nH9XtVwghsY/uFyyxwQkUp/moqI0n6GMjDrZZo t1gnxmFv6hxzAlmzkkAR2M9Wi8n5WsjNze7ZAF3/CYWDgsRMN2e84/Raw7jj/xiE7XVy hkN8qcsYb8lg99PtF2uwGljwdiTkhHk8W48UIt/h/fXWLVVMmwse+yNEQGzuvbZwvGH4 hgC5A6W+V0TocVAq8xWDBlLOJBfkdcBPqyOxMtLco7hIHGi1dSytV3+WLXtCO7ehZiXh mXtg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1772459931; x=1773064731; h=in-reply-to:content-disposition:mime-version:references:message-id :subject:cc:to:from:date:x-gm-gg:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=CeiEMsIq1M19XQRSyjWmM83RqV4mUxb0zPC+IH30st0=; b=cGMAwnbQ6bbwvDUXn0soMLkfWSjd7xBWojjRc+LR82pm1fegxfvCc/ShDym68Vkupl zYpiE0WNJwGWe6w5dCgt5avOm4YqJ58UtXLUo1uLOhSi2PZ0Pf9IWBlamuMNnT571g7s 5Js2obovOrnhGP6+afIB04AVcpWLQXZ4dU9lgjHZWagorguJ8MCjLOEApxF587nod5fS mnn/SvsQJNuAdlGYqh/hdB1yCivZvzWLhAfAHtgYl6RQluoxOvrvXyMwFODxjQKOGAg9 JRuoZWTx9KWmfh+0QiSmG/1IkvrIDM0s9jcmqf4w2O5gKMib/LIZi0inTvmLZ9ooQZ8l lNig== X-Gm-Message-State: AOJu0YyVFOHtStQLQmWFDiNmChH4A/m5h2unRYmALeMvdSF8/k2W7dRs LOQvi8Od1ieJgIldGRUKCf45iBbwq7gziazpRDgw8lOJRq4su1dmRdWRH2sZBxl8is9AkTARKoN fkH7wVq07d4uiIPaQoRyCgOGd2r9mgs+9m30tIuCDpCryPSHR7Axr0ciXpUkcytRBQw== X-Gm-Gg: ATEYQzws3B1j3JhYefJzjyYh2pdh4M+b4DzMb7Gga3bDwnZR6dFrOpwLKEvYfAzfDtQ cGSRNfjZY0mP5jaX9DUIXoIA69Rbt5uysn4GG10uz+01DSlkwSZHX7dkZMtngSPLHccbAZnbtTp MV/ZTypjOXrUDym56qyzVPQw5mEXWg/Q8cD2FjX1FxIHykMFvd148clS125/BbS2Z/VI51f0s81 NOvMBjORARgPNwx3v5C6PiI7cJrdOdZsdVqo6l54UUSdI4btZ1uLgDpe7xik5DADFrZ6VG71ITX K8WSJ2/G6S81wBGOb2ejPF2S/0hsNE2wl9oDvpYdUPQPUEm4p26Q5I6CFACXP8KFGUhvcNMeOTq wxAb+4R5LIdZydVPxa4hzDOEI8MgcJnnaTUo9Li3WC3x2VEKJXhU= X-Received: by 2002:a05:600c:4f11:b0:477:7925:f7fb with SMTP id 5b1f17b1804b1-483c9babeaamr234251725e9.10.1772459931333; Mon, 02 Mar 2026 05:58:51 -0800 (PST) X-Received: by 2002:a05:600c:4f11:b0:477:7925:f7fb with SMTP id 5b1f17b1804b1-483c9babeaamr234251295e9.10.1772459930831; Mon, 02 Mar 2026 05:58:50 -0800 (PST) Received: from jlelli-thinkpadt14gen4.remote.csb ([151.29.73.19]) by smtp.gmail.com with ESMTPSA id ffacd0b85a97d-439b41831easm10784198f8f.12.2026.03.02.05.58.49 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 02 Mar 2026 05:58:50 -0800 (PST) Date: Mon, 2 Mar 2026 14:58:48 +0100 From: Juri Lelli To: Gabriele Monaco Cc: linux-kernel@vger.kernel.org, Steven Rostedt , Nam Cao , Juri Lelli , Jonathan Corbet , linux-trace-kernel@vger.kernel.org, linux-doc@vger.kernel.org, Tomas Glozar , Clark Williams , John Kacur Subject: Re: [PATCH v6 05/16] Documentation/rv: Add documentation about hybrid automata Message-ID: References: <20260225095122.80683-1-gmonaco@redhat.com> <20260225095122.80683-6-gmonaco@redhat.com> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20260225095122.80683-6-gmonaco@redhat.com> Hello, On 25/02/26 10:51, Gabriele Monaco wrote: > Describe theory and implementation of hybrid automata in the dedicated > page hybrid_automata.rst > Include a section on how to integrate a hybrid automaton in > monitor_synthesis.rst > Also remove a hanging $ in deterministic_automata.rst > > Reviewed-by: Nam Cao > Signed-off-by: Gabriele Monaco > --- ... > diff --git a/Documentation/trace/rv/hybrid_automata.rst b/Documentation/trace/rv/hybrid_automata.rst > new file mode 100644 > index 000000000000..39c037a71b89 > --- /dev/null > +++ b/Documentation/trace/rv/hybrid_automata.rst > @@ -0,0 +1,341 @@ > +Hybrid Automata > +=============== ... > +Stall model with invariants (iteration 2) > +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ > + > +The first iteration isn't exactly what was intended, we can change the model as: > + > +- *X* = { ``dequeued``, ``enqueued``, ``running``} > +- *E* = { ``enqueue``, ``dequeue``, ``switch_in``} > +- *V* = { ``clk`` } > +- x\ :subscript:`0` = ``dequeue`` > +- X\ :subscript:`m` = {``dequeue``} > +- *f* = > + - *f*\ (``enqueued``, ``switch_in``) = ``running`` > + - *f*\ (``running``, ``dequeue``) = ``dequeued`` > + - *f*\ (``dequeued``, ``enqueue``, ``reset(clk)``) = ``enqueued`` ^^^ > +- *i* = > + - *i*\ (``enqueued``) = ``clk < threshold`` > + > +Graphically:: > + > + | > + | > + v > + #=========================# > + H dequeued H <+ > + #=========================# | > + | | > + | enqueue; reset(clk) | > + v | > + +-------------------------+ | > + | enqueued | | > + | clk < threshold | | dequeue > + +-------------------------+ | > + | | > + | switch_in | > + v | > + +-------------------------+ | > + | running | -+ > + +-------------------------+ ... > + 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); Considering the spec above, does the 'event' need to be 'enqueue' instead of 'sched_wakeup' (or the other way around)? Or maybe it's equivalent? Thanks, Juri