From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from us-smtp-delivery-124.mimecast.com (us-smtp-delivery-124.mimecast.com [170.10.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 0B5CC4968E4 for ; Wed, 1 Jul 2026 12:29:26 +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=1782908968; cv=none; b=UUbX7XxXjpt+sbcTBdSUoqTmz2VRnpnAw1n0X+ssjMJ5q9Qk2fXlxGW95h3wuql3vcgjZpRq5DszsPFXRnn1V2VxpIwS+iUcJRutfIpSk+7D4YTllzNe5LxXh6h65LOMYWFjGkvqhN+f47y7EzzHSLhUvypYkxQGaS/rtXz62HA= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1782908968; c=relaxed/simple; bh=EsRgTGwn9/ciJwe1BkaH+LEHpHlf8QDoSBbMPs4cZVY=; h=Message-ID:Subject:From:To:Cc:Date:In-Reply-To:References: Content-Type:MIME-Version; b=k1V2HTYesmfGgHyg11JO9qdnCj389rOXJw4879pR5fD3LH4vxJd/xyC1t25RbP9+8ScefA9t6jPi/UCN6Ww6eOcpmIGNaJwjKvfGHKdYlA6kSIooLtB6JA3JtiiFBP4CZjeWgFrc2w3NDGu+8OG9YuBHProVpKpe3JL0KFbShWA= 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=DnGyxBLJ; dkim=pass (2048-bit key) header.d=redhat.com header.i=@redhat.com header.b=SL6mUymt; 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="DnGyxBLJ"; dkim=pass (2048-bit key) header.d=redhat.com header.i=@redhat.com header.b="SL6mUymt" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1782908966; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references:autocrypt:autocrypt; bh=8QBml1wXQrKkB4Dbp2yh/EBSKR66LFRDhLUx+zmUXDw=; b=DnGyxBLJJC7K1d7dbqdL6xChLQMKb9lljY90OQkodpZPpXQAZGzc6GZjexN0al1i1Yq57b az0OalWQFUfpCTFYTWn7cVF4rFsjDuDo06IFBg9fX7479jAjzKv8wKp9RTXfI/sjvf+/BH IMuHvH6bOyM32DMLLY1+tVRNp6+dKEM= Received: from mail-wm1-f71.google.com (mail-wm1-f71.google.com [209.85.128.71]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-255-kBV8HsFgODyXkCNNiJzyvg-1; Wed, 01 Jul 2026 08:29:23 -0400 X-MC-Unique: kBV8HsFgODyXkCNNiJzyvg-1 X-Mimecast-MFC-AGG-ID: kBV8HsFgODyXkCNNiJzyvg_1782908962 Received: by mail-wm1-f71.google.com with SMTP id 5b1f17b1804b1-493bc2b376fso3649635e9.3 for ; Wed, 01 Jul 2026 05:29:22 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=google; t=1782908962; x=1783513762; darn=vger.kernel.org; h=mime-version:user-agent:content-transfer-encoding:autocrypt :references:in-reply-to:date:cc:to:from:subject:message-id:from:to :cc:subject:date:message-id:reply-to; bh=8QBml1wXQrKkB4Dbp2yh/EBSKR66LFRDhLUx+zmUXDw=; b=SL6mUymt9O2j3NjXXcD4VjA8HECRahGlEVSS7X5Wgq/dv2QlAOk30Rwg6iOgRqEnFn uNCBD2QGci8iX8eMKrLiCHp+mLUP4hles+72Xiev7G6wcyciSAFbdaQYAPtNcRlSQkI2 CfiObUKhfloDNX0z1v9LaghXHqXXYHS7A9xTEaGP94c2Ybp1+N7zc4FyJVH/kZNvvHx8 RiYmcFsvHsZDfSgw7UrZE5yugdxqT5TN2uoIhPAhQM8Q6tWha8jVePVT5yDit53jLuRV +YEOREK0sx9eP1uzLpAA8TMXMnaP5dKGAwCICgPtmRK4obwefb9b9se7msduFanp1rRi 5MNw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1782908962; x=1783513762; h=mime-version:user-agent:content-transfer-encoding:autocrypt :references:in-reply-to:date:cc:to:from:subject:message-id:x-gm-gg :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=8QBml1wXQrKkB4Dbp2yh/EBSKR66LFRDhLUx+zmUXDw=; b=c7Wi23RBUBaR//TzLcD82YYUX3g6eo8n3+jPt3d13qmoPf8KP/7lVAGAaioLUwsBHj 7Y46JYpvIW+fKiYVBqRrR8vFq4GeOel5qbR5kOYCkkPck2QXhJGuvi2mZi7XMshjh1uC Z/63Mj9hOqYv4vr/Fae4yX3dOHw7rSDLP1KlEsCaAvOmoNJ+a5b4iRrefHH/nh2mvRl7 3JAOBDmn0tUuGFc3lfPd14yiCquD6xxdts41iGzyFr8TvqryRmSYGuR86f1+9hlmS2jy 12eISH1dA8sjyvrGpNDR/8sgjF3Df/YwRdS5iQkQszkG+3TFqqbLUzucgE/Y8KMCADmN /0JA== X-Forwarded-Encrypted: i=1; AFNElJ+ewYAaviAPd8LyP2Pvsj+gtaBd2ZS5pY7tdCEXOtX0Wdxt9hFVxVK6h83Gc0g/mSFLZzQJjv81l3V1H9U=@vger.kernel.org X-Gm-Message-State: AOJu0Yz+P3BSC31Blh/wjB4zlR2B6vUK5oHbMAidCbzo+TxOJFEO+5lS BsYuYv+fiW1Cw85vX6pKcbUmVv7KN4II8hbGVsTuNz9t6KHe1/yXnMRXMsqHF8mXvJgUBIK5x1P +em6iviF5GoWzj1XPM/eF8FKBtcBN+QiV98glm08qeqZS+XEj6g2uRUd6UVcDyuH0Cw== X-Gm-Gg: AfdE7ck238EuB2P719cMjbuMiWDcV8tJIL99Z0IgAJCU1BT6IPVEKk65VNjd5LK0YKn j1UZrLVSj5GBnTBUgQIVaTDn2sSKpLhHnyWQdJgD9ahqW/hv4FhPKkbSUYbL1hTqES7gO45OGls 4VgY03gPRN8qW1l2bWDe1SQqhPStXLCRQg+bJgMKRzKv0oDBsBr/YFZ7fpfxKiZ9skxPX4uSGQP dGjvWtZX1Al/E63CtHbZZZko4Kh72P6sMGDhwYqkK0uOGIGwggMoo5W/BC49QIkqflQrSKrUago ZJN1+v1ScF9PHyI4d6qvomHTf8UmxB7vrvr7rCYmXLykvbnD1VkcvAaUOHhVdf9rC0oRQsCTqFO oQQvobVhQFyEWnDgv/Fw3m2oWFypJW8QY/PAwUqcHPES97mPPMT25Y/rO6LAktvr8eXdzefn14T ecUBJ2 X-Received: by 2002:a05:600c:6792:b0:493:bd71:6084 with SMTP id 5b1f17b1804b1-493c2b96797mr22805675e9.31.1782908961664; Wed, 01 Jul 2026 05:29:21 -0700 (PDT) X-Received: by 2002:a05:600c:6792:b0:493:bd71:6084 with SMTP id 5b1f17b1804b1-493c2b96797mr22805175e9.31.1782908961210; Wed, 01 Jul 2026 05:29:21 -0700 (PDT) Received: from gmonaco-thinkpadt14gen3.rmtit.csb (212-8-243-115.hosted-by-worldstream.net. [212.8.243.115]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-493be810c02sm79547145e9.11.2026.07.01.05.29.20 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 01 Jul 2026 05:29:20 -0700 (PDT) Message-ID: <72909c5431d8a6564aaab10056b9c59d5750d956.camel@redhat.com> Subject: Re: [PATCH v2 2/4] rv/rtapp/sleep: Update nanosleep rule From: Gabriele Monaco To: Nam Cao Cc: Steven Rostedt , linux-trace-kernel@vger.kernel.org, linux-doc@vger.kernel.org, linux-kernel@vger.kernel.org Date: Wed, 01 Jul 2026 14:29:19 +0200 In-Reply-To: References: Autocrypt: addr=gmonaco@redhat.com; prefer-encrypt=mutual; keydata=mDMEZuK5YxYJKwYBBAHaRw8BAQdAmJ3dM9Sz6/Hodu33Qrf8QH2bNeNbOikqYtxWFLVm0 1a0JEdhYnJpZWxlIE1vbmFjbyA8Z21vbmFjb0BrZXJuZWwub3JnPoiZBBMWCgBBFiEEysoR+AuB3R Zwp6j270psSVh4TfIFAmjKX2MCGwMFCQWjmoAFCwkIBwICIgIGFQoJCAsCBBYCAwECHgcCF4AACgk Q70psSVh4TfIQuAD+JulczTN6l7oJjyroySU55Fbjdvo52xiYYlMjPG7dCTsBAMFI7dSL5zg98I+8 cXY1J7kyNsY6/dcipqBM4RMaxXsOtCRHYWJyaWVsZSBNb25hY28gPGdtb25hY29AcmVkaGF0LmNvb T6InAQTFgoARAIbAwUJBaOagAULCQgHAgIiAgYVCgkICwIEFgIDAQIeBwIXgBYhBMrKEfgLgd0WcK eo9u9KbElYeE3yBQJoymCyAhkBAAoJEO9KbElYeE3yjX4BAJ/ETNnlHn8OjZPT77xGmal9kbT1bC1 7DfrYVISWV2Y1AP9HdAMhWNAvtCtN2S1beYjNybuK6IzWYcFfeOV+OBWRDQ== Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable User-Agent: Evolution 3.60.2 (3.60.2-1.fc44) Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 On Fri, 2026-06-19 at 09:21 +0200, Nam Cao wrote: > CLOCK_REALTIME is the only clock that often is misused in real-time > applications. The other clocks either are safe for real-time uses > (CLOCK_TAI, CLOCK_MONOTONIC, CLOCK_BOOTTIME) or are unlikely to be misuse= d > (CLOCK_AUX, CLOCK_PROCESS_CPUTIME_ID). >=20 > Update the monitor to only warn about CLOCK_REALTIME. >=20 > While at it, update the out-of-sync documentation. >=20 > Signed-off-by: Nam Cao Looks good, thanks. Reviewed-by: Gabriele Monaco > --- > =C2=A0Documentation/trace/rv/monitor_rtapp.rst=C2=A0 | 17 +++++--- > =C2=A0kernel/trace/rv/monitors/sleep/sleep.c=C2=A0=C2=A0=C2=A0 | 12 ++---= - > =C2=A0kernel/trace/rv/monitors/sleep/sleep.h=C2=A0=C2=A0=C2=A0 | 52 +++++= ++++++------------ > =C2=A0tools/verification/models/rtapp/sleep.ltl |=C2=A0 2 +- > =C2=A04 files changed, 39 insertions(+), 44 deletions(-) >=20 > diff --git a/Documentation/trace/rv/monitor_rtapp.rst > b/Documentation/trace/rv/monitor_rtapp.rst > index 01656bf7080a..570be67a8f3b 100644 > --- a/Documentation/trace/rv/monitor_rtapp.rst > +++ b/Documentation/trace/rv/monitor_rtapp.rst > @@ -51,12 +51,13 @@ The `sleep` monitor reports real-time threads sleepin= g in > a manner that may > =C2=A0cause undesirable latency. Real-time applications should only put a= real-time > =C2=A0thread to sleep for one of the following reasons: > =C2=A0 > -=C2=A0 - Cyclic work: real-time thread sleeps waiting for the next cycle= . For this > -=C2=A0=C2=A0=C2=A0 case, only the `clock_nanosleep` syscall should be us= ed with > `TIMER_ABSTIME` > -=C2=A0=C2=A0=C2=A0 (to avoid time drift) and `CLOCK_MONOTONIC` (to avoid= the clock being > -=C2=A0=C2=A0=C2=A0 changed). No other method is safe for real-time. For = example, threads > -=C2=A0=C2=A0=C2=A0 waiting for timerfd can be woken by softirq which pro= vides no real-time > -=C2=A0=C2=A0=C2=A0 guarantee. > +=C2=A0 - Cyclic work: real-time thread sleeps waiting for the next > +=C2=A0=C2=A0=C2=A0 cycle. For this case, only the `clock_nanosleep` sysc= all should be > +=C2=A0=C2=A0=C2=A0 used with `TIMER_ABSTIME` (to avoid time drift). Addi= tionally, > +=C2=A0=C2=A0=C2=A0 `CLOCK_REALTIME` should not be used (to avoid the clo= ck being > +=C2=A0=C2=A0=C2=A0 changed). No other method is safe for real-time. For = example, > +=C2=A0=C2=A0=C2=A0 threads waiting for timerfd can be woken by softirq w= hich provides > +=C2=A0=C2=A0=C2=A0 no real-time guarantee. > =C2=A0=C2=A0 - Real-time thread waiting for something to happen (e.g. ano= ther thread > =C2=A0=C2=A0=C2=A0=C2=A0 releasing shared resources, or a completion sign= al from another thread). > In > =C2=A0=C2=A0=C2=A0=C2=A0 this case, only futexes (FUTEX_LOCK_PI, FUTEX_LO= CK_PI2 or one of > @@ -99,14 +100,16 @@ The monitor's specification is:: > =C2=A0 > =C2=A0=C2=A0 RT_VALID_SLEEP_REASON =3D FUTEX_WAIT > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 or RT_FR= IENDLY_NANOSLEEP > +=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 or EPOLL_WAIT > =C2=A0 > =C2=A0=C2=A0 RT_FRIENDLY_NANOSLEEP =3D CLOCK_NANOSLEEP > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 and NANOSLEEP_= TIMER_ABSTIME > -=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 and NANOSLEEP_CLOCK_= MONOTONIC > +=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 and not NANOSLEEP_CL= OCK_REALTIME > =C2=A0 > =C2=A0=C2=A0 RT_FRIENDLY_WAKE =3D WOKEN_BY_EQUAL_OR_HIGHER_PRIO > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 or WOKEN_BY_HARDIRQ > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 or WOKEN_BY_NMI > +=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 or ABORT_SLEEP > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 or KTHREAD_SHOULD_STOP > =C2=A0 > =C2=A0=C2=A0 ALLOWLIST =3D BLOCK_ON_RT_MUTEX > diff --git a/kernel/trace/rv/monitors/sleep/sleep.c > b/kernel/trace/rv/monitors/sleep/sleep.c > index d6b677fab8f8..638be7d8747f 100644 > --- a/kernel/trace/rv/monitors/sleep/sleep.c > +++ b/kernel/trace/rv/monitors/sleep/sleep.c > @@ -44,8 +44,7 @@ static void ltl_atoms_init(struct task_struct *task, st= ruct > ltl_monitor *mon, bo > =C2=A0 > =C2=A0 if (task_creation) { > =C2=A0 ltl_atom_set(mon, LTL_KTHREAD_SHOULD_STOP, false); > - ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false); > - ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false); > + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, false); > =C2=A0 ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false); > =C2=A0 ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false); > =C2=A0 ltl_atom_set(mon, LTL_FUTEX_WAIT, false); > @@ -60,8 +59,7 @@ static void ltl_atoms_init(struct task_struct *task, st= ruct > ltl_monitor *mon, bo > =C2=A0 /* kernel tasks do not do syscall */ > =C2=A0 ltl_atom_set(mon, LTL_FUTEX_WAIT, false); > =C2=A0 ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false); > - ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false); > - ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false); > + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, false); > =C2=A0 ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false); > =C2=A0 ltl_atom_set(mon, LTL_CLOCK_NANOSLEEP, false); > =C2=A0 ltl_atom_set(mon, LTL_EPOLL_WAIT, false); > @@ -136,8 +134,7 @@ static void handle_sys_enter(void *data, struct pt_re= gs > *regs, long id) > =C2=A0 case __NR_clock_nanosleep_time64: > =C2=A0#endif > =C2=A0 syscall_get_arguments(current, regs, args); > - ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, args[0] =3D=3D > CLOCK_MONOTONIC); > - ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, args[0] =3D=3D > CLOCK_TAI); > + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, args[0] =3D=3D > CLOCK_REALTIME); > =C2=A0 ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, args[1] =3D=3D > TIMER_ABSTIME); > =C2=A0 ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, true); > =C2=A0 break; > @@ -178,8 +175,7 @@ static void handle_sys_exit(void *data, struct pt_reg= s > *regs, long ret) > =C2=A0 > =C2=A0 ltl_atom_set(mon, LTL_FUTEX_LOCK_PI, false); > =C2=A0 ltl_atom_set(mon, LTL_FUTEX_WAIT, false); > - ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_MONOTONIC, false); > - ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_TAI, false); > + ltl_atom_set(mon, LTL_NANOSLEEP_CLOCK_REALTIME, false); > =C2=A0 ltl_atom_set(mon, LTL_NANOSLEEP_TIMER_ABSTIME, false); > =C2=A0 ltl_atom_set(mon, LTL_EPOLL_WAIT, false); > =C2=A0 ltl_atom_update(current, LTL_CLOCK_NANOSLEEP, false); > diff --git a/kernel/trace/rv/monitors/sleep/sleep.h > b/kernel/trace/rv/monitors/sleep/sleep.h > index 403dc2852c52..2fe2ec7edae8 100644 > --- a/kernel/trace/rv/monitors/sleep/sleep.h > +++ b/kernel/trace/rv/monitors/sleep/sleep.h > @@ -20,8 +20,7 @@ enum ltl_atom { > =C2=A0 LTL_FUTEX_WAIT, > =C2=A0 LTL_KERNEL_THREAD, > =C2=A0 LTL_KTHREAD_SHOULD_STOP, > - LTL_NANOSLEEP_CLOCK_MONOTONIC, > - LTL_NANOSLEEP_CLOCK_TAI, > + LTL_NANOSLEEP_CLOCK_REALTIME, > =C2=A0 LTL_NANOSLEEP_TIMER_ABSTIME, > =C2=A0 LTL_RT, > =C2=A0 LTL_SCHEDULE_IN, > @@ -46,8 +45,7 @@ static const char *ltl_atom_str(enum ltl_atom atom) > =C2=A0 "fu_wa", > =C2=A0 "ker_th", > =C2=A0 "kth_sh_st", > - "na_cl_mo", > - "na_cl_ta", > + "na_cl_re", > =C2=A0 "na_ti_ab", > =C2=A0 "rt", > =C2=A0 "sch_in", > @@ -87,8 +85,7 @@ static void ltl_start(struct task_struct *task, struct > ltl_monitor *mon) > =C2=A0 bool schedule_in =3D test_bit(LTL_SCHEDULE_IN, mon->atoms); > =C2=A0 bool rt =3D test_bit(LTL_RT, mon->atoms); > =C2=A0 bool nanosleep_timer_abstime =3D test_bit(LTL_NANOSLEEP_TIMER_ABST= IME, > mon->atoms); > - bool nanosleep_clock_tai =3D test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon- > >atoms); > - bool nanosleep_clock_monotonic =3D > test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms); > + bool nanosleep_clock_realtime =3D > test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms); > =C2=A0 bool kthread_should_stop =3D test_bit(LTL_KTHREAD_SHOULD_STOP, mon= - > >atoms); > =C2=A0 bool kernel_thread =3D test_bit(LTL_KERNEL_THREAD, mon->atoms); > =C2=A0 bool futex_wait =3D test_bit(LTL_FUTEX_WAIT, mon->atoms); > @@ -97,17 +94,17 @@ static void ltl_start(struct task_struct *task, struc= t > ltl_monitor *mon) > =C2=A0 bool clock_nanosleep =3D test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms)= ; > =C2=A0 bool block_on_rt_mutex =3D test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->at= oms); > =C2=A0 bool abort_sleep =3D test_bit(LTL_ABORT_SLEEP, mon->atoms); > - bool val42 =3D task_is_rcu || task_is_migration; > - bool val43 =3D futex_lock_pi || val42; > - bool val5 =3D block_on_rt_mutex || val43; > - bool val34 =3D abort_sleep || kthread_should_stop; > - bool val35 =3D woken_by_nmi || val34; > - bool val36 =3D woken_by_hardirq || val35; > - bool val14 =3D woken_by_equal_or_higher_prio || val36; > + bool val41 =3D task_is_rcu || task_is_migration; > + bool val42 =3D futex_lock_pi || val41; > + bool val5 =3D block_on_rt_mutex || val42; > + bool val33 =3D abort_sleep || kthread_should_stop; > + bool val34 =3D woken_by_nmi || val33; > + bool val35 =3D woken_by_hardirq || val34; > + bool val14 =3D woken_by_equal_or_higher_prio || val35; > =C2=A0 bool val13 =3D !schedule_in; > - bool val26 =3D nanosleep_clock_monotonic || nanosleep_clock_tai; > - bool val27 =3D nanosleep_timer_abstime && val26; > - bool val18 =3D clock_nanosleep && val27; > + bool val25 =3D !nanosleep_clock_realtime; > + bool val26 =3D nanosleep_timer_abstime && val25; > + bool val18 =3D clock_nanosleep && val26; > =C2=A0 bool val20 =3D val18 || epoll_wait; > =C2=A0 bool val9 =3D futex_wait || val20; > =C2=A0 bool val11 =3D val9 || kernel_thread; > @@ -138,8 +135,7 @@ ltl_possible_next_states(struct ltl_monitor *mon, uns= igned > int state, unsigned l > =C2=A0 bool schedule_in =3D test_bit(LTL_SCHEDULE_IN, mon->atoms); > =C2=A0 bool rt =3D test_bit(LTL_RT, mon->atoms); > =C2=A0 bool nanosleep_timer_abstime =3D test_bit(LTL_NANOSLEEP_TIMER_ABST= IME, > mon->atoms); > - bool nanosleep_clock_tai =3D test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon- > >atoms); > - bool nanosleep_clock_monotonic =3D > test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms); > + bool nanosleep_clock_realtime =3D > test_bit(LTL_NANOSLEEP_CLOCK_REALTIME, mon->atoms); > =C2=A0 bool kthread_should_stop =3D test_bit(LTL_KTHREAD_SHOULD_STOP, mon= - > >atoms); > =C2=A0 bool kernel_thread =3D test_bit(LTL_KERNEL_THREAD, mon->atoms); > =C2=A0 bool futex_wait =3D test_bit(LTL_FUTEX_WAIT, mon->atoms); > @@ -148,17 +144,17 @@ ltl_possible_next_states(struct ltl_monitor *mon, > unsigned int state, unsigned l > =C2=A0 bool clock_nanosleep =3D test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms)= ; > =C2=A0 bool block_on_rt_mutex =3D test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->at= oms); > =C2=A0 bool abort_sleep =3D test_bit(LTL_ABORT_SLEEP, mon->atoms); > - bool val42 =3D task_is_rcu || task_is_migration; > - bool val43 =3D futex_lock_pi || val42; > - bool val5 =3D block_on_rt_mutex || val43; > - bool val34 =3D abort_sleep || kthread_should_stop; > - bool val35 =3D woken_by_nmi || val34; > - bool val36 =3D woken_by_hardirq || val35; > - bool val14 =3D woken_by_equal_or_higher_prio || val36; > + bool val41 =3D task_is_rcu || task_is_migration; > + bool val42 =3D futex_lock_pi || val41; > + bool val5 =3D block_on_rt_mutex || val42; > + bool val33 =3D abort_sleep || kthread_should_stop; > + bool val34 =3D woken_by_nmi || val33; > + bool val35 =3D woken_by_hardirq || val34; > + bool val14 =3D woken_by_equal_or_higher_prio || val35; > =C2=A0 bool val13 =3D !schedule_in; > - bool val26 =3D nanosleep_clock_monotonic || nanosleep_clock_tai; > - bool val27 =3D nanosleep_timer_abstime && val26; > - bool val18 =3D clock_nanosleep && val27; > + bool val25 =3D !nanosleep_clock_realtime; > + bool val26 =3D nanosleep_timer_abstime && val25; > + bool val18 =3D clock_nanosleep && val26; > =C2=A0 bool val20 =3D val18 || epoll_wait; > =C2=A0 bool val9 =3D futex_wait || val20; > =C2=A0 bool val11 =3D val9 || kernel_thread; > diff --git a/tools/verification/models/rtapp/sleep.ltl > b/tools/verification/models/rtapp/sleep.ltl > index 464c84b9df87..5923e58d7810 100644 > --- a/tools/verification/models/rtapp/sleep.ltl > +++ b/tools/verification/models/rtapp/sleep.ltl > @@ -9,7 +9,7 @@ RT_VALID_SLEEP_REASON =3D FUTEX_WAIT > =C2=A0 > =C2=A0RT_FRIENDLY_NANOSLEEP =3D CLOCK_NANOSLEEP > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 and NANOSLEEP_TIMER_ABSTIM= E > -=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 and (NANOSLEEP_CLOCK_MONOTONIC o= r NANOSLEEP_CLOCK_TAI) > +=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 and not NANOSLEEP_CLOCK_REALTIME > =C2=A0 > =C2=A0RT_FRIENDLY_WAKE =3D WOKEN_BY_EQUAL_OR_HIGHER_PRIO > =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0 or WOKEN_BY_HARDIRQ