From nobody Wed Oct 8 00:42:34 2025 Received: from galois.linutronix.de (Galois.linutronix.de [193.142.43.55]) (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 84C1A2FF492; Fri, 4 Jul 2025 13:20:36 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=193.142.43.55 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1751635240; cv=none; b=iE5ANt06c4rdJ9C+pG4D+NyGTzGMxkIycpI3EcTajgJsgsQOczjC/OoHMuKzuIz0LMb2Idk/3kwj7RHvpJJRrSSnK1BR0Ff/mjNBy1N2vqWVA4SLpMy4zWE9i1NkV9KyVmlo3CG8J8O3aCOElgMPf25YiuISRkQD5yAet0nzdEg= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1751635240; c=relaxed/simple; bh=WgE1aO9YUvOmlhuTjVRspOHWrraepbPoXdmSTVuPrz4=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=A64ExRMbidpUQP9/jdkqCp3ENwPAMv/xTumiBmLBfb0yai2kfzgem+RCrRUzPDSfldG7tgGFGk8VboP/+BAI2mFH/nj5ReUdxId13uziU/Fb92PhOAGPrIm/tsUz+wecl54hVnd1h5ogzpSdYtdzIeC1ptxzA9n0nrDOVZ4n1lo= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de; spf=pass smtp.mailfrom=linutronix.de; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=pAgtoTwL; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=uQLC9bdl; arc=none smtp.client-ip=193.142.43.55 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=linutronix.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=linutronix.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="pAgtoTwL"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="uQLC9bdl" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1751635234; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=WwJdSQU9Mp7gY25s96zSaz0i/71ZPlHWpcJ0xxxuTBQ=; b=pAgtoTwLBpU5MrSFotMwA/D6E2PjCcHJklgVGNKRZKNs1OUVObmotzytCbPCOnC5fkW3wS L21eDGssK1oMC4JlVYDEWZDuuFVVFi38stN0sFxMME8D1PKoBZPBsBFani8y3ZqFU7Tv9a BWrBrjnKNqK6/sNaothpc4ffp61pGWNrgu7ltYLgLRpcyrHYTX7G1WMIicZN/ceThWzwyc ijJoM+e8w3Gw85OWvobzNAIZIb29JXWbwJOdPmkRKDGGdgrJBSahPi6QUYUd/3+F5TB+7B f82/LLrppdnJR3f5Y2VLUwvndYm+8/MaqvPNJ3+mkHp6Oyg2C+oL4AOCXQq9fA== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1751635234; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=WwJdSQU9Mp7gY25s96zSaz0i/71ZPlHWpcJ0xxxuTBQ=; b=uQLC9bdly0qhj4b2xgn0HAHHsDIaQLy+mgyMQVl6nuq6u6mzss5C5VGAPmg6KrAEz4HOuf 6gB+iSaTHdZw9RAg== To: Steven Rostedt , Masami Hiramatsu , Mathieu Desnoyers , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: Gabriele Monaco , john.ogness@linutronix.de, Nam Cao Subject: [PATCH v11 10/21] Documentation/rv: Prepare monitor synthesis document for LTL inclusion Date: Fri, 4 Jul 2025 15:20:02 +0200 Message-Id: In-Reply-To: References: 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" 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. Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao --- 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 e80e0057feb4..8e411b76ec82 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.39.5