From patchwork Wed Apr 16 06:51:16 2025 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Nam Cao X-Patchwork-Id: 14053365 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 8E9E622D4E2; Wed, 16 Apr 2025 06:52:00 +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=1744786324; cv=none; b=Wh0ZSQJC4jG1rkSeOKJ2UODBJ1/LLccG7HcUarfyJWWbmMjeSGAmQOX/i0V7QME3xSzqMoyNoYM9vHn56pyfjg1rjJFkfa0KzmlZpaoBCS916IjXHx3tm3Fd1q5gAzuORCacOz93WRUAcvDTfWyMlCZKawhIx+X20kUzdVYWG+g= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1744786324; c=relaxed/simple; bh=WgE1aO9YUvOmlhuTjVRspOHWrraepbPoXdmSTVuPrz4=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=n80pXSmwps2wmovKb7HARyVCYo6q4yC3Ht+2n0JudlDp07//Y5TJRRwanN1VZ3I65FDSLhaV3wYoZREpJizSFAGx9LEp0HRYZgBHV46h0zY1XZ68fTwk/6zayY2D4SzvQQzbdBmvOKt3utR4+gEFcpMTlb3+giuj2nBf4adn7+8= 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=iN1q22+3; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b=+u3PiEcl; 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="iN1q22+3"; dkim=permerror (0-bit key) header.d=linutronix.de header.i=@linutronix.de header.b="+u3PiEcl" From: Nam Cao DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020; t=1744786317; 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=iN1q22+3hRt9s6gkC/jFxDYNduEET3f2Dy4M5gGh8NWx7dRDFHJE+PIiGLmRRx7dKu8GR6 f0IGPYMKekCUv5/nMeOFr4i3ZRMZrF55+jHkVglDz5dVn3pqEGXr2/g55NyvZZLujdmSJO jj2jn2IllXKwybtYA34mtfhffBeU2nq98n+7V9ocWSEV2lOQmOHHe3fuOu6vQ+0pGa38Ln n8bnBDm1GsodyMm4qJF1gl3t/MLo9JJkseEkuDyy4/Ls9Cp6S8O+XVkPaN+VHVCKNJubFX m7Ki/00vFGXdDBZa0L/VrO0PycjTvqE0VTBVRmSBtNqJY3H/b4Z6WoUAZPuuWw== DKIM-Signature: v=1; a=ed25519-sha256; c=relaxed/relaxed; d=linutronix.de; s=2020e; t=1744786317; 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=+u3PiEclLldP9VUhW0OqvIqdYk6497mviT1Ygcn4QJbjayY0M/cwMipf9wCj3JbGktWrPQ lbVY/zmJgTIH06BA== To: Steven Rostedt , Gabriele Monaco , linux-trace-kernel@vger.kernel.org, linux-kernel@vger.kernel.org Cc: john.ogness@linutronix.de, Nam Cao Subject: [PATCH v3 10/22] Documentation/rv: Prepare monitor synthesis document for LTL inclusion Date: Wed, 16 Apr 2025 08:51:16 +0200 Message-Id: In-Reply-To: References: Precedence: bulk X-Mailing-List: linux-trace-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 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 => monitor_synthesis.rst} | 20 +++++++++---------- 2 files changed, 11 insertions(+), 11 deletions(-) rename Documentation/trace/rv/{da_monitor_synthesis.rst => monitor_synthesis.rst} (92%) diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst index e80e0057feb4..8e411b76ec82 100644 --- a/Documentation/trace/rv/index.rst +++ b/Documentation/trace/rv/index.rst @@ -8,7 +8,7 @@ Runtime Verification 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/Documentation/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 -======================================== +Runtime Verification Monitor Synthesis +====================================== The starting point for the application of runtime verification (RV) techniques is the *specification* or *modeling* of the desired (or undesired) behavior @@ -36,24 +36,24 @@ below:: | +----> panic ? +-------> -DA monitor synthesis +RV monitor synthesis -------------------- The synthesis of automata-based models into the Linux *RV monitor* abstraction -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. -dot2k +rvgen ----- -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. For example, it is possible to transform the wip.dot model present in [1] into a per-cpu monitor with the following command:: - $ dot2k -d wip.dot -t per_cpu + $ rvgen monitor -c da -s wip.dot -t per_cpu This will create a directory named wip/ with the following files: @@ -87,7 +87,7 @@ the second for monitors with per-cpu instances, and the third with per-task instances. 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. For example, the wip model with two states and three events can be @@ -134,7 +134,7 @@ Final remarks ------------- 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. [1] For details about deterministic automata format and the translation @@ -142,6 +142,6 @@ from one representation to another, see:: Documentation/trace/rv/deterministic_automata.rst -[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.