From nobody Mon Feb 9 13:58:44 2026 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.129.124]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 1DCDF221277 for ; Fri, 16 Jan 2026 12:41:00 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.129.124 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1768567263; cv=none; b=uzZJHvWWSY3vWkpEPawTNs7UXNEn4xcjyOMvt+uIHohJMuj5dr4ewsC1TirbwXQnHeN3y8F4ONBeivkqn3kbdl0CnBA5djZAufkyMVL/qTs5R6bNHG1OXkG51w+oIZ30DBaBRk27XGZHEou2Pl+B6Nxikt3QKkEOLZMSk/QRyPY= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1768567263; c=relaxed/simple; bh=VP/RwWS8tSy5WWuRe/K3hUMVCX1znf8xUfRIOMZN64U=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=QfW+/f3bf92fLT0TiOma/ymKZeatA6NGIo9aSD9CS8zYtZ5PKUI4RkPbczpsR6q+N1v47iTH1pWykYlb1Ciz1JvknpYpSzmkKhgeNQ8RgdABJyaQ30yvyIOn4oRJAVXaFW1FwDl7TNN7iI+OMcyHeO2TfrNXCh9PS67rK3iqCTA= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com; spf=pass smtp.mailfrom=redhat.com; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b=a6BA3Xys; arc=none smtp.client-ip=170.10.129.124 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=quarantine dis=none) header.from=redhat.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=redhat.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=redhat.com header.i=@redhat.com header.b="a6BA3Xys" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1768567260; 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=vLpeu4A2UKAqTMt9/lrOMyA7DXUyISK6lakz2qqidVg=; b=a6BA3XysNCREZKvcwWdaomAaEnjiErFJU93UEVAl7Ocv27jSuogUEukEBNW4fUjfAefJnc ZMhH5nj9qrX6Am0hl66xLfEXwYc998GW5+4CEuyMRYqEECzD9vX5jDoWWZgUtslqPT7Ydk 7/mUsBaEqmTa33JHv/0BuZkyiZdamp0= Received: from mx-prod-mc-08.mail-002.prod.us-west-2.aws.redhat.com (ec2-35-165-154-97.us-west-2.compute.amazonaws.com [35.165.154.97]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-673-MZ3HPFOFMNifGYmyPTfyYA-1; Fri, 16 Jan 2026 07:40:56 -0500 X-MC-Unique: MZ3HPFOFMNifGYmyPTfyYA-1 X-Mimecast-MFC-AGG-ID: MZ3HPFOFMNifGYmyPTfyYA_1768567255 Received: from mx-prod-int-05.mail-002.prod.us-west-2.aws.redhat.com (mx-prod-int-05.mail-002.prod.us-west-2.aws.redhat.com [10.30.177.17]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mx-prod-mc-08.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTPS id 665C2180044D; Fri, 16 Jan 2026 12:40:55 +0000 (UTC) Received: from gmonaco-thinkpadt14gen3.rmtit.csb (unknown [10.45.224.42]) by mx-prod-int-05.mail-002.prod.us-west-2.aws.redhat.com (Postfix) with ESMTP id 8CAC11955F22; Fri, 16 Jan 2026 12:40:50 +0000 (UTC) From: Gabriele Monaco To: linux-kernel@vger.kernel.org, Steven Rostedt , Nam Cao , Juri Lelli , Gabriele Monaco , Jonathan Corbet , Masami Hiramatsu , linux-trace-kernel@vger.kernel.org, linux-doc@vger.kernel.org Cc: Peter Zijlstra , Tomas Glozar , Clark Williams , John Kacur Subject: [PATCH v4 15/15] rv: Add dl_server specific monitors Date: Fri, 16 Jan 2026 13:39:11 +0100 Message-ID: <20260116123911.130300-16-gmonaco@redhat.com> In-Reply-To: <20260116123911.130300-1-gmonaco@redhat.com> References: <20260116123911.130300-1-gmonaco@redhat.com> 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 X-Scanned-By: MIMEDefang 3.0 on 10.30.177.17 Content-Type: text/plain; charset="utf-8" Add monitors to validate the behaviour of the deadline server. The currently implemented monitors are: * boost fair tasks run either independently or boosted * laxity deferrable servers wait for zero-laxity and run Cc: Peter Zijlstra Reviewed-by: Nam Cao Signed-off-by: Gabriele Monaco --- Notes: V4 * Rely on enqueue/dequeue tracepoints instead of syscalls * Improve timing conditions in laxity and handle resume action * Remove fragile Stopping state from boost Documentation/trace/rv/monitor_deadline.rst | 118 +++++++++ kernel/trace/rv/Kconfig | 2 + kernel/trace/rv/Makefile | 2 + kernel/trace/rv/monitors/boost/Kconfig | 15 ++ kernel/trace/rv/monitors/boost/boost.c | 232 ++++++++++++++++ kernel/trace/rv/monitors/boost/boost.h | 146 +++++++++++ kernel/trace/rv/monitors/boost/boost_trace.h | 19 ++ kernel/trace/rv/monitors/laxity/Kconfig | 14 + kernel/trace/rv/monitors/laxity/laxity.c | 248 ++++++++++++++++++ kernel/trace/rv/monitors/laxity/laxity.h | 133 ++++++++++ .../trace/rv/monitors/laxity/laxity_trace.h | 19 ++ kernel/trace/rv/rv_trace.h | 2 + tools/verification/models/deadline/boost.dot | 48 ++++ tools/verification/models/deadline/laxity.dot | 37 +++ 14 files changed, 1035 insertions(+) create mode 100644 kernel/trace/rv/monitors/boost/Kconfig create mode 100644 kernel/trace/rv/monitors/boost/boost.c create mode 100644 kernel/trace/rv/monitors/boost/boost.h create mode 100644 kernel/trace/rv/monitors/boost/boost_trace.h create mode 100644 kernel/trace/rv/monitors/laxity/Kconfig create mode 100644 kernel/trace/rv/monitors/laxity/laxity.c create mode 100644 kernel/trace/rv/monitors/laxity/laxity.h create mode 100644 kernel/trace/rv/monitors/laxity/laxity_trace.h create mode 100644 tools/verification/models/deadline/boost.dot create mode 100644 tools/verification/models/deadline/laxity.dot diff --git a/Documentation/trace/rv/monitor_deadline.rst b/Documentation/tr= ace/rv/monitor_deadline.rst index a5492c77ea9e..b4e4c125cafd 100644 --- a/Documentation/trace/rv/monitor_deadline.rst +++ b/Documentation/trace/rv/monitor_deadline.rst @@ -150,3 +150,121 @@ is applied:: +--------------+ <- dl_server_idle sched_switch_suspend ^ | | +------ dl_throttle;is_constr_dl =3D=3D 1 || is_defer =3D=3D 1 ---= ---+ + +Monitor boost +~~~~~~~~~~~~~ + +The boost monitor ensures tasks associated to a server (e.g. fair tasks) r= un +either independently or boosted in a timely manner. +Unlike other models, the ``running`` state (and the ``switch_in/out`` even= ts) +indicates that any fair task is running, this needs to happen within a +threshold that depends on server deadline and remaining runtime, whenever a +task is ready. + +The following chart is simplified to avoid confusion, several less importa= nt +self-loops on states have been removed and event names have been simplifie= d: + +* ``idle`` (``dl_server_idle``) occurs when the CPU runs the idle task. +* ``start/stop`` (``dl_server_start/stop``) start and stop the server. +* ``switch`` (``sched_switch_in/out``) represented as a double arrow to + indicate both edges are present: ``ready -- switch_in -> running`` and + ``running -- switch_out -> ready``. As stated above this fires when any = fair + task starts or stops to running. +* ``resume/resume_throttle``: a fair task woke up, potentially when the se= rver + is throttled (no runtime left), this event is especially frequent on self + loops (no state change during a wakeup) but is removed here for clarity. +* arrows merge with an ``x`` sign to indicate they are the same event goin= g to + the same state (but with different origins, e.g. ``{idle/throttled} -- s= top + -> stopped``). The ``+`` sign indicates standard crossings or corners. + +Refer to the dot file for the full specification:: + + | + v + #=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D# sto= p;reset(clk) + H H <---------------+ + +------------>H stopped H | + | H H | + | #=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D# = | + | ^ | | + | | | | replenish;reset(c= lk) + | stop | | +--+ + | | start;reset(clk) +-----------------+ | | + | | v | | v + | +---------------+ <---------- switch --------> +-------= --+ + | +- resume -> | ready | | = | + | | | | -replenish;reset(clk) | runnin= g | + | | +- idle - | clk < thesh() | | | = | + | | | +---------------+ <-+ +---------------- +-------= --+ + | | | | ^ | ^ | + | | | | | throttle | | + | | | | |replenish;reset(clk) | | | + | | | throttle | | replenish;reset(clk) | + | | | | | | | | + | | | v | v | | + | | | +---------+ switch +-------------------+ | | + x---+--+-- | | <----------> | throttled_running | --------+ | + | | | |throttled| +-------------------+ | + | | | | | -----+ | | + | | | +---------+ | | | + | | | ^ | | | + | | | resume_throttle | | | + stop | | | | | | + | | v | | | | + | +---------+ <-----------x--- idle ---x-----------------------------+ + | | | + +-- | idle | <--+ + | | | replenish;reset(clk) + +---------+ ---+ + +Monitor laxity +~~~~~~~~~~~~~~ + +The laxity monitor ensure deferrable servers go to a zero-laxity wait unle= ss +already running and run in starvation cases. The model can stay in the +zero-laxity wait only for up to a period, then the server either prepares = to +stop (after ``idle_wait``) or prepares to boost a task (``running``). Boos= ting +(``sched_switch_in``) is only allowed in the ``running`` state. +``dl_replenish_running`` should not be allowed in ``running``, but can hap= pen +as soon as the server started, the model allows this only within a short +threshold:: + + | + +---- dl_server_stop -----+ | + | v v + | #=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# + | +------- H stopped H + | | #=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# + | | | ^ + | | dl_server_start_running; dl_server_stop + | | reset(clk) | + | | v | dl_replenish_running; + | | +-------------------------------------+ clk < REPLENISH_NS + | | | | -------------+ + | | | running | | + | | | | <------------+ + | | +-------------------------------------+ + | | | ^ ^ + | | dl_throttle dl_replenish_running | + | | v | | + | | +-------------------+ -+ | + | | | replenish_wait | | dl_replenish_idle;reset= (clk) + | | | clk < period_ns() | ----------------+--------------------------= ----+ + | | +-------------------+ | = | + | | | | = | + | | dl_replenish;reset(clk) | dl_replenish_running = | + | | v | = | + | dl_server_start; +--------------------------+ dl_replenish;reset(c= lk) | + | reset(clk) | zero_laxity_wait | -------------+ = | + | | | clk < period_ns() | | = | + | +---------------> | | <------------+ = | + | +--------------------------+ = | + | | ^ = | + | dl_replenish_idle;reset(clk) | dl_replenish;reset(clk) = | + | v | = | + | +------------------------+ | = | + +----------------- | idle_wait | -+ = | + | clk < period_ns() | = | + +------------------------+ <--------------------------= ----+ + ^ dl_replenish_idle;reset(clk) + +-------------+ diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig index 719cdcfb6d41..139443e0e51c 100644 --- a/kernel/trace/rv/Kconfig +++ b/kernel/trace/rv/Kconfig @@ -82,6 +82,8 @@ source "kernel/trace/rv/monitors/stall/Kconfig" source "kernel/trace/rv/monitors/deadline/Kconfig" source "kernel/trace/rv/monitors/nomiss/Kconfig" source "kernel/trace/rv/monitors/throttle/Kconfig" +source "kernel/trace/rv/monitors/boost/Kconfig" +source "kernel/trace/rv/monitors/laxity/Kconfig" # Add new deadline monitors here =20 # Add new monitors here diff --git a/kernel/trace/rv/Makefile b/kernel/trace/rv/Makefile index 15a1edc8bd0f..4cf15c189a96 100644 --- a/kernel/trace/rv/Makefile +++ b/kernel/trace/rv/Makefile @@ -21,6 +21,8 @@ obj-$(CONFIG_RV_MON_STALL) +=3D monitors/stall/stall.o obj-$(CONFIG_RV_MON_DEADLINE) +=3D monitors/deadline/deadline.o obj-$(CONFIG_RV_MON_NOMISS) +=3D monitors/nomiss/nomiss.o obj-$(CONFIG_RV_MON_THROTTLE) +=3D monitors/throttle/throttle.o +obj-$(CONFIG_RV_MON_BOOST) +=3D monitors/boost/boost.o +obj-$(CONFIG_RV_MON_LAXITY) +=3D monitors/laxity/laxity.o # Add new monitors here obj-$(CONFIG_RV_REACTORS) +=3D rv_reactors.o obj-$(CONFIG_RV_REACT_PRINTK) +=3D reactor_printk.o diff --git a/kernel/trace/rv/monitors/boost/Kconfig b/kernel/trace/rv/monit= ors/boost/Kconfig new file mode 100644 index 000000000000..3fa121f77729 --- /dev/null +++ b/kernel/trace/rv/monitors/boost/Kconfig @@ -0,0 +1,15 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_BOOST + depends on RV + depends on RV_MON_DEADLINE + default y + select HA_MON_EVENTS_ID + bool "boost monitor" + help + Monitor to ensure tasks associated to a server (e.g. fair tasks) run + either independently or boosted in a timely manner. + This monitor is part of the deadline monitors collection. + + For further information, see: + Documentation/trace/rv/monitor_deadline.rst diff --git a/kernel/trace/rv/monitors/boost/boost.c b/kernel/trace/rv/monit= ors/boost/boost.c new file mode 100644 index 000000000000..c8ae75cb6fd7 --- /dev/null +++ b/kernel/trace/rv/monitors/boost/boost.c @@ -0,0 +1,232 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "boost" + +#include +#include + +#define RV_MON_TYPE RV_MON_PER_OBJ +#define DA_SKIP_AUTO_ALLOC +#define HA_TIMER_TYPE HA_TIMER_WHEEL +typedef struct sched_dl_entity *monitor_target; +#include "boost.h" +#include +#include + +static inline u64 server_threshold_ns(struct ha_monitor *ha_mon) +{ + struct sched_dl_entity *dl_se =3D ha_get_target(ha_mon); + + return dl_se->dl_deadline + TICK_NSEC - dl_se->runtime; +} + +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_boost env, u64 = time_ns) +{ + if (env =3D=3D clk_boost) + return ha_get_clk_ns(ha_mon, env, time_ns); + return ENV_INVALID_VALUE; +} + +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_boost env, u= 64 time_ns) +{ + if (env =3D=3D clk_boost) + ha_reset_clk_ns(ha_mon, env, time_ns); +} + +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state =3D=3D ready_boost) + return ha_check_invariant_ns(ha_mon, clk_boost, time_ns); + return true; +} + +static inline bool ha_verify_guards(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + bool res =3D true; + + if (curr_state =3D=3D idle_boost && event =3D=3D dl_replenish_boost) + ha_reset_env(ha_mon, clk_boost, time_ns); + else if (curr_state =3D=3D ready_boost && event =3D=3D dl_replenish_boost) + ha_reset_env(ha_mon, clk_boost, time_ns); + else if (curr_state =3D=3D running_boost && event =3D=3D dl_replenish_boo= st) + ha_reset_env(ha_mon, clk_boost, time_ns); + else if (curr_state =3D=3D stopped_boost && event =3D=3D dl_server_start_= boost) + ha_reset_env(ha_mon, clk_boost, time_ns); + else if (curr_state =3D=3D throttled_boost && event =3D=3D dl_replenish_b= oost) + ha_reset_env(ha_mon, clk_boost, time_ns); + else if (curr_state =3D=3D throttled_running_boost && event =3D=3D dl_rep= lenish_boost) + ha_reset_env(ha_mon, clk_boost, time_ns); + return res; +} + +static inline void ha_setup_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (next_state =3D=3D curr_state && event !=3D dl_replenish_boost) + return; + if (next_state =3D=3D ready_boost) + ha_start_timer_ns(ha_mon, clk_boost, server_threshold_ns(ha_mon), time_n= s); + else if (curr_state =3D=3D ready_boost) + ha_cancel_timer(ha_mon); +} + +static bool ha_verify_constraint(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns); + + return true; +} + +static void handle_dl_replenish(void *data, struct sched_dl_entity *dl_se,= int cpu) +{ + da_handle_event(EXPAND_ID(dl_se, cpu), dl_replenish_boost); +} + +static void handle_sched_switch(void *data, bool preempt, + struct task_struct *prev, + struct task_struct *next, + unsigned int prev_state) +{ + struct sched_dl_entity *dl_se =3D get_fair_server(next); + int cpu =3D task_cpu(next); + + /* + * The server is available in next only if the next task is boosted, + * otherwise we need to retrieve it. + * This monitor considers switch in/out whenever a task related to the + * server (i.e. fair) is scheduled in or out, boosted or not. + * Any switch to the same policy is ignored. + * PI boosted tasks are not considered fair. + */ + if (!dl_se || (next->policy =3D=3D prev->policy && !is_idle_task(next) && + !is_idle_task(prev))) + return; + if (is_idle_task(next)) + da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_idle_boost); + else if (next->policy =3D=3D SCHED_NORMAL && !rt_or_dl_task(next)) + da_handle_event(EXPAND_ID(dl_se, cpu), sched_switch_in_boost); + else if (prev->policy =3D=3D SCHED_NORMAL && !is_idle_task(prev)) + da_handle_event(EXPAND_ID(dl_se, cpu), sched_switch_out_boost); +} + +static void handle_sched_enqueue(void *data, struct task_struct *tsk, int = cpu) +{ + struct sched_dl_entity *dl_se =3D get_fair_server(tsk); + + if (dl_se && tsk->policy =3D=3D SCHED_NORMAL) { + da_handle_event(EXPAND_ID(dl_se, cpu), + dl_se->runtime > 0 ? + dl_server_resume_boost : + dl_server_resume_throttled_boost); + } +} + +static void handle_sched_dequeue(void *data, struct task_struct *tsk, int = cpu) +{ + struct sched_dl_entity *dl_se =3D get_fair_server(tsk); + + /* + * A dequeue is counted as switching out only in case of a change in + * scheduler where the task is moved to another scheduler's runqueue. + */ + if (dl_se && tsk->policy =3D=3D SCHED_NORMAL && task_is_running(tsk) && s= ched_task_on_rq(tsk)) + da_handle_event(EXPAND_ID(dl_se, cpu), sched_switch_out_boost); +} + +static void handle_dl_server_start(void *data, struct sched_dl_entity *dl_= se, int cpu) +{ + da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_start_boost); +} + +static void handle_dl_server_stop(void *data, struct sched_dl_entity *dl_s= e, int cpu) +{ + da_handle_start_event(EXPAND_ID(dl_se, cpu), dl_server_stop_boost); +} + +static void handle_dl_throttle(void *data, struct sched_dl_entity *dl_se, = int cpu) +{ + da_handle_event(EXPAND_ID(dl_se, cpu), dl_throttle_boost); +} + +static int enable_boost(void) +{ + int retval; + + retval =3D da_monitor_init(); + if (retval) + return retval; + + retval =3D init_storage(true); + if (retval) + return retval; + rv_attach_trace_probe("boost", sched_dl_replenish_tp, handle_dl_replenish= ); + rv_attach_trace_probe("boost", sched_dl_server_start_tp, handle_dl_server= _start); + rv_attach_trace_probe("boost", sched_dl_server_stop_tp, handle_dl_server_= stop); + rv_attach_trace_probe("boost", sched_dl_throttle_tp, handle_dl_throttle); + rv_attach_trace_probe("boost", sched_enqueue_tp, handle_sched_enqueue); + rv_attach_trace_probe("boost", sched_dequeue_tp, handle_sched_dequeue); + rv_attach_trace_probe("boost", sched_switch, handle_sched_switch); + + return 0; +} + +static void disable_boost(void) +{ + rv_this.enabled =3D 0; + + rv_detach_trace_probe("boost", sched_dl_replenish_tp, handle_dl_replenish= ); + rv_detach_trace_probe("boost", sched_dl_server_start_tp, handle_dl_server= _start); + rv_detach_trace_probe("boost", sched_dl_server_stop_tp, handle_dl_server_= stop); + rv_detach_trace_probe("boost", sched_dl_throttle_tp, handle_dl_throttle); + rv_detach_trace_probe("boost", sched_enqueue_tp, handle_sched_enqueue); + rv_detach_trace_probe("boost", sched_dequeue_tp, handle_sched_dequeue); + rv_detach_trace_probe("boost", sched_switch, handle_sched_switch); + + da_monitor_destroy(); +} + +static struct rv_monitor rv_this =3D { + .name =3D "boost", + .description =3D "fair tasks run either independently or boosted.", + .enable =3D enable_boost, + .disable =3D disable_boost, + .reset =3D da_monitor_reset_all, + .enabled =3D 0, +}; + +static int __init register_boost(void) +{ + return rv_register_monitor(&rv_this, &rv_deadline); +} + +static void __exit unregister_boost(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_boost); +module_exit(unregister_boost); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Gabriele Monaco "); +MODULE_DESCRIPTION("boost: fair tasks run either independently or boosted.= "); diff --git a/kernel/trace/rv/monitors/boost/boost.h b/kernel/trace/rv/monit= ors/boost/boost.h new file mode 100644 index 000000000000..70757f25a90d --- /dev/null +++ b/kernel/trace/rv/monitors/boost/boost.h @@ -0,0 +1,146 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of boost automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME boost + +enum states_boost { + stopped_boost, + idle_boost, + ready_boost, + running_boost, + throttled_boost, + throttled_running_boost, + state_max_boost, +}; + +#define INVALID_STATE state_max_boost + +enum events_boost { + dl_replenish_boost, + dl_server_idle_boost, + dl_server_resume_boost, + dl_server_resume_throttled_boost, + dl_server_start_boost, + dl_server_stop_boost, + dl_throttle_boost, + sched_switch_in_boost, + sched_switch_out_boost, + event_max_boost, +}; + +enum envs_boost { + clk_boost, + env_max_boost, + env_max_stored_boost =3D env_max_boost, +}; + +_Static_assert(env_max_stored_boost <=3D MAX_HA_ENV_LEN, "Not enough slots= "); +#define HA_CLK_NS + +struct automaton_boost { + char *state_names[state_max_boost]; + char *event_names[event_max_boost]; + char *env_names[env_max_boost]; + unsigned char function[state_max_boost][event_max_boost]; + unsigned char initial_state; + bool final_states[state_max_boost]; +}; + +static const struct automaton_boost automaton_boost =3D { + .state_names =3D { + "stopped", + "idle", + "ready", + "running", + "throttled", + "throttled_running", + }, + .event_names =3D { + "dl_replenish", + "dl_server_idle", + "dl_server_resume", + "dl_server_resume_throttled", + "dl_server_start", + "dl_server_stop", + "dl_throttle", + "sched_switch_in", + "sched_switch_out", + }, + .env_names =3D { + "clk", + }, + .function =3D { + { + INVALID_STATE, + stopped_boost, + stopped_boost, + stopped_boost, + ready_boost, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + stopped_boost, + }, + { + idle_boost, + idle_boost, + ready_boost, + throttled_boost, + INVALID_STATE, + stopped_boost, + idle_boost, + INVALID_STATE, + INVALID_STATE, + }, + { + ready_boost, + idle_boost, + ready_boost, + ready_boost, + INVALID_STATE, + stopped_boost, + throttled_boost, + running_boost, + ready_boost, + }, + { + running_boost, + idle_boost, + running_boost, + running_boost, + INVALID_STATE, + stopped_boost, + throttled_running_boost, + INVALID_STATE, + ready_boost, + }, + { + ready_boost, + idle_boost, + INVALID_STATE, + throttled_boost, + INVALID_STATE, + stopped_boost, + throttled_boost, + throttled_running_boost, + INVALID_STATE, + }, + { + running_boost, + idle_boost, + INVALID_STATE, + throttled_running_boost, + INVALID_STATE, + INVALID_STATE, + throttled_running_boost, + INVALID_STATE, + throttled_boost, + }, + }, + .initial_state =3D stopped_boost, + .final_states =3D { 1, 0, 0, 0, 0, 0 }, +}; diff --git a/kernel/trace/rv/monitors/boost/boost_trace.h b/kernel/trace/rv= /monitors/boost/boost_trace.h new file mode 100644 index 000000000000..7e422b0e586d --- /dev/null +++ b/kernel/trace/rv/monitors/boost/boost_trace.h @@ -0,0 +1,19 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_BOOST +DEFINE_EVENT(event_da_monitor_id, event_boost, + TP_PROTO(int id, char *state, char *event, char *next_state, bool fi= nal_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_boost, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); + +DEFINE_EVENT(error_env_da_monitor_id, error_env_boost, + TP_PROTO(int id, char *state, char *event, char *env), + TP_ARGS(id, state, event, env)); +#endif /* CONFIG_RV_MON_BOOST */ diff --git a/kernel/trace/rv/monitors/laxity/Kconfig b/kernel/trace/rv/moni= tors/laxity/Kconfig new file mode 100644 index 000000000000..7ba69405d09b --- /dev/null +++ b/kernel/trace/rv/monitors/laxity/Kconfig @@ -0,0 +1,14 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_LAXITY + depends on RV + depends on RV_MON_DEADLINE + default y + select HA_MON_EVENTS_ID + bool "laxity monitor" + help + Monitor to ensure deferrable servers go to a zero-laxity wait unless + already running and run in starvation cases. + + For further information, see: + Documentation/trace/rv/monitor_deadline.rst diff --git a/kernel/trace/rv/monitors/laxity/laxity.c b/kernel/trace/rv/mon= itors/laxity/laxity.c new file mode 100644 index 000000000000..3e9cd795586e --- /dev/null +++ b/kernel/trace/rv/monitors/laxity/laxity.c @@ -0,0 +1,248 @@ +// SPDX-License-Identifier: GPL-2.0 +#include +#include +#include +#include +#include +#include +#include + +#define MODULE_NAME "laxity" + +#include +#include + +#define RV_MON_TYPE RV_MON_PER_OBJ +#define HA_TIMER_TYPE HA_TIMER_WHEEL +/* The start condition is on server_stop, allocation likely fails on PREEM= PT_RT */ +#define DA_SKIP_AUTO_ALLOC +typedef struct sched_dl_entity *monitor_target; +#include "laxity.h" +#include +#include + +/* allow replenish when running only right after server start */ +#define REPLENISH_NS TICK_NSEC + +static inline u64 period_ns(struct ha_monitor *ha_mon) +{ + return ha_get_target(ha_mon)->dl_period + TICK_NSEC; +} + +static u64 ha_get_env(struct ha_monitor *ha_mon, enum envs_laxity env, u64= time_ns) +{ + if (env =3D=3D clk_laxity) + return ha_get_clk_ns(ha_mon, env, time_ns); + return ENV_INVALID_VALUE; +} + +static void ha_reset_env(struct ha_monitor *ha_mon, enum envs_laxity env, = u64 time_ns) +{ + if (env =3D=3D clk_laxity) + ha_reset_clk_ns(ha_mon, env, time_ns); +} + +static inline bool ha_verify_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state =3D=3D idle_wait_laxity) + return ha_check_invariant_ns(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D replenish_wait_laxity) + return ha_check_invariant_ns(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D zero_laxity_wait_laxity) + return ha_check_invariant_ns(ha_mon, clk_laxity, time_ns); + return true; +} + +static inline void ha_convert_inv_guard(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (curr_state =3D=3D next_state) + return; + if (curr_state =3D=3D zero_laxity_wait_laxity) + ha_inv_to_guard(ha_mon, clk_laxity, period_ns(ha_mon), time_ns); +} + +static inline bool ha_verify_guards(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + bool res =3D true; + + if (curr_state =3D=3D idle_wait_laxity && event =3D=3D dl_replenish_idle_= laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D idle_wait_laxity && event =3D=3D dl_replenish_= laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D replenish_wait_laxity && event =3D=3D dl_reple= nish_running_laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D replenish_wait_laxity && event =3D=3D dl_reple= nish_laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D replenish_wait_laxity && event =3D=3D dl_reple= nish_idle_laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D running_laxity && event =3D=3D dl_throttle_lax= ity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D running_laxity && event =3D=3D dl_replenish_ru= nning_laxity) + res =3D ha_monitor_env_invalid(ha_mon, clk_laxity) || + ha_get_env(ha_mon, clk_laxity, time_ns) < REPLENISH_NS; + else if (curr_state =3D=3D stopped_laxity && event =3D=3D dl_server_start= _running_laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D stopped_laxity && event =3D=3D dl_server_start= _laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D zero_laxity_wait_laxity && event =3D=3D dl_rep= lenish_idle_laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D zero_laxity_wait_laxity && event =3D=3D dl_rep= lenish_running_laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + else if (curr_state =3D=3D zero_laxity_wait_laxity && event =3D=3D dl_rep= lenish_laxity) + ha_reset_env(ha_mon, clk_laxity, time_ns); + return res; +} + +static inline void ha_setup_invariants(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (next_state =3D=3D curr_state && event !=3D dl_replenish_laxity && + event !=3D dl_replenish_idle_laxity) + return; + if (next_state =3D=3D idle_wait_laxity) + ha_start_timer_ns(ha_mon, clk_laxity, period_ns(ha_mon), time_ns); + else if (next_state =3D=3D replenish_wait_laxity) + ha_start_timer_ns(ha_mon, clk_laxity, period_ns(ha_mon), time_ns); + else if (next_state =3D=3D zero_laxity_wait_laxity) + ha_start_timer_ns(ha_mon, clk_laxity, period_ns(ha_mon), time_ns); + else if (curr_state =3D=3D idle_wait_laxity) + ha_cancel_timer(ha_mon); + else if (curr_state =3D=3D replenish_wait_laxity) + ha_cancel_timer(ha_mon); + else if (curr_state =3D=3D zero_laxity_wait_laxity) + ha_cancel_timer(ha_mon); +} + +static bool ha_verify_constraint(struct ha_monitor *ha_mon, + enum states curr_state, enum events event, + enum states next_state, u64 time_ns) +{ + if (!ha_verify_invariants(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_convert_inv_guard(ha_mon, curr_state, event, next_state, time_ns); + + if (!ha_verify_guards(ha_mon, curr_state, event, next_state, time_ns)) + return false; + + ha_setup_invariants(ha_mon, curr_state, event, next_state, time_ns); + + return true; +} + +static void handle_dl_replenish(void *data, struct sched_dl_entity *dl_se,= int cpu) +{ + /* Special replenish happening after throttle, ignore it */ + if (dl_se->dl_defer_running && dl_se->dl_throttled) + return; + if (dl_se->dl_defer_running) + da_handle_event(EXPAND_ID(dl_se, cpu), dl_replenish_running_laxity); + else if (idle_cpu(cpu)) + da_handle_event(EXPAND_ID(dl_se, cpu), dl_replenish_idle_laxity); + else + da_handle_event(EXPAND_ID(dl_se, cpu), dl_replenish_laxity); +} + +static void handle_dl_server_start(void *data, struct sched_dl_entity *dl_= se, int cpu) +{ + if (dl_se->dl_defer_running) + da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_start_running_laxity); + else + da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_start_laxity); +} + +static void handle_dl_server_stop(void *data, struct sched_dl_entity *dl_s= e, int cpu) +{ + da_handle_start_event(EXPAND_ID(dl_se, cpu), dl_server_stop_laxity); +} + +static void handle_dl_throttle(void *data, struct sched_dl_entity *dl_se, = int cpu) +{ + da_handle_event(EXPAND_ID(dl_se, cpu), dl_throttle_laxity); +} + +static void handle_sched_switch(void *data, bool preempt, + struct task_struct *prev, + struct task_struct *next, + unsigned int prev_state) +{ + if (next->dl_server) + da_handle_event(EXPAND_ID(next->dl_server, task_cpu(next)), + sched_switch_in_laxity); +} + +static void handle_sched_enqueue(void *data, struct task_struct *tsk, int = cpu) +{ + struct sched_dl_entity *dl_se =3D get_fair_server(tsk); + + if (dl_se && tsk->policy =3D=3D SCHED_NORMAL) + da_handle_event(EXPAND_ID(dl_se, cpu), dl_server_resume_laxity); +} + +static int enable_laxity(void) +{ + int retval; + + retval =3D da_monitor_init(); + if (retval) + return retval; + + retval =3D init_storage(true); + if (retval) + return retval; + rv_attach_trace_probe("laxity", sched_dl_replenish_tp, handle_dl_replenis= h); + rv_attach_trace_probe("laxity", sched_dl_server_start_tp, handle_dl_serve= r_start); + rv_attach_trace_probe("laxity", sched_dl_server_stop_tp, handle_dl_server= _stop); + rv_attach_trace_probe("laxity", sched_dl_throttle_tp, handle_dl_throttle); + rv_attach_trace_probe("laxity", sched_switch, handle_sched_switch); + rv_attach_trace_probe("laxity", sched_enqueue_tp, handle_sched_enqueue); + + return 0; +} + +static void disable_laxity(void) +{ + rv_this.enabled =3D 0; + + rv_detach_trace_probe("laxity", sched_dl_replenish_tp, handle_dl_replenis= h); + rv_detach_trace_probe("laxity", sched_dl_server_start_tp, handle_dl_serve= r_start); + rv_detach_trace_probe("laxity", sched_dl_server_stop_tp, handle_dl_server= _stop); + rv_detach_trace_probe("laxity", sched_dl_throttle_tp, handle_dl_throttle); + rv_detach_trace_probe("laxity", sched_switch, handle_sched_switch); + rv_detach_trace_probe("laxity", sched_enqueue_tp, handle_sched_enqueue); + + da_monitor_destroy(); +} + +static struct rv_monitor rv_this =3D { + .name =3D "laxity", + .description =3D "deferrable servers wait for zero-laxity and run.", + .enable =3D enable_laxity, + .disable =3D disable_laxity, + .reset =3D da_monitor_reset_all, + .enabled =3D 0, +}; + +static int __init register_laxity(void) +{ + return rv_register_monitor(&rv_this, &rv_deadline); +} + +static void __exit unregister_laxity(void) +{ + rv_unregister_monitor(&rv_this); +} + +module_init(register_laxity); +module_exit(unregister_laxity); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("Gabriele Monaco "); +MODULE_DESCRIPTION("laxity: deferrable servers wait for zero-laxity and ru= n."); diff --git a/kernel/trace/rv/monitors/laxity/laxity.h b/kernel/trace/rv/mon= itors/laxity/laxity.h new file mode 100644 index 000000000000..d89dd296bf51 --- /dev/null +++ b/kernel/trace/rv/monitors/laxity/laxity.h @@ -0,0 +1,133 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Automatically generated C representation of laxity automaton + * For further information about this format, see kernel documentation: + * Documentation/trace/rv/deterministic_automata.rst + */ + +#define MONITOR_NAME laxity + +enum states_laxity { + stopped_laxity, + idle_wait_laxity, + replenish_wait_laxity, + running_laxity, + zero_laxity_wait_laxity, + state_max_laxity, +}; + +#define INVALID_STATE state_max_laxity + +enum events_laxity { + dl_replenish_laxity, + dl_replenish_idle_laxity, + dl_replenish_running_laxity, + dl_server_resume_laxity, + dl_server_start_laxity, + dl_server_start_running_laxity, + dl_server_stop_laxity, + dl_throttle_laxity, + sched_switch_in_laxity, + event_max_laxity, +}; + +enum envs_laxity { + clk_laxity, + env_max_laxity, + env_max_stored_laxity =3D env_max_laxity, +}; + +_Static_assert(env_max_stored_laxity <=3D MAX_HA_ENV_LEN, "Not enough slot= s"); +#define HA_CLK_NS + +struct automaton_laxity { + char *state_names[state_max_laxity]; + char *event_names[event_max_laxity]; + char *env_names[env_max_laxity]; + unsigned char function[state_max_laxity][event_max_laxity]; + unsigned char initial_state; + bool final_states[state_max_laxity]; +}; + +static const struct automaton_laxity automaton_laxity =3D { + .state_names =3D { + "stopped", + "idle_wait", + "replenish_wait", + "running", + "zero_laxity_wait", + }, + .event_names =3D { + "dl_replenish", + "dl_replenish_idle", + "dl_replenish_running", + "dl_server_resume", + "dl_server_start", + "dl_server_start_running", + "dl_server_stop", + "dl_throttle", + "sched_switch_in", + }, + .env_names =3D { + "clk", + }, + .function =3D { + { + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + stopped_laxity, + zero_laxity_wait_laxity, + running_laxity, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + }, + { + zero_laxity_wait_laxity, + idle_wait_laxity, + INVALID_STATE, + zero_laxity_wait_laxity, + INVALID_STATE, + INVALID_STATE, + stopped_laxity, + INVALID_STATE, + INVALID_STATE, + }, + { + zero_laxity_wait_laxity, + idle_wait_laxity, + running_laxity, + replenish_wait_laxity, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + }, + { + INVALID_STATE, + INVALID_STATE, + running_laxity, + running_laxity, + INVALID_STATE, + INVALID_STATE, + stopped_laxity, + replenish_wait_laxity, + running_laxity, + }, + { + zero_laxity_wait_laxity, + idle_wait_laxity, + running_laxity, + zero_laxity_wait_laxity, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + INVALID_STATE, + }, + }, + .initial_state =3D stopped_laxity, + .final_states =3D { 1, 0, 0, 0, 0 }, +}; diff --git a/kernel/trace/rv/monitors/laxity/laxity_trace.h b/kernel/trace/= rv/monitors/laxity/laxity_trace.h new file mode 100644 index 000000000000..32580dba8f42 --- /dev/null +++ b/kernel/trace/rv/monitors/laxity/laxity_trace.h @@ -0,0 +1,19 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_LAXITY +DEFINE_EVENT(event_da_monitor_id, event_laxity, + TP_PROTO(int id, char *state, char *event, char *next_state, bool fi= nal_state), + TP_ARGS(id, state, event, next_state, final_state)); + +DEFINE_EVENT(error_da_monitor_id, error_laxity, + TP_PROTO(int id, char *state, char *event), + TP_ARGS(id, state, event)); + +DEFINE_EVENT(error_env_da_monitor_id, error_env_laxity, + TP_PROTO(int id, char *state, char *event, char *env), + TP_ARGS(id, state, event, env)); +#endif /* CONFIG_RV_MON_LAXITY */ diff --git a/kernel/trace/rv/rv_trace.h b/kernel/trace/rv/rv_trace.h index 1bf0f3666ee4..f1d55c39dc48 100644 --- a/kernel/trace/rv/rv_trace.h +++ b/kernel/trace/rv/rv_trace.h @@ -190,6 +190,8 @@ DECLARE_EVENT_CLASS(error_env_da_monitor_id, #include #include #include +#include +#include // Add new monitors based on CONFIG_HA_MON_EVENTS_ID here =20 #endif diff --git a/tools/verification/models/deadline/boost.dot b/tools/verificat= ion/models/deadline/boost.dot new file mode 100644 index 000000000000..aaab7d08fae6 --- /dev/null +++ b/tools/verification/models/deadline/boost.dot @@ -0,0 +1,48 @@ +digraph state_automaton { + center =3D true; + size =3D "7,11"; + {node [shape =3D circle] "idle"}; + {node [shape =3D circle] "ready"}; + {node [shape =3D circle] "running"}; + {node [shape =3D plaintext, style=3Dinvis, label=3D""] "__init_stopped"}; + {node [shape =3D doublecircle] "stopped"}; + {node [shape =3D circle] "stopped"}; + {node [shape =3D circle] "throttled"}; + {node [shape =3D circle] "throttled_running"}; + "__init_stopped" -> "stopped"; + "idle" [label =3D "idle"]; + "idle" -> "idle" [ label =3D "dl_server_idle\ndl_replenish;reset(clk)\ndl= _throttle" ]; + "idle" -> "ready" [ label =3D "dl_server_resume" ]; + "idle" -> "stopped" [ label =3D "dl_server_stop" ]; + "idle" -> "throttled" [ label =3D "dl_server_resume_throttled" ]; + "ready" [label =3D "ready\nclk < server_threshold_ns()"]; + "ready" -> "idle" [ label =3D "dl_server_idle" ]; + "ready" -> "ready" [ label =3D "sched_switch_out\ndl_server_resume_thrott= led\ndl_server_resume\ndl_replenish;reset(clk)" ]; + "ready" -> "running" [ label =3D "sched_switch_in" ]; + "ready" -> "stopped" [ label =3D "dl_server_stop" ]; + "ready" -> "throttled" [ label =3D "dl_throttle" ]; + "running" [label =3D "running"]; + "running" -> "idle" [ label =3D "dl_server_idle" ]; + "running" -> "ready" [ label =3D "sched_switch_out" ]; + "running" -> "running" [ label =3D "dl_server_resume_throttled\ndl_server= _resume\ndl_replenish;reset(clk)" ]; + "running" -> "stopped" [ label =3D "dl_server_stop" ]; + "running" -> "throttled_running" [ label =3D "dl_throttle" ]; + "stopped" [label =3D "stopped", color =3D green3]; + "stopped" -> "ready" [ label =3D "dl_server_start;reset(clk)" ]; + "stopped" -> "stopped" [ label =3D "dl_server_idle\nsched_switch_out\ndl_= server_resume\ndl_server_resume_throttled" ]; + "throttled" [label =3D "throttled"]; + "throttled" -> "idle" [ label =3D "dl_server_idle" ]; + "throttled" -> "ready" [ label =3D "dl_replenish;reset(clk)" ]; + "throttled" -> "stopped" [ label =3D "dl_server_stop" ]; + "throttled" -> "throttled" [ label =3D "dl_throttle\ndl_server_resume_thr= ottled" ]; + "throttled" -> "throttled_running" [ label =3D "sched_switch_in" ]; + "throttled_running" [label =3D "throttled_running"]; + "throttled_running" -> "idle" [ label =3D "dl_server_idle" ]; + "throttled_running" -> "running" [ label =3D "dl_replenish;reset(clk)" ]; + "throttled_running" -> "throttled" [ label =3D "sched_switch_out" ]; + "throttled_running" -> "throttled_running" [ label =3D "dl_throttle\ndl_s= erver_resume_throttled" ]; + { rank =3D min ; + "__init_stopped"; + "stopped"; + } +} diff --git a/tools/verification/models/deadline/laxity.dot b/tools/verifica= tion/models/deadline/laxity.dot new file mode 100644 index 000000000000..acece40c7971 --- /dev/null +++ b/tools/verification/models/deadline/laxity.dot @@ -0,0 +1,37 @@ +digraph state_automaton { + center =3D true; + size =3D "7,11"; + {node [shape =3D circle] "idle_wait"}; + {node [shape =3D circle] "replenish_wait"}; + {node [shape =3D circle] "running"}; + {node [shape =3D plaintext, style=3Dinvis, label=3D""] "__init_stopped"}; + {node [shape =3D doublecircle] "stopped"}; + {node [shape =3D circle] "stopped"}; + {node [shape =3D circle] "zero_laxity_wait"}; + "__init_stopped" -> "stopped"; + "idle_wait" [label =3D "idle_wait\nclk < period_ns()"]; + "idle_wait" -> "idle_wait" [ label =3D "dl_replenish_idle;reset(clk)" ]; + "idle_wait" -> "stopped" [ label =3D "dl_server_stop" ]; + "idle_wait" -> "zero_laxity_wait" [ label =3D "dl_replenish;reset(clk)\nd= l_server_resume" ]; + "replenish_wait" [label =3D "replenish_wait\nclk < period_ns()"]; + "replenish_wait" -> "idle_wait" [ label =3D "dl_replenish_idle;reset(clk)= " ]; + "replenish_wait" -> "replenish_wait" [ label =3D "dl_server_resume" ]; + "replenish_wait" -> "running" [ label =3D "dl_replenish_running;reset(clk= )" ]; + "replenish_wait" -> "zero_laxity_wait" [ label =3D "dl_replenish;reset(cl= k)" ]; + "running" [label =3D "running"]; + "running" -> "replenish_wait" [ label =3D "dl_throttle;reset(clk)" ]; + "running" -> "running" [ label =3D "sched_switch_in\ndl_server_resume\ndl= _replenish_running;clk < REPLENISH_NS" ]; + "running" -> "stopped" [ label =3D "dl_server_stop" ]; + "stopped" [label =3D "stopped", color =3D green3]; + "stopped" -> "running" [ label =3D "dl_server_start_running;reset(clk)" ]; + "stopped" -> "stopped" [ label =3D "dl_server_resume" ]; + "stopped" -> "zero_laxity_wait" [ label =3D "dl_server_start;reset(clk)" = ]; + "zero_laxity_wait" [label =3D "zero_laxity_wait\nclk < period_ns()"]; + "zero_laxity_wait" -> "idle_wait" [ label =3D "dl_replenish_idle;reset(cl= k)" ]; + "zero_laxity_wait" -> "running" [ label =3D "dl_replenish_running;reset(c= lk)" ]; + "zero_laxity_wait" -> "zero_laxity_wait" [ label =3D "dl_replenish;reset(= clk)\ndl_server_resume" ]; + { rank =3D min ; + "__init_stopped"; + "stopped"; + } +} --=20 2.52.0