From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 87D1025A32E for ; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475658; cv=none; b=HokVqP2rid9/r74+YRId8jPlWDaO2A0AAk5VM6ehqUKr9UBVnL7rVpp73FWWaYn2yi9S0WtHG+RVMiZNDf9Mb4AtDfL0Ie/jgS5ScYnMgqtFasUclZ4I/O88IGU5yxRvNEahUWwg/9sFq0wHO/Nbcc9zlvbm4ng3xWwCjsH45gw= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475658; c=relaxed/simple; bh=lJAJPMjorckSa1MQsNEN+TaX/8IGzovjdFYDSD0sZwE=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=ck9mma9cXedLHVLIfAaKVXfqkqchATaPUQJQRafDjORhlIAmoAHlHgeQMLATkDkViAPBrE/43+GNmXfkLcyvA/Cdb+cMUcXt6FTBmSgHblmKfBIpzAVnTsqJP0nl4Diygwq5GAi+UI9IjxrluTTN2f2WdAnvrU+I5381NRWHX0o= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=pBzfVGiG; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="pBzfVGiG" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 27815C4CEE7; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475658; bh=lJAJPMjorckSa1MQsNEN+TaX/8IGzovjdFYDSD0sZwE=; h=Date:From:To:Cc:Subject:References:From; b=pBzfVGiGNB0nILUaeuCTqQXD5cRLnDwGRWYE0enal5hCs0mxN/r7bXqhoGrCgOfzF g0NMl45Mmxnm7PqDm6VoaA4ef+43lN0yMwj18zuqTteAhXpi0NkUgbsz4yhBhy8HyF t8jYfQ61fmhPpn9V3dzyVTknO01dnR+tT6eBN8/SWtWrbZ/WEg+fV7zUvjkQY09TfT qNjQiqD+3ZgeQ5Ph+Sz8h9+T7Kr+XvdlAC7dV4+aMJIvCYS/lwEOdpuM6z9VovghAs so5wwvsnzjt95OhbZJdLBYQYJ8PT5WdmVwMKhGZSDlaJtPQ/AtYIAuuVSchbL/DmCg a2x31dBqIfwPA== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Y-00000001QcN-14vN; Fri, 25 Jul 2025 16:34:24 -0400 Message-ID: <20250725203424.107916458@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:33:58 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , John Ogness , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Josh Poimboeuf , Petr Mladek , kernel test robot , "Peter Zijlstra (Intel)" , Nam Cao Subject: [for-next][PATCH 01/25] objtool: Add vpanic() to the noreturn list References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao vpanic() does not return. However, objtool doesn't know this and gets confused: kernel/trace/rv/reactor_panic.o: warning: objtool: rv_panic_reaction(): une= xpected end of section .text Add vpanic() to the list of noreturn functions. Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Cc: Josh Poimboeuf Cc: Petr Mladek Link: https://lore.kernel.org/073f826ebec18b2bb59cba88606cd865d8039fd2.1752= 232374.git.namcao@linutronix.de Reported-by: kernel test robot Closes: https://lore.kernel.org/oe-kbuild-all/202507110826.2ekbVdWZ-lkp@int= el.com/ Acked-by: Peter Zijlstra (Intel) Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/objtool/noreturns.h | 1 + 1 file changed, 1 insertion(+) diff --git a/tools/objtool/noreturns.h b/tools/objtool/noreturns.h index eacfe3b0a8d1..6a922d046b8e 100644 --- a/tools/objtool/noreturns.h +++ b/tools/objtool/noreturns.h @@ -38,6 +38,7 @@ NORETURN(mpt_halt_firmware) NORETURN(mwait_play_dead) NORETURN(nmi_panic_self_stop) NORETURN(panic) +NORETURN(vpanic) NORETURN(panic_smp_self_stop) NORETURN(rest_init) NORETURN(rewind_stack_and_make_dead) --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 B07BA25A352 for ; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475658; cv=none; b=J6b7N59xsSu2dd8Y3pQOxKw5M+ppOdY8S71VzYTMQc3zMlclGXxE1rWE7kFITO78SvImoJpMKmsKl5iIUNh6+C/phCspQqVVor7Bt0ybQPiMz/r6oIxbyBO55iOhX0clpGLlcgENkpxa6khrFXrTVmGQXbgDNCyGB8yQhAerhoQ= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475658; c=relaxed/simple; bh=vLVShok0cMXltuEHQ/ZOFR7qvRYl1xl7zH6FxAy5Phc=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=kJ11BiCE6hRo0jB02FrFgu1RjRo4SIAqhW65/gUrv4lqH8qUBoHVXcLNGu8R+xktHh449HOhYuDKNW7SBgXZfwOM/BnxRDaS215H2Z9jH9S5Qfpi+E5LZjuXdvOkvEILKk4VyZZTIODfst8PuU5Yf3gYZtjn/VWCsjv1+vSPcfE= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=LxDYlbmc; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="LxDYlbmc" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 4D3CDC4CEF8; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475658; bh=vLVShok0cMXltuEHQ/ZOFR7qvRYl1xl7zH6FxAy5Phc=; h=Date:From:To:Cc:Subject:References:From; b=LxDYlbmcM3QpRznRHmDlcxRlkQZDbbvufapeqa7H2jS/kAoeFNBah9kP4mSazIUif KpX3nY433mdLcCLr82Gc3NMbB8xs1tnYBH6Xp2P3oj/Owm3qE/u/EnLIckMat4vUXT /t14/rgpiM8Ng/6z9o36wW+S+fBDIcUgruH9t5VqST5UrxTW4lLEO//COPumN5j5xy ree8/nT4ERhbmHAt/fhT4EQA+CrcutcXr2SWrEN9ND4EUR+4C1uHfaua1ir8Tqf+sL 5HhjS6XwCfwGyDKphiq97oh5LB9uJnRs1iJBzmmULdZNz8RI3javTxMpHJydAHYhli EHsoR3MHhz+Qg== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Y-00000001Qcs-1mjn; Fri, 25 Jul 2025 16:34:24 -0400 Message-ID: <20250725203424.278638879@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:33:59 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , John Ogness , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Josh Poimboeuf , Petr Mladek , Stephen Rothwell , "Peter Zijlstra (Intel)" , Nam Cao Subject: [for-next][PATCH 02/25] panic: Fix up description of vpanic() References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao The description above vpanic() has the wrong function name. Fix it up. Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Cc: Josh Poimboeuf Cc: Petr Mladek Link: https://lore.kernel.org/23a7e8add6546b155371b7e0fbb37bb1def13d6e.1752= 232374.git.namcao@linutronix.de Reported-by: Stephen Rothwell Closes: https://lore.kernel.org/lkml/20250711183802.2d8c124d@canb.auug.org.= au/ Acked-by: Peter Zijlstra (Intel) Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- kernel/panic.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/panic.c b/kernel/panic.c index 6a1823c383d0..2a499facde13 100644 --- a/kernel/panic.c +++ b/kernel/panic.c @@ -307,7 +307,7 @@ static void panic_other_cpus_shutdown(bool crash_kexec) } =20 /** - * panic - halt the system + * vpanic - halt the system * @fmt: The text string to print * @args: Arguments for the format string * --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 ED57F25B1E0 for ; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; cv=none; b=KtrF3X/mMqR5+eqpGUbVZZLd9vUuTz9IVm7auryxgvGENoeWX+hTyKIwhVlxd10mHQjXPV/Nros2rwCDyvRRDyux/q0AedTjqQChThQoXLY1sSB0NoeNYLHXQ+pitIU7f+FSyaANcrTXaUVON0aAx+1WL40CIGfct9J/Os24tLg= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; c=relaxed/simple; bh=HEWgbF62D++gFU89ATiq9jPjAUKcvvzrEkAmBFR1mhY=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=eaEIHVGr4v1qp4gfQAfaUquQ7s2Ple42SA9mQ5et0dDIqrvvXn527TGfJcyeRNIrQbhFVetPRP+nrXLZgNejJsJ+pOSNeo/vDkmvi3NvVbZ3rlXZWckf4x2L/WjwEbVvQd+Qg2YWjM9ntLZ9pOzw1Hmbn+Mzx4hfH8ODUXQ5da4= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=I14vs8kN; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="I14vs8kN" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 86374C4CEFA; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475658; bh=HEWgbF62D++gFU89ATiq9jPjAUKcvvzrEkAmBFR1mhY=; h=Date:From:To:Cc:Subject:References:From; b=I14vs8kNPy2w1Bze3lY9cExYdxXKJaayqRlubpRvXspeAldOMmsr8vrG65OhxrTZt EQS9d2HPUhiPHK5KU6D8Sl2VWuf5cSa/n3sD7G9kHeSfhaLLFSSTB5dTd1kbY1r8Sy wbDgLdQK/YYqRyleCdMa45RxNAiaGiC8lero5eAdurJ6Ma5zQRuNNQyWgwL9apabcL l6sJCwBmE6eRMXZpoL+64vibklSoUnIW9f3E2042X0h6gkdprzCkFAlP5ohaFfLCY/ g4FoQpEHYfzmFZ7AXDqCRvZwVS/EUcPR5SuTeytTdasOK/+Rdo0d7PKy9N64hYbmdb dGZi1FqMpjqBg== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Y-00000001QdM-2TdR; Fri, 25 Jul 2025 16:34:24 -0400 Message-ID: <20250725203424.446385917@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:00 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , John Ogness , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 03/25] rv/ltl: Do not execute the Buchi automaton twice on start condition References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao On start condition of a Buchi automaton, the automaton is executed twice. This is fine for now, as all the current LTL operators do not care about this. But it would break the 'next' operator, which will be introduced in a follow-up patch. Prepare for the introduction of the 'next' operator, only execute the automaton once on start condition. Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/9379f4e7b9c1c69a6dca3e20a22936c850a25ca7.1752= 239482.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/rv/ltl_monitor.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h index 9a583125b566..67031a774e3d 100644 --- a/include/rv/ltl_monitor.h +++ b/include/rv/ltl_monitor.h @@ -167,8 +167,10 @@ static void ltl_atom_update(struct task_struct *task, = enum ltl_atom atom, bool v ltl_atom_set(mon, atom, value); ltl_atoms_fetch(task, mon); =20 - if (!rv_ltl_valid_state(mon)) + if (!rv_ltl_valid_state(mon)) { ltl_attempt_start(task, mon); + return; + } =20 ltl_validate(task, mon); } --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 EBF9525B1CB for ; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; cv=none; b=GSCuqtF8LcljpaEi8rahYV+dshOguDw7+vxE/AQTcQH3fr8LPzjrKnwz9HK4+p8GmFoD3gSsWBFMYsdfjSA8kXFbMIvSYX9+1KxjS7ZomWx+/pQ2+T58UXdzthHGktcKvpOIW2iMp9be9mlt6N5LxlNU4w3ij/QY+YR6IGYyfoU= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; c=relaxed/simple; bh=j7Sci6wUtswBUD7ElKgRRNjyvsKXDwtfKOKLQTwMuEk=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=d683Plzp0ucimHHdFwev7eaRLL/hqvn8z0UB2FlxDl+E/DyDw0W6Npl00W1IACw/mH1U0v973oiZO0vEVfw1eGszDZym66ojTjIMJ6ycoAQCxGmTWB2V22rZqMDZjT0WgAMeADaW/tSA/Qine3P1yjWp5pWsGjljID/ZVc9gWRY= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=T0AT2nNh; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="T0AT2nNh" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 9F69AC4CEFD; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475658; bh=j7Sci6wUtswBUD7ElKgRRNjyvsKXDwtfKOKLQTwMuEk=; h=Date:From:To:Cc:Subject:References:From; b=T0AT2nNhKYf6m6VNM+YdVrh0ybH6amC+EhK6wckSom9Ee0wxNe8ZvTkSiYa8CR8X5 SJ8KfXX1WuFLFNQUthiI9elP4zPs6M5QQhkN1YXl+qClpsMdL24pZVZIiPBxn8RYg5 lb5wlSTXVKI1bJ/1U5vuKOe8RgeT15USCntNnYfUXTYsja4WIcEX4Vn1wjjqx00Q1b HG90v0XyDraeT5NRuzJw1DZ4Jit1Kx6FcE1ryLQljGb5+dzalf4PEX2VgxV8T8t/Xw A9ZJL19eDjYSCC5Aj/zWpxRrt4IMmJTpnSVkM8U4XR9LdzK0aWGayV8YxVngQ/f9mc B6AIhYaIfRB0Q== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Y-00000001Qdq-3BTM; Fri, 25 Jul 2025 16:34:24 -0400 Message-ID: <20250725203424.611163377@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:01 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 04/25] verification/dot2k: Make a separate dot2k_templates/Kconfig_container References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao A generated container's Kconfig has an incorrect line: select DA_MON_EVENTS_IMPLICIT This is due to container generation uses the same template Kconfig file as deterministic automaton monitor. Therefore, make a separate Kconfig template for container which has only the necessaries for container. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/d54fd7ee120785bec5695220e837dbbd6efb30e5.1751= 634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/dot2/dot2k.py | 3 ++- tools/verification/dot2/dot2k_templates/Kconfig_container | 5 +++++ 2 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 tools/verification/dot2/dot2k_templates/Kconfig_contain= er diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot= 2k.py index 745d35a4a379..dd4b5528a4f2 100644 --- a/tools/verification/dot2/dot2k.py +++ b/tools/verification/dot2/dot2k.py @@ -35,6 +35,7 @@ class dot2k(Dot2c): self.states =3D [] self.main_c =3D self.__read_file(self.monitor_templates_dir + = "main_container.c") self.main_h =3D self.__read_file(self.monitor_templates_dir + = "main_container.h") + self.kconfig =3D self.__read_file(self.monitor_templates_dir += "Kconfig_container") else: super().__init__(file_path, extra_params.get("model_name")) =20 @@ -44,7 +45,7 @@ class dot2k(Dot2c): self.monitor_type =3D MonitorType self.main_c =3D self.__read_file(self.monitor_templates_dir + = "main.c") self.trace_h =3D self.__read_file(self.monitor_templates_dir += "trace.h") - self.kconfig =3D self.__read_file(self.monitor_templates_dir + "Kc= onfig") + self.kconfig =3D self.__read_file(self.monitor_templates_dir += "Kconfig") self.enum_suffix =3D "_%s" % self.name self.description =3D extra_params.get("description", self.name) or= "auto-generated" self.auto_patch =3D extra_params.get("auto_patch") diff --git a/tools/verification/dot2/dot2k_templates/Kconfig_container b/to= ols/verification/dot2/dot2k_templates/Kconfig_container new file mode 100644 index 000000000000..a606111949c2 --- /dev/null +++ b/tools/verification/dot2/dot2k_templates/Kconfig_container @@ -0,0 +1,5 @@ +config RV_MON_%%MODEL_NAME_UP%% + depends on RV + bool "%%MODEL_NAME%% monitor" + help + %%DESCRIPTION%% --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 0EB6725B2FA for ; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; cv=none; b=btSYtYCQR1MELErdoeTNCVUMyfMuAmI40gnRTvWwD60U10lq6Y5XND/5yZonzUHCCH/IeG8QH0I9apo4uBcDXZVbuMMvN33o9/CEoRXKrgk3VxtTyC/zqnSA19FBuzFmeZmEYLBq8lfpl6XifV0FKtow6tDgS6GHno+VCArfUes= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; c=relaxed/simple; bh=5GJGshMMt43RPwKYyto06JVmYi0YebWLNetCQjz6aKI=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=fEZtBSZKZUOG6wxFWNOryzDIFhT658ZE3snYRYrzB2k21cz6pVjeO460joYyE40B4KiAxlhVnzFmNkdUhb+19GoC9dJ5cfbOzvHL20xTkOa0L6sQcBgNQCY4VHF2SQL8+FukvdCi8KNyouV3021zTQupd9tHiUbApyvZhfFpCu0= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=jh6oy8pw; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="jh6oy8pw" Received: by smtp.kernel.org (Postfix) with ESMTPSA id D63D6C4CEE7; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475658; bh=5GJGshMMt43RPwKYyto06JVmYi0YebWLNetCQjz6aKI=; h=Date:From:To:Cc:Subject:References:From; b=jh6oy8pwsi2obmuoI/NP9nwIkCyjIMA0xr3l/TDAWTJ0KO5R8x0o74qKZUP/q5F8S sHwm4lykbMJho/sh36s0bFI1f4Sk9XrgJT+oDXXH4/ryN3T311Ln8BbyVgjjJ+rx4l PUEibxpORLlyZ0v8agGdIIE/oHK9z2tdWUwaBvJgz2YKjmpCbAh7FkuG4we8SwmTtw /xaBPVAqJt1aUvn1uEUe8nOzoCswTvJrn8MuLZAMI3LoziaExrSfafcQLFfjKXw5b9 2xtweYySTfGB9wiQQPY1SqfjRiar+AXU6Vwaxqpk7MR7H7QlcjYgr0I1RKJnCwFffs vRDQtjG9hvawA== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Y-00000001QeK-3sKb; Fri, 25 Jul 2025 16:34:24 -0400 Message-ID: <20250725203424.778464609@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:02 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 05/25] verification/dot2k: Remove __buff_to_string() References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao str.join() can do what __buff_to_string() does. Therefore replace __buff_to_string() to make the scripts more pythonic. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/860d6002659f604c743e0f23d5cf3c99ea6a82d8.1751= 634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/dot2/dot2k.py | 21 ++++++--------------- 1 file changed, 6 insertions(+), 15 deletions(-) diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot= 2k.py index dd4b5528a4f2..0922754454b9 100644 --- a/tools/verification/dot2/dot2k.py +++ b/tools/verification/dot2/dot2k.py @@ -109,15 +109,6 @@ class dot2k(Dot2c): fd.close() return content =20 - def __buff_to_string(self, buff): - string =3D "" - - for line in buff: - string =3D string + line + "\n" - - # cut off the last \n - return string[:-1] - def fill_monitor_type(self): return self.monitor_type.upper() =20 @@ -148,19 +139,19 @@ class dot2k(Dot2c): buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, even= t, self.enum_suffix)); buff.append("}") buff.append("") - return self.__buff_to_string(buff) + return '\n'.join(buff) =20 def fill_tracepoint_attach_probe(self): buff =3D [] for event in self.events: buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoin= t */, handle_%s);" % (self.name, event)) - return self.__buff_to_string(buff) + return '\n'.join(buff) =20 def fill_tracepoint_detach_helper(self): buff =3D [] for event in self.events: buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoin= t */, handle_%s);" % (self.name, event)) - return self.__buff_to_string(buff) + return '\n'.join(buff) =20 def fill_main_c(self): main_c =3D self.main_c @@ -210,7 +201,7 @@ class dot2k(Dot2c): buff =3D self.fill_model_h_header() buff +=3D self.format_model() =20 - return self.__buff_to_string(buff) + return '\n'.join(buff) =20 def fill_monitor_class_type(self): if self.monitor_type =3D=3D "per_task": @@ -242,7 +233,7 @@ class dot2k(Dot2c): tp_args_c =3D ", ".join([b for a,b in tp_args]) buff.append(" TP_PROTO(%s)," % tp_proto_c) buff.append(" TP_ARGS(%s)" % tp_args_c) - return self.__buff_to_string(buff) + return '\n'.join(buff) =20 def fill_monitor_deps(self): buff =3D [] @@ -250,7 +241,7 @@ class dot2k(Dot2c): if self.parent: buff.append(" depends on RV_MON_%s" % self.parent.upper()) buff.append(" default y") - return self.__buff_to_string(buff) + return '\n'.join(buff) =20 def fill_trace_h(self): trace_h =3D self.trace_h --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 1BB7225B301 for ; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; cv=none; b=jNySdnrjgGFPhOC66c/UAhuUUH4XBKkpnitjw8AnHy3yRfGMBtgIPVk6lPN5tsRWyfIpagTtcV/j0paRdWqOJ+A4oTpNa12dE4GilIYsD0c2P53AnSE6EIS9DP6ptMBw7wkPnpI68L9/sPS6ZEqCxZNQ8o1rPFc6Xg11NcUq6+o= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; c=relaxed/simple; bh=+9pg9Dd6aGe5iyXDhhHxg3GB3DTvajjJM8WZNONOvJs=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=g8V2PULbuyL1hWiz83JTpe5DO3ULo4Q0NiWb+qq/laz12GfYVhvNAhNVg9P/NerXokjsPwBj8FEKonmfH4vWdRI6opvyjCy7goPKfky0hv6sNOcsrUL7yZ+gvCGy4Vl5bwZUGjdHgMyqGOg2CQ0KIcr9CD+HzCtaitqNv0Nul4g= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=T5KFRLHI; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="T5KFRLHI" Received: by smtp.kernel.org (Postfix) with ESMTPSA id E9D0FC4CEEF; Fri, 25 Jul 2025 20:34:18 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475659; bh=+9pg9Dd6aGe5iyXDhhHxg3GB3DTvajjJM8WZNONOvJs=; h=Date:From:To:Cc:Subject:References:From; b=T5KFRLHITpXBupmdmBL8oLBAPdspJbTfR/4pY5ms+wjiylUYFPSmuesmW9MwqBdRm sTvfIEHxQhlM1BNgjHmGVU+QnPPDB1quONoW/fEAzbEzeEuKu8uexHf9nmRA2faENu YUUV34Vxpwy7zmIjn3V24MSIn5D9a7xlRdW77a5QfmVD6Z0UVtuB6Wb/ASXCuBZm5P rOTtK6k8pOeLzlemIYmmu73ZyxKIKAH0Pbjux6xsMPuAqE0sa4V7bGuSMi7416kWBl 6sIbIDYUKfZB78q60Y0iBk0ozOaR5JlBq2tlc4EfGCi/bapUmVDfVeZSq/eAcqYXxa BGLjVk8eiv+oQ== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Z-00000001Qeo-0Mt0; Fri, 25 Jul 2025 16:34:25 -0400 Message-ID: <20250725203424.945032683@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:03 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 06/25] verification/dot2k: Replace is_container() hack with subparsers References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao dot2k is used for both generating deterministic automaton (DA) monitor and generating container monitor. Generating DA monitor and generating container requires different parameters. This is implemented by peeking at sys.argv and check whether "--container" is specified, and use that information to make some parameters optional or required. This works, but is quite hacky and ugly. Replace this hack with Python's built-in subparsers. The old commands: python3 dot2/dot2k -d wip.dot -t per_cpu python3 dot2/dot2k -n sched --container are equivalent to the new commands: python3 dot2/dot2k monitor -d wip.dot -t per_cpu python3 dot2/dot2k container -n sched Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/23c4e3c6e10c39e86d8e6a289208dde407efc4a8.1751= 634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/dot2/dot2k | 37 +++++++++++++++++--------------- tools/verification/dot2/dot2k.py | 2 +- 2 files changed, 21 insertions(+), 18 deletions(-) diff --git a/tools/verification/dot2/dot2k b/tools/verification/dot2/dot2k index 767064f415e7..133fb17d9d47 100644 --- a/tools/verification/dot2/dot2k +++ b/tools/verification/dot2/dot2k @@ -13,30 +13,33 @@ if __name__ =3D=3D '__main__': import argparse import sys =20 - def is_container(): - """Should work even before parsing the arguments""" - return "-c" in sys.argv or "--container" in sys.argv - parser =3D argparse.ArgumentParser(description=3D'transform .dot file = into kernel rv monitor') - parser.add_argument('-d', "--dot", dest=3D"dot_file", required=3Dnot i= s_container()) - parser.add_argument('-t', "--monitor_type", dest=3D"monitor_type", req= uired=3Dnot is_container(), - help=3Df"Available options: {', '.join(dot2k.monit= or_types.keys())}") - parser.add_argument('-n', "--model_name", dest=3D"model_name", require= d=3Dis_container()) parser.add_argument("-D", "--description", dest=3D"description", requi= red=3DFalse) parser.add_argument("-a", "--auto_patch", dest=3D"auto_patch", action=3D"store_true", required=3DFalse, help=3D"Patch the kernel in place") - parser.add_argument("-p", "--parent", dest=3D"parent", - required=3DFalse, help=3D"Create a monitor nested = to parent") - parser.add_argument("-c", "--container", dest=3D"container", - action=3D"store_true", required=3DFalse, - help=3D"Create an empty monitor to be used as a co= ntainer") + + subparsers =3D parser.add_subparsers(dest=3D"subcmd", required=3DTrue) + + monitor_parser =3D subparsers.add_parser("monitor") + monitor_parser.add_argument('-n', "--model_name", dest=3D"model_name") + monitor_parser.add_argument("-p", "--parent", dest=3D"parent", + required=3DFalse, help=3D"Create a monitor= nested to parent") + monitor_parser.add_argument('-d', "--dot", dest=3D"dot_file") + monitor_parser.add_argument('-t', "--monitor_type", dest=3D"monitor_ty= pe", + help=3Df"Available options: {', '.join(dot= 2k.monitor_types.keys())}") + + container_parser =3D subparsers.add_parser("container") + container_parser.add_argument('-n', "--model_name", dest=3D"model_name= ", required=3DTrue) + params =3D parser.parse_args() =20 - if not is_container(): - print("Opening and parsing the dot file %s" % params.dot_file) try: - monitor=3Ddot2k(params.dot_file, params.monitor_type, vars(params)) + if params.subcmd =3D=3D "monitor": + print("Opening and parsing the dot file %s" % params.dot_file) + monitor =3D dot2k(params.dot_file, params.monitor_type, vars(p= arams)) + else: + monitor =3D dot2k(None, None, vars(params)) except Exception as e: print('Error: '+ str(e)) print("Sorry : :-(") @@ -45,7 +48,7 @@ if __name__ =3D=3D '__main__': print("Writing the monitor into the directory %s" % monitor.name) monitor.print_files() print("Almost done, checklist") - if not is_container(): + if params.subcmd =3D=3D "monitor": print(" - Edit the %s/%s.c to add the instrumentation" % (monitor= .name, monitor.name)) print(monitor.fill_tracepoint_tooltip()) print(monitor.fill_makefile_tooltip()) diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot= 2k.py index 0922754454b9..9ec99e297012 100644 --- a/tools/verification/dot2/dot2k.py +++ b/tools/verification/dot2/dot2k.py @@ -19,7 +19,7 @@ class dot2k(Dot2c): monitor_type =3D "per_cpu" =20 def __init__(self, file_path, MonitorType, extra_params=3D{}): - self.container =3D extra_params.get("container") + self.container =3D extra_params.get("subcmd") =3D=3D "container" self.parent =3D extra_params.get("parent") self.__fill_rv_templates_dir() =20 --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 AAC7725C70C for ; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; cv=none; b=tROuTQmCaFNIzmD2enz3DiWL56aWettqGNC5Ei6vuNEpWuwwkTd+rqYZ0LgTjE+Xi3uv981dJBp6iVZJ7vWdlmOKfGMK12HCO68AaavNo09hx1SDgTZxs1NGcfChJIKUidGNj+5QAu0s9Qv26SlquLU0iavpdIPIF90stLkicN4= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; c=relaxed/simple; bh=zYfTKOa6h3U1XrTfzqWW6+lsb4ZafI7zKrTqCiYO9a0=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=GSfWnqCGXhZS/NdY1hXGT2TXiWDKqFlWIyNFLavSVQbclJcijJ4UoYbDlzo5uGs+/E4I8eCoeeDRG3Rlogr8V9/G9YEtUPW5FtblEPw79EEJVzf8V0ZG5UF3rdbCs9a5zqPy9x9qg/Fnxk6+m/6Qe8IUvzHTEFMuMFjhR0itoTQ= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=czWVlIOU; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="czWVlIOU" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 1B4EBC4CEF7; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475659; bh=zYfTKOa6h3U1XrTfzqWW6+lsb4ZafI7zKrTqCiYO9a0=; h=Date:From:To:Cc:Subject:References:From; b=czWVlIOUPEiDBjfR212QM6KX86zgJNhjNIwKATlWulgXyprnj3dhn6N6KjoR+Cc0E qOSKkR8S4VBLi+62mYjANBu9RBg/5wiqYO4qn4maBNC/ysk9Lz7UgmYZRyH232SPzF AWGQ4F26tFLKx3YnhgyIEqifGzDD4AH9qO0s+kIpng4KdNIiI/epzpHvTV8+mQFg3W cNjacEg568RRUsYMVLq1c2NJrlQ/lLe5fWn00ipT9V7XZLtn+i1KaOAFOBi8iT94zf tq2nzTcnNSqmmwofKfsEAzSSQQVtuSDGRG/PGhHQTG+6APHNpiR02gPWqw0GTnnsap d4UYr3HopK+9w== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Z-00000001QfI-14V8; Fri, 25 Jul 2025 16:34:25 -0400 Message-ID: <20250725203425.109309356@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:04 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 07/25] verification/dot2k: Prepare the frontend for LTL inclusion References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao The dot2k tool has some code that can be reused for linear temporal logic monitor. Prepare its frontend for LTL inclusion: 1. Rename to be generic: rvgen 2. Replace the parameter --dot with 2 parameters: --class: to specific the monitor class, can be 'da' or 'ltl' --spec: the monitor specification file, .dot file for DA, and .ltl file for LTL The old command: python3 dot2/dot2k monitor -d wip.dot -t per_cpu is equivalent to the new commands: python3 rvgen monitor -c da -s wip.dot -t per_cpu Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751= 634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/{dot2 =3D> rvgen}/Makefile | 10 +++++----- .../{dot2/dot2k =3D> rvgen/__main__.py} | 18 +++++++++++++----- tools/verification/{dot2 =3D> rvgen}/dot2c | 2 +- .../{dot2 =3D> rvgen}/dot2k_templates/Kconfig | 0 .../dot2k_templates/Kconfig_container | 0 .../{dot2 =3D> rvgen}/dot2k_templates/main.c | 0 .../dot2k_templates/main_container.c | 0 .../dot2k_templates/main_container.h | 0 .../{dot2 =3D> rvgen}/dot2k_templates/trace.h | 0 .../{dot2 =3D> rvgen/rvgen}/automata.py | 0 .../{dot2 =3D> rvgen/rvgen}/dot2c.py | 2 +- .../{dot2 =3D> rvgen/rvgen}/dot2k.py | 10 +++++----- 12 files changed, 25 insertions(+), 17 deletions(-) rename tools/verification/{dot2 =3D> rvgen}/Makefile (55%) rename tools/verification/{dot2/dot2k =3D> rvgen/__main__.py} (72%) rename tools/verification/{dot2 =3D> rvgen}/dot2c (97%) rename tools/verification/{dot2 =3D> rvgen}/dot2k_templates/Kconfig (100%) rename tools/verification/{dot2 =3D> rvgen}/dot2k_templates/Kconfig_contai= ner (100%) rename tools/verification/{dot2 =3D> rvgen}/dot2k_templates/main.c (100%) rename tools/verification/{dot2 =3D> rvgen}/dot2k_templates/main_container= .c (100%) rename tools/verification/{dot2 =3D> rvgen}/dot2k_templates/main_container= .h (100%) rename tools/verification/{dot2 =3D> rvgen}/dot2k_templates/trace.h (100%) rename tools/verification/{dot2 =3D> rvgen/rvgen}/automata.py (100%) rename tools/verification/{dot2 =3D> rvgen/rvgen}/dot2c.py (99%) rename tools/verification/{dot2 =3D> rvgen/rvgen}/dot2k.py (98%) diff --git a/tools/verification/dot2/Makefile b/tools/verification/rvgen/Ma= kefile similarity index 55% rename from tools/verification/dot2/Makefile rename to tools/verification/rvgen/Makefile index 021beb07a521..cea9c21c3bce 100644 --- a/tools/verification/dot2/Makefile +++ b/tools/verification/rvgen/Makefile @@ -3,7 +3,7 @@ INSTALL=3Dinstall prefix ?=3D /usr bindir ?=3D $(prefix)/bin mandir ?=3D $(prefix)/share/man -miscdir ?=3D $(prefix)/share/dot2 +miscdir ?=3D $(prefix)/share/rvgen srcdir ?=3D $(prefix)/src =20 PYLIB ?=3D $(shell python3 -c 'import sysconfig; print (sysconfig.get_pa= th("purelib"))') @@ -16,11 +16,11 @@ clean: =20 .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) rvgen/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/automata.= py + $(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ - $(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py - $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/ + $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py + $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen =20 mkdir -p ${miscdir}/ cp -rp dot2k_templates $(DESTDIR)$(miscdir)/ diff --git a/tools/verification/dot2/dot2k b/tools/verification/rvgen/__mai= n__.py similarity index 72% rename from tools/verification/dot2/dot2k rename to tools/verification/rvgen/__main__.py index 133fb17d9d47..994d320ad2d1 100644 --- a/tools/verification/dot2/dot2k +++ b/tools/verification/rvgen/__main__.py @@ -9,11 +9,11 @@ # Documentation/trace/rv/da_monitor_synthesis.rst =20 if __name__ =3D=3D '__main__': - from dot2.dot2k import dot2k + from rvgen.dot2k import dot2k import argparse import sys =20 - parser =3D argparse.ArgumentParser(description=3D'transform .dot file = into kernel rv monitor') + parser =3D argparse.ArgumentParser(description=3D'Generate kernel rv m= onitor') parser.add_argument("-D", "--description", dest=3D"description", requi= red=3DFalse) parser.add_argument("-a", "--auto_patch", dest=3D"auto_patch", action=3D"store_true", required=3DFalse, @@ -25,7 +25,9 @@ if __name__ =3D=3D '__main__': monitor_parser.add_argument('-n', "--model_name", dest=3D"model_name") monitor_parser.add_argument("-p", "--parent", dest=3D"parent", required=3DFalse, help=3D"Create a monitor= nested to parent") - monitor_parser.add_argument('-d', "--dot", dest=3D"dot_file") + monitor_parser.add_argument('-c', "--class", dest=3D"monitor_class", + help=3D"Monitor class, either \"da\" or \"= ltl\"") + monitor_parser.add_argument('-s', "--spec", dest=3D"spec", help=3D"Mon= itor specification file") monitor_parser.add_argument('-t', "--monitor_type", dest=3D"monitor_ty= pe", help=3Df"Available options: {', '.join(dot= 2k.monitor_types.keys())}") =20 @@ -36,8 +38,14 @@ if __name__ =3D=3D '__main__': =20 try: if params.subcmd =3D=3D "monitor": - print("Opening and parsing the dot file %s" % params.dot_file) - monitor =3D dot2k(params.dot_file, params.monitor_type, vars(p= arams)) + print("Opening and parsing the specification file %s" % params= .spec) + if params.monitor_class =3D=3D "da": + monitor =3D dot2k(params.spec, params.monitor_type, vars(p= arams)) + elif params.monitor_class =3D=3D "ltl": + raise NotImplementedError + else: + print("Unknown monitor class:", params.monitor_class) + sys.exit(1) else: monitor =3D dot2k(None, None, vars(params)) except Exception as e: diff --git a/tools/verification/dot2/dot2c b/tools/verification/rvgen/dot2c similarity index 97% rename from tools/verification/dot2/dot2c rename to tools/verification/rvgen/dot2c index 3fe89ab88b65..bf0c67c5b66c 100644 --- a/tools/verification/dot2/dot2c +++ b/tools/verification/rvgen/dot2c @@ -14,7 +14,7 @@ # Documentation/trace/rv/deterministic_automata.rst =20 if __name__ =3D=3D '__main__': - from dot2 import dot2c + from rvgen import dot2c import argparse import sys =20 diff --git a/tools/verification/dot2/dot2k_templates/Kconfig b/tools/verifi= cation/rvgen/dot2k_templates/Kconfig similarity index 100% rename from tools/verification/dot2/dot2k_templates/Kconfig rename to tools/verification/rvgen/dot2k_templates/Kconfig diff --git a/tools/verification/dot2/dot2k_templates/Kconfig_container b/to= ols/verification/rvgen/dot2k_templates/Kconfig_container similarity index 100% rename from tools/verification/dot2/dot2k_templates/Kconfig_container rename to tools/verification/rvgen/dot2k_templates/Kconfig_container diff --git a/tools/verification/dot2/dot2k_templates/main.c b/tools/verific= ation/rvgen/dot2k_templates/main.c similarity index 100% rename from tools/verification/dot2/dot2k_templates/main.c rename to tools/verification/rvgen/dot2k_templates/main.c diff --git a/tools/verification/dot2/dot2k_templates/main_container.c b/too= ls/verification/rvgen/dot2k_templates/main_container.c similarity index 100% rename from tools/verification/dot2/dot2k_templates/main_container.c rename to tools/verification/rvgen/dot2k_templates/main_container.c diff --git a/tools/verification/dot2/dot2k_templates/main_container.h b/too= ls/verification/rvgen/dot2k_templates/main_container.h similarity index 100% rename from tools/verification/dot2/dot2k_templates/main_container.h rename to tools/verification/rvgen/dot2k_templates/main_container.h diff --git a/tools/verification/dot2/dot2k_templates/trace.h b/tools/verifi= cation/rvgen/dot2k_templates/trace.h similarity index 100% rename from tools/verification/dot2/dot2k_templates/trace.h rename to tools/verification/rvgen/dot2k_templates/trace.h diff --git a/tools/verification/dot2/automata.py b/tools/verification/rvgen= /rvgen/automata.py similarity index 100% rename from tools/verification/dot2/automata.py rename to tools/verification/rvgen/rvgen/automata.py diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/rvgen/rv= gen/dot2c.py similarity index 99% rename from tools/verification/dot2/dot2c.py rename to tools/verification/rvgen/rvgen/dot2c.py index fa2816ac7b61..6009caf568d9 100644 --- a/tools/verification/dot2/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -13,7 +13,7 @@ # For further information, see: # Documentation/trace/rv/deterministic_automata.rst =20 -from dot2.automata import Automata +from .automata import Automata =20 class Dot2c(Automata): enum_suffix =3D "" diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/rvgen/rv= gen/dot2k.py similarity index 98% rename from tools/verification/dot2/dot2k.py rename to tools/verification/rvgen/rvgen/dot2k.py index 9ec99e297012..e29462413194 100644 --- a/tools/verification/dot2/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -8,13 +8,13 @@ # For further information, see: # Documentation/trace/rv/da_monitor_synthesis.rst =20 -from dot2.dot2c import Dot2c +from .dot2c import Dot2c import platform import os =20 class dot2k(Dot2c): monitor_types =3D { "global" : 1, "per_cpu" : 2, "per_task" : 3 } - monitor_templates_dir =3D "dot2/dot2k_templates/" + monitor_templates_dir =3D "rvgen/dot2k_templates/" rv_dir =3D "kernel/trace/rv" monitor_type =3D "per_cpu" =20 @@ -60,14 +60,14 @@ class dot2k(Dot2c): if platform.system() !=3D "Linux": raise OSError("I can only run on Linux.") =20 - kernel_path =3D "/lib/modules/%s/build/tools/verification/dot2/dot= 2k_templates/" % (platform.release()) + kernel_path =3D "/lib/modules/%s/build/tools/verification/rvgen/do= t2k_templates/" % (platform.release()) =20 if os.path.exists(kernel_path): self.monitor_templates_dir =3D kernel_path return =20 - if os.path.exists("/usr/share/dot2/dot2k_templates/"): - self.monitor_templates_dir =3D "/usr/share/dot2/dot2k_template= s/" + if os.path.exists("/usr/share/rvgen/dot2k_templates/"): + self.monitor_templates_dir =3D "/usr/share/rvgen/dot2k_templat= es/" return =20 raise FileNotFoundError("Could not find the template directory, do= you have the kernel source installed?") --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 6ACCA25BEE8 for ; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; cv=none; b=UR861iOgoczi5ZfKwq7YKIkvljdbt+HMFrF21wgJmvF9zUEmfO9emvSXbNlKbtyiEuyw9QWRz3gv5JSHzFHfh0Hnwy2C+iX0PG3ktQip+qv/fJ3a1PmXShkyRoxyf8PDTxBu8Hkqv8if+9mL+rpaZSpC6eGcT0iouE+1BkxZeyA= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; c=relaxed/simple; bh=NzQcSoVc4SoQj1qhynNfoGMUtUUgH4vBZODSdQ15mPg=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=Q9hrdQj1WyJACMdQfQHjlQ5xHS10T/HT3jIvm5b9D5aID7S8ENkd+YYt6F49Yfw9GBbPnROMOHz7nDw5OkLiJsWV2xNu7njKgYqF+3pIGsblLPYdYAhoJFyNK5f7cLieJPNEQtbbH8VtW7NAg+fcLpWX0+fQkQ8KODLP74ZOTcw= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=dLAmlDpl; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="dLAmlDpl" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 492E3C4CEF9; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475659; bh=NzQcSoVc4SoQj1qhynNfoGMUtUUgH4vBZODSdQ15mPg=; h=Date:From:To:Cc:Subject:References:From; b=dLAmlDplLEkF5plS1ML2W0c6Y99DwxOD+tbu11kAMsi3tfraGzQrmnwRU+c9aTdP7 +414UImKvdrkjqAJHm+6W1USB8+0EhdREjrR/uZg0WiMXeICK0CFG50eOIdCnik5pL XBeNVMHcD6QgWFgswWMvdob8A001RTWGjfCZxAAzlyo13ND/WZDYn9bGSQAJKLGImE rLGQz8Qgj/If0cituNP2irkbxAK4QLDFuwQEGLGjBs4Fdgtv6hFfVXIFLbIQzIRP5h UI6Tj/phQuBVM/+lBU6txFFXcEzlbIuny41MNSsqihqXHiQ69tptjgH/dyfxz9l3Jm bf1gervQVsaqw== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Z-00000001Qfo-1lPj; Fri, 25 Jul 2025 16:34:25 -0400 Message-ID: <20250725203425.275466334@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:05 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 08/25] Documentation/rv: Prepare monitor synthesis document for LTL inclusion References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao Monitor synthesis from deterministic automaton and linear temporal logic have a lot in common. Therefore a single document should describe both. Change da_monitor_synthesis.rst to monitor_synthesis.rst. LTL monitor synthesis will be added to this file by a follow-up commit. This makes the diff far easier to read. If renaming and adding LTL info is done in a single commit, git wouldn't recognize it as a rename, but a file removal and a file addition. While at it, correct the old dot2k commands to the new rvgen commands. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/d91c6e4600287f4732d68a014219e576a75ce6dc.1751= 634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- Documentation/trace/rv/index.rst | 2 +- ...or_synthesis.rst =3D> monitor_synthesis.rst} | 20 +++++++++---------- 2 files changed, 11 insertions(+), 11 deletions(-) rename Documentation/trace/rv/{da_monitor_synthesis.rst =3D> monitor_synth= esis.rst} (92%) diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/inde= x.rst index 26042dff70bb..9a2342bd20ca 100644 --- a/Documentation/trace/rv/index.rst +++ b/Documentation/trace/rv/index.rst @@ -8,7 +8,7 @@ Runtime Verification =20 runtime-verification.rst deterministic_automata.rst - da_monitor_synthesis.rst + monitor_synthesis.rst da_monitor_instrumentation.rst monitor_wip.rst monitor_wwnr.rst diff --git a/Documentation/trace/rv/da_monitor_synthesis.rst b/Documentatio= n/trace/rv/monitor_synthesis.rst similarity index 92% rename from Documentation/trace/rv/da_monitor_synthesis.rst rename to Documentation/trace/rv/monitor_synthesis.rst index 0a92729c8a9b..85624062073b 100644 --- a/Documentation/trace/rv/da_monitor_synthesis.rst +++ b/Documentation/trace/rv/monitor_synthesis.rst @@ -1,5 +1,5 @@ -Deterministic Automata Monitor Synthesis -=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D +Runtime Verification Monitor Synthesis +=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D =20 The starting point for the application of runtime verification (RV) techni= ques is the *specification* or *modeling* of the desired (or undesired) behavior @@ -36,24 +36,24 @@ below:: | +----> panic ? +-------> =20 -DA monitor synthesis +RV monitor synthesis -------------------- =20 The synthesis of automata-based models into the Linux *RV monitor* abstrac= tion -is automated by the dot2k tool and the rv/da_monitor.h header file that +is automated by the rvgen tool and the rv/da_monitor.h header file that contains a set of macros that automatically generate the monitor's code. =20 -dot2k +rvgen ----- =20 -The dot2k utility leverages dot2c by converting an automaton model in +The rvgen utility leverages dot2c by converting an automaton model in the DOT format into the C representation [1] and creating the skeleton of a kernel monitor in C. =20 For example, it is possible to transform the wip.dot model present in [1] into a per-cpu monitor with the following command:: =20 - $ dot2k -d wip.dot -t per_cpu + $ rvgen monitor -c da -s wip.dot -t per_cpu =20 This will create a directory named wip/ with the following files: =20 @@ -87,7 +87,7 @@ the second for monitors with per-cpu instances, and the t= hird with per-task instances. =20 In all cases, the 'name' argument is a string that identifies the monitor,= and -the 'type' argument is the data type used by dot2k on the representation of +the 'type' argument is the data type used by rvgen on the representation of the model in C. =20 For example, the wip model with two states and three events can be @@ -134,7 +134,7 @@ Final remarks ------------- =20 With the monitor synthesis in place using the rv/da_monitor.h and -dot2k, the developer's work should be limited to the instrumentation +rvgen, the developer's work should be limited to the instrumentation of the system, increasing the confidence in the overall approach. =20 [1] For details about deterministic automata format and the translation @@ -142,6 +142,6 @@ from one representation to another, see:: =20 Documentation/trace/rv/deterministic_automata.rst =20 -[2] dot2k appends the monitor's name suffix to the events enums to +[2] rvgen appends the monitor's name suffix to the events enums to avoid conflicting variables when exporting the global vmlinux.h use by BPF programs. --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 9CFA025BF1B for ; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; cv=none; b=qTLdWEdDZtC9WI8F3JiKrBXVb6EVUs1eT56ZjSaYp2iXy1Jt2LLLdu1RyLyf0G25kep1epLqI1W1AK4/rYMM5H4IYDovqUDE8pZPY2cp+L+SuEOYFDjNPZ+zGoocO1Ozqk87TwYofTzbRqLSTUnd9MMasBJpwwKUNfpMZBYGsjU= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475659; c=relaxed/simple; bh=OwQGGSG3VOQzKbOitie3JFQ3glP3Vf5wiKIpEFVcxSE=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=nX6Nl3lhV0iwV8lDOMcNgWBiileqJBmS5qs+LDoIp/QlGygalTjDmwgARCjyIRfpaZoL/emggWmz+mqvuCARB8Rb8FLZsGazRWM0zuA36IGcDa1+AwYvTZm+u6aSjAVYPD3KIAcUei4h8nzgGKQ1jdSjP5FDdV62TbMycZ5lAzE= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=Cgztlak1; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="Cgztlak1" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 709F7C4CEF4; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475659; bh=OwQGGSG3VOQzKbOitie3JFQ3glP3Vf5wiKIpEFVcxSE=; h=Date:From:To:Cc:Subject:References:From; b=Cgztlak1/JgZUWo5dvJbxGug4RbmPSX0PbXKM+HpDvLxhZmCqpJ3fqINiF4Zv2zn6 Bzn6KMTXPEbTiF0q099ipjUGWOS6n8fOZ+DFGJaU4wo3x47JWKBCJweYfmqMBBpH5k kuWknCciRps0wsmFkg9z2H7LU+a0/lWm0FDbTxdJc+JYt29ckJklHTdOwEvpZKn4MF wiHpjdnm2Nig/xaDLRunN6H/UDgEoIpAkcP4O2tN9EEIQAYKqWB0Ybkb0KpHfMo3qI vpz4k8/C0LvS+WSzZO5DSwQSnwt4WYhIBC56bFRsE+gZ5GclkPIN4guGRXE8yTilv+ aNhqZYH35+psg== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Z-00000001QgK-2Syo; Fri, 25 Jul 2025 16:34:25 -0400 Message-ID: <20250725203425.440732886@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:06 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 09/25] verification/rvgen: Restructure the templates files References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao To simply the scripts and to allow easy integration of new monitor types, restructure the template files as followed: 1. Move the template files to be in the same directory as the rvgen package. Furthermore, the installation will now only install the templates to the package directory, not /usr/share/. This simplify templates reading, as the scripts do not need to find the templates at multiple places. 2. Move dot2k_templates/* to: - templates/dot2k/ - templates/container/ This allows sharing templates reading code between DA monitor generation and container generation (and any future generation type). For template files which can be shared between different generation types, support putting them in templates/ This restructure aligns with the recommendation from: https://python-packaging.readthedocs.io/en/latest/non-code-files.html Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/462d90273f96804d3ba850474877d5f727031258.1751= 634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/rvgen/Makefile | 5 +- tools/verification/rvgen/rvgen/dot2k.py | 47 ++++++++----------- .../templates}/Kconfig | 0 .../templates/container/Kconfig} | 0 .../templates/container/main.c} | 0 .../templates/container/main.h} | 0 .../templates/dot2k}/main.c | 0 .../templates/dot2k}/trace.h | 0 8 files changed, 20 insertions(+), 32 deletions(-) rename tools/verification/rvgen/{dot2k_templates =3D> rvgen/templates}/Kco= nfig (100%) rename tools/verification/rvgen/{dot2k_templates/Kconfig_container =3D> rv= gen/templates/container/Kconfig} (100%) rename tools/verification/rvgen/{dot2k_templates/main_container.c =3D> rvg= en/templates/container/main.c} (100%) rename tools/verification/rvgen/{dot2k_templates/main_container.h =3D> rvg= en/templates/container/main.h} (100%) rename tools/verification/rvgen/{dot2k_templates =3D> rvgen/templates/dot2= k}/main.c (100%) rename tools/verification/rvgen/{dot2k_templates =3D> rvgen/templates/dot2= k}/trace.h (100%) diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/M= akefile index cea9c21c3bce..8d08825e7e54 100644 --- a/tools/verification/rvgen/Makefile +++ b/tools/verification/rvgen/Makefile @@ -3,7 +3,6 @@ INSTALL=3Dinstall prefix ?=3D /usr bindir ?=3D $(prefix)/bin mandir ?=3D $(prefix)/share/man -miscdir ?=3D $(prefix)/share/rvgen srcdir ?=3D $(prefix)/src =20 PYLIB ?=3D $(shell python3 -c 'import sysconfig; print (sysconfig.get_pa= th("purelib"))') @@ -21,6 +20,4 @@ install: $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen - - mkdir -p ${miscdir}/ - cp -rp dot2k_templates $(DESTDIR)$(miscdir)/ + cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/ diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index e29462413194..a9ed97d0b224 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -14,14 +14,16 @@ import os =20 class dot2k(Dot2c): monitor_types =3D { "global" : 1, "per_cpu" : 2, "per_task" : 3 } - monitor_templates_dir =3D "rvgen/dot2k_templates/" rv_dir =3D "kernel/trace/rv" monitor_type =3D "per_cpu" =20 def __init__(self, file_path, MonitorType, extra_params=3D{}): self.container =3D extra_params.get("subcmd") =3D=3D "container" self.parent =3D extra_params.get("parent") - self.__fill_rv_templates_dir() + if self.container: + self.abs_template_dir =3D os.path.join(os.path.dirname(__file_= _), "templates/container") + else: + self.abs_template_dir =3D os.path.join(os.path.dirname(__file_= _), "templates/dot2k") =20 if self.container: if file_path: @@ -33,9 +35,7 @@ class dot2k(Dot2c): self.name =3D extra_params.get("model_name") self.events =3D [] self.states =3D [] - self.main_c =3D self.__read_file(self.monitor_templates_dir + = "main_container.c") - self.main_h =3D self.__read_file(self.monitor_templates_dir + = "main_container.h") - self.kconfig =3D self.__read_file(self.monitor_templates_dir += "Kconfig_container") + self.main_h =3D self._read_template_file("main.h") else: super().__init__(file_path, extra_params.get("model_name")) =20 @@ -43,35 +43,16 @@ class dot2k(Dot2c): if self.monitor_type is None: raise ValueError("Unknown monitor type: %s" % MonitorType) self.monitor_type =3D MonitorType - self.main_c =3D self.__read_file(self.monitor_templates_dir + = "main.c") - self.trace_h =3D self.__read_file(self.monitor_templates_dir += "trace.h") - self.kconfig =3D self.__read_file(self.monitor_templates_dir += "Kconfig") + self.trace_h =3D self._read_template_file("trace.h") + + self.main_c =3D self._read_template_file("main.c") + self.kconfig =3D self._read_template_file("Kconfig") self.enum_suffix =3D "_%s" % self.name self.description =3D extra_params.get("description", self.name) or= "auto-generated" self.auto_patch =3D extra_params.get("auto_patch") if self.auto_patch: self.__fill_rv_kernel_dir() =20 - def __fill_rv_templates_dir(self): - - if os.path.exists(self.monitor_templates_dir): - return - - if platform.system() !=3D "Linux": - raise OSError("I can only run on Linux.") - - kernel_path =3D "/lib/modules/%s/build/tools/verification/rvgen/do= t2k_templates/" % (platform.release()) - - if os.path.exists(kernel_path): - self.monitor_templates_dir =3D kernel_path - return - - if os.path.exists("/usr/share/rvgen/dot2k_templates/"): - self.monitor_templates_dir =3D "/usr/share/rvgen/dot2k_templat= es/" - return - - raise FileNotFoundError("Could not find the template directory, do= you have the kernel source installed?") - def __fill_rv_kernel_dir(self): =20 # first try if we are running in the kernel tree root @@ -109,6 +90,16 @@ class dot2k(Dot2c): fd.close() return content =20 + def _read_template_file(self, file): + try: + path =3D os.path.join(self.abs_template_dir, file) + return self.__read_file(path) + except Exception: + # Specific template file not found. Try the generic template f= ile in the template/ + # directory, which is one level up + path =3D os.path.join(self.abs_template_dir, "..", file) + return self.__read_file(path) + def fill_monitor_type(self): return self.monitor_type.upper() =20 diff --git a/tools/verification/rvgen/dot2k_templates/Kconfig b/tools/verif= ication/rvgen/rvgen/templates/Kconfig similarity index 100% rename from tools/verification/rvgen/dot2k_templates/Kconfig rename to tools/verification/rvgen/rvgen/templates/Kconfig diff --git a/tools/verification/rvgen/dot2k_templates/Kconfig_container b/t= ools/verification/rvgen/rvgen/templates/container/Kconfig similarity index 100% rename from tools/verification/rvgen/dot2k_templates/Kconfig_container rename to tools/verification/rvgen/rvgen/templates/container/Kconfig diff --git a/tools/verification/rvgen/dot2k_templates/main_container.c b/to= ols/verification/rvgen/rvgen/templates/container/main.c similarity index 100% rename from tools/verification/rvgen/dot2k_templates/main_container.c rename to tools/verification/rvgen/rvgen/templates/container/main.c diff --git a/tools/verification/rvgen/dot2k_templates/main_container.h b/to= ols/verification/rvgen/rvgen/templates/container/main.h similarity index 100% rename from tools/verification/rvgen/dot2k_templates/main_container.h rename to tools/verification/rvgen/rvgen/templates/container/main.h diff --git a/tools/verification/rvgen/dot2k_templates/main.c b/tools/verifi= cation/rvgen/rvgen/templates/dot2k/main.c similarity index 100% rename from tools/verification/rvgen/dot2k_templates/main.c rename to tools/verification/rvgen/rvgen/templates/dot2k/main.c diff --git a/tools/verification/rvgen/dot2k_templates/trace.h b/tools/verif= ication/rvgen/rvgen/templates/dot2k/trace.h similarity index 100% rename from tools/verification/rvgen/dot2k_templates/trace.h rename to tools/verification/rvgen/rvgen/templates/dot2k/trace.h --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 4F90125D1F7 for ; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; cv=none; b=ij1OejeN4mMri4/UO3CYnRhQrR7ed3WkcqNugh2YbSXEK8x+/XhXrSJ5fDkpxbBZ8jeip5TovmpTEwhSD3k7G6Y5LYWpTm73570cLF3YVWWGKtz8MFUcjrbeCPevkS9PPbZfhhzPWZq6G9N7DPPABuHa1RqfxmQ5FBmsosWaRns= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; c=relaxed/simple; bh=LQfrwZrWRYIqKVVIR3iO+TsksQaspGY3o5laAGrgm+M=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=E57/ztfAZU9CkwJ7v3B4f1Y+RNwf+X66FW3N7rd1kVtFyHXYc0jH33LIoiYLxprdeWC30BLU/HhQ+7ydk3G5BixIK1/qDaSC+3t1pEN+YMyANlCfgou7vuxZu2wVp93p1HGClNHKwEWZyQLLfCPMmTDPRUQeoGuuLIWdpb4TCsg= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=I5yDnq9n; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="I5yDnq9n" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 98177C4CEF8; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475659; bh=LQfrwZrWRYIqKVVIR3iO+TsksQaspGY3o5laAGrgm+M=; h=Date:From:To:Cc:Subject:References:From; b=I5yDnq9nnqqKdAaYfM2cVUkZh8EqBGtXH5qiA805hZc1sqBVPwv6q+ecN5zeeN1vO UKFEXzLpeQg9k4S/vWLLOmxr5JKxrlNpEMUzi79YeSgKG4mgPd0AptHAsSXGI9PRcU KtTKkiJCLVT+B8ofOfY0Rw25hXlbfLafEyBt/SiKUEIEmsiW/vmNZR588Il81g32X3 PCqBQ5DiqzQXpmBYvr79K+cTVGJNydAJDDaHXUQedSlCtLgtwoRUSa0QTxHdcNAFj+ Ry+HokwWrqIkTfhTtUTFjkU688Rdt39YTuk6ug87eWIRbuFCdOldXTLjoOWOJTcMjl kyXa4cwuji7WA== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Z-00000001Qgp-3BCN; Fri, 25 Jul 2025 16:34:25 -0400 Message-ID: <20250725203425.609981956@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:07 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 10/25] verification/rvgen: Restructure the classes to prepare for LTL inclusion References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao Both container generation and DA monitor generation is implemented in the class dot2k. That requires some ugly "if is_container ... else ...". If linear temporal logic support is added at the current state, the "if else" chain is longer and uglier. Furthermore, container generation is irrevelant to .dot files. It is therefore illogical to be implemented in class "dot2k". Clean it up, restructure the dot2k class into the following class hierarchy: (RVGenerator) /\ / \ / \ / \ / \ (Container) (Monitor) /\ / \ / \ / \ (dot2k) [ltl2k] <- intended This allows a simple and clean integration of LTL. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/692137a581ba6bee7a64d37fb7173ae137c47bbd.1751= 634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/rvgen/Makefile | 2 + tools/verification/rvgen/__main__.py | 6 +- tools/verification/rvgen/rvgen/container.py | 22 ++ tools/verification/rvgen/rvgen/dot2k.py | 275 ++------------------ tools/verification/rvgen/rvgen/generator.py | 264 +++++++++++++++++++ 5 files changed, 308 insertions(+), 261 deletions(-) create mode 100644 tools/verification/rvgen/rvgen/container.py create mode 100644 tools/verification/rvgen/rvgen/generator.py diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/M= akefile index 8d08825e7e54..cca8c9ba82e8 100644 --- a/tools/verification/rvgen/Makefile +++ b/tools/verification/rvgen/Makefile @@ -19,5 +19,7 @@ install: $(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py + $(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/containe= r.py + $(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generato= r.py $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/ diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvge= n/__main__.py index 994d320ad2d1..63ecf0c37034 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -10,6 +10,8 @@ =20 if __name__ =3D=3D '__main__': from rvgen.dot2k import dot2k + from rvgen.generator import Monitor + from rvgen.container import Container import argparse import sys =20 @@ -29,7 +31,7 @@ if __name__ =3D=3D '__main__': help=3D"Monitor class, either \"da\" or \"= ltl\"") monitor_parser.add_argument('-s', "--spec", dest=3D"spec", help=3D"Mon= itor specification file") monitor_parser.add_argument('-t', "--monitor_type", dest=3D"monitor_ty= pe", - help=3Df"Available options: {', '.join(dot= 2k.monitor_types.keys())}") + help=3Df"Available options: {', '.join(Mon= itor.monitor_types.keys())}") =20 container_parser =3D subparsers.add_parser("container") container_parser.add_argument('-n', "--model_name", dest=3D"model_name= ", required=3DTrue) @@ -47,7 +49,7 @@ if __name__ =3D=3D '__main__': print("Unknown monitor class:", params.monitor_class) sys.exit(1) else: - monitor =3D dot2k(None, None, vars(params)) + monitor =3D Container(vars(params)) except Exception as e: print('Error: '+ str(e)) print("Sorry : :-(") diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verificati= on/rvgen/rvgen/container.py new file mode 100644 index 000000000000..47d8ab2ad3ec --- /dev/null +++ b/tools/verification/rvgen/rvgen/container.py @@ -0,0 +1,22 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira +# +# Generator for runtime verification monitor container + +from . import generator + + +class Container(generator.RVGenerator): + template_dir =3D "container" + + def __init__(self, extra_params=3D{}): + super().__init__(extra_params) + self.name =3D extra_params.get("model_name") + self.main_h =3D self._read_template_file("main.h") + + def fill_model_h(self): + main_h =3D self.main_h + main_h =3D main_h.replace("%%MODEL_NAME%%", self.name) + return main_h diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/r= vgen/rvgen/dot2k.py index a9ed97d0b224..ed0a3c901106 100644 --- a/tools/verification/rvgen/rvgen/dot2k.py +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -9,108 +9,21 @@ # Documentation/trace/rv/da_monitor_synthesis.rst =20 from .dot2c import Dot2c -import platform -import os +from .generator import Monitor =20 -class dot2k(Dot2c): - monitor_types =3D { "global" : 1, "per_cpu" : 2, "per_task" : 3 } - rv_dir =3D "kernel/trace/rv" - monitor_type =3D "per_cpu" =20 - def __init__(self, file_path, MonitorType, extra_params=3D{}): - self.container =3D extra_params.get("subcmd") =3D=3D "container" - self.parent =3D extra_params.get("parent") - if self.container: - self.abs_template_dir =3D os.path.join(os.path.dirname(__file_= _), "templates/container") - else: - self.abs_template_dir =3D os.path.join(os.path.dirname(__file_= _), "templates/dot2k") - - if self.container: - if file_path: - raise ValueError("A container does not require a dot file") - if MonitorType: - raise ValueError("A container does not require a monitor t= ype") - if self.parent: - raise ValueError("A container cannot have a parent") - self.name =3D extra_params.get("model_name") - self.events =3D [] - self.states =3D [] - self.main_h =3D self._read_template_file("main.h") - else: - super().__init__(file_path, extra_params.get("model_name")) +class dot2k(Monitor, Dot2c): + template_dir =3D "dot2k" =20 - self.monitor_type =3D self.monitor_types.get(MonitorType) - if self.monitor_type is None: - raise ValueError("Unknown monitor type: %s" % MonitorType) - self.monitor_type =3D MonitorType - self.trace_h =3D self._read_template_file("trace.h") - - self.main_c =3D self._read_template_file("main.c") - self.kconfig =3D self._read_template_file("Kconfig") + def __init__(self, file_path, MonitorType, extra_params=3D{}): + self.monitor_type =3D MonitorType + Monitor.__init__(self, extra_params) + Dot2c.__init__(self, file_path, extra_params.get("model_name")) self.enum_suffix =3D "_%s" % self.name - self.description =3D extra_params.get("description", self.name) or= "auto-generated" - self.auto_patch =3D extra_params.get("auto_patch") - if self.auto_patch: - self.__fill_rv_kernel_dir() - - def __fill_rv_kernel_dir(self): - - # first try if we are running in the kernel tree root - if os.path.exists(self.rv_dir): - return - - # offset if we are running inside the kernel tree from verificatio= n/dot2 - kernel_path =3D os.path.join("../..", self.rv_dir) - - if os.path.exists(kernel_path): - self.rv_dir =3D kernel_path - return - - if platform.system() !=3D "Linux": - raise OSError("I can only run on Linux.") - - kernel_path =3D os.path.join("/lib/modules/%s/build" % platform.re= lease(), self.rv_dir) - - # if the current kernel is from a distro this may not be a full ke= rnel tree - # verify that one of the files we are going to modify is available - if os.path.exists(os.path.join(kernel_path, "rv_trace.h")): - self.rv_dir =3D kernel_path - return - - raise FileNotFoundError("Could not find the rv directory, do you h= ave the kernel source installed?") - - def __read_file(self, path): - try: - fd =3D open(path, 'r') - except OSError: - raise Exception("Cannot open the file: %s" % path) - - content =3D fd.read() - - fd.close() - return content - - def _read_template_file(self, file): - try: - path =3D os.path.join(self.abs_template_dir, file) - return self.__read_file(path) - except Exception: - # Specific template file not found. Try the generic template f= ile in the template/ - # directory, which is one level up - path =3D os.path.join(self.abs_template_dir, "..", file) - return self.__read_file(path) =20 def fill_monitor_type(self): return self.monitor_type.upper() =20 - def fill_parent(self): - return "&rv_%s" % self.parent if self.parent else "NULL" - - def fill_include_parent(self): - if self.parent: - return "#include \n" % (self.parent, self.pa= rent) - return "" - def fill_tracepoint_handlers_skel(self): buff =3D [] for event in self.events: @@ -144,30 +57,6 @@ class dot2k(Dot2c): buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoin= t */, handle_%s);" % (self.name, event)) return '\n'.join(buff) =20 - def fill_main_c(self): - main_c =3D self.main_c - monitor_type =3D self.fill_monitor_type() - min_type =3D self.get_minimun_type() - nr_events =3D len(self.events) - tracepoint_handlers =3D self.fill_tracepoint_handlers_skel() - tracepoint_attach =3D self.fill_tracepoint_attach_probe() - tracepoint_detach =3D self.fill_tracepoint_detach_helper() - parent =3D self.fill_parent() - parent_include =3D self.fill_include_parent() - - main_c =3D main_c.replace("%%MONITOR_TYPE%%", monitor_type) - main_c =3D main_c.replace("%%MIN_TYPE%%", min_type) - main_c =3D main_c.replace("%%MODEL_NAME%%", self.name) - main_c =3D main_c.replace("%%NR_EVENTS%%", str(nr_events)) - main_c =3D main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoi= nt_handlers) - main_c =3D main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_atta= ch) - main_c =3D main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_deta= ch) - main_c =3D main_c.replace("%%DESCRIPTION%%", self.description) - main_c =3D main_c.replace("%%PARENT%%", parent) - main_c =3D main_c.replace("%%INCLUDE_PARENT%%", parent_include) - - return main_c - def fill_model_h_header(self): buff =3D [] buff.append("/* SPDX-License-Identifier: GPL-2.0 */") @@ -226,147 +115,15 @@ class dot2k(Dot2c): buff.append(" TP_ARGS(%s)" % tp_args_c) return '\n'.join(buff) =20 - def fill_monitor_deps(self): - buff =3D [] - buff.append(" # XXX: add dependencies if there") - if self.parent: - buff.append(" depends on RV_MON_%s" % self.parent.upper()) - buff.append(" default y") - return '\n'.join(buff) - - def fill_trace_h(self): - trace_h =3D self.trace_h - monitor_class =3D self.fill_monitor_class() - monitor_class_type =3D self.fill_monitor_class_type() - tracepoint_args_skel_event =3D self.fill_tracepoint_args_skel("eve= nt") - tracepoint_args_skel_error =3D self.fill_tracepoint_args_skel("err= or") - trace_h =3D trace_h.replace("%%MODEL_NAME%%", self.name) - trace_h =3D trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper()) - trace_h =3D trace_h.replace("%%MONITOR_CLASS%%", monitor_class) - trace_h =3D trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_clas= s_type) - trace_h =3D trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", trac= epoint_args_skel_event) - trace_h =3D trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", trac= epoint_args_skel_error) - return trace_h - - def fill_kconfig(self): - kconfig =3D self.kconfig - monitor_class_type =3D self.fill_monitor_class_type() - monitor_deps =3D self.fill_monitor_deps() - kconfig =3D kconfig.replace("%%MODEL_NAME%%", self.name) - kconfig =3D kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper()) - kconfig =3D kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_clas= s_type) - kconfig =3D kconfig.replace("%%DESCRIPTION%%", self.description) - kconfig =3D kconfig.replace("%%MONITOR_DEPS%%", monitor_deps) - return kconfig - - def fill_main_container_h(self): - main_h =3D self.main_h - main_h =3D main_h.replace("%%MODEL_NAME%%", self.name) - return main_h - - def __patch_file(self, file, marker, line): - file_to_patch =3D os.path.join(self.rv_dir, file) - content =3D self.__read_file(file_to_patch) - content =3D content.replace(marker, line + "\n" + marker) - self.__write_file(file_to_patch, content) - - def fill_tracepoint_tooltip(self): - monitor_class_type =3D self.fill_monitor_class_type() - if self.auto_patch: - self.__patch_file("rv_trace.h", - "// Add new monitors based on CONFIG_%s here" = % monitor_class_type, - "#include " % (self.na= me, self.name)) - return " - Patching %s/rv_trace.h, double check the result" %= self.rv_dir - - return """ - Edit %s/rv_trace.h: -Add this line where other tracepoints are included and %s is defined: -#include -""" % (self.rv_dir, monitor_class_type, self.name, self.name) - - def fill_kconfig_tooltip(self): - if self.auto_patch: - self.__patch_file("Kconfig", - "# Add new monitors here", - "source \"kernel/trace/rv/monitors/%s/Kconfig\= "" % (self.name)) - return " - Patching %s/Kconfig, double check the result" % se= lf.rv_dir - - return """ - Edit %s/Kconfig: -Add this line where other monitors are included: -source \"kernel/trace/rv/monitors/%s/Kconfig\" -""" % (self.rv_dir, self.name) - - def fill_makefile_tooltip(self): - name =3D self.name - name_up =3D name.upper() - if self.auto_patch: - self.__patch_file("Makefile", - "# Add new monitors here", - "obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o= " % (name_up, name, name)) - return " - Patching %s/Makefile, double check the result" % s= elf.rv_dir - - return """ - Edit %s/Makefile: -Add this line where other monitors are included: -obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o -""" % (self.rv_dir, name_up, name, name) - - def fill_monitor_tooltip(self): - if self.auto_patch: - return " - Monitor created in %s/monitors/%s" % (self.rv_dir,= self. name) - return " - Move %s/ to the kernel's monitor directory (%s/monitor= s)" % (self.name, self.rv_dir) - - def __create_directory(self): - path =3D self.name - if self.auto_patch: - path =3D os.path.join(self.rv_dir, "monitors", path) - try: - os.mkdir(path) - except FileExistsError: - return - except: - print("Fail creating the output dir: %s" % self.name) - - def __write_file(self, file_name, content): - try: - file =3D open(file_name, 'w') - except: - print("Fail writing to file: %s" % file_name) - - file.write(content) - - file.close() - - def __create_file(self, file_name, content): - path =3D "%s/%s" % (self.name, file_name) - if self.auto_patch: - path =3D os.path.join(self.rv_dir, "monitors", path) - self.__write_file(path, content) - - def __get_main_name(self): - path =3D "%s/%s" % (self.name, "main.c") - if not os.path.exists(path): - return "main.c" - return "__main.c" - - def print_files(self): - main_c =3D self.fill_main_c() - - self.__create_directory() - - path =3D "%s.c" % self.name - self.__create_file(path, main_c) + def fill_main_c(self): + main_c =3D super().fill_main_c() =20 - if self.container: - main_h =3D self.fill_main_container_h() - path =3D "%s.h" % self.name - self.__create_file(path, main_h) - else: - model_h =3D self.fill_model_h() - path =3D "%s.h" % self.name - self.__create_file(path, model_h) + min_type =3D self.get_minimun_type() + nr_events =3D len(self.events) + monitor_type =3D self.fill_monitor_type() =20 - trace_h =3D self.fill_trace_h() - path =3D "%s_trace.h" % self.name - self.__create_file(path, trace_h) + main_c =3D main_c.replace("%%MIN_TYPE%%", min_type) + main_c =3D main_c.replace("%%NR_EVENTS%%", str(nr_events)) + main_c =3D main_c.replace("%%MONITOR_TYPE%%", monitor_type) =20 - kconfig =3D self.fill_kconfig() - self.__create_file("Kconfig", kconfig) + return main_c diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py new file mode 100644 index 000000000000..19d0078a3803 --- /dev/null +++ b/tools/verification/rvgen/rvgen/generator.py @@ -0,0 +1,264 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira +# +# Abtract class for generating kernel runtime verification monitors from s= pecification file + +import platform +import os + + +class RVGenerator: + rv_dir =3D "kernel/trace/rv" + + def __init__(self, extra_params=3D{}): + self.name =3D extra_params.get("model_name") + self.parent =3D extra_params.get("parent") + self.abs_template_dir =3D \ + os.path.join(os.path.dirname(__file__), "templates", self.temp= late_dir) + self.main_c =3D self._read_template_file("main.c") + self.kconfig =3D self._read_template_file("Kconfig") + self.description =3D extra_params.get("description", self.name) or= "auto-generated" + self.auto_patch =3D extra_params.get("auto_patch") + if self.auto_patch: + self.__fill_rv_kernel_dir() + + def __fill_rv_kernel_dir(self): + + # first try if we are running in the kernel tree root + if os.path.exists(self.rv_dir): + return + + # offset if we are running inside the kernel tree from verificatio= n/dot2 + kernel_path =3D os.path.join("../..", self.rv_dir) + + if os.path.exists(kernel_path): + self.rv_dir =3D kernel_path + return + + if platform.system() !=3D "Linux": + raise OSError("I can only run on Linux.") + + kernel_path =3D os.path.join("/lib/modules/%s/build" % platform.re= lease(), self.rv_dir) + + # if the current kernel is from a distro this may not be a full ke= rnel tree + # verify that one of the files we are going to modify is available + if os.path.exists(os.path.join(kernel_path, "rv_trace.h")): + self.rv_dir =3D kernel_path + return + + raise FileNotFoundError("Could not find the rv directory, do you h= ave the kernel source installed?") + + def _read_file(self, path): + try: + fd =3D open(path, 'r') + except OSError: + raise Exception("Cannot open the file: %s" % path) + + content =3D fd.read() + + fd.close() + return content + + def _read_template_file(self, file): + try: + path =3D os.path.join(self.abs_template_dir, file) + return self._read_file(path) + except Exception: + # Specific template file not found. Try the generic template f= ile in the template/ + # directory, which is one level up + path =3D os.path.join(self.abs_template_dir, "..", file) + return self._read_file(path) + + def fill_parent(self): + return "&rv_%s" % self.parent if self.parent else "NULL" + + def fill_include_parent(self): + if self.parent: + return "#include \n" % (self.parent, self.pa= rent) + return "" + + def fill_tracepoint_handlers_skel(self): + return "NotImplemented" + + def fill_tracepoint_attach_probe(self): + return "NotImplemented" + + def fill_tracepoint_detach_helper(self): + return "NotImplemented" + + def fill_main_c(self): + main_c =3D self.main_c + tracepoint_handlers =3D self.fill_tracepoint_handlers_skel() + tracepoint_attach =3D self.fill_tracepoint_attach_probe() + tracepoint_detach =3D self.fill_tracepoint_detach_helper() + parent =3D self.fill_parent() + parent_include =3D self.fill_include_parent() + + main_c =3D main_c.replace("%%MODEL_NAME%%", self.name) + main_c =3D main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoi= nt_handlers) + main_c =3D main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_atta= ch) + main_c =3D main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_deta= ch) + main_c =3D main_c.replace("%%DESCRIPTION%%", self.description) + main_c =3D main_c.replace("%%PARENT%%", parent) + main_c =3D main_c.replace("%%INCLUDE_PARENT%%", parent_include) + + return main_c + + def fill_model_h(self): + return "NotImplemented" + + def fill_monitor_class_type(self): + return "NotImplemented" + + def fill_monitor_class(self): + return "NotImplemented" + + def fill_tracepoint_args_skel(self, tp_type): + return "NotImplemented" + + def fill_monitor_deps(self): + buff =3D [] + buff.append(" # XXX: add dependencies if there") + if self.parent: + buff.append(" depends on RV_MON_%s" % self.parent.upper()) + buff.append(" default y") + return '\n'.join(buff) + + def fill_kconfig(self): + kconfig =3D self.kconfig + monitor_class_type =3D self.fill_monitor_class_type() + monitor_deps =3D self.fill_monitor_deps() + kconfig =3D kconfig.replace("%%MODEL_NAME%%", self.name) + kconfig =3D kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper()) + kconfig =3D kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_clas= s_type) + kconfig =3D kconfig.replace("%%DESCRIPTION%%", self.description) + kconfig =3D kconfig.replace("%%MONITOR_DEPS%%", monitor_deps) + return kconfig + + def __patch_file(self, file, marker, line): + file_to_patch =3D os.path.join(self.rv_dir, file) + content =3D self._read_file(file_to_patch) + content =3D content.replace(marker, line + "\n" + marker) + self.__write_file(file_to_patch, content) + + def fill_tracepoint_tooltip(self): + monitor_class_type =3D self.fill_monitor_class_type() + if self.auto_patch: + self.__patch_file("rv_trace.h", + "// Add new monitors based on CONFIG_%s here" = % monitor_class_type, + "#include " % (self.na= me, self.name)) + return " - Patching %s/rv_trace.h, double check the result" %= self.rv_dir + + return """ - Edit %s/rv_trace.h: +Add this line where other tracepoints are included and %s is defined: +#include +""" % (self.rv_dir, monitor_class_type, self.name, self.name) + + def fill_kconfig_tooltip(self): + if self.auto_patch: + self.__patch_file("Kconfig", + "# Add new monitors here", + "source \"kernel/trace/rv/monitors/%s/Kconfig\= "" % (self.name)) + return " - Patching %s/Kconfig, double check the result" % se= lf.rv_dir + + return """ - Edit %s/Kconfig: +Add this line where other monitors are included: +source \"kernel/trace/rv/monitors/%s/Kconfig\" +""" % (self.rv_dir, self.name) + + def fill_makefile_tooltip(self): + name =3D self.name + name_up =3D name.upper() + if self.auto_patch: + self.__patch_file("Makefile", + "# Add new monitors here", + "obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o= " % (name_up, name, name)) + return " - Patching %s/Makefile, double check the result" % s= elf.rv_dir + + return """ - Edit %s/Makefile: +Add this line where other monitors are included: +obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o +""" % (self.rv_dir, name_up, name, name) + + def fill_monitor_tooltip(self): + if self.auto_patch: + return " - Monitor created in %s/monitors/%s" % (self.rv_dir,= self. name) + return " - Move %s/ to the kernel's monitor directory (%s/monitor= s)" % (self.name, self.rv_dir) + + def __create_directory(self): + path =3D self.name + if self.auto_patch: + path =3D os.path.join(self.rv_dir, "monitors", path) + try: + os.mkdir(path) + except FileExistsError: + return + except: + print("Fail creating the output dir: %s" % self.name) + + def __write_file(self, file_name, content): + try: + file =3D open(file_name, 'w') + except: + print("Fail writing to file: %s" % file_name) + + file.write(content) + + file.close() + + def _create_file(self, file_name, content): + path =3D "%s/%s" % (self.name, file_name) + if self.auto_patch: + path =3D os.path.join(self.rv_dir, "monitors", path) + self.__write_file(path, content) + + def __get_main_name(self): + path =3D "%s/%s" % (self.name, "main.c") + if not os.path.exists(path): + return "main.c" + return "__main.c" + + def print_files(self): + main_c =3D self.fill_main_c() + + self.__create_directory() + + path =3D "%s.c" % self.name + self._create_file(path, main_c) + + model_h =3D self.fill_model_h() + path =3D "%s.h" % self.name + self._create_file(path, model_h) + + kconfig =3D self.fill_kconfig() + self._create_file("Kconfig", kconfig) + + +class Monitor(RVGenerator): + monitor_types =3D { "global" : 1, "per_cpu" : 2, "per_task" : 3 } + + def __init__(self, extra_params=3D{}): + super().__init__(extra_params) + self.trace_h =3D self._read_template_file("trace.h") + + def fill_trace_h(self): + trace_h =3D self.trace_h + monitor_class =3D self.fill_monitor_class() + monitor_class_type =3D self.fill_monitor_class_type() + tracepoint_args_skel_event =3D self.fill_tracepoint_args_skel("eve= nt") + tracepoint_args_skel_error =3D self.fill_tracepoint_args_skel("err= or") + trace_h =3D trace_h.replace("%%MODEL_NAME%%", self.name) + trace_h =3D trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper()) + trace_h =3D trace_h.replace("%%MONITOR_CLASS%%", monitor_class) + trace_h =3D trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_clas= s_type) + trace_h =3D trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", trac= epoint_args_skel_event) + trace_h =3D trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", trac= epoint_args_skel_error) + return trace_h + + def print_files(self): + super().print_files() + trace_h =3D self.fill_trace_h() + path =3D "%s_trace.h" % self.name + self._create_file(path, trace_h) --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 4F89923F421 for ; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; cv=none; b=TK0MGu0+seMoNFzJOLakx7XgRNj669YRP/XcuIqJKSVU5WPNJkcbzWAwPLGl4FFlAXtFz02kGykK3vpQWenEOf/8N6aWkPOWEBJDcU39aH2mOJi/CZxQGynn0J2eVHzk4TopQRYhb+IIDRRypAtNJktENxJUqY6zNUXy8/L0ry0= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; c=relaxed/simple; bh=s4Nmof7rTdITh+6kUle4dTnOGGbKHVQPxgZCLbxQbng=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=RTr4oiLxw96nTlSz5sdl1OwD6nt4kDFgyo3rZx05O5zHkwYqq9pMV+slRw2J1rrMzXDttZlDs1tGGv/mO4PQWkOxbNA43HEotouyRWqgC4Vk9e01MxhvPd7j6xI0KSMy4FbHFZDc3l2XKuprFUhp9bKBtfNxC6yTAPAdoW+4XTY= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=KR+9pR0V; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="KR+9pR0V" Received: by smtp.kernel.org (Postfix) with ESMTPSA id C1993C4CEE7; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475659; bh=s4Nmof7rTdITh+6kUle4dTnOGGbKHVQPxgZCLbxQbng=; h=Date:From:To:Cc:Subject:References:From; b=KR+9pR0Vgi29zmwfR0YEFiuCar1nMT8zcyGraCO2dG13TqzUJgDXSu2zHhJ3+pbdU Cq7KLpLRg8mo3mowax7qcz8ZvEWw8EUzWNmGWZT/Jml+VdOhCScAPQ8iDuvrfYI5fs l1XKt7j46j03WGltVwIbJvyzYdAIDPmVeBN4qG7T3wNpyWhgfs/BGpfoCdFiHGq4n1 g38TuoYNT95FXlUBA6VxZ4Bki9/y1s77Fa4a6l/JEyK/mLRRKECG0YIRgfhXIDSuIV lCT5CSsXDLV/tM0DfRXIZU+du0FGkRx0POoQB7N7Mozdfkow841nzgZfUkGBVNAB9a t3A3y0msle0NA== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7Z-00000001QhK-3soI; Fri, 25 Jul 2025 16:34:25 -0400 Message-ID: <20250725203425.779410521@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:08 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 11/25] verification/rvgen: Add support for linear temporal logic References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao Add support for generating RV monitors from linear temporal logic, similar to the generation of deterministic automaton monitors. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/f3c63b363ff9c5af3302ba2b5d92a26a98700eaf.1751= 634289.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/rvgen/.gitignore | 3 + tools/verification/rvgen/Makefile | 2 + tools/verification/rvgen/__main__.py | 3 +- tools/verification/rvgen/rvgen/ltl2ba.py | 540 ++++++++++++++++++ tools/verification/rvgen/rvgen/ltl2k.py | 252 ++++++++ .../rvgen/rvgen/templates/ltl2k/main.c | 102 ++++ .../rvgen/rvgen/templates/ltl2k/trace.h | 14 + 7 files changed, 915 insertions(+), 1 deletion(-) create mode 100644 tools/verification/rvgen/.gitignore create mode 100644 tools/verification/rvgen/rvgen/ltl2ba.py create mode 100644 tools/verification/rvgen/rvgen/ltl2k.py create mode 100644 tools/verification/rvgen/rvgen/templates/ltl2k/main.c create mode 100644 tools/verification/rvgen/rvgen/templates/ltl2k/trace.h diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen= /.gitignore new file mode 100644 index 000000000000..1e288a076560 --- /dev/null +++ b/tools/verification/rvgen/.gitignore @@ -0,0 +1,3 @@ +__pycache__/ +parser.out +parsetab.py diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/M= akefile index cca8c9ba82e8..cfc4056c1e87 100644 --- a/tools/verification/rvgen/Makefile +++ b/tools/verification/rvgen/Makefile @@ -21,5 +21,7 @@ install: $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py $(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/containe= r.py $(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generato= r.py + $(INSTALL) rvgen/ltl2ba.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2ba.py + $(INSTALL) rvgen/ltl2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2k.py $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/ diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvge= n/__main__.py index 63ecf0c37034..fa6fc1f4de2f 100644 --- a/tools/verification/rvgen/__main__.py +++ b/tools/verification/rvgen/__main__.py @@ -12,6 +12,7 @@ if __name__ =3D=3D '__main__': from rvgen.dot2k import dot2k from rvgen.generator import Monitor from rvgen.container import Container + from rvgen.ltl2k import ltl2k import argparse import sys =20 @@ -44,7 +45,7 @@ if __name__ =3D=3D '__main__': if params.monitor_class =3D=3D "da": monitor =3D dot2k(params.spec, params.monitor_type, vars(p= arams)) elif params.monitor_class =3D=3D "ltl": - raise NotImplementedError + monitor =3D ltl2k(params.spec, params.monitor_type, vars(p= arams)) else: print("Unknown monitor class:", params.monitor_class) sys.exit(1) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/= rvgen/rvgen/ltl2ba.py new file mode 100644 index 000000000000..d11840af7f5f --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -0,0 +1,540 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Implementation based on +# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). +# Simple On-the-fly Automatic Verification of Linear Temporal Logic. +# https://doi.org/10.1007/978-0-387-34892-6_1 +# With extra optimizations + +from ply.lex import lex +from ply.yacc import yacc + +# Grammar: +# ltl ::=3D opd | ( ltl ) | ltl binop ltl | unop ltl +# +# Operands (opd): +# true, false, user-defined names +# +# Unary Operators (unop): +# always +# eventually +# not +# +# Binary Operators (binop): +# until +# and +# or +# imply +# equivalent + +tokens =3D ( + 'AND', + 'OR', + 'IMPLY', + 'UNTIL', + 'ALWAYS', + 'EVENTUALLY', + 'VARIABLE', + 'LITERAL', + 'NOT', + 'LPAREN', + 'RPAREN', + 'ASSIGN', +) + +t_AND =3D r'and' +t_OR =3D r'or' +t_IMPLY =3D r'imply' +t_UNTIL =3D r'until' +t_ALWAYS =3D r'always' +t_EVENTUALLY =3D r'eventually' +t_VARIABLE =3D r'[A-Z_0-9]+' +t_LITERAL =3D r'true|false' +t_NOT =3D r'not' +t_LPAREN =3D r'\(' +t_RPAREN =3D r'\)' +t_ASSIGN =3D r'=3D' +t_ignore_COMMENT =3D r'\#.*' +t_ignore =3D ' \t\n' + +def t_error(t): + raise ValueError(f"Illegal character '{t.value[0]}'") + +lexer =3D lex() + +class GraphNode: + uid =3D 0 + + def __init__(self, incoming: set['GraphNode'], new, old, _next): + self.init =3D False + self.outgoing =3D set() + self.labels =3D set() + self.incoming =3D incoming.copy() + self.new =3D new.copy() + self.old =3D old.copy() + self.next =3D _next.copy() + self.id =3D GraphNode.uid + GraphNode.uid +=3D 1 + + def expand(self, node_set): + if not self.new: + for nd in node_set: + if nd.old =3D=3D self.old and nd.next =3D=3D self.next: + nd.incoming |=3D self.incoming + return node_set + + new_current_node =3D GraphNode({self}, self.next, set(), set()) + return new_current_node.expand({self} | node_set) + n =3D self.new.pop() + return n.expand(self, node_set) + + def __lt__(self, other): + return self.id < other.id + +class ASTNode: + uid =3D 1 + + def __init__(self, op): + self.op =3D op + self.id =3D ASTNode.uid + ASTNode.uid +=3D 1 + + def __hash__(self): + return hash(self.op) + + def __eq__(self, other): + return self is other + + def __iter__(self): + yield self + yield from self.op + + def negate(self): + self.op =3D self.op.negate() + return self + + def expand(self, node, node_set): + return self.op.expand(self, node, node_set) + + def __str__(self): + if isinstance(self.op, Literal): + return str(self.op.value) + if isinstance(self.op, Variable): + return self.op.name.lower() + return "val" + str(self.id) + + def normalize(self): + # Get rid of: + # - ALWAYS + # - EVENTUALLY + # - IMPLY + # And move all the NOT to be inside + self.op =3D self.op.normalize() + return self + +class BinaryOp: + op_str =3D "not_supported" + + def __init__(self, left: ASTNode, right: ASTNode): + self.left =3D left + self.right =3D right + + def __hash__(self): + return hash((self.left, self.right)) + + def __iter__(self): + yield from self.left + yield from self.right + + def normalize(self): + raise NotImplementedError + + def negate(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.left.op.is_temporal(): + return True + if self.right.op.is_temporal(): + return True + return self._is_temporal() + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + raise NotImplementedError + +class AndOp(BinaryOp): + op_str =3D '&&' + + def normalize(self): + return self + + def negate(self): + return OrOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old.add(n) + return node.expand(node_set) + + tmp =3D GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return tmp.expand(node_set) + +class OrOp(BinaryOp): + op_str =3D '||' + + def normalize(self): + return self + + def negate(self): + return AndOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old |=3D {n} + return node.expand(node_set) + + node1 =3D GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next) + node2 =3D GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class UntilOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return VOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 =3D GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next | {n}) + node2 =3D GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class VOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return UntilOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 =3D GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next | {n}) + node2 =3D GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class ImplyOp(BinaryOp): + def normalize(self): + # P -> Q =3D=3D=3D !P | Q + return OrOp(self.left.negate(), self.right) + + def _is_temporal(self): + return False + + def negate(self): + # !(P -> Q) =3D=3D=3D !(!P | Q) =3D=3D=3D P & !Q + return AndOp(self.left, self.right.negate()) + +class UnaryOp: + def __init__(self, child: ASTNode): + self.child =3D child + + def __iter__(self): + yield from self.child + + def __hash__(self): + return hash(self.child) + + def normalize(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.child.op.is_temporal(): + return True + return self._is_temporal() + + def negate(self): + raise NotImplementedError + +class EventuallyOp(UnaryOp): + def __str__(self): + return "eventually " + str(self.child) + + def normalize(self): + # <>F =3D=3D true U F + return UntilOp(ASTNode(Literal(True)), self.child) + + def _is_temporal(self): + return True + + def negate(self): + # !<>F =3D=3D [](!F) + return AlwaysOp(self.child.negate()).normalize() + +class AlwaysOp(UnaryOp): + def normalize(self): + # []F =3D=3D=3D !(true U !F) =3D=3D false V F + new =3D ASTNode(Literal(False)) + return VOp(new, self.child) + + def _is_temporal(self): + return True + + def negate(self): + # ![]F =3D=3D <>(!F) + return EventuallyOp(self.child.negate()).normalize() + +class NotOp(UnaryOp): + def __str__(self): + return "!" + str(self.child) + + def normalize(self): + return self.child.op.negate() + + def negate(self): + return self.child.op + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if n.op.child is f: + return node_set + node.old |=3D {n} + return node.expand(node_set) + +class Variable: + def __init__(self, name: str): + self.name =3D name + + def __hash__(self): + return hash(self.name) + + def __iter__(self): + yield from () + + def negate(self): + new =3D ASTNode(self) + return NotOp(new) + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if isinstance(f, NotOp) and f.op.child is n: + return node_set + node.old |=3D {n} + return node.expand(node_set) + +class Literal: + def __init__(self, value: bool): + self.value =3D value + + def __iter__(self): + yield from () + + def __hash__(self): + return hash(self.value) + + def __str__(self): + if self.value: + return "true" + return "false" + + def negate(self): + self.value =3D not self.value + return self + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.value: + return node_set + node.old |=3D {n} + return node.expand(node_set) + +def p_spec(p): + ''' + spec : assign + | assign spec + ''' + if len(p) =3D=3D 3: + p[2].append(p[1]) + p[0] =3D p[2] + else: + p[0] =3D [p[1]] + +def p_assign(p): + ''' + assign : VARIABLE ASSIGN ltl + ''' + p[0] =3D (p[1], p[3]) + +def p_ltl(p): + ''' + ltl : opd + | binop + | unop + ''' + p[0] =3D p[1] + +def p_opd(p): + ''' + opd : VARIABLE + | LITERAL + | LPAREN ltl RPAREN + ''' + if p[1] =3D=3D "true": + p[0] =3D ASTNode(Literal(True)) + elif p[1] =3D=3D "false": + p[0] =3D ASTNode(Literal(False)) + elif p[1] =3D=3D '(': + p[0] =3D p[2] + else: + p[0] =3D ASTNode(Variable(p[1])) + +def p_unop(p): + ''' + unop : ALWAYS ltl + | EVENTUALLY ltl + | NOT ltl + ''' + if p[1] =3D=3D "always": + op =3D AlwaysOp(p[2]) + elif p[1] =3D=3D "eventually": + op =3D EventuallyOp(p[2]) + elif p[1] =3D=3D "not": + op =3D NotOp(p[2]) + else: + raise ValueError(f"Invalid unary operator {p[1]}") + + p[0] =3D ASTNode(op) + +def p_binop(p): + ''' + binop : opd UNTIL ltl + | opd AND ltl + | opd OR ltl + | opd IMPLY ltl + ''' + if p[2] =3D=3D "and": + op =3D AndOp(p[1], p[3]) + elif p[2] =3D=3D "until": + op =3D UntilOp(p[1], p[3]) + elif p[2] =3D=3D "or": + op =3D OrOp(p[1], p[3]) + elif p[2] =3D=3D "imply": + op =3D ImplyOp(p[1], p[3]) + else: + raise ValueError(f"Invalid binary operator {p[2]}") + + p[0] =3D ASTNode(op) + +parser =3D yacc() + +def parse_ltl(s: str) -> ASTNode: + spec =3D parser.parse(s) + + rule =3D None + subexpr =3D {} + + for assign in spec: + if assign[0] =3D=3D "RULE": + rule =3D assign[1] + else: + subexpr[assign[0]] =3D assign[1] + + if rule is None: + raise ValueError("Please define your specification in the \"RULE = =3D \" format") + + for node in rule: + if not isinstance(node.op, Variable): + continue + replace =3D subexpr.get(node.op.name) + if replace is not None: + node.op =3D replace.op + + return rule + +def create_graph(s: str): + atoms =3D set() + + ltl =3D parse_ltl(s) + for c in ltl: + c.normalize() + if isinstance(c.op, Variable): + atoms.add(c.op.name) + + init =3D GraphNode(set(), set(), set(), set()) + head =3D GraphNode({init}, {ltl}, set(), set()) + graph =3D sorted(head.expand(set())) + + for i, node in enumerate(graph): + # The id assignment during graph generation has gaps. Reassign them + node.id =3D i + + for incoming in node.incoming: + if incoming is init: + node.init =3D True + else: + incoming.outgoing.add(node) + for o in node.old: + if not o.op.is_temporal(): + node.labels.add(str(o)) + + return sorted(atoms), graph, ltl diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/r= vgen/rvgen/ltl2k.py new file mode 100644 index 000000000000..92e713861d86 --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -0,0 +1,252 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only + +from pathlib import Path +from . import generator +from . import ltl2ba + +COLUMN_LIMIT =3D 100 + +def line_len(line: str) -> int: + tabs =3D line.count('\t') + return tabs * 7 + len(line) + +def break_long_line(line: str, indent=3D'') -> list[str]: + result =3D [] + while line_len(line) > COLUMN_LIMIT: + i =3D line[:COLUMN_LIMIT - line_len(line)].rfind(' ') + result.append(line[:i]) + line =3D indent + line[i + 1:] + if line: + result.append(line) + return result + +def build_condition_string(node: ltl2ba.GraphNode): + if not node.labels: + return "(true)" + + result =3D "(" + + first =3D True + for label in sorted(node.labels): + if not first: + result +=3D " && " + result +=3D label + first =3D False + + result +=3D ")" + + return result + +def abbreviate_atoms(atoms: list[str]) -> list[str]: + def shorten(s: str) -> str: + skip =3D ["is", "by", "or", "and"] + return '_'.join([x[:2] for x in s.lower().split('_') if x not in s= kip]) + + abbrs =3D [] + for atom in atoms: + for i in range(len(atom), -1, -1): + if sum(a.startswith(atom[:i]) for a in atoms) > 1: + break + share =3D atom[:i] + unique =3D atom[i:] + abbrs.append((shorten(share) + shorten(unique))) + return abbrs + +class ltl2k(generator.Monitor): + template_dir =3D "ltl2k" + + def __init__(self, file_path, MonitorType, extra_params=3D{}): + if MonitorType !=3D "per_task": + raise NotImplementedError("Only per_task monitor is supported = for LTL") + super().__init__(extra_params) + with open(file_path) as f: + self.atoms, self.ba, self.ltl =3D ltl2ba.create_graph(f.read()) + self.atoms_abbr =3D abbreviate_atoms(self.atoms) + self.name =3D extra_params.get("model_name") + if not self.name: + self.name =3D Path(file_path).stem + + def _fill_states(self) -> str: + buf =3D [ + "enum ltl_buchi_state {", + ] + + for node in self.ba: + buf.append("\tS%i," % node.id) + buf.append("\tRV_NUM_BA_STATES") + buf.append("};") + buf.append("static_assert(RV_NUM_BA_STATES <=3D RV_MAX_BA_STATES);= ") + return buf + + def _fill_atoms(self): + buf =3D ["enum ltl_atom {"] + for a in sorted(self.atoms): + buf.append("\tLTL_%s," % a) + buf.append("\tLTL_NUM_ATOM") + buf.append("};") + buf.append("static_assert(LTL_NUM_ATOM <=3D RV_MAX_LTL_ATOM);") + return buf + + def _fill_atoms_to_string(self): + buf =3D [ + "static const char *ltl_atom_str(enum ltl_atom atom)", + "{", + "\tstatic const char *const names[] =3D {" + ] + + for name in self.atoms_abbr: + buf.append("\t\t\"%s\"," % name) + + buf.extend([ + "\t};", + "", + "\treturn names[atom];", + "}" + ]) + return buf + + def _fill_atom_values(self): + buf =3D [] + for node in self.ltl: + if node.op.is_temporal(): + continue + + if isinstance(node.op, ltl2ba.Variable): + buf.append("\tbool %s =3D test_bit(LTL_%s, mon->atoms);" %= (node, node.op.name)) + elif isinstance(node.op, ltl2ba.AndOp): + buf.append("\tbool %s =3D %s && %s;" % (node, node.op.left= , node.op.right)) + elif isinstance(node.op, ltl2ba.OrOp): + buf.append("\tbool %s =3D %s || %s;" % (node, node.op.left= , node.op.right)) + elif isinstance(node.op, ltl2ba.NotOp): + buf.append("\tbool %s =3D !%s;" % (node, node.op.child)) + buf.reverse() + + buf2 =3D [] + for line in buf: + buf2.extend(break_long_line(line, "\t ")) + return buf2 + + def _fill_transitions(self): + buf =3D [ + "static void", + "ltl_possible_next_states(struct ltl_monitor *mon, unsigned in= t state, unsigned long *next)", + "{" + ] + buf.extend(self._fill_atom_values()) + buf.extend([ + "", + "\tswitch (state) {" + ]) + + for node in self.ba: + buf.append("\tcase S%i:" % node.id) + + for o in sorted(node.outgoing): + line =3D "\t\tif " + indent =3D "\t\t " + + line +=3D build_condition_string(o) + lines =3D break_long_line(line, indent) + buf.extend(lines) + + buf.append("\t\t\t__set_bit(S%i, next);" % o.id) + buf.append("\t\tbreak;") + buf.extend([ + "\t}", + "}" + ]) + + return buf + + def _fill_start(self): + buf =3D [ + "static void ltl_start(struct task_struct *task, struct ltl_mo= nitor *mon)", + "{" + ] + buf.extend(self._fill_atom_values()) + buf.append("") + + for node in self.ba: + if not node.init: + continue + + line =3D "\tif " + indent =3D "\t " + + line +=3D build_condition_string(node) + lines =3D break_long_line(line, indent) + buf.extend(lines) + + buf.append("\t\t__set_bit(S%i, mon->states);" % node.id) + buf.append("}") + return buf + + def fill_tracepoint_handlers_skel(self): + buff =3D [] + buff.append("static void handle_example_event(void *data, /* XXX: = fill header */)") + buff.append("{") + buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.= atoms[0]) + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, han= dle_example_event);" \ + % self.name + + def fill_tracepoint_detach_helper(self): + return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, han= dle_sample_event);" \ + % self.name + + def fill_atoms_init(self): + buff =3D [] + for a in self.atoms: + buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a) + return '\n'.join(buff) + + def fill_model_h(self): + buf =3D [ + "/* SPDX-License-Identifier: GPL-2.0 */", + "", + "/*", + " * C implementation of Buchi automaton, automatically generat= ed by", + " * tools/verification/rvgen from the linear temporal logic sp= ecification.", + " * For further information, see kernel documentation:", + " * Documentation/trace/rv/linear_temporal_logic.rst", + " */", + "", + "#include ", + "", + "#define MONITOR_NAME " + self.name, + "" + ] + + buf.extend(self._fill_atoms()) + buf.append('') + + buf.extend(self._fill_atoms_to_string()) + buf.append('') + + buf.extend(self._fill_states()) + buf.append('') + + buf.extend(self._fill_start()) + buf.append('') + + buf.extend(self._fill_transitions()) + buf.append('') + + return '\n'.join(buf) + + def fill_monitor_class_type(self): + return "LTL_MON_EVENTS_ID" + + def fill_monitor_class(self): + return "ltl_monitor_id" + + def fill_main_c(self): + main_c =3D super().fill_main_c() + main_c =3D main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init()) + + return main_c diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/= verification/rvgen/rvgen/templates/ltl2k/main.c new file mode 100644 index 000000000000..f85d076fbf78 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c @@ -0,0 +1,102 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "%%MODEL_NAME%%" + +/* + * XXX: include required tracepoint headers, e.g., + * #include + */ +#include +%%INCLUDE_PARENT%% + +/* + * This is the self-generated part of the monitor. Generally, there is no = need + * to touch this section. + */ +#include "%%MODEL_NAME%%.h" +#include + +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *= mon) +{ + /* + * This is called everytime the Buchi automaton is triggered. + * + * This function could be used to fetch the atomic propositions which + * are expensive to trace. It is possible only if the atomic proposition + * does not need to be updated at precise time. + * + * It is recommended to use tracepoints and ltl_atom_update() instead. + */ +} + +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *m= on, bool task_creation) +{ + /* + * This should initialize as many atomic propositions as possible. + * + * @task_creation indicates whether the task is being created. This is + * false if the task is already running before the monitor is enabled. + */ +%%ATOMS_INIT%% +} + +/* + * This is the instrumentation part of the monitor. + * + * This is the section where manual work is required. Here the kernel even= ts + * are translated into model's event. + */ +%%TRACEPOINT_HANDLERS_SKEL%% +static int enable_%%MODEL_NAME%%(void) +{ + int retval; + + retval =3D ltl_monitor_init(); + if (retval) + return retval; + +%%TRACEPOINT_ATTACH%% + + return 0; +} + +static void disable_%%MODEL_NAME%%(void) +{ +%%TRACEPOINT_DETACH%% + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_%%MODEL_NAME%% =3D { + .name =3D "%%MODEL_NAME%%", + .description =3D "%%DESCRIPTION%%", + .enable =3D enable_%%MODEL_NAME%%, + .disable =3D disable_%%MODEL_NAME%%, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_%%MODEL_NAME%%); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR(/* TODO */); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h b/tools= /verification/rvgen/rvgen/templates/ltl2k/trace.h new file mode 100644 index 000000000000..49394c4b0f1c --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% +DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *= next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 3CC9925CC74 for ; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; cv=none; b=rV4cHSn/TXlUj6FhDvBY5X3cTAXYNeEysjDLFeYO5EcuWPwf6H/NCGrRjco33TYcpaEUiMqJPppY3KLbyvzXagb8C/2v9Dty9OTiP6I0bDu7VVOzosbTfRHOqpUCWHW18b7iGMTvKuwKjx/Ht88JFr+AxgWNiL9vBqYbQUhBUBw= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; c=relaxed/simple; bh=ZISno9eS5a6bTSGSn8Ss3fpvtTwzj7g+0Knv26qUhm8=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=bng4QVthmfRe0URvtTeLYbanq+l6zoH0+DMMyYV7sVq1NaViq26IaXmY5vOJZg8zt0MCB19Py8MsefHkpMruHFoq5eLg1x2PNK1f9cn4I79Meq3w68Gd2D35ZL8UX2lisalVEL61t8dJ84GlMmlKwjjPpGYkDIcTyvpYvIHzbEg= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=LADCA8+1; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="LADCA8+1" Received: by smtp.kernel.org (Postfix) with ESMTPSA id EC911C4CEEF; Fri, 25 Jul 2025 20:34:19 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475660; bh=ZISno9eS5a6bTSGSn8Ss3fpvtTwzj7g+0Knv26qUhm8=; h=Date:From:To:Cc:Subject:References:From; b=LADCA8+1JIg32Lpm4UekHWq0CCinLSaKjxg5hodhm746g4utxyq4SAh6Ea3o+W0L6 i5PQH34ceJ9QhOzjMp/nKdCldkEAAQ31bsKyQutp9k4CJkoBLm6xU+U2iDVgaUYwmd BuNEjLijznzK00EEW8WlmJs//ZWw66FSJTsfX9LUg4okFe/ZitCaNvHqeQYiwU0Omn TR9H+Vxo9I23aM0eIyDcOLcJUX6jFTuvXWiQec2PnJ+2fAJFvG6T47+XvjQdyDLzFM 2jcHc6RBSjrgNTA8NI/1yi/CS3cBW+sSdeFPcdkFId5dyMo52Cdr9iRjoMI5V+U1IC MkemKdvf3IeVg== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7a-00000001Qhq-0OHy; Fri, 25 Jul 2025 16:34:26 -0400 Message-ID: <20250725203425.948530483@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:09 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 12/25] Documentation/rv: Add documentation for linear temporal logic monitors References: <20250725203357.087558746@kernel.org> 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="utf-8" Content-Transfer-Encoding: quoted-printable From: Nam Cao Add documents describing linear temporal logic runtime verification monitors and how to generate them using rvgen. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/be13719e66fd8da147d7c69d5365aa23c52b743f.1751= 634289.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- Documentation/trace/rv/index.rst | 1 + .../trace/rv/linear_temporal_logic.rst | 133 +++++++++++++++ Documentation/trace/rv/monitor_synthesis.rst | 156 ++++++++++++++++-- 3 files changed, 274 insertions(+), 16 deletions(-) create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/inde= x.rst index 9a2342bd20ca..a2812ac5cfeb 100644 --- a/Documentation/trace/rv/index.rst +++ b/Documentation/trace/rv/index.rst @@ -8,6 +8,7 @@ Runtime Verification =20 runtime-verification.rst deterministic_automata.rst + linear_temporal_logic.rst monitor_synthesis.rst da_monitor_instrumentation.rst monitor_wip.rst diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentati= on/trace/rv/linear_temporal_logic.rst new file mode 100644 index 000000000000..57f107fcf6dd --- /dev/null +++ b/Documentation/trace/rv/linear_temporal_logic.rst @@ -0,0 +1,133 @@ +Linear temporal logic +=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D + +Introduction +------------ + +Runtime verification monitor is a verification technique which checks that= the +kernel follows a specification. It does so by using tracepoints to monitor= the +kernel's execution trace, and verifying that the execution trace sastifies= the +specification. + +Initially, the specification can only be written in the form of determinis= tic +automaton (DA). However, while attempting to implement DA monitors for so= me +complex specifications, deterministic automaton is found to be inappropria= te as +the specification language. The automaton is complicated, hard to understa= nd, +and error-prone. + +Thus, RV monitors based on linear temporal logic (LTL) are introduced. Thi= s type +of monitor uses LTL as specification instead of DA. For some cases, writin= g the +specification as LTL is more concise and intuitive. + +Many materials explain LTL in details. One book is:: + + Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, Th= e MIT + Press, 2008. + +Grammar +------- + +Unlike some existing syntax, kernel's implementation of LTL is more verbos= e. +This is motivated by considering that the people who read the LTL specific= ations +may not be well-versed in LTL. + +Grammar: + ltl ::=3D opd | ( ltl ) | ltl binop ltl | unop ltl + +Operands (opd): + true, false, user-defined names consisting of upper-case characters, d= igits, + and underscore. + +Unary Operators (unop): + always + eventually + not + +Binary Operators (binop): + until + and + or + imply + equivalent + +This grammar is ambiguous: operator precedence is not defined. Parentheses= must +be used. + +Example linear temporal logic +----------------------------- +.. code-block:: + + RAIN imply (GO_OUTSIDE imply HAVE_UMBRELLA) + +means: if it is raining, going outside means having an umbrella. + +.. code-block:: + + RAIN imply (WET until not RAIN) + +means: if it is raining, it is going to be wet until the rain stops. + +.. code-block:: + + RAIN imply eventually not RAIN + +means: if it is raining, rain will eventually stop. + +The above examples are referring to the current time instance only. For ke= rnel +verification, the `always` operator is usually desirable, to specify that +something is always true at the present and for all future. For example:: + + always (RAIN imply eventually not RAIN) + +means: *all* rain eventually stops. + +In the above examples, `RAIN`, `GO_OUTSIDE`, `HAVE_UMBRELLA` and `WET` are= the +"atomic propositions". + +Monitor synthesis +----------------- + +To synthesize an LTL into a kernel monitor, the `rvgen` tool can be used: +`tools/verification/rvgen`. The specification needs to be provided as a fi= le, +and it must have a "RULE =3D LTL" assignment. For example:: + + RULE =3D always (ACQUIRE imply ((not KILLED and not CRASHED) until REL= EASE)) + +which says: if `ACQUIRE`, then `RELEASE` must happen before `KILLED` or +`CRASHED`. + +The LTL can be broken down using sub-expressions. The above is equivalent = to: + + .. code-block:: + + RULE =3D always (ACQUIRE imply (ALIVE until RELEASE)) + ALIVE =3D not KILLED and not CRASHED + +From this specification, `rvgen` generates the C implementation of a Buchi +automaton - a non-deterministic state machine which checks the satisfiabil= ity of +the LTL. See Documentation/trace/rv/monitor_synthesis.rst for details on u= sing +`rvgen`. + +References +---------- + +One book covering model checking and linear temporal logic is:: + + Christel Baier and Joost-Pieter Katoen: Principles of Model Checking, Th= e MIT + Press, 2008. + +For an example of using linear temporal logic in software testing, see:: + + Ruijie Meng, Zhen Dong, Jialin Li, Ivan Beschastnikh, and Abhik Roychoud= hury. + 2022. Linear-time temporal logic guided greybox fuzzing. In Proceedings = of the + 44th International Conference on Software Engineering (ICSE '22). Assoc= iation + for Computing Machinery, New York, NY, USA, 1343=E2=80=931355. + https://doi.org/10.1145/3510003.3510082 + +The kernel's LTL monitor implementation is based on:: + + Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). Simple On-the-fly + Automatic Verification of Linear Temporal Logic. In: Dembi=C5=84ski, P.,= =C5=9Aredniawa, + M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995.= IFIP + Advances in Information and Communication Technology. Springer, Boston, = MA. + https://doi.org/10.1007/978-0-387-34892-6_1 diff --git a/Documentation/trace/rv/monitor_synthesis.rst b/Documentation/t= race/rv/monitor_synthesis.rst index 85624062073b..ac808a7554f5 100644 --- a/Documentation/trace/rv/monitor_synthesis.rst +++ b/Documentation/trace/rv/monitor_synthesis.rst @@ -39,16 +39,18 @@ below:: RV monitor synthesis -------------------- =20 -The synthesis of automata-based models into the Linux *RV monitor* abstrac= tion -is automated by the rvgen tool and the rv/da_monitor.h header file that -contains a set of macros that automatically generate the monitor's code. +The synthesis of a specification into the Linux *RV monitor* abstraction is +automated by the rvgen tool and the header file containing common code for +creating monitors. The header files are: + + * rv/da_monitor.h for deterministic automaton monitor. + * rv/ltl_monitor.h for linear temporal logic monitor. =20 rvgen ----- =20 -The rvgen utility leverages dot2c by converting an automaton model in -the DOT format into the C representation [1] and creating the skeleton of -a kernel monitor in C. +The rvgen utility converts a specification into the C presentation and cre= ating +the skeleton of a kernel monitor in C. =20 For example, it is possible to transform the wip.dot model present in [1] into a per-cpu monitor with the following command:: @@ -63,18 +65,38 @@ This will create a directory named wip/ with the follow= ing files: The wip.c file contains the monitor declaration and the starting point for the system instrumentation. =20 -Monitor macros --------------- +Similarly, a linear temporal logic monitor can be generated with the follo= wing +command:: + + $ rvgen monitor -c ltl -s pagefault.ltl -t per_task + +This generates pagefault/ directory with: + +- pagefault.h: The Buchi automaton (the non-deterministic state machine to + verify the specification) +- pagefault.c: The skeleton for the RV monitor + +Monitor header files +-------------------- + +The header files: + +- `rv/da_monitor.h` for deterministic automaton monitor +- `rv/ltl_monitor` for linear temporal logic monitor + +include common macros and static functions for implementing *Monitor +Instance(s)*. =20 -The rv/da_monitor.h enables automatic code generation for the *Monitor -Instance(s)* using C macros. +The benefits of having all common functionalities in a single header file = are +3-fold: =20 -The benefits of the usage of macro for monitor synthesis are 3-fold as it: + - Reduce the code duplication; + - Facilitate the bug fix/improvement; + - Avoid the case of developers changing the core of the monitor code to + manipulate the model in a (let's say) non-standard way. =20 -- 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. +rv/da_monitor.h ++++++++++++++++ =20 This initial implementation presents three different types of monitor inst= ances: =20 @@ -130,10 +152,112 @@ While the event "preempt_enabled" will use:: To notify the monitor that the system will be returning to the initial sta= te, so the system and the monitor should be in sync. =20 +rv/ltl_monitor.h +++++++++++++++++ +This file must be combined with the $(MODEL_NAME).h file (generated by `rv= gen`) +to be complete. For example, for the `pagefault` monitor, the `pagefault.c` +source file must include:: + + #include "pagefault.h" + #include + +(the skeleton monitor file generated by `rvgen` already does this). + +`$(MODEL_NAME).h` (`pagefault.h` in the above example) includes the +implementation of the Buchi automaton - a non-deterministic state machine = that +verifies the LTL specification. While `rv/ltl_monitor.h` includes the comm= on +helper functions to interact with the Buchi automaton and to implement an = RV +monitor. An important definition in `$(MODEL_NAME).h` is:: + + enum ltl_atom { + LTL_$(FIRST_ATOMIC_PROPOSITION), + LTL_$(SECOND_ATOMIC_PROPOSITION), + ... + LTL_NUM_ATOM + }; + +which is the list of atomic propositions present in the LTL specification +(prefixed with "LTL\_" to avoid name collision). This `enum` is passed to = the +functions interacting with the Buchi automaton. + +While generating code, `rvgen` cannot understand the meaning of the atomic +propositions. Thus, that task is left for manual work. The recommended pra= tice +is adding tracepoints to places where the atomic propositions change; and = in the +tracepoints' handlers: the Buchi automaton is executed using:: + + void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool = value) + +which tells the Buchi automaton that the atomic proposition `atom` is now +`value`. The Buchi automaton checks whether the LTL specification is still +satisfied, and invokes the monitor's error tracepoint and the reactor if +violation is detected. + +Tracepoints and `ltl_atom_update()` should be used whenever possible. Howe= ver, +it is sometimes not the most convenient. For some atomic propositions whic= h are +changed in multiple places in the kernel, it is cumbersome to trace all th= ose +places. Furthermore, it may not be important that the atomic propositions = are +updated at precise times. For example, considering the following linear te= mporal +logic:: + + RULE =3D always (RT imply not PAGEFAULT) + +This LTL states that a real-time task does not raise page faults. For this +specification, it is not important when `RT` changes, as long as it has the +correct value when `PAGEFAULT` is true. Motivated by this case, another +function is introduced:: + + void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon) + +This function is called whenever the Buchi automaton is triggered. Therefo= re, it +can be manually implemented to "fetch" `RT`:: + + void ltl_atom_fetch(struct task_struct *task, struct ltl_monitor *mon) + { + ltl_atom_set(mon, LTL_RT, rt_task(task)); + } + +Effectively, whenever `PAGEFAULT` is updated with a call to `ltl_atom_upda= te()`, +`RT` is also fetched. Thus, the LTL specification can be verified without +tracing `RT` everywhere. + +For atomic propositions which act like events, they usually need to be set= (or +cleared) and then immediately cleared (or set). A convenient function is +provided:: + + void ltl_atom_pulse(struct task_struct *task, enum ltl_atom atom, bool v= alue) + +which is equivalent to:: + + ltl_atom_update(task, atom, value); + ltl_atom_update(task, atom, !value); + +To initialize the atomic propositions, the following function must be +implemented:: + + ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool t= ask_creation) + +This function is called for all running tasks when the monitor is enabled.= It is +also called for new tasks created after the enabling the monitor. It should +initialize as many atomic propositions as possible, for example:: + + void ltl_atom_init(struct task_struct *task, struct ltl_monitor *mon, bo= ol task_creation) + { + ltl_atom_set(mon, LTL_RT, rt_task(task)); + if (task_creation) + ltl_atom_set(mon, LTL_PAGEFAULT, false); + } + +Atomic propositions not initialized by `ltl_atom_init()` will stay in the +unknown state until relevant tracepoints are hit, which can take some time= . As +monitoring for a task cannot be done until all atomic propositions is know= n for +the task, the monitor may need some time to start validating tasks which h= ave +been running before the monitor is enabled. Therefore, it is recommended to +start the tasks of interest after enabling the monitor. + Final remarks ------------- =20 -With the monitor synthesis in place using the rv/da_monitor.h and +With the monitor synthesis in place using the header files and rvgen, the developer's work should be limited to the instrumentation of the system, increasing the confidence in the overall approach. =20 --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 7BB1125FA0A for ; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; cv=none; b=Q+G00jf7l3VGSmG1gAEKAhktrdRnGoQyVcvbc+tOhloUzZI4zwjCWevqKlc8mRuFw/Qisw0HDsLay11Oxls8+8DuCJlETIAlD39/5s9fgS0b9zEA5WPxAJIKwfsbZt+h+2jYqRdNQWDVKVtCt48MxxdzgNGOLT66ZRFZHufT9ZM= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; c=relaxed/simple; bh=aCHzKauITVbkU95T3gbGxEkQQvBBWjzWN4yhLLim4IU=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=UzqzIxgK9/VeS0l1pn69mAvLCkUyjxrwHewvOj7Si8bU05X1HDMMSEIyLeLrFzgUM9ChR8V1GPan+AGXIwI+rLb8FaNisCxwnC7UsLl58f4j8jIvkJPvnBKmxwTsm9ziI9awg4TGgeOJciOUblp2EmrBmkCTGd9AbV7k6ZNaCaU= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=EHBu6pEe; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="EHBu6pEe" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 21247C4CEF6; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475660; bh=aCHzKauITVbkU95T3gbGxEkQQvBBWjzWN4yhLLim4IU=; h=Date:From:To:Cc:Subject:References:From; b=EHBu6pEeK38XLQwp/wMtOanXO6kTx/Ry4zGnTFHHg6H3nEVv2qoJMkEjnp9zowTfh slJpYEF1BT/VElhkwvvrtp06fuxtboYUqGdT4NZRh5arTWO4s8DpIeQQdppjgrh242 CDYeUO12+56iEm/rIFSNQsDYKLTL//vn0lpUBXjZi2mD1PedX/e10AMdbW7/P1rrYx RjUTy6UZLknPRkI/pdZRBxds4EBF40drxALk1s6uP5GVJ2J2V7UFHJhhuVKVc/7OER A3XYOxG+HI+x70CCmRrPLUgbeSYNVtEJB87gyW7r2tyTX7OitAJ7jpSKmPBmy3f0Nl V1PU2u4+h1dUw== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7a-00000001QiL-17Mq; Fri, 25 Jul 2025 16:34:26 -0400 Message-ID: <20250725203426.115179584@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:10 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , John Ogness , Masami Hiramatsu , Mathieu Desnoyers , Nam Cao , Gabriele Monaco Subject: [for-next][PATCH 13/25] verification/rvgen: Support the next operator References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao The 'next' operator is a unary operator. It is defined as: "next time, the operand must be true". Support this operator. For RV monitors, "next time" means the next invocation of ltl_validate(). Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/9c32cec04dd18d2e956fddd84b0e0a2503daa75a.1752= 239482.git.namcao@linutronix.de Signed-off-by: Nam Cao Tested-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) --- .../trace/rv/linear_temporal_logic.rst | 1 + tools/verification/rvgen/rvgen/ltl2ba.py | 26 +++++++++++++++++++ 2 files changed, 27 insertions(+) diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentati= on/trace/rv/linear_temporal_logic.rst index 57f107fcf6dd..9eee09d9cacf 100644 --- a/Documentation/trace/rv/linear_temporal_logic.rst +++ b/Documentation/trace/rv/linear_temporal_logic.rst @@ -41,6 +41,7 @@ Operands (opd): Unary Operators (unop): always eventually + next not =20 Binary Operators (binop): diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/= rvgen/rvgen/ltl2ba.py index d11840af7f5f..f14e6760ac3d 100644 --- a/tools/verification/rvgen/rvgen/ltl2ba.py +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -19,6 +19,7 @@ from ply.yacc import yacc # Unary Operators (unop): # always # eventually +# next # not # # Binary Operators (binop): @@ -35,6 +36,7 @@ tokens =3D ( 'UNTIL', 'ALWAYS', 'EVENTUALLY', + 'NEXT', 'VARIABLE', 'LITERAL', 'NOT', @@ -48,6 +50,7 @@ t_OR =3D r'or' t_IMPLY =3D r'imply' t_UNTIL =3D r'until' t_ALWAYS =3D r'always' +t_NEXT =3D r'next' t_EVENTUALLY =3D r'eventually' t_VARIABLE =3D r'[A-Z_0-9]+' t_LITERAL =3D r'true|false' @@ -327,6 +330,26 @@ class AlwaysOp(UnaryOp): # ![]F =3D=3D <>(!F) return EventuallyOp(self.child.negate()).normalize() =20 +class NextOp(UnaryOp): + def normalize(self): + return self + + def _is_temporal(self): + return True + + def negate(self): + # not (next A) =3D=3D next (not A) + self.child =3D self.child.negate() + return self + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + tmp =3D GraphNode(node.incoming, + node.new, + node.old | {n}, + node.next | {n.op.child}) + return tmp.expand(node_set) + class NotOp(UnaryOp): def __str__(self): return "!" + str(self.child) @@ -452,12 +475,15 @@ def p_unop(p): ''' unop : ALWAYS ltl | EVENTUALLY ltl + | NEXT ltl | NOT ltl ''' if p[1] =3D=3D "always": op =3D AlwaysOp(p[2]) elif p[1] =3D=3D "eventually": op =3D EventuallyOp(p[2]) + elif p[1] =3D=3D "next": + op =3D NextOp(p[2]) elif p[1] =3D=3D "not": op =3D NotOp(p[2]) else: --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 6A93B25D216 for ; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; cv=none; b=SvQ0QBXCsoQ2xBFM+ryY5Buoyc2aaWVo23bTVN9isT66ePRH46jErFo8enO0UND75Yg3hMs25FD4sKItS+T/W9z3pfKsbWMy/9bcZu24iEj8Z6VMS7pejgBZ5cDuqw/1h/yEeyttGFs/WxIM/u6McliBVDHJJ7l3M16t+3foVRc= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; c=relaxed/simple; bh=jT6VsTh7t2bLtsbZyW2hkaBCthCsV0UlHy6KPrDqwxk=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=oPw/ziwVQ8TDzekM7H4wYtSRtiu1M8xuXR2fBnN5b2a1RivdyaYMpJmonBNTPo1d/HPpxySAFHhVAjE2qRoWUvJC8niUw25chYie2OsIpH8TZW6XlwDKjIZ9aRdCgasOxPW+w7f6lyIgZl/8HgUNK+C++wFSu3vJAHUSZ7ens5M= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=f6YURAYo; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="f6YURAYo" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 489C3C4AF09; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475660; bh=jT6VsTh7t2bLtsbZyW2hkaBCthCsV0UlHy6KPrDqwxk=; h=Date:From:To:Cc:Subject:References:From; b=f6YURAYoaTsgY6EPCB9gIELyi1biojaP/35Ybn5ZfJvi5FeieuG6U8Uejqc5b50la bzsCeBg3XrknTtvpKcdsgERCvFCDcmwZyWwnrs/QGOMi3Xg0mvBgTm5c33rE4z4k5c tAHtlaX4tMIShjQae0UofuyBElVmS3TRXnKrxc4Sgr+7uXFGvY7xl5lob0NEIGolaq m7nvsvUVHilxHi2Epl2OP8LgXTojKyMUksinBntuERKEuRtkoN9hzSY9yahTSwmNsR XINuVdAzUxmS9jDVqsQt6eJ6yERPeXUO16W5bTQ/BA6T9l99s5Gyyak3ya1A56Hi3H 7NzTdV14aBZfQ== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7a-00000001Qir-1ozP; Fri, 25 Jul 2025 16:34:26 -0400 Message-ID: <20250725203426.287986900@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:11 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 14/25] verification/rvgen: Generate each variable definition only once References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao If a variable appears multiple times in the specification, ltl2k generates multiple variable definitions. This fails the build. Make sure each variable is only defined once. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/107dcf0d0aa8482d5fbe0314c3138f61cd284e91.1752= 850449.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- tools/verification/rvgen/rvgen/ltl2k.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/r= vgen/rvgen/ltl2k.py index 92e713861d86..59da351792ec 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -112,14 +112,16 @@ class ltl2k(generator.Monitor): if node.op.is_temporal(): continue =20 - if isinstance(node.op, ltl2ba.Variable): - buf.append("\tbool %s =3D test_bit(LTL_%s, mon->atoms);" %= (node, node.op.name)) - elif isinstance(node.op, ltl2ba.AndOp): + if isinstance(node.op, ltl2ba.AndOp): buf.append("\tbool %s =3D %s && %s;" % (node, node.op.left= , node.op.right)) elif isinstance(node.op, ltl2ba.OrOp): buf.append("\tbool %s =3D %s || %s;" % (node, node.op.left= , node.op.right)) elif isinstance(node.op, ltl2ba.NotOp): buf.append("\tbool %s =3D !%s;" % (node, node.op.child)) + + for atom in self.atoms: + buf.append("\tbool %s =3D test_bit(LTL_%s, mon->atoms);" % (at= om.lower(), atom)) + buf.reverse() =20 buf2 =3D [] --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 8E6EB25D8F0 for ; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; cv=none; b=Kjmgop3LYkJ356JqhY6+XI0+3VrsHKG5oTa7QADXybERxLojYT1zqpRiH4EGBRXTagGMmYGKBJAR9tGrbDdfIaFouOQxOo3MnlHijkKS393q7sesgzsn4dIPZiE44+uj/Mti6EoUZntcZALmXthv+u6pXbQ7h7c5y3Kfctft890= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; c=relaxed/simple; bh=dV9ILFIh/3u1oAiaH6inUJD2barGO5qcmaWu31d+lZc=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=b1Aue/UsOt605e4uIc8lOXMMmDpOBKN7lQtbNu6lpYfkhz+3G37DzZkQM2sX4GXax90pBkFfUjf2ut4trzWDZ45YEqA+xflfr2TET+KsQMamUVNzk8xxPiluhGhmr5zXaP9wYE99pwmfiT8T86aX5uCw53h6WuHGyf69ilhi1/o= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=JTWQ7p00; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="JTWQ7p00" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 71127C4CEE7; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475660; bh=dV9ILFIh/3u1oAiaH6inUJD2barGO5qcmaWu31d+lZc=; h=Date:From:To:Cc:Subject:References:From; b=JTWQ7p00G3TTz7F+9okT4l1BDb/e50AUS+YuIIbpmelyYlU+82JS1vSSM3RhomTjJ y3rf0m5kZScaerSt/4xnSIMmxAK1qJBCDaRcKDoiD/h/8YduXKZVtzadfit3LHbIYB oKMBcENy4a1n5ukM+WykzQ9RRD7L/LE8wVTn+UIAYERcPacEIkcSDcy6kTByQxoCWg uW/tTFLHz35Sf9HD0UMeVxUaA1HLGFP6hErox1hxUpsLTCAFs5Pm+nmIkRlJchxJBv /+s7zcD4DGV5q+MMep8T7m6janxiZ0bhY4dBYkN1P0qq0W2du3AArF9nchyYbZRlgw dDCqTRQg+EHoA== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7a-00000001QjL-2WXa; Fri, 25 Jul 2025 16:34:26 -0400 Message-ID: <20250725203426.457432560@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:12 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Nam Cao , Gabriele Monaco Subject: [for-next][PATCH 15/25] verification/rvgen: Do not generate unused variables References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao ltl2k generates all variable definition in both ltl_start() and ltl_possible_next_states(). However, these two functions may not use all the variables, causing "unused variable" compiler warning. Change the script to only generate used variables. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/636b2b2d99a9bd46a9f77a078d44ebd7ffc7508c.1752= 850449.git.namcao@linutronix.de Signed-off-by: Nam Cao Reviewed-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) --- tools/verification/rvgen/rvgen/ltl2k.py | 25 +++++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/r= vgen/rvgen/ltl2k.py index 59da351792ec..b075f98d50c4 100644 --- a/tools/verification/rvgen/rvgen/ltl2k.py +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -106,20 +106,25 @@ class ltl2k(generator.Monitor): ]) return buf =20 - def _fill_atom_values(self): + def _fill_atom_values(self, required_values): buf =3D [] for node in self.ltl: - if node.op.is_temporal(): + if str(node) not in required_values: continue =20 if isinstance(node.op, ltl2ba.AndOp): buf.append("\tbool %s =3D %s && %s;" % (node, node.op.left= , node.op.right)) + required_values |=3D {str(node.op.left), str(node.op.right= )} elif isinstance(node.op, ltl2ba.OrOp): buf.append("\tbool %s =3D %s || %s;" % (node, node.op.left= , node.op.right)) + required_values |=3D {str(node.op.left), str(node.op.right= )} elif isinstance(node.op, ltl2ba.NotOp): buf.append("\tbool %s =3D !%s;" % (node, node.op.child)) + required_values.add(str(node.op.child)) =20 for atom in self.atoms: + if atom.lower() not in required_values: + continue buf.append("\tbool %s =3D test_bit(LTL_%s, mon->atoms);" % (at= om.lower(), atom)) =20 buf.reverse() @@ -135,7 +140,13 @@ class ltl2k(generator.Monitor): "ltl_possible_next_states(struct ltl_monitor *mon, unsigned in= t state, unsigned long *next)", "{" ] - buf.extend(self._fill_atom_values()) + + required_values =3D set() + for node in self.ba: + for o in sorted(node.outgoing): + required_values |=3D o.labels + + buf.extend(self._fill_atom_values(required_values)) buf.extend([ "", "\tswitch (state) {" @@ -166,7 +177,13 @@ class ltl2k(generator.Monitor): "static void ltl_start(struct task_struct *task, struct ltl_mo= nitor *mon)", "{" ] - buf.extend(self._fill_atom_values()) + + required_values =3D set() + for node in self.ba: + if node.init: + required_values |=3D node.labels + + buf.extend(self._fill_atom_values(required_values)) buf.append("") =20 for node in self.ba: --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 BD50C25DB12 for ; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; cv=none; b=gdx2ZhTo6FedYhSgUe3spP/XKvp80ZjSsmuOcEsmfokhDhooLdd5rDdMlDPNT2Ev/zm0Qi/u72SJ0SzdD33eT9yg6fYyfAlm4qJHQFhNFrwP8H8d/wFzU0ikj7YL7QU62/V1fTjB7a1zFsR1VFKZrmS3G//NtalzNhaiZd1axhc= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; c=relaxed/simple; bh=KOt0VqG5p6PfjLU6UfHkWtrmGh01+J8PpffJ4qd+E5g=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=pHsuGJuDoaU7XCbcJJaohrICTsvyScQgIUHNmw4Dfsni2qX/6oWn1BS7joRmue5y36Xxo7op8h04R9AbWhZvz7i+TE194qP6/3x9KsmY2aGVuPgWj2ixHirtUZ7s5hCuBEPG8qDTy38v5EN5pb8JCIyMYmpCSiw94hWTs+ZvCjc= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=KBaWFaZo; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="KBaWFaZo" Received: by smtp.kernel.org (Postfix) with ESMTPSA id A0AC4C4CEF8; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475660; bh=KOt0VqG5p6PfjLU6UfHkWtrmGh01+J8PpffJ4qd+E5g=; h=Date:From:To:Cc:Subject:References:From; b=KBaWFaZoylqva5wCDWTPDCqFkW0gY+b3UQ789xXleHE7hh1d03oZK/TpxI4NL3q4N 8XB7RLFpKkPgeA5U46Yrs8HPWExXo5NhSr70svLV5et3r8jXvvQyQlbqsfj5nhhb0k 1t2WyaMT/6bRg/TwAAuVikf3kBlMY9A3qbDAG6mt/6NVaLyYqs3ZJbirJqhTbrkKVs ZRvqCa/e3L9jeMJRorsYlaW0JAralNKJBcVs2Op5pGru8bqSi4bXelU9deE7AlVPb/ M+x5gLy816Ea8NlEvC7cSsJ9F5EYP5KBlJT7st/uqsjcutAIuQpbu8MuumDGBgM/wn Kr35sr0e7VkXg== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7a-00000001Qjq-3EII; Fri, 25 Jul 2025 16:34:26 -0400 Message-ID: <20250725203426.624183928@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:13 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Nam Cao , Juri Lelli , Clark Williams , Gabriele Monaco Subject: [for-next][PATCH 16/25] tools/rv: Do not skip idle in trace References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Gabriele Monaco Currently, the userspace RV tool skips trace events triggered by the RV tool itself, this can be changed by passing the parameter -s, which sets the variable config_my_pid to 0 (instead of the tool's PID). This has the side effect of skipping events generated by idle (PID 0). Set config_my_pid to -1 (an invalid pid) to avoid skipping idle. Cc: Nam Cao Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-2-gmonaco@redhat.com Fixes: 6d60f89691fc ("tools/rv: Add in-kernel monitor interface") Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) --- tools/verification/rv/src/in_kernel.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/= src/in_kernel.c index c0dcee795c0d..4bb746ea6e17 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -431,7 +431,7 @@ ikm_event_handler(struct trace_seq *s, struct tep_recor= d *record, =20 if (config_has_id && (config_my_pid =3D=3D id)) return 0; - else if (config_my_pid && (config_my_pid =3D=3D pid)) + else if (config_my_pid =3D=3D pid) return 0; =20 tep_print_event(trace_event->tep, s, record, "%16s-%-8d [%.3d] ", @@ -734,7 +734,7 @@ static int parse_arguments(char *monitor_name, int argc= , char **argv) config_reactor =3D optarg; break; case 's': - config_my_pid =3D 0; + config_my_pid =3D -1; break; case 't': config_trace =3D 1; --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 DE2C725DD1E for ; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; cv=none; b=EJlWAV9Oq9UqcTifVu2fKstOePYJyI5HpTSaovQbZBWRtr0jLOv27paQeN6Mkz6zWPv7YxsYSBaj8ZsloY4vif/XOcexhbRkhC55htK1OZ8VUA+pJf8khhNddVIyqIL4N1xD6EclHFfs9oQDbnb55Ht6DK2Y4/9wD3C+wJ+w4lg= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475660; c=relaxed/simple; bh=v3dRc6gn7lynJJ8xeHW8GTHQpld+ulORhv4T4YMRbqo=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=LMLq2CQ5+ZmRWC0o7VteHKHDf6mu5z+8uSQmxRTDfuW9cNDNt277/hEVAjEFxS7+y87f468gE14QJ0920NKgU1omAmuyJLUZRgQeuG7WOXI7/uvo7RPXAJRfw0XJxMCzjaxUl9zOlWl1i9Nvl2dInb0dNoF934MEM1cDtEDusyE= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=fAPZoiw9; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="fAPZoiw9" Received: by smtp.kernel.org (Postfix) with ESMTPSA id C14A2C4CEEF; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475660; bh=v3dRc6gn7lynJJ8xeHW8GTHQpld+ulORhv4T4YMRbqo=; h=Date:From:To:Cc:Subject:References:From; b=fAPZoiw9iaD3nENTz5hl19Nx1sIBM0dhhzWUePsXIo70lo0Xtqypjw26G/Ceu0lVl K6waiVKpcgnYBSGn0bE1UsxTnMIlg852zscpToBpiI7kF8Twbl9E6EV1ifNaCA6owI /6Etchoh6ObQgVxXdavFWGm3PmpcgkSftLmKpvTSXXekMe3c+FZHYRm2hlL+h0Q91u RQerX66Q/1FlclXGmj0s6htvGJ14ntOtiG67Q0oBrXiSvNkDeN4n3f3AQoOTRAj5ro wR/cieIJF2+Z0QZhqJl744ElyQxumVDefH2D39OEJhqXrip4sDBAOAC1ECdzOZNzLz XDy9FejB46SyQ== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7a-00000001QkL-3w2j; Fri, 25 Jul 2025 16:34:26 -0400 Message-ID: <20250725203426.791145358@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:14 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Nam Cao , Juri Lelli , Clark Williams , Gabriele Monaco Subject: [for-next][PATCH 17/25] tools/rv: Stop gracefully also on SIGTERM References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Gabriele Monaco Currently the userspace RV tool starts a monitor and waits for the user to press Ctrl-C (SIGINT) to terminate and stop the monitor. This doesn't account for a scenario where a user starts RV in background and simply kills it (SIGTERM unless the user specifies differently). E.g.: # rv mon wip & # kill % Would terminate RV without stopping the monitor and next RV executions won't start correctly. Register the signal handler used for SIGINT also to SIGTERM. Cc: Nam Cao Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-3-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) --- tools/verification/rv/src/rv.c | 1 + 1 file changed, 1 insertion(+) diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c index 239de054d1e0..b8fe24a87d97 100644 --- a/tools/verification/rv/src/rv.c +++ b/tools/verification/rv/src/rv.c @@ -191,6 +191,7 @@ int main(int argc, char **argv) * and exit. */ signal(SIGINT, stop_rv); + signal(SIGTERM, stop_rv); =20 rv_mon(argc - 1, &argv[1]); } --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 1165C25EFBC for ; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; cv=none; b=XgfndTpRk2BK1p7K1qKetkPHg6Yw6dBLEK5x/KmAL1T+CLo+sGh1s0VJ1HB8QT2/dH5G9Q1gP6igCEimfQNvBih100xUGwyWO3xBRrgdmqb/xLHiEGkw9RJDt+jF9r1KYe/o5RAk5/MCgCuH1djBXU/0Ddoj2LWScuLFt6HKl6Y= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; c=relaxed/simple; bh=HmPwwr0STQFM6zKduNr617yvWGb7nAv+yoQY4KfCDz4=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=CtaqqMK3GYXXKT+kCaytcIG2+byzV95GwVPtNMbPfiKvIvLBPLJJ2hDW2L1l7dAQCADE9/zXLN44G5MM3Zm1xhFL1kXhG3+xCLc+ixS7o+7pvB1F4MeTaoQ0lsMO21Hcy2zdL2Dojny2QTjJ9f3T5mskNNGkaF4aJQyvMuC23NE= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=nlWLQNrm; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="nlWLQNrm" Received: by smtp.kernel.org (Postfix) with ESMTPSA id EB5D8C4CEE7; Fri, 25 Jul 2025 20:34:20 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475661; bh=HmPwwr0STQFM6zKduNr617yvWGb7nAv+yoQY4KfCDz4=; h=Date:From:To:Cc:Subject:References:From; b=nlWLQNrmlt5OxTVnpiDZ5UZ7q3wCLX696E4r3A91FM2Z87jLJa1TUO9AL4VZa060Y Bq06jUuZSrB1mE2f66YjYZc/+vrp4leT5rRg/Jq8u6/aqE3ExCdFBIRUoAR5schcrS YmBRaYTGJ57V62ePpmziIV1a6j4ApaG0pGhW+SYiiyzkCAnFRqZgpod+6zsGvSS0nI m2y1T/6BpMfIcNNwrOh7ULHsh5RnIzjEJwcG+e22gnLNzOdP7KpX3Pd+VMobaYZJrq II5+elRwyBOr0rhhU+n6VHEiGn2g4RO0r9D/AVmzGLZnDBPEfb4ixtYgFUNKSNd+Ee XRQiGUlJQqf7g== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7b-00000001Qkq-0Rue; Fri, 25 Jul 2025 16:34:27 -0400 Message-ID: <20250725203426.960255412@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:15 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Juri Lelli , Clark Williams , Nam Cao , Gabriele Monaco Subject: [for-next][PATCH 18/25] tools/dot2c: Fix generated files going over 100 column limit References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Gabriele Monaco The dot2c.py script generates all states in a single line. This breaks the 100 column limit when the state machines are non-trivial. Change dot2c.py to generate the states in separate lines in case the generated line is going to be too long. Also adapt existing monitors with line length over the limit. Cc: Masami Hiramatsu Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-4-gmonaco@redhat.com Suggested-by: Nam Cao Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) --- kernel/trace/rv/monitors/snep/snep.h | 14 ++++++++++++-- tools/verification/rvgen/rvgen/dot2c.py | 20 +++++++++++--------- 2 files changed, 23 insertions(+), 11 deletions(-) diff --git a/kernel/trace/rv/monitors/snep/snep.h b/kernel/trace/rv/monitor= s/snep/snep.h index 6d16b9ad931e..4cd9abb77b7b 100644 --- a/kernel/trace/rv/monitors/snep/snep.h +++ b/kernel/trace/rv/monitors/snep/snep.h @@ -41,8 +41,18 @@ static const struct automaton_snep automaton_snep =3D { "schedule_exit" }, .function =3D { - { non_scheduling_context_snep, non_scheduling_context_snep, scheduling_c= ontex_snep, INVALID_STATE }, - { INVALID_STATE, INVALID_STATE, INV= ALID_STATE, non_scheduling_context_snep }, + { + non_scheduling_context_snep, + non_scheduling_context_snep, + scheduling_contex_snep, + INVALID_STATE + }, + { + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + non_scheduling_context_snep + }, }, .initial_state =3D non_scheduling_context_snep, .final_states =3D { 1, 0 }, diff --git a/tools/verification/rvgen/rvgen/dot2c.py b/tools/verification/r= vgen/rvgen/dot2c.py index 6009caf568d9..b9b6f14cc536 100644 --- a/tools/verification/rvgen/rvgen/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -152,28 +152,30 @@ class Dot2c(Automata): max_state_name =3D max(self.states, key =3D len).__len__() return max(max_state_name, self.invalid_state_str.__len__()) =20 - def __get_state_string_length(self): - maxlen =3D self.__get_max_strlen_of_states() + self.enum_suffix.__= len__() - return "%" + str(maxlen) + "s" - def get_aut_init_function(self): nr_states =3D self.states.__len__() nr_events =3D self.events.__len__() buff =3D [] =20 - strformat =3D self.__get_state_string_length() - + maxlen =3D self.__get_max_strlen_of_states() + len(self.enum_suffi= x) + tab_braces =3D 2 * 8 + 2 + 1 # "\t\t{ " ... "}" + comma_space =3D 2 # ", " count last comma here + linetoolong =3D tab_braces + (maxlen + comma_space) * nr_events > = self.line_length for x in range(nr_states): - line =3D "\t\t{ " + line =3D "\t\t{\n" if linetoolong else "\t\t{ " for y in range(nr_events): next_state =3D self.function[x][y] if next_state !=3D self.invalid_state_str: next_state =3D self.function[x][y] + self.enum_suffix =20 + if linetoolong: + line +=3D "\t\t\t%s" % next_state + else: + line +=3D "%*s" % (maxlen, next_state) if y !=3D nr_events-1: - line =3D line + strformat % next_state + ", " + line +=3D ",\n" if linetoolong else ", " else: - line =3D line + strformat % next_state + " }," + line +=3D "\n\t\t}," if linetoolong else " }," buff.append(line) =20 return self.__buff_to_string(buff) --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 40EA125F96D for ; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; cv=none; b=QT/+vFHbuLbamFkp6BDp7PUxassv1LUPbdi33Ay3cSy/QAfuuujll+Gv5LiP7vwpGXh2h+YfWGJLlzMhHAihmWIvjurTjRLXisIvfcHPxOd4fL/sQNbRH5K3DwDmmgWL+SITcZc1/rTTQt2FAr9aDYewd/shv+5Sn8gSSFz59Jo= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; c=relaxed/simple; bh=5npNIdNOxU6nl+F6cCfxhjYp6GZooHL2IR9nKtVZYgo=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=i3Db7NhNhFUPC3VHn9cPK8UMZ4g7kac2oiJptZKOZtLbBHenym02E0Uv3wjaoKHD0V6HZjpuI/21Qz8jenUo0Ns30Bm48vI32aDSFPb9Mpb+ddrVOZykuR0lWmSCdZMx7zoIFpNCYeb+OMs9UfP8ekbwFExrAzsa9X1nvwSO3r0= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=Lzc9WVq+; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="Lzc9WVq+" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 223C3C4CEF4; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475661; bh=5npNIdNOxU6nl+F6cCfxhjYp6GZooHL2IR9nKtVZYgo=; h=Date:From:To:Cc:Subject:References:From; b=Lzc9WVq+3C3x0hB1WdjsVutatSsD/e1wJ/LbbSthO/4DehG/W//umUHjYefaiuT2l C8l/v39eHeIPpOXVOVo5v7Wysx4L6ciZo+UCID6qlKVnCVEwyX8Ye8iih7TTcrJeLj IwTGPyPrPlwIGycxgdug5riadutLfMeXZUegtBk0BVa5k/AqPipygdrCOUOStMQMZz mSAFaE+RxJSW8iz40ASHiadC6No5e7sFfpB/vQIUN02zlvYdDbwTR72N9S1JT3qRHo t43G9u37DL4+kRSaHh+2ExMXwRTZUjNE6xyWRI3LS1jFgnNnG6Mqi3JVcPoMUQp816 LkL/5JPcoutuA== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7b-00000001QlM-1ANg; Fri, 25 Jul 2025 16:34:27 -0400 Message-ID: <20250725203427.130326086@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:16 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Juri Lelli , Clark Williams , Nam Cao , Gabriele Monaco Subject: [for-next][PATCH 19/25] verification/rvgen: Organise Kconfig entries for nested monitors References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Gabriele Monaco The current behaviour of rvgen when running with the -a option is to append the necessary lines at the end of the configuration for Kconfig, Makefile and tracepoints. This is not always the desired behaviour in case of nested monitors: while tracepoints are not affected by nesting and the Makefile's only requirement is that the parent monitor is built before its children, in the Kconfig it is better to have children defined right after their parent, otherwise the result has wrong indentation: [*] foo_parent monitor [*] foo_child1 monitor [*] foo_child2 monitor [*] bar_parent monitor [*] bar_child1 monitor [*] bar_child2 monitor [*] foo_child3 monitor [*] foo_child4 monitor Adapt rvgen to look for a different marker for nested monitors in the Kconfig file and append the line right after the last sibling, instead of the last monitor. Also add the marker when creating a new parent monitor. Cc: Masami Hiramatsu Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-5-gmonaco@redhat.com Reviewed-by: Nam Cao Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) --- kernel/trace/rv/Kconfig | 5 +++++ tools/verification/rvgen/rvgen/container.py | 10 ++++++++++ tools/verification/rvgen/rvgen/generator.py | 16 +++++++++++----- 3 files changed, 26 insertions(+), 5 deletions(-) diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index c11bf7e61ebf..26017378f79b 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -43,6 +43,7 @@ config RV_PER_TASK_MONITORS =20 source "kernel/trace/rv/monitors/wip/Kconfig" source "kernel/trace/rv/monitors/wwnr/Kconfig" + source "kernel/trace/rv/monitors/sched/Kconfig" source "kernel/trace/rv/monitors/tss/Kconfig" source "kernel/trace/rv/monitors/sco/Kconfig" @@ -50,9 +51,13 @@ source "kernel/trace/rv/monitors/snroc/Kconfig" source "kernel/trace/rv/monitors/scpd/Kconfig" source "kernel/trace/rv/monitors/snep/Kconfig" source "kernel/trace/rv/monitors/sncid/Kconfig" +# Add new sched monitors here + source "kernel/trace/rv/monitors/rtapp/Kconfig" source "kernel/trace/rv/monitors/pagefault/Kconfig" source "kernel/trace/rv/monitors/sleep/Kconfig" +# Add new rtapp monitors here + # Add new monitors here =20 config RV_REACTORS diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verificati= on/rvgen/rvgen/container.py index 47d8ab2ad3ec..51f188530b4d 100644 --- a/tools/verification/rvgen/rvgen/container.py +++ b/tools/verification/rvgen/rvgen/container.py @@ -20,3 +20,13 @@ class Container(generator.RVGenerator): main_h =3D self.main_h main_h =3D main_h.replace("%%MODEL_NAME%%", self.name) return main_h + + def fill_kconfig_tooltip(self): + """Override to produce a marker for this container in the Kconfig"= "" + container_marker =3D self._kconfig_marker(self.name) + "\n" + result =3D super().fill_kconfig_tooltip() + if self.auto_patch: + self._patch_file("Kconfig", + self._kconfig_marker(), container_marker) + return result + return result + container_marker diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verificati= on/rvgen/rvgen/generator.py index 19d0078a3803..3441385c1177 100644 --- a/tools/verification/rvgen/rvgen/generator.py +++ b/tools/verification/rvgen/rvgen/generator.py @@ -137,7 +137,8 @@ class RVGenerator: kconfig =3D kconfig.replace("%%MONITOR_DEPS%%", monitor_deps) return kconfig =20 - def __patch_file(self, file, marker, line): + def _patch_file(self, file, marker, line): + assert self.auto_patch file_to_patch =3D os.path.join(self.rv_dir, file) content =3D self._read_file(file_to_patch) content =3D content.replace(marker, line + "\n" + marker) @@ -146,7 +147,7 @@ class RVGenerator: def fill_tracepoint_tooltip(self): monitor_class_type =3D self.fill_monitor_class_type() if self.auto_patch: - self.__patch_file("rv_trace.h", + self._patch_file("rv_trace.h", "// Add new monitors based on CONFIG_%s here" = % monitor_class_type, "#include " % (self.na= me, self.name)) return " - Patching %s/rv_trace.h, double check the result" %= self.rv_dir @@ -156,10 +157,15 @@ Add this line where other tracepoints are included an= d %s is defined: #include """ % (self.rv_dir, monitor_class_type, self.name, self.name) =20 + def _kconfig_marker(self, container=3DNone) -> str: + return "# Add new %smonitors here" % (container + " " + if container else "") + def fill_kconfig_tooltip(self): if self.auto_patch: - self.__patch_file("Kconfig", - "# Add new monitors here", + # monitors with a container should stay together in the Kconfig + self._patch_file("Kconfig", + self._kconfig_marker(self.parent), "source \"kernel/trace/rv/monitors/%s/Kconfig\= "" % (self.name)) return " - Patching %s/Kconfig, double check the result" % se= lf.rv_dir =20 @@ -172,7 +178,7 @@ source \"kernel/trace/rv/monitors/%s/Kconfig\" name =3D self.name name_up =3D name.upper() if self.auto_patch: - self.__patch_file("Makefile", + self._patch_file("Makefile", "# Add new monitors here", "obj-$(CONFIG_RV_MON_%s) +=3D monitors/%s/%s.o= " % (name_up, name, name)) return " - Patching %s/Makefile, double check the result" % s= elf.rv_dir --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 6A1F225F998 for ; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; cv=none; b=X/2EQ6O0/8vO/XJBd6F3GCth/AtH3s923g0tg9kZu3OXnZT3MvV4Z1NzLRRdEqzyDf/euv8jTUFaRk+TEyRsvNu3YzBuF3dYFMEDehQ8/kdxlip/mngtc1yTj9YTKPbFAXoovgzgnH7NN7v65a4WZgyYQLeYdj276FNmbzlT9Qs= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; c=relaxed/simple; bh=lDIeUP7gycBcCkJz7HkOKpX24qAEDV/0w3NBoR6udJI=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=C7ZfrUhaMeRrf+c09XlP2AjSehnLiMaSOl2l4b1VS34otmUA/+/XBJ/IZedpc/armlpcTOnq4zBT9h3fICU3UWihGhzfzLY+DcLJp464N5Kn4ZStYwAylZN4szuFgAVQqoMD0VZIHcYAw5lvsJV1OzKLpFXB1OfY+xSsTHjKjOQ= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=Xrza58Oq; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="Xrza58Oq" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 4D820C4CEF8; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475661; bh=lDIeUP7gycBcCkJz7HkOKpX24qAEDV/0w3NBoR6udJI=; h=Date:From:To:Cc:Subject:References:From; b=Xrza58OqoMApTVUN8863ejqmQw8Q7JtoOnpt/Lgxjj0TRp9lj/pZenDANIq0rOxaR 7ML8scrUfqIo7menIMnYUUauMopGvpWIXhFbHbU4tPnX5hAQDLtjoB0YjppmmdE9tZ qTiOrZaQmTl5+9KCf+cIhD4xmNd3F00oi1Y8V5nd4C1fSZLZejixw5Arv8UJhk7r9t f1qzSl406bKG7UNeM3YTYeoIjGhuDORurg6iAsNn5AnykEDLtn9vH22D/WKyYLb6cL oqYFa5fjmexyrGAC+DMWxts50Kf3pB5jCJ4MnEiRH6D0CBci8XMCh40AGWzhLCCcMI MS9V675Ww04Og== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7b-00000001Qlr-1t5C; Fri, 25 Jul 2025 16:34:27 -0400 Message-ID: <20250725203427.299291833@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:17 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Juri Lelli , Clark Williams , Nam Cao , Gabriele Monaco Subject: [for-next][PATCH 20/25] rv: Return init error when registering monitors References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Gabriele Monaco Monitors generated with dot2k have their registration function (the one called during monitor initialisation) return always 0, even if the registration failed on RV side. This can hide potential errors. Return the value returned by the RV register function. Cc: Masami Hiramatsu Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-6-gmonaco@redhat.com Reviewed-by: Nam Cao Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google) --- kernel/trace/rv/monitors/sched/sched.c | 3 +-- kernel/trace/rv/monitors/sco/sco.c | 3 +-- kernel/trace/rv/monitors/scpd/scpd.c | 3 +-- kernel/trace/rv/monitors/sncid/sncid.c | 3 +-- kernel/trace/rv/monitors/snep/snep.c | 3 +-- kernel/trace/rv/monitors/snroc/snroc.c | 3 +-- kernel/trace/rv/monitors/tss/tss.c | 3 +-- kernel/trace/rv/monitors/wip/wip.c | 3 +-- kernel/trace/rv/monitors/wwnr/wwnr.c | 3 +-- tools/verification/rvgen/rvgen/templates/container/main.c | 3 +-- tools/verification/rvgen/rvgen/templates/dot2k/main.c | 3 +-- 11 files changed, 11 insertions(+), 22 deletions(-) diff --git a/kernel/trace/rv/monitors/sched/sched.c b/kernel/trace/rv/monit= ors/sched/sched.c index 905e03c3c934..d04db4b543f9 100644 --- a/kernel/trace/rv/monitors/sched/sched.c +++ b/kernel/trace/rv/monitors/sched/sched.c @@ -21,8 +21,7 @@ struct rv_monitor rv_sched =3D { =20 static int __init register_sched(void) { - rv_register_monitor(&rv_sched, NULL); - return 0; + return rv_register_monitor(&rv_sched, NULL); } =20 static void __exit unregister_sched(void) diff --git a/kernel/trace/rv/monitors/sco/sco.c b/kernel/trace/rv/monitors/= sco/sco.c index 4cff59220bfc..66f4639d46ac 100644 --- a/kernel/trace/rv/monitors/sco/sco.c +++ b/kernel/trace/rv/monitors/sco/sco.c @@ -71,8 +71,7 @@ static struct rv_monitor rv_sco =3D { =20 static int __init register_sco(void) { - rv_register_monitor(&rv_sco, &rv_sched); - return 0; + return rv_register_monitor(&rv_sco, &rv_sched); } =20 static void __exit unregister_sco(void) diff --git a/kernel/trace/rv/monitors/scpd/scpd.c b/kernel/trace/rv/monitor= s/scpd/scpd.c index cbdd6a5f8d7f..299703cd72b0 100644 --- a/kernel/trace/rv/monitors/scpd/scpd.c +++ b/kernel/trace/rv/monitors/scpd/scpd.c @@ -79,8 +79,7 @@ static struct rv_monitor rv_scpd =3D { =20 static int __init register_scpd(void) { - rv_register_monitor(&rv_scpd, &rv_sched); - return 0; + return rv_register_monitor(&rv_scpd, &rv_sched); } =20 static void __exit unregister_scpd(void) diff --git a/kernel/trace/rv/monitors/sncid/sncid.c b/kernel/trace/rv/monit= ors/sncid/sncid.c index f5037cd6214c..3e1ee715a0fb 100644 --- a/kernel/trace/rv/monitors/sncid/sncid.c +++ b/kernel/trace/rv/monitors/sncid/sncid.c @@ -79,8 +79,7 @@ static struct rv_monitor rv_sncid =3D { =20 static int __init register_sncid(void) { - rv_register_monitor(&rv_sncid, &rv_sched); - return 0; + return rv_register_monitor(&rv_sncid, &rv_sched); } =20 static void __exit unregister_sncid(void) diff --git a/kernel/trace/rv/monitors/snep/snep.c b/kernel/trace/rv/monitor= s/snep/snep.c index 0076ba6d7ea4..2adc3108d60c 100644 --- a/kernel/trace/rv/monitors/snep/snep.c +++ b/kernel/trace/rv/monitors/snep/snep.c @@ -79,8 +79,7 @@ static struct rv_monitor rv_snep =3D { =20 static int __init register_snep(void) { - rv_register_monitor(&rv_snep, &rv_sched); - return 0; + return rv_register_monitor(&rv_snep, &rv_sched); } =20 static void __exit unregister_snep(void) diff --git a/kernel/trace/rv/monitors/snroc/snroc.c b/kernel/trace/rv/monit= ors/snroc/snroc.c index bb1f60d55296..540e686e699f 100644 --- a/kernel/trace/rv/monitors/snroc/snroc.c +++ b/kernel/trace/rv/monitors/snroc/snroc.c @@ -68,8 +68,7 @@ static struct rv_monitor rv_snroc =3D { =20 static int __init register_snroc(void) { - rv_register_monitor(&rv_snroc, &rv_sched); - return 0; + return rv_register_monitor(&rv_snroc, &rv_sched); } =20 static void __exit unregister_snroc(void) diff --git a/kernel/trace/rv/monitors/tss/tss.c b/kernel/trace/rv/monitors/= tss/tss.c index 542787e6524f..0452fcd9edcf 100644 --- a/kernel/trace/rv/monitors/tss/tss.c +++ b/kernel/trace/rv/monitors/tss/tss.c @@ -74,8 +74,7 @@ static struct rv_monitor rv_tss =3D { =20 static int __init register_tss(void) { - rv_register_monitor(&rv_tss, &rv_sched); - return 0; + return rv_register_monitor(&rv_tss, &rv_sched); } =20 static void __exit unregister_tss(void) diff --git a/kernel/trace/rv/monitors/wip/wip.c b/kernel/trace/rv/monitors/= wip/wip.c index ed758fec8608..4b4e99615a11 100644 --- a/kernel/trace/rv/monitors/wip/wip.c +++ b/kernel/trace/rv/monitors/wip/wip.c @@ -71,8 +71,7 @@ static struct rv_monitor rv_wip =3D { =20 static int __init register_wip(void) { - rv_register_monitor(&rv_wip, NULL); - return 0; + return rv_register_monitor(&rv_wip, NULL); } =20 static void __exit unregister_wip(void) diff --git a/kernel/trace/rv/monitors/wwnr/wwnr.c b/kernel/trace/rv/monitor= s/wwnr/wwnr.c index 172f31c4b0f3..4145bea2729e 100644 --- a/kernel/trace/rv/monitors/wwnr/wwnr.c +++ b/kernel/trace/rv/monitors/wwnr/wwnr.c @@ -70,8 +70,7 @@ static struct rv_monitor rv_wwnr =3D { =20 static int __init register_wwnr(void) { - rv_register_monitor(&rv_wwnr, NULL); - return 0; + return rv_register_monitor(&rv_wwnr, NULL); } =20 static void __exit unregister_wwnr(void) diff --git a/tools/verification/rvgen/rvgen/templates/container/main.c b/to= ols/verification/rvgen/rvgen/templates/container/main.c index 89fc17cf8958..7d9b2f95c7e9 100644 --- a/tools/verification/rvgen/rvgen/templates/container/main.c +++ b/tools/verification/rvgen/rvgen/templates/container/main.c @@ -21,8 +21,7 @@ struct rv_monitor rv_%%MODEL_NAME%% =3D { =20 static int __init register_%%MODEL_NAME%%(void) { - rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); - return 0; + return rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); } =20 static void __exit unregister_%%MODEL_NAME%%(void) diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/= verification/rvgen/rvgen/templates/dot2k/main.c index 83044a20c89a..e0fd1134bd85 100644 --- a/tools/verification/rvgen/rvgen/templates/dot2k/main.c +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -74,8 +74,7 @@ static struct rv_monitor rv_%%MODEL_NAME%% =3D { =20 static int __init register_%%MODEL_NAME%%(void) { - rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); - return 0; + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); } =20 static void __exit unregister_%%MODEL_NAME%%(void) --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 91BE625FA2C for ; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; cv=none; b=oyBpNfuPYf++798BEAQj5rig8SLAHX8uRP/H9vnVPt9hCl07rZrkbG2d6uzV7Kn1SlbIaFc71tW1TyHZzU+OeNAcj+9dQhRLUF3Xma5Gm8S8rVLOFcZF7zSz5U8b39BTwM6eWxUynA3QRnH8wlwKP6BZj3yxTchHjRTopP43O04= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475661; c=relaxed/simple; bh=mnMaRWRSouXLjic4p7/eniTlbsyexL3Z/zySAdm/g5s=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=sa7e0h7im3fGfrk/eMLJn14b0EFkrtHFfJlx+tE25TXh8QKJDnCGNgjHnLQ8nUQKz4N85xeoENDWJZXt++W6IDI2yAW3r1AlqDmU5Uy+jemySW43mKS2kDQZU3dieCL+GRz1FRJnHpN79tj3DvYK7phEWOXgCao/AQ1HlLJTuio= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=AfYo3tgb; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="AfYo3tgb" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 73CB0C4CEF4; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475661; bh=mnMaRWRSouXLjic4p7/eniTlbsyexL3Z/zySAdm/g5s=; h=Date:From:To:Cc:Subject:References:From; b=AfYo3tgbxnXkr3TV56fiSPcC/igsfZNKzB0vEc8152d9DtzNXIuV1yf9at7W8HXYF K+Sh3dbdyjTH6rG40VN9yaSV6ehigcGoJ53glNed2pnIoK3pk3sVT4lf2dKBSeM5mr N1iXrTt44B1PH359O5t7nV5eq2hPB4F4CYgak3Z7Yfo2i57fmKF/rR5tI3SiAN9hdJ GSCYW6y9RAV3xl2EdJTxz7EPfSphoSB81p07FnWf8Vyj9F6n/C8/cXg3knxZkEig6n sMpCisJj9wLJ84ntrDIPa0zG9L/XuI2mtKloG11NV5FBYg0fLqtpjRtNaSX5ik0+RD Ckey/G+s5bJFw== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7b-00000001QmM-2bpB; Fri, 25 Jul 2025 16:34:27 -0400 Message-ID: <20250725203427.471623294@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:18 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 21/25] rv: Remove unused field in struct rv_monitor_def References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao rv_monitor_def::task_monitor is not used. Delete it. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/502d94f2696435690a2b1fdbe80a9e56c96fcabf.1753= 378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- kernel/trace/rv/rv.h | 1 - 1 file changed, 1 deletion(-) diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h index 98fca0a1adbc..873364094402 100644 --- a/kernel/trace/rv/rv.h +++ b/kernel/trace/rv/rv.h @@ -41,7 +41,6 @@ struct rv_monitor_def { struct rv_reactor_def *rdef; bool reacting; #endif - bool task_monitor; }; =20 struct dentry *get_monitors_root(void); --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 45132261595 for ; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475662; cv=none; b=grHcBqIZC+DXysB1G2cOBgJmerY+IdMx22+9oVykIqcYUlCtYL79nxO5d/qaLU17wYVZ4wGqyTTii9f/+72B1EdWDxeeJxthPsrzR9OtLcXLLdJ8PDpHEm6rhh4v86GmPFAP+a4D6l54skAj7gw7NuCwKRRMwAzSSaTAcm/8nRI= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475662; c=relaxed/simple; bh=BgRRGmQ+7MJ1KOKcah+kRc9McDNBvacvKTwrBrrVM6o=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=Nsm76O67h82RgemByHmPhzsQRByHzBMsD4rXLZOrf8nxr1h5BScfN9HfP4Hx16nHsBZEB8NpuoH/r2zd8zYnJjeCbJH0/cIzxI6IxMqJxkaWyOnTS71tDUE9ppbWgwvvFosR7nFqiqZdl7GhgiLLpR2yB1ZFyfE+0nmnDoqh010= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=ieQp1JpC; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="ieQp1JpC" Received: by smtp.kernel.org (Postfix) with ESMTPSA id A4F71C4CEEF; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475661; bh=BgRRGmQ+7MJ1KOKcah+kRc9McDNBvacvKTwrBrrVM6o=; h=Date:From:To:Cc:Subject:References:From; b=ieQp1JpCJojcuvfPJg5oRDmVxpw8aHCBr9WdGIhXWW9YeBlkGTtqjqb3OjIFQdzhI sLJz6a4svLj66r0qAm9z/v28ktbSVB1eIrG5MokkX65swxqBqtYpAfwm+iZwHp9ah+ aSlRj+MPNd5WlpPRjQQ6dT38uAFhTvyBvSTQqDBLw0nQMwdar4kiPh4dx3BqTVe6pI 6xsFacWVebAVwUjbKK7ApRb1cVj2i+oF/1S8e/PlD9h4+f12OBV6O0tuoq1WQH7VMx 4Rp8/yLFLQaXQw5IrKG0Ps+0Iiolke5rjMEX2b35kmPbHguZ0ng+kiQcfFSxFvPQOc w0T0/jNY3gQ8w== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7b-00000001Qmr-3JW9; Fri, 25 Jul 2025 16:34:27 -0400 Message-ID: <20250725203427.645088485@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:19 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 22/25] rv: Merge struct rv_monitor_def into struct rv_monitor References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao Each struct rv_monitor has a unique struct rv_monitor_def associated with it. struct rv_monitor is statically allocated, while struct rv_monitor_def is dynamically allocated. This makes the code more complicated than it should be: - Lookup is required to get the associated rv_monitor_def from rv_monitor - Dynamic memory allocation is required for rv_monitor_def. This is harder to get right compared to static memory. For instance, there is an existing mistake: rv_unregister_monitor() does not free the memory allocated by rv_register_monitor(). This is fortunately not a real memory leak problem, as rv_unregister_monitor() is never called. Simplify and merge rv_monitor_def into rv_monitor. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/194449c00f87945c207aab4c96920c75796a4f53.1753= 378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 8 ++ kernel/trace/rv/rv.c | 211 +++++++++++++++------------------- kernel/trace/rv/rv.h | 27 ++--- kernel/trace/rv/rv_reactors.c | 62 +++++----- 4 files changed, 140 insertions(+), 168 deletions(-) diff --git a/include/linux/rv.h b/include/linux/rv.h index 97baf58d88b2..dba53aecdfab 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -7,6 +7,9 @@ #ifndef _LINUX_RV_H #define _LINUX_RV_H =20 +#include +#include + #define MAX_DA_NAME_LEN 32 =20 #ifdef CONFIG_RV @@ -98,8 +101,13 @@ struct rv_monitor { void (*disable)(void); void (*reset)(void); #ifdef CONFIG_RV_REACTORS + struct rv_reactor_def *rdef; __printf(1, 2) void (*react)(const char *msg, ...); + bool reacting; #endif + struct list_head list; + struct rv_monitor *parent; + struct dentry *root_d; }; =20 bool rv_monitoring_on(void); diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c index 108429d16ec1..6c0be2fdc52d 100644 --- a/kernel/trace/rv/rv.c +++ b/kernel/trace/rv/rv.c @@ -210,9 +210,9 @@ void rv_put_task_monitor_slot(int slot) * Monitors with a parent are nested, * Monitors without a parent could be standalone or containers. */ -bool rv_is_nested_monitor(struct rv_monitor_def *mdef) +bool rv_is_nested_monitor(struct rv_monitor *mon) { - return mdef->parent !=3D NULL; + return mon->parent !=3D NULL; } =20 /* @@ -223,16 +223,16 @@ bool rv_is_nested_monitor(struct rv_monitor_def *mdef) * for enable()/disable(). Use this condition to find empty containers. * Keep both conditions in case we have some non-compliant containers. */ -bool rv_is_container_monitor(struct rv_monitor_def *mdef) +bool rv_is_container_monitor(struct rv_monitor *mon) { - struct rv_monitor_def *next; + struct rv_monitor *next; =20 - if (list_is_last(&mdef->list, &rv_monitors_list)) + if (list_is_last(&mon->list, &rv_monitors_list)) return false; =20 - next =3D list_next_entry(mdef, list); + next =3D list_next_entry(mon, list); =20 - return next->parent =3D=3D mdef->monitor || !mdef->monitor->enable; + return next->parent =3D=3D mon || !mon->enable; } =20 /* @@ -241,10 +241,10 @@ bool rv_is_container_monitor(struct rv_monitor_def *m= def) static ssize_t monitor_enable_read_data(struct file *filp, char __user *us= er_buf, size_t count, loff_t *ppos) { - struct rv_monitor_def *mdef =3D filp->private_data; + struct rv_monitor *mon =3D filp->private_data; const char *buff; =20 - buff =3D mdef->monitor->enabled ? "1\n" : "0\n"; + buff =3D mon->enabled ? "1\n" : "0\n"; =20 return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff)+= 1); } @@ -252,14 +252,14 @@ static ssize_t monitor_enable_read_data(struct file *= filp, char __user *user_buf /* * __rv_disable_monitor - disabled an enabled monitor */ -static int __rv_disable_monitor(struct rv_monitor_def *mdef, bool sync) +static int __rv_disable_monitor(struct rv_monitor *mon, bool sync) { lockdep_assert_held(&rv_interface_lock); =20 - if (mdef->monitor->enabled) { - mdef->monitor->enabled =3D 0; - if (mdef->monitor->disable) - mdef->monitor->disable(); + if (mon->enabled) { + mon->enabled =3D 0; + if (mon->disable) + mon->disable(); =20 /* * Wait for the execution of all events to finish. @@ -273,90 +273,90 @@ static int __rv_disable_monitor(struct rv_monitor_def= *mdef, bool sync) return 0; } =20 -static void rv_disable_single(struct rv_monitor_def *mdef) +static void rv_disable_single(struct rv_monitor *mon) { - __rv_disable_monitor(mdef, true); + __rv_disable_monitor(mon, true); } =20 -static int rv_enable_single(struct rv_monitor_def *mdef) +static int rv_enable_single(struct rv_monitor *mon) { int retval; =20 lockdep_assert_held(&rv_interface_lock); =20 - if (mdef->monitor->enabled) + if (mon->enabled) return 0; =20 - retval =3D mdef->monitor->enable(); + retval =3D mon->enable(); =20 if (!retval) - mdef->monitor->enabled =3D 1; + mon->enabled =3D 1; =20 return retval; } =20 -static void rv_disable_container(struct rv_monitor_def *mdef) +static void rv_disable_container(struct rv_monitor *mon) { - struct rv_monitor_def *p =3D mdef; + struct rv_monitor *p =3D mon; int enabled =3D 0; =20 list_for_each_entry_continue(p, &rv_monitors_list, list) { - if (p->parent !=3D mdef->monitor) + if (p->parent !=3D mon) break; enabled +=3D __rv_disable_monitor(p, false); } if (enabled) tracepoint_synchronize_unregister(); - mdef->monitor->enabled =3D 0; + mon->enabled =3D 0; } =20 -static int rv_enable_container(struct rv_monitor_def *mdef) +static int rv_enable_container(struct rv_monitor *mon) { - struct rv_monitor_def *p =3D mdef; + struct rv_monitor *p =3D mon; int retval =3D 0; =20 list_for_each_entry_continue(p, &rv_monitors_list, list) { - if (retval || p->parent !=3D mdef->monitor) + if (retval || p->parent !=3D mon) break; retval =3D rv_enable_single(p); } if (retval) - rv_disable_container(mdef); + rv_disable_container(mon); else - mdef->monitor->enabled =3D 1; + mon->enabled =3D 1; return retval; } =20 /** * rv_disable_monitor - disable a given runtime monitor - * @mdef: Pointer to the monitor definition structure. + * @mon: Pointer to the monitor definition structure. * * Returns 0 on success. */ -int rv_disable_monitor(struct rv_monitor_def *mdef) +int rv_disable_monitor(struct rv_monitor *mon) { - if (rv_is_container_monitor(mdef)) - rv_disable_container(mdef); + if (rv_is_container_monitor(mon)) + rv_disable_container(mon); else - rv_disable_single(mdef); + rv_disable_single(mon); =20 return 0; } =20 /** * rv_enable_monitor - enable a given runtime monitor - * @mdef: Pointer to the monitor definition structure. + * @mon: Pointer to the monitor definition structure. * * Returns 0 on success, error otherwise. */ -int rv_enable_monitor(struct rv_monitor_def *mdef) +int rv_enable_monitor(struct rv_monitor *mon) { int retval; =20 - if (rv_is_container_monitor(mdef)) - retval =3D rv_enable_container(mdef); + if (rv_is_container_monitor(mon)) + retval =3D rv_enable_container(mon); else - retval =3D rv_enable_single(mdef); + retval =3D rv_enable_single(mon); =20 return retval; } @@ -367,7 +367,7 @@ int rv_enable_monitor(struct rv_monitor_def *mdef) static ssize_t monitor_enable_write_data(struct file *filp, const char __u= ser *user_buf, size_t count, loff_t *ppos) { - struct rv_monitor_def *mdef =3D filp->private_data; + struct rv_monitor *mon =3D filp->private_data; int retval; bool val; =20 @@ -378,9 +378,9 @@ static ssize_t monitor_enable_write_data(struct file *f= ilp, const char __user *u mutex_lock(&rv_interface_lock); =20 if (val) - retval =3D rv_enable_monitor(mdef); + retval =3D rv_enable_monitor(mon); else - retval =3D rv_disable_monitor(mdef); + retval =3D rv_disable_monitor(mon); =20 mutex_unlock(&rv_interface_lock); =20 @@ -399,12 +399,12 @@ static const struct file_operations interface_enable_= fops =3D { static ssize_t monitor_desc_read_data(struct file *filp, char __user *user= _buf, size_t count, loff_t *ppos) { - struct rv_monitor_def *mdef =3D filp->private_data; + struct rv_monitor *mon =3D filp->private_data; char buff[256]; =20 memset(buff, 0, sizeof(buff)); =20 - snprintf(buff, sizeof(buff), "%s\n", mdef->monitor->description); + snprintf(buff, sizeof(buff), "%s\n", mon->description); =20 return simple_read_from_buffer(user_buf, count, ppos, buff, strlen(buff) = + 1); } @@ -419,37 +419,37 @@ static const struct file_operations interface_desc_fo= ps =3D { * the monitor dir, where the specific options of the monitor * are exposed. */ -static int create_monitor_dir(struct rv_monitor_def *mdef, struct rv_monit= or_def *parent) +static int create_monitor_dir(struct rv_monitor *mon, struct rv_monitor *p= arent) { struct dentry *root =3D parent ? parent->root_d : get_monitors_root(); - const char *name =3D mdef->monitor->name; + const char *name =3D mon->name; struct dentry *tmp; int retval; =20 - mdef->root_d =3D rv_create_dir(name, root); - if (!mdef->root_d) + mon->root_d =3D rv_create_dir(name, root); + if (!mon->root_d) return -ENOMEM; =20 - tmp =3D rv_create_file("enable", RV_MODE_WRITE, mdef->root_d, mdef, &inte= rface_enable_fops); + tmp =3D rv_create_file("enable", RV_MODE_WRITE, mon->root_d, mon, &interf= ace_enable_fops); if (!tmp) { retval =3D -ENOMEM; goto out_remove_root; } =20 - tmp =3D rv_create_file("desc", RV_MODE_READ, mdef->root_d, mdef, &interfa= ce_desc_fops); + tmp =3D rv_create_file("desc", RV_MODE_READ, mon->root_d, mon, &interface= _desc_fops); if (!tmp) { retval =3D -ENOMEM; goto out_remove_root; } =20 - retval =3D reactor_populate_monitor(mdef); + retval =3D reactor_populate_monitor(mon); if (retval) goto out_remove_root; =20 return 0; =20 out_remove_root: - rv_remove(mdef->root_d); + rv_remove(mon->root_d); return retval; } =20 @@ -458,13 +458,12 @@ static int create_monitor_dir(struct rv_monitor_def *= mdef, struct rv_monitor_def */ static int monitors_show(struct seq_file *m, void *p) { - struct rv_monitor_def *mon_def =3D p; + struct rv_monitor *mon =3D p; =20 - if (mon_def->parent) - seq_printf(m, "%s:%s\n", mon_def->parent->name, - mon_def->monitor->name); + if (mon->parent) + seq_printf(m, "%s:%s\n", mon->parent->name, mon->name); else - seq_printf(m, "%s\n", mon_def->monitor->name); + seq_printf(m, "%s\n", mon->name); return 0; } =20 @@ -496,13 +495,13 @@ static void *available_monitors_next(struct seq_file = *m, void *p, loff_t *pos) */ static void *enabled_monitors_next(struct seq_file *m, void *p, loff_t *po= s) { - struct rv_monitor_def *m_def =3D p; + struct rv_monitor *mon =3D p; =20 (*pos)++; =20 - list_for_each_entry_continue(m_def, &rv_monitors_list, list) { - if (m_def->monitor->enabled) - return m_def; + list_for_each_entry_continue(mon, &rv_monitors_list, list) { + if (mon->enabled) + return mon; } =20 return NULL; @@ -510,7 +509,7 @@ static void *enabled_monitors_next(struct seq_file *m, = void *p, loff_t *pos) =20 static void *enabled_monitors_start(struct seq_file *m, loff_t *pos) { - struct rv_monitor_def *m_def; + struct rv_monitor *mon; loff_t l; =20 mutex_lock(&rv_interface_lock); @@ -518,15 +517,15 @@ static void *enabled_monitors_start(struct seq_file *= m, loff_t *pos) if (list_empty(&rv_monitors_list)) return NULL; =20 - m_def =3D list_entry(&rv_monitors_list, struct rv_monitor_def, list); + mon =3D list_entry(&rv_monitors_list, struct rv_monitor, list); =20 for (l =3D 0; l <=3D *pos; ) { - m_def =3D enabled_monitors_next(m, m_def, &l); - if (!m_def) + mon =3D enabled_monitors_next(m, mon, &l); + if (!mon) break; } =20 - return m_def; + return mon; } =20 /* @@ -566,13 +565,13 @@ static const struct file_operations available_monitor= s_ops =3D { */ static void disable_all_monitors(void) { - struct rv_monitor_def *mdef; + struct rv_monitor *mon; int enabled =3D 0; =20 mutex_lock(&rv_interface_lock); =20 - list_for_each_entry(mdef, &rv_monitors_list, list) - enabled +=3D __rv_disable_monitor(mdef, false); + list_for_each_entry(mon, &rv_monitors_list, list) + enabled +=3D __rv_disable_monitor(mon, false); =20 if (enabled) { /* @@ -598,7 +597,7 @@ static ssize_t enabled_monitors_write(struct file *filp= , const char __user *user size_t count, loff_t *ppos) { char buff[MAX_RV_MONITOR_NAME_SIZE + 2]; - struct rv_monitor_def *mdef; + struct rv_monitor *mon; int retval =3D -EINVAL; bool enable =3D true; char *ptr, *tmp; @@ -633,17 +632,17 @@ static ssize_t enabled_monitors_write(struct file *fi= lp, const char __user *user if (tmp) ptr =3D tmp+1; =20 - list_for_each_entry(mdef, &rv_monitors_list, list) { - if (strcmp(ptr, mdef->monitor->name) !=3D 0) + list_for_each_entry(mon, &rv_monitors_list, list) { + if (strcmp(ptr, mon->name) !=3D 0) continue; =20 /* * Monitor found! */ if (enable) - retval =3D rv_enable_monitor(mdef); + retval =3D rv_enable_monitor(mon); else - retval =3D rv_disable_monitor(mdef); + retval =3D rv_disable_monitor(mon); =20 if (!retval) retval =3D count; @@ -702,11 +701,11 @@ static void turn_monitoring_off(void) =20 static void reset_all_monitors(void) { - struct rv_monitor_def *mdef; + struct rv_monitor *mon; =20 - list_for_each_entry(mdef, &rv_monitors_list, list) { - if (mdef->monitor->enabled && mdef->monitor->reset) - mdef->monitor->reset(); + list_for_each_entry(mon, &rv_monitors_list, list) { + if (mon->enabled && mon->reset) + mon->reset(); } } =20 @@ -768,10 +767,10 @@ static const struct file_operations monitoring_on_fop= s =3D { .read =3D monitoring_on_read_data, }; =20 -static void destroy_monitor_dir(struct rv_monitor_def *mdef) +static void destroy_monitor_dir(struct rv_monitor *mon) { - reactor_cleanup_monitor(mdef); - rv_remove(mdef->root_d); + reactor_cleanup_monitor(mon); + rv_remove(mon->root_d); } =20 /** @@ -783,7 +782,7 @@ static void destroy_monitor_dir(struct rv_monitor_def *= mdef) */ int rv_register_monitor(struct rv_monitor *monitor, struct rv_monitor *par= ent) { - struct rv_monitor_def *r, *p =3D NULL; + struct rv_monitor *r; int retval =3D 0; =20 if (strlen(monitor->name) >=3D MAX_RV_MONITOR_NAME_SIZE) { @@ -795,49 +794,31 @@ int rv_register_monitor(struct rv_monitor *monitor, s= truct rv_monitor *parent) mutex_lock(&rv_interface_lock); =20 list_for_each_entry(r, &rv_monitors_list, list) { - if (strcmp(monitor->name, r->monitor->name) =3D=3D 0) { + if (strcmp(monitor->name, r->name) =3D=3D 0) { pr_info("Monitor %s is already registered\n", monitor->name); retval =3D -EEXIST; goto out_unlock; } } =20 - if (parent) { - list_for_each_entry(r, &rv_monitors_list, list) { - if (strcmp(parent->name, r->monitor->name) =3D=3D 0) { - p =3D r; - break; - } - } - } - - if (p && rv_is_nested_monitor(p)) { + if (parent && rv_is_nested_monitor(parent)) { pr_info("Parent monitor %s is already nested, cannot nest further\n", parent->name); retval =3D -EINVAL; goto out_unlock; } =20 - r =3D kzalloc(sizeof(struct rv_monitor_def), GFP_KERNEL); - if (!r) { - retval =3D -ENOMEM; - goto out_unlock; - } - - r->monitor =3D monitor; - r->parent =3D parent; + monitor->parent =3D parent; =20 - retval =3D create_monitor_dir(r, p); - if (retval) { - kfree(r); - goto out_unlock; - } + retval =3D create_monitor_dir(monitor, parent); + if (retval) + return retval; =20 /* keep children close to the parent for easier visualisation */ - if (p) - list_add(&r->list, &p->list); + if (parent) + list_add(&monitor->list, &parent->list); else - list_add_tail(&r->list, &rv_monitors_list); + list_add_tail(&monitor->list, &rv_monitors_list); =20 out_unlock: mutex_unlock(&rv_interface_lock); @@ -852,17 +833,11 @@ int rv_register_monitor(struct rv_monitor *monitor, s= truct rv_monitor *parent) */ int rv_unregister_monitor(struct rv_monitor *monitor) { - struct rv_monitor_def *ptr, *next; - mutex_lock(&rv_interface_lock); =20 - list_for_each_entry_safe(ptr, next, &rv_monitors_list, list) { - if (strcmp(monitor->name, ptr->monitor->name) =3D=3D 0) { - rv_disable_monitor(ptr); - list_del(&ptr->list); - destroy_monitor_dir(ptr); - } - } + rv_disable_monitor(monitor); + list_del(&monitor->list); + destroy_monitor_dir(monitor); =20 mutex_unlock(&rv_interface_lock); return 0; diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h index 873364094402..f039ec1c9156 100644 --- a/kernel/trace/rv/rv.h +++ b/kernel/trace/rv/rv.h @@ -32,34 +32,23 @@ struct rv_reactor_def { }; #endif =20 -struct rv_monitor_def { - struct list_head list; - struct rv_monitor *monitor; - struct rv_monitor *parent; - struct dentry *root_d; -#ifdef CONFIG_RV_REACTORS - struct rv_reactor_def *rdef; - bool reacting; -#endif -}; - struct dentry *get_monitors_root(void); -int rv_disable_monitor(struct rv_monitor_def *mdef); -int rv_enable_monitor(struct rv_monitor_def *mdef); -bool rv_is_container_monitor(struct rv_monitor_def *mdef); -bool rv_is_nested_monitor(struct rv_monitor_def *mdef); +int rv_disable_monitor(struct rv_monitor *mon); +int rv_enable_monitor(struct rv_monitor *mon); +bool rv_is_container_monitor(struct rv_monitor *mon); +bool rv_is_nested_monitor(struct rv_monitor *mon); =20 #ifdef CONFIG_RV_REACTORS -int reactor_populate_monitor(struct rv_monitor_def *mdef); -void reactor_cleanup_monitor(struct rv_monitor_def *mdef); +int reactor_populate_monitor(struct rv_monitor *mon); +void reactor_cleanup_monitor(struct rv_monitor *mon); int init_rv_reactors(struct dentry *root_dir); #else -static inline int reactor_populate_monitor(struct rv_monitor_def *mdef) +static inline int reactor_populate_monitor(struct rv_monitor *mon) { return 0; } =20 -static inline void reactor_cleanup_monitor(struct rv_monitor_def *mdef) +static inline void reactor_cleanup_monitor(struct rv_monitor *mon) { return; } diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c index 740603670dd1..7cc620a1be1a 100644 --- a/kernel/trace/rv/rv_reactors.c +++ b/kernel/trace/rv/rv_reactors.c @@ -138,10 +138,10 @@ static const struct file_operations available_reactor= s_ops =3D { */ static int monitor_reactor_show(struct seq_file *m, void *p) { - struct rv_monitor_def *mdef =3D m->private; + struct rv_monitor *mon =3D m->private; struct rv_reactor_def *rdef =3D p; =20 - if (mdef->rdef =3D=3D rdef) + if (mon->rdef =3D=3D rdef) seq_printf(m, "[%s]\n", rdef->reactor->name); else seq_printf(m, "%s\n", rdef->reactor->name); @@ -158,41 +158,41 @@ static const struct seq_operations monitor_reactors_s= eq_ops =3D { .show =3D monitor_reactor_show }; =20 -static void monitor_swap_reactors_single(struct rv_monitor_def *mdef, +static void monitor_swap_reactors_single(struct rv_monitor *mon, struct rv_reactor_def *rdef, bool reacting, bool nested) { bool monitor_enabled; =20 /* nothing to do */ - if (mdef->rdef =3D=3D rdef) + if (mon->rdef =3D=3D rdef) return; =20 - monitor_enabled =3D mdef->monitor->enabled; + monitor_enabled =3D mon->enabled; if (monitor_enabled) - rv_disable_monitor(mdef); + rv_disable_monitor(mon); =20 /* swap reactor's usage */ - mdef->rdef->counter--; + mon->rdef->counter--; rdef->counter++; =20 - mdef->rdef =3D rdef; - mdef->reacting =3D reacting; - mdef->monitor->react =3D rdef->reactor->react; + mon->rdef =3D rdef; + mon->reacting =3D reacting; + mon->react =3D rdef->reactor->react; =20 /* enable only once if iterating through a container */ if (monitor_enabled && !nested) - rv_enable_monitor(mdef); + rv_enable_monitor(mon); } =20 -static void monitor_swap_reactors(struct rv_monitor_def *mdef, +static void monitor_swap_reactors(struct rv_monitor *mon, struct rv_reactor_def *rdef, bool reacting) { - struct rv_monitor_def *p =3D mdef; + struct rv_monitor *p =3D mon; =20 - if (rv_is_container_monitor(mdef)) + if (rv_is_container_monitor(mon)) list_for_each_entry_continue(p, &rv_monitors_list, list) { - if (p->parent !=3D mdef->monitor) + if (p->parent !=3D mon) break; monitor_swap_reactors_single(p, rdef, reacting, true); } @@ -202,7 +202,7 @@ static void monitor_swap_reactors(struct rv_monitor_def= *mdef, * All nested monitors are enabled also if they were off, we may refine * this logic in the future. */ - monitor_swap_reactors_single(mdef, rdef, reacting, false); + monitor_swap_reactors_single(mon, rdef, reacting, false); } =20 static ssize_t @@ -210,7 +210,7 @@ monitor_reactors_write(struct file *file, const char __= user *user_buf, size_t count, loff_t *ppos) { char buff[MAX_RV_REACTOR_NAME_SIZE + 2]; - struct rv_monitor_def *mdef; + struct rv_monitor *mon; struct rv_reactor_def *rdef; struct seq_file *seq_f; int retval =3D -EINVAL; @@ -237,7 +237,7 @@ monitor_reactors_write(struct file *file, const char __= user *user_buf, * See monitor_reactors_open() */ seq_f =3D file->private_data; - mdef =3D seq_f->private; + mon =3D seq_f->private; =20 mutex_lock(&rv_interface_lock); =20 @@ -252,7 +252,7 @@ monitor_reactors_write(struct file *file, const char __= user *user_buf, else enable =3D true; =20 - monitor_swap_reactors(mdef, rdef, enable); + monitor_swap_reactors(mon, rdef, enable); =20 retval =3D count; break; @@ -268,7 +268,7 @@ monitor_reactors_write(struct file *file, const char __= user *user_buf, */ static int monitor_reactors_open(struct inode *inode, struct file *file) { - struct rv_monitor_def *mdef =3D inode->i_private; + struct rv_monitor *mon =3D inode->i_private; struct seq_file *seq_f; int ret; =20 @@ -284,7 +284,7 @@ static int monitor_reactors_open(struct inode *inode, s= truct file *file) /* * Copy the create file "private" data to the seq_file private data. */ - seq_f->private =3D mdef; + seq_f->private =3D mon; =20 return 0; }; @@ -454,37 +454,37 @@ static const struct file_operations reacting_on_fops = =3D { =20 /** * reactor_populate_monitor - creates per monitor reactors file - * @mdef: monitor's definition. + * @mon: The monitor. * * Returns 0 if successful, error otherwise. */ -int reactor_populate_monitor(struct rv_monitor_def *mdef) +int reactor_populate_monitor(struct rv_monitor *mon) { struct dentry *tmp; =20 - tmp =3D rv_create_file("reactors", RV_MODE_WRITE, mdef->root_d, mdef, &mo= nitor_reactors_ops); + tmp =3D rv_create_file("reactors", RV_MODE_WRITE, mon->root_d, mon, &moni= tor_reactors_ops); if (!tmp) return -ENOMEM; =20 /* * Configure as the rv_nop reactor. */ - mdef->rdef =3D get_reactor_rdef_by_name("nop"); - mdef->rdef->counter++; - mdef->reacting =3D false; + mon->rdef =3D get_reactor_rdef_by_name("nop"); + mon->rdef->counter++; + mon->reacting =3D false; =20 return 0; } =20 /** * reactor_cleanup_monitor - cleanup a monitor reference - * @mdef: monitor's definition. + * @mon: the monitor. */ -void reactor_cleanup_monitor(struct rv_monitor_def *mdef) +void reactor_cleanup_monitor(struct rv_monitor *mon) { lockdep_assert_held(&rv_interface_lock); - mdef->rdef->counter--; - WARN_ON_ONCE(mdef->rdef->counter < 0); + mon->rdef->counter--; + WARN_ON_ONCE(mon->rdef->counter < 0); } =20 /* --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 56CB02638AF for ; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475663; cv=none; b=I0sJ0dfGeEK6kVgHYNcieI/2RIl33uNgIbN4PW5J8QDWBFZEDZaElBOb0L+SstNi1+gFLWLmVYzcgI/zNOJds8kGLhbHxppiq2lOtFaNSh4aLIQGsZBkCs45SE2U5n1MxD+AvuPKsUtZEMFJvttM3j9Sce6sg8WDJ5i6EUxfDbQ= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475663; c=relaxed/simple; bh=o4IL2Ph/MRJs8yCWP6+HvkGSsKELCJPor7WmK/2GjqQ=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=A5UOT4q5ZmyN4NTauMk5THjHvKCHU0FWmbrTzmD12JFXIwUtmbtQdsl1OdQDH7MdauWFdGta1LL5VaC05qcGoomvJn42Md82+0QznVbsM3CfSlu5mA2bSF/NQ67MbQAd1+eqecedcQmUqE0gTXrGelCHSMCSCVxh4o99uJdzLGo= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=oM4/4AWA; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="oM4/4AWA" Received: by smtp.kernel.org (Postfix) with ESMTPSA id C7BF2C4CEF6; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475661; bh=o4IL2Ph/MRJs8yCWP6+HvkGSsKELCJPor7WmK/2GjqQ=; h=Date:From:To:Cc:Subject:References:From; b=oM4/4AWADMzXgZK9NcMQXF8D3Im5yxDclb1oK1ioaF6Ah/+oTNS9miN9mM2szad/N 1JjNpOZtRp23ryik+HVl3WCOSfTtTPBAr0baU9kw2gqlxiRhV913oFExIeB0/r9IRV JhwYCOuj201MvWRHGAn6paIijqZ2Snb7XrwBqY97rhRxlPBnWlpMLpGntvqlxiRfjp 50PVokGUhqXdv0QIqEiCLH3/HPJWYRxwg5lMjUxOy3pABRI3paZcuHgNikEciTVzwH DmUgn0kvuMAzbKdrJOlKw5ZbPe8YJBP7kN6pDEaWBEEx1GFQmYHCyR68zVxfg0W/4V GrWblTsGTxR5g== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7b-00000001QnN-41at; Fri, 25 Jul 2025 16:34:27 -0400 Message-ID: <20250725203427.811864815@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:20 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 23/25] rv: Merge struct rv_reactor_def into struct rv_reactor References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao Each struct rv_reactor has a unique struct rv_reactor_def associated with it. struct rv_reactor is statically allocated, while struct rv_reactor_def is dynamically allocated. This makes the code more complicated than it should be: - Lookup is required to get the associated rv_reactor_def from rv_reactor - Dynamic memory allocation is required for rv_reactor_def. This is harder to get right compared to static memory. For instance, there is an existing mistake: rv_unregister_reactor() does not free the memory allocated by rv_register_reactor(). This is fortunately not a real memory leak problem as rv_unregister_reactor() is never called. Simplify and merge rv_reactor_def into rv_reactor. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/71cb91c86cd40df5b8c492b788787f2a73c3eaa3.1753= 378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 5 +- kernel/trace/rv/rv.h | 9 ---- kernel/trace/rv/rv_reactors.c | 92 +++++++++++++++-------------------- 3 files changed, 43 insertions(+), 63 deletions(-) diff --git a/include/linux/rv.h b/include/linux/rv.h index dba53aecdfab..c22c9b8c1567 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -90,6 +90,9 @@ struct rv_reactor { const char *name; const char *description; __printf(1, 2) void (*react)(const char *msg, ...); + struct list_head list; + /* protected by the monitor interface lock */ + int counter; }; #endif =20 @@ -101,7 +104,7 @@ struct rv_monitor { void (*disable)(void); void (*reset)(void); #ifdef CONFIG_RV_REACTORS - struct rv_reactor_def *rdef; + struct rv_reactor *reactor; __printf(1, 2) void (*react)(const char *msg, ...); bool reacting; #endif diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h index f039ec1c9156..8c38f9dd41bc 100644 --- a/kernel/trace/rv/rv.h +++ b/kernel/trace/rv/rv.h @@ -23,15 +23,6 @@ struct rv_interface { extern struct mutex rv_interface_lock; extern struct list_head rv_monitors_list; =20 -#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 dentry *get_monitors_root(void); int rv_disable_monitor(struct rv_monitor *mon); int rv_enable_monitor(struct rv_monitor *mon); diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c index 7cc620a1be1a..2c7909e6d0e7 100644 --- a/kernel/trace/rv/rv_reactors.c +++ b/kernel/trace/rv/rv_reactors.c @@ -70,12 +70,12 @@ */ static LIST_HEAD(rv_reactors_list); =20 -static struct rv_reactor_def *get_reactor_rdef_by_name(char *name) +static struct rv_reactor *get_reactor_rdef_by_name(char *name) { - struct rv_reactor_def *r; + struct rv_reactor *r; =20 list_for_each_entry(r, &rv_reactors_list, list) { - if (strcmp(name, r->reactor->name) =3D=3D 0) + if (strcmp(name, r->name) =3D=3D 0) return r; } return NULL; @@ -86,9 +86,9 @@ static struct rv_reactor_def *get_reactor_rdef_by_name(ch= ar *name) */ static int reactors_show(struct seq_file *m, void *p) { - struct rv_reactor_def *rea_def =3D p; + struct rv_reactor *reactor =3D p; =20 - seq_printf(m, "%s\n", rea_def->reactor->name); + seq_printf(m, "%s\n", reactor->name); return 0; } =20 @@ -139,12 +139,12 @@ static const struct file_operations available_reactor= s_ops =3D { static int monitor_reactor_show(struct seq_file *m, void *p) { struct rv_monitor *mon =3D m->private; - struct rv_reactor_def *rdef =3D p; + struct rv_reactor *reactor =3D p; =20 - if (mon->rdef =3D=3D rdef) - seq_printf(m, "[%s]\n", rdef->reactor->name); + if (mon->reactor =3D=3D reactor) + seq_printf(m, "[%s]\n", reactor->name); else - seq_printf(m, "%s\n", rdef->reactor->name); + seq_printf(m, "%s\n", reactor->name); return 0; } =20 @@ -159,13 +159,13 @@ static const struct seq_operations monitor_reactors_s= eq_ops =3D { }; =20 static void monitor_swap_reactors_single(struct rv_monitor *mon, - struct rv_reactor_def *rdef, + struct rv_reactor *reactor, bool reacting, bool nested) { bool monitor_enabled; =20 /* nothing to do */ - if (mon->rdef =3D=3D rdef) + if (mon->reactor =3D=3D reactor) return; =20 monitor_enabled =3D mon->enabled; @@ -173,12 +173,12 @@ static void monitor_swap_reactors_single(struct rv_mo= nitor *mon, rv_disable_monitor(mon); =20 /* swap reactor's usage */ - mon->rdef->counter--; - rdef->counter++; + mon->reactor->counter--; + reactor->counter++; =20 - mon->rdef =3D rdef; + mon->reactor =3D reactor; mon->reacting =3D reacting; - mon->react =3D rdef->reactor->react; + mon->react =3D reactor->react; =20 /* enable only once if iterating through a container */ if (monitor_enabled && !nested) @@ -186,7 +186,7 @@ static void monitor_swap_reactors_single(struct rv_moni= tor *mon, } =20 static void monitor_swap_reactors(struct rv_monitor *mon, - struct rv_reactor_def *rdef, bool reacting) + struct rv_reactor *reactor, bool reacting) { struct rv_monitor *p =3D mon; =20 @@ -194,7 +194,7 @@ static void monitor_swap_reactors(struct rv_monitor *mo= n, list_for_each_entry_continue(p, &rv_monitors_list, list) { if (p->parent !=3D mon) break; - monitor_swap_reactors_single(p, rdef, reacting, true); + monitor_swap_reactors_single(p, reactor, reacting, true); } /* * This call enables and disables the monitor if they were active. @@ -202,7 +202,7 @@ static void monitor_swap_reactors(struct rv_monitor *mo= n, * All nested monitors are enabled also if they were off, we may refine * this logic in the future. */ - monitor_swap_reactors_single(mon, rdef, reacting, false); + monitor_swap_reactors_single(mon, reactor, reacting, false); } =20 static ssize_t @@ -211,7 +211,7 @@ monitor_reactors_write(struct file *file, const char __= user *user_buf, { char buff[MAX_RV_REACTOR_NAME_SIZE + 2]; struct rv_monitor *mon; - struct rv_reactor_def *rdef; + struct rv_reactor *reactor; struct seq_file *seq_f; int retval =3D -EINVAL; bool enable; @@ -243,16 +243,16 @@ monitor_reactors_write(struct file *file, const char = __user *user_buf, =20 retval =3D -EINVAL; =20 - list_for_each_entry(rdef, &rv_reactors_list, list) { - if (strcmp(ptr, rdef->reactor->name) !=3D 0) + list_for_each_entry(reactor, &rv_reactors_list, list) { + if (strcmp(ptr, reactor->name) !=3D 0) continue; =20 - if (rdef =3D=3D get_reactor_rdef_by_name("nop")) + if (strcmp(reactor->name, "nop")) enable =3D false; else enable =3D true; =20 - monitor_swap_reactors(mon, rdef, enable); + monitor_swap_reactors(mon, reactor, enable); =20 retval =3D count; break; @@ -299,23 +299,16 @@ static const struct file_operations monitor_reactors_= ops =3D { =20 static int __rv_register_reactor(struct rv_reactor *reactor) { - struct rv_reactor_def *r; + struct rv_reactor *r; =20 list_for_each_entry(r, &rv_reactors_list, list) { - if (strcmp(reactor->name, r->reactor->name) =3D=3D 0) { + if (strcmp(reactor->name, r->name) =3D=3D 0) { pr_info("Reactor %s is already registered\n", reactor->name); return -EINVAL; } } =20 - r =3D kzalloc(sizeof(struct rv_reactor_def), GFP_KERNEL); - if (!r) - return -ENOMEM; - - r->reactor =3D reactor; - r->counter =3D 0; - - list_add_tail(&r->list, &rv_reactors_list); + list_add_tail(&reactor->list, &rv_reactors_list); =20 return 0; } @@ -350,26 +343,19 @@ int rv_register_reactor(struct rv_reactor *reactor) */ int rv_unregister_reactor(struct rv_reactor *reactor) { - struct rv_reactor_def *ptr, *next; int ret =3D 0; =20 mutex_lock(&rv_interface_lock); =20 - list_for_each_entry_safe(ptr, next, &rv_reactors_list, list) { - if (strcmp(reactor->name, ptr->reactor->name) =3D=3D 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); - ret =3D -EBUSY; - break; - } - } + if (!reactor->counter) { + list_del(&reactor->list); + } else { + printk(KERN_WARNING + "rv: the rv_reactor %s is in use by %d monitor(s)\n", + reactor->name, reactor->counter); + printk(KERN_WARNING "rv: the rv_reactor %s cannot be removed\n", + reactor->name); + ret =3D -EBUSY; } =20 mutex_unlock(&rv_interface_lock); @@ -469,8 +455,8 @@ int reactor_populate_monitor(struct rv_monitor *mon) /* * Configure as the rv_nop reactor. */ - mon->rdef =3D get_reactor_rdef_by_name("nop"); - mon->rdef->counter++; + mon->reactor =3D get_reactor_rdef_by_name("nop"); + mon->reactor->counter++; mon->reacting =3D false; =20 return 0; @@ -483,8 +469,8 @@ int reactor_populate_monitor(struct rv_monitor *mon) void reactor_cleanup_monitor(struct rv_monitor *mon) { lockdep_assert_held(&rv_interface_lock); - mon->rdef->counter--; - WARN_ON_ONCE(mon->rdef->counter < 0); + mon->reactor->counter--; + WARN_ON_ONCE(mon->reactor->counter < 0); } =20 /* --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 1CF30261581 for ; Fri, 25 Jul 2025 20:34:22 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475662; cv=none; b=UFQ5IItPzkDfKP6Q+ew9PpNpjbWqSnaySpDB5YNJIXOx/lMhRstxpvnx2y0hh/cdeeID/1hKuKzoM9Jgd5pdlG/4YxU0FDD5zEv0frtLB4mMdLfcPPw0KW7XK7EgwHpYpKPIqycc/8+j0Jf/SRUxvjinwlFAQtKOCn99PQyci2E= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475662; c=relaxed/simple; bh=Z6cQujRZpzoUyq30TVQ5FlDuRLcQ+CsV3Q3ydT4Kitg=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=KUoVl1PraUHsVfu+OQbKxCurmHEAeGDVHUXLxy7cNYctY71M0YRpjx67+3+TEqir5LPmSlDhW7f3nHju2/DqiWyS6OohvtrqmUQ+joOA9UR+Dsf+7SfNZGX+HRLVi0yuXnNlx2DYhZ3fSNmaqO/dKvwmJg1fIjb+sBFjdSllNq8= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=bs+VwZ48; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="bs+VwZ48" Received: by smtp.kernel.org (Postfix) with ESMTPSA id F2F60C4CEF4; Fri, 25 Jul 2025 20:34:21 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475662; bh=Z6cQujRZpzoUyq30TVQ5FlDuRLcQ+CsV3Q3ydT4Kitg=; h=Date:From:To:Cc:Subject:References:From; b=bs+VwZ48/4TLM/FAsSgNTR1sznJQwdqbmUNPN76Gm/5Q3wYWqhcKEoouYnNrW+rKQ 6d2y18+LgpkqdNK/GqAvNBmkOJ99yy+pM/5BmB99WXrhr1DjEpbzJ02BNBEq7iYyI2 WvymFLV5K/PkMY8ogxACul+IZNiYWeXbUV0oyulVKBgV+Q0xnxpTdNgMxV52qwEfJB JZHuNkx4L/RtSyCKOkewmcOZpBcXpOfT5VulPDQ4xE/BnP8WPnQGC5B1hTGBy+C6Ml tFdw3jO4byMXLB3DoDxuCdD9mvp92NiXbAD4jJuAD3ZTl7VPJzwhDS6VE69IH3/Kz8 D5buTryQ8ExuQ== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7c-00000001Qns-0YbC; Fri, 25 Jul 2025 16:34:28 -0400 Message-ID: <20250725203427.982046449@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:21 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 24/25] rv: Remove rv_reactors reference counter References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao rv_reactor has a reference counter to ensure it is not removed while monitors are still using it. However, this is futile, as __exit functions are not expected to fail and will proceed normally despite rv_unregister_reactor() returning an error. At the moment, reactors do not support being built as modules, therefore they are never removed and the reference counters are not necessary. If we support building RV reactors as modules in the future, kernel module's centralized facilities such as try_module_get(), module_put() or MODULE_SOFTDEP should be used instead of this custom implementation. Remove this reference counter. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/bb946398436a5e17fb0f5b842ef3313c02291852.1753= 378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 2 -- kernel/trace/rv/rv.c | 1 - kernel/trace/rv/rv.h | 6 ------ kernel/trace/rv/rv_reactors.c | 33 ++------------------------------- 4 files changed, 2 insertions(+), 40 deletions(-) diff --git a/include/linux/rv.h b/include/linux/rv.h index c22c9b8c1567..2f867d6f72ba 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -91,8 +91,6 @@ struct rv_reactor { const char *description; __printf(1, 2) void (*react)(const char *msg, ...); struct list_head list; - /* protected by the monitor interface lock */ - int counter; }; #endif =20 diff --git a/kernel/trace/rv/rv.c b/kernel/trace/rv/rv.c index 6c0be2fdc52d..6c8498743b98 100644 --- a/kernel/trace/rv/rv.c +++ b/kernel/trace/rv/rv.c @@ -769,7 +769,6 @@ static const struct file_operations monitoring_on_fops = =3D { =20 static void destroy_monitor_dir(struct rv_monitor *mon) { - reactor_cleanup_monitor(mon); rv_remove(mon->root_d); } =20 diff --git a/kernel/trace/rv/rv.h b/kernel/trace/rv/rv.h index 8c38f9dd41bc..1485a70c1bf4 100644 --- a/kernel/trace/rv/rv.h +++ b/kernel/trace/rv/rv.h @@ -31,7 +31,6 @@ bool rv_is_nested_monitor(struct rv_monitor *mon); =20 #ifdef CONFIG_RV_REACTORS int reactor_populate_monitor(struct rv_monitor *mon); -void reactor_cleanup_monitor(struct rv_monitor *mon); int init_rv_reactors(struct dentry *root_dir); #else static inline int reactor_populate_monitor(struct rv_monitor *mon) @@ -39,11 +38,6 @@ static inline int reactor_populate_monitor(struct rv_mon= itor *mon) return 0; } =20 -static inline void reactor_cleanup_monitor(struct rv_monitor *mon) -{ - return; -} - static inline int init_rv_reactors(struct dentry *root_dir) { return 0; diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c index 2c7909e6d0e7..a8e849e6cd85 100644 --- a/kernel/trace/rv/rv_reactors.c +++ b/kernel/trace/rv/rv_reactors.c @@ -172,10 +172,6 @@ static void monitor_swap_reactors_single(struct rv_mon= itor *mon, if (monitor_enabled) rv_disable_monitor(mon); =20 - /* swap reactor's usage */ - mon->reactor->counter--; - reactor->counter++; - mon->reactor =3D reactor; mon->reacting =3D reacting; mon->react =3D reactor->react; @@ -343,23 +339,10 @@ int rv_register_reactor(struct rv_reactor *reactor) */ int rv_unregister_reactor(struct rv_reactor *reactor) { - int ret =3D 0; - mutex_lock(&rv_interface_lock); - - if (!reactor->counter) { - list_del(&reactor->list); - } else { - printk(KERN_WARNING - "rv: the rv_reactor %s is in use by %d monitor(s)\n", - reactor->name, reactor->counter); - printk(KERN_WARNING "rv: the rv_reactor %s cannot be removed\n", - reactor->name); - ret =3D -EBUSY; - } - + list_del(&reactor->list); mutex_unlock(&rv_interface_lock); - return ret; + return 0; } =20 /* @@ -456,23 +439,11 @@ int reactor_populate_monitor(struct rv_monitor *mon) * Configure as the rv_nop reactor. */ mon->reactor =3D get_reactor_rdef_by_name("nop"); - mon->reactor->counter++; mon->reacting =3D false; =20 return 0; } =20 -/** - * reactor_cleanup_monitor - cleanup a monitor reference - * @mon: the monitor. - */ -void reactor_cleanup_monitor(struct rv_monitor *mon) -{ - lockdep_assert_held(&rv_interface_lock); - mon->reactor->counter--; - WARN_ON_ONCE(mon->reactor->counter < 0); -} - /* * Nop reactor register */ --=20 2.47.2 From nobody Mon Oct 6 01:21:11 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (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 4F05A2620C6 for ; Fri, 25 Jul 2025 20:34:22 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475662; cv=none; b=YQ/4oD2T0SVMn5olmFI2RWk8FTriyiOhEd/wvylXzejCcq6Z7PsRg+HivOezM/EKdXwOwBz2KpE1lJ6yGQb5KWRQJ1zFyx7DzpWDt/8ZA/keszmWZ8Me75fuaOhwXzlr3+2G3jQCFIchqWwMkXSi8wx4wU5AyqEY5myv57Z9n+s= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1753475662; c=relaxed/simple; bh=5FhrJdRrPXoJDitTnpTHro5cJdUMVk+R5P5dbrBa2Cg=; h=Message-ID:Date:From:To:Cc:Subject:References:MIME-Version: Content-Type; b=imzVv2QkZUzDlXr+r62C/5UGZuZmdTTYUBpxpRNzZEHsW3tRl/VcWTl4uhkByu2+47SgoUvNkm1S3voYyAGfzUk0Q4kLXu6VUKXdIbaWOzQ65hPx7ahS4srLMyU9gLLb52Ooeyx3sO2570yUfjocBCUARi5or4vnQMCGvM+U9bw= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=I/x613I4; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="I/x613I4" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 30C37C4CEFA; Fri, 25 Jul 2025 20:34:22 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1753475662; bh=5FhrJdRrPXoJDitTnpTHro5cJdUMVk+R5P5dbrBa2Cg=; h=Date:From:To:Cc:Subject:References:From; b=I/x613I4RGsiR3wFpiWVjaJ4SBVzNEg4djRH9YERWNA6J3E/3Yb37yiS8bCA1jvGB 6S5LiV5z1pIoFuFWqrqbeZJZLqiVeg6IAK/h2cT3levApFPnj0cpGOw85y2dA7mTxY 8ni28MzV1/YJaC8rVKK1WwCq3D9qUYgmKH+a4HYAZfgZ4oUSigDjfmXkFPOrpF79j7 O/OjkWBz8+x2bMa8J/JukqTHOGqiD4o4QixBCtoHtRIePKPb7BIXg0aHOrEm6HSvJw MdRmGF96Bk41rQ/dEPcciL2WnmoAgsimNWedIdGaYRxt50l9rUdA+qv4OVRocPvs3v SKm5HYLy483uw== Received: from rostedt by gandalf with local (Exim 4.98.2) (envelope-from ) id 1ufP7c-00000001QoN-1HQK; Fri, 25 Jul 2025 16:34:28 -0400 Message-ID: <20250725203428.155244648@kernel.org> User-Agent: quilt/0.68 Date: Fri, 25 Jul 2025 16:34:22 -0400 From: Steven Rostedt To: linux-kernel@vger.kernel.org Cc: Tomas Glozar , John Kacur , Masami Hiramatsu , Mathieu Desnoyers , Gabriele Monaco , Nam Cao Subject: [for-next][PATCH 25/25] rv: Remove struct rv_monitor::reacting References: <20250725203357.087558746@kernel.org> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Nam Cao The field 'reacting' in struct rv_monitor is set but never used. Delete it. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/a6c16f845d2f1a09c4d0934ab83f3cb14478a71d.1753= 378331.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google) --- include/linux/rv.h | 1 - kernel/trace/rv/rv_reactors.c | 19 +++++-------------- 2 files changed, 5 insertions(+), 15 deletions(-) diff --git a/include/linux/rv.h b/include/linux/rv.h index 2f867d6f72ba..80731242fe60 100644 --- a/include/linux/rv.h +++ b/include/linux/rv.h @@ -104,7 +104,6 @@ struct rv_monitor { #ifdef CONFIG_RV_REACTORS struct rv_reactor *reactor; __printf(1, 2) void (*react)(const char *msg, ...); - bool reacting; #endif struct list_head list; struct rv_monitor *parent; diff --git a/kernel/trace/rv/rv_reactors.c b/kernel/trace/rv/rv_reactors.c index a8e849e6cd85..106f2c4740f2 100644 --- a/kernel/trace/rv/rv_reactors.c +++ b/kernel/trace/rv/rv_reactors.c @@ -160,7 +160,7 @@ static const struct seq_operations monitor_reactors_seq= _ops =3D { =20 static void monitor_swap_reactors_single(struct rv_monitor *mon, struct rv_reactor *reactor, - bool reacting, bool nested) + bool nested) { bool monitor_enabled; =20 @@ -173,7 +173,6 @@ static void monitor_swap_reactors_single(struct rv_moni= tor *mon, rv_disable_monitor(mon); =20 mon->reactor =3D reactor; - mon->reacting =3D reacting; mon->react =3D reactor->react; =20 /* enable only once if iterating through a container */ @@ -181,8 +180,7 @@ static void monitor_swap_reactors_single(struct rv_moni= tor *mon, rv_enable_monitor(mon); } =20 -static void monitor_swap_reactors(struct rv_monitor *mon, - struct rv_reactor *reactor, bool reacting) +static void monitor_swap_reactors(struct rv_monitor *mon, struct rv_reacto= r *reactor) { struct rv_monitor *p =3D mon; =20 @@ -190,7 +188,7 @@ static void monitor_swap_reactors(struct rv_monitor *mo= n, list_for_each_entry_continue(p, &rv_monitors_list, list) { if (p->parent !=3D mon) break; - monitor_swap_reactors_single(p, reactor, reacting, true); + monitor_swap_reactors_single(p, reactor, true); } /* * This call enables and disables the monitor if they were active. @@ -198,7 +196,7 @@ static void monitor_swap_reactors(struct rv_monitor *mo= n, * All nested monitors are enabled also if they were off, we may refine * this logic in the future. */ - monitor_swap_reactors_single(mon, reactor, reacting, false); + monitor_swap_reactors_single(mon, reactor, false); } =20 static ssize_t @@ -210,7 +208,6 @@ monitor_reactors_write(struct file *file, const char __= user *user_buf, struct rv_reactor *reactor; struct seq_file *seq_f; int retval =3D -EINVAL; - bool enable; char *ptr; int len; =20 @@ -243,12 +240,7 @@ monitor_reactors_write(struct file *file, const char _= _user *user_buf, if (strcmp(ptr, reactor->name) !=3D 0) continue; =20 - if (strcmp(reactor->name, "nop")) - enable =3D false; - else - enable =3D true; - - monitor_swap_reactors(mon, reactor, enable); + monitor_swap_reactors(mon, reactor); =20 retval =3D count; break; @@ -439,7 +431,6 @@ int reactor_populate_monitor(struct rv_monitor *mon) * Configure as the rv_nop reactor. */ mon->reactor =3D get_reactor_rdef_by_name("nop"); - mon->reacting =3D false; =20 return 0; } --=20 2.47.2