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.133.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 8E3FA335566 for ; Tue, 19 May 2026 12:58:11 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=170.10.133.124 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1779195493; cv=none; b=HH4iD22qLSykPepxRaxCoJo51UtBqzOYCZ1a/Xp/5G9NQlKWgTNYIE7tJV8U7tfsvau3geSE0eCof67ub/Qh+ioj1IaKa0UKBImgcMaumZ69mercwdgnGgdyHoEycEnks70EyBK8s/Qbj/lEBKLxOP+KEIm8S/OnHbAZQsul3LY= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1779195493; c=relaxed/simple; bh=vPS1pmqAXUourfCsEOKPpk/vJUWdlbHEpYbyio9DkOc=; h=Message-ID:Subject:From:To:Cc:Date:In-Reply-To:References: Content-Type:MIME-Version; b=uWhy76LX2ynXZupHaiRo6lSp5hWXioT48cUT39CMGKWbB6Ec4gW3eorGlRX20bfSokquHfbAyj+UGaeI/kOLupZn67xjNnX2T/i7xro0pU4WLYITb/U4MtKbAZPGhuE+TBlvl7iLmh+kg/8YpU5nYg0JzoLc7o7rr6hzPYINLKA= 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=Dk7vQCXY; dkim=pass (2048-bit key) header.d=redhat.com header.i=@redhat.com header.b=qsDUvX43; arc=none smtp.client-ip=170.10.133.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="Dk7vQCXY"; dkim=pass (2048-bit key) header.d=redhat.com header.i=@redhat.com header.b="qsDUvX43" DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1779195490; 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=RU31FpX0lvZwHpAUR7pLSx9bMohAu0sEBHOkXaeR8yw=; b=Dk7vQCXY1OrXwlG7/+/a1gMj0qT+vPOiv45YvNSIHrt7PFqsgJVIv6G4/JcdRIfT7FVFkk ckv4O5cMiW1tRXk7Cw/a6j4OrBbVVu+O+6FMuYZIUTYhN/+IgeWnQP8t4a5LpwRTL/URPN EZ9mdWv+xOsxWAvgN7YuQzcsWoDiOMM= Received: from mail-ed1-f70.google.com (mail-ed1-f70.google.com [209.85.208.70]) by relay.mimecast.com with ESMTP with STARTTLS (version=TLSv1.3, cipher=TLS_AES_256_GCM_SHA384) id us-mta-594-zhyB4t7XNk-jraf4QwnarQ-1; Tue, 19 May 2026 08:58:09 -0400 X-MC-Unique: zhyB4t7XNk-jraf4QwnarQ-1 X-Mimecast-MFC-AGG-ID: zhyB4t7XNk-jraf4QwnarQ_1779195488 Received: by mail-ed1-f70.google.com with SMTP id 4fb4d7f45d1cf-67c414217ccso4106613a12.3 for ; Tue, 19 May 2026 05:58:09 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=google; t=1779195488; x=1779800288; 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=RU31FpX0lvZwHpAUR7pLSx9bMohAu0sEBHOkXaeR8yw=; b=qsDUvX43fby6RHpnmmkLBhiBaeraZNJMbuYRE3dtscACFm1WY5a6ccvQymbfibtm40 X8tA3137kBM800pJIU5Hnomr+Ae47fwTKbioS71PtMQ4hgKGUZD8zPSoyjZirgnf+K81 orWau+478eiWlEg3NWSD7N2WF9Qb03Z/Q8kZm2KhEbt2rladoAP6idB/SgtbACIrzXhs eDV/0Z8ZeadX/kVoga0+h2qcS206t6Z/3zSJV0Cs7PNA+r+Fp6p5nN4GC/2OAN9nQtiL bGPbHSTAfjXB1UokrHzmeLKJRya/yv8E8TiDiVxEMZ8mhib/DCevojWI6eEKv1TOCeuk meXw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1779195488; x=1779800288; 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=RU31FpX0lvZwHpAUR7pLSx9bMohAu0sEBHOkXaeR8yw=; b=MUtZ5V9Xtwrup6sjW9UKo5RvnupQeQTqq9FIzzEl2vVIWnGIVy4SigRUB6dOOmmvp3 H2RCgE0jzVX2BovMJIYU8QmkjCex+GmeW6DdDEnX+atCz3Q3lbRF0MxnL46U33Pgtquh qxTBg38nkTcY5S2zrb4qNGtuRxfMUR3v72phQ9kxBkYsdcNiradWeTXzoPLgwWQUPq73 cdfbKSFaUb0G8h6AZESyLzf4kUQebHApF9FR9mTNi3+GunNty0/3mV82Zk7PJ8lFbrmd w3rKyabkml6x90cm/9/eia0w+q/vD0N0gZ7kEyXQM1G3BhSXOEoR+WsDd8lnyFc34Alc f07w== X-Forwarded-Encrypted: i=1; AFNElJ8Ks3TZa+Zqds/vZqU0CyGM7L3tRPX46qhe2iNNswdnU9A4M+3d9J5XSfK+PZHC0f1vc0tNTtM1cwsyWhI=@vger.kernel.org X-Gm-Message-State: AOJu0Yzq0Z8Rm4Ch+6mm8eY15dqPCicL8Rgvuxbe7tzppDgzUggXUjxw 7n1KTGn5wfVdnsb9JI2kAbV+u6wVsljQbT8c3gmFVA6KB96+QhaMUsUo9K0K4SDocHP2AF5UZiD byJLZe0ybRHce/GT1O3QyrX25rII4q0s7VpRcSp6fdDlAE6dn92dCrDnTp/umopWyfQ== X-Gm-Gg: Acq92OHYaraCNDQwAD9WoZwivDDDswa64f7VfYlLUTfNzSWHqWMu6HRWr5QCGSeY+MR v33s1R1W5iBUKmLf8sIb10p/x9EgpMOzWlE6GTJNVTg75dO2W9cCkAdrV/PJk/fHtK3KRk8eYtT F5W8cbBGKuSWrCMgnJiTG2eTfTAeHqF8W1NuAsYqgwkAOtyB65DtC9mu0RSeWdkPoJYUTSlo2pT +zxm9WTrKmD8TnU6uAz7KHY/d53tN8yE4+s5xQKlWWyzbtPLnDJDMZg84XS3gxmb+YD1yLILHOV adtcyxKohMUZHUBsKkuXCi+NXOePsvn7xzXSP941tTroLnmw+ZCCHmXoNpJHH7WedfAGad7ZVsR UNnYA7YiMPMeM7uJqbKeLQm7AvFtpb5HiP0BRaQcTFq3vXHLD9SJxFxJfRKru81wxc/af4QMM5H pwmDjDDK5ElBMpu0g= X-Received: by 2002:aa7:c4e7:0:b0:670:8b38:5717 with SMTP id 4fb4d7f45d1cf-683bd581a49mr7272450a12.24.1779195487954; Tue, 19 May 2026 05:58:07 -0700 (PDT) X-Received: by 2002:aa7:c4e7:0:b0:670:8b38:5717 with SMTP id 4fb4d7f45d1cf-683bd581a49mr7272428a12.24.1779195487409; Tue, 19 May 2026 05:58:07 -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 4fb4d7f45d1cf-6831197bf00sm6537667a12.31.2026.05.19.05.58.06 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 19 May 2026 05:58:07 -0700 (PDT) Message-ID: <5af6afbfa32ede2db7f21412c8c21831f0eefd04.camel@redhat.com> Subject: Re: [PATCH 2/3] rv/rtapp/sleep: Update nanosleep rule From: Gabriele Monaco To: Nam Cao Cc: Steven Rostedt , linux-kernel@vger.kernel.org, linux-trace-kernel@vger.kernel.org Date: Tue, 19 May 2026 14:58:05 +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.1 (3.60.1-1.fc44) Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 On Tue, 2026-05-19 at 09:49 +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 > The rtapp monitor's purpose is warning people about common mistakes with > real-time design. However, warning about all clock types generates too mu= ch > false positives. I'm fine with the change, but are those really false positives? >From what I understand before this change we would report any non-rt-friend= ly clock type, now only realtime. What we are skipping would still be true positives, just so uncommon not to justify the extra complexity, right? Or do you mean an RT task using CLOCK_AUX is a false positive because likel= y the users weren't even trying to do real-time? Thanks, Gabriele >=20 > Update the monitor to only warn about CLOCK_REALTIME. >=20 > Signed-off-by: Nam Cao > --- > =C2=A0kernel/trace/rv/monitors/sleep/sleep.c=C2=A0=C2=A0=C2=A0 | 10 ++--- > =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=A03 files changed, 28 insertions(+), 36 deletions(-) >=20 > diff --git a/kernel/trace/rv/monitors/sleep/sleep.c > b/kernel/trace/rv/monitors/sleep/sleep.c > index 0a36f5519e6b..e01ac56b3f4a 100644 > --- a/kernel/trace/rv/monitors/sleep/sleep.c > +++ b/kernel/trace/rv/monitors/sleep/sleep.c > @@ -43,9 +43,7 @@ static void ltl_atoms_init(struct task_struct *task, st= ruct > ltl_monitor *mon, bo > =C2=A0 ltl_atom_set(mon, LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO, false); > =C2=A0 > =C2=A0 if (task_creation) { > - 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); > @@ -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 95dc2727c059..ed1ac7ad008e 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_SLEEP, > @@ -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 "sl", > @@ -87,8 +85,7 @@ static void ltl_start(struct task_struct *task, struct > ltl_monitor *mon) > =C2=A0 bool sleep =3D test_bit(LTL_SLEEP, 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 !wake; > - 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 sleep =3D test_bit(LTL_SLEEP, 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 !wake; > - 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 6f26c4810f78..2637bc48a620 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