@@ -15,6 +15,7 @@ enum ltl_atom {
1515 LTL_ABORT_SLEEP ,
1616 LTL_BLOCK_ON_RT_MUTEX ,
1717 LTL_CLOCK_NANOSLEEP ,
18+ LTL_EPOLL_WAIT ,
1819 LTL_FUTEX_LOCK_PI ,
1920 LTL_FUTEX_WAIT ,
2021 LTL_KERNEL_THREAD ,
@@ -40,6 +41,7 @@ static const char *ltl_atom_str(enum ltl_atom atom)
4041 "ab_sl" ,
4142 "bl_on_rt_mu" ,
4243 "cl_na" ,
44+ "ep_wa" ,
4345 "fu_lo_pi" ,
4446 "fu_wa" ,
4547 "ker_th" ,
@@ -75,39 +77,41 @@ static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);
7577
7678static void ltl_start (struct task_struct * task , struct ltl_monitor * mon )
7779{
78- bool task_is_migration = test_bit (LTL_TASK_IS_MIGRATION , mon -> atoms );
79- bool task_is_rcu = test_bit (LTL_TASK_IS_RCU , mon -> atoms );
80- bool val40 = task_is_rcu || task_is_migration ;
81- bool futex_lock_pi = test_bit (LTL_FUTEX_LOCK_PI , mon -> atoms );
82- bool val41 = futex_lock_pi || val40 ;
83- bool block_on_rt_mutex = test_bit (LTL_BLOCK_ON_RT_MUTEX , mon -> atoms );
84- bool val5 = block_on_rt_mutex || val41 ;
85- bool kthread_should_stop = test_bit (LTL_KTHREAD_SHOULD_STOP , mon -> atoms );
86- bool abort_sleep = test_bit (LTL_ABORT_SLEEP , mon -> atoms );
87- bool val32 = abort_sleep || kthread_should_stop ;
8880 bool woken_by_nmi = test_bit (LTL_WOKEN_BY_NMI , mon -> atoms );
89- bool val33 = woken_by_nmi || val32 ;
9081 bool woken_by_hardirq = test_bit (LTL_WOKEN_BY_HARDIRQ , mon -> atoms );
91- bool val34 = woken_by_hardirq || val33 ;
9282 bool woken_by_equal_or_higher_prio = test_bit (LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO ,
9383 mon -> atoms );
94- bool val14 = woken_by_equal_or_higher_prio || val34 ;
9584 bool wake = test_bit (LTL_WAKE , mon -> atoms );
96- bool val13 = !wake ;
97- bool kernel_thread = test_bit (LTL_KERNEL_THREAD , mon -> atoms );
85+ bool task_is_rcu = test_bit (LTL_TASK_IS_RCU , mon -> atoms );
86+ bool task_is_migration = test_bit (LTL_TASK_IS_MIGRATION , mon -> atoms );
87+ bool sleep = test_bit (LTL_SLEEP , mon -> atoms );
88+ bool rt = test_bit (LTL_RT , mon -> atoms );
89+ bool nanosleep_timer_abstime = test_bit (LTL_NANOSLEEP_TIMER_ABSTIME , mon -> atoms );
9890 bool nanosleep_clock_tai = test_bit (LTL_NANOSLEEP_CLOCK_TAI , mon -> atoms );
9991 bool nanosleep_clock_monotonic = test_bit (LTL_NANOSLEEP_CLOCK_MONOTONIC , mon -> atoms );
100- bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai ;
101- bool nanosleep_timer_abstime = test_bit (LTL_NANOSLEEP_TIMER_ABSTIME , mon -> atoms );
102- bool val25 = nanosleep_timer_abstime && val24 ;
103- bool clock_nanosleep = test_bit (LTL_CLOCK_NANOSLEEP , mon -> atoms );
104- bool val18 = clock_nanosleep && val25 ;
92+ bool kthread_should_stop = test_bit (LTL_KTHREAD_SHOULD_STOP , mon -> atoms );
93+ bool kernel_thread = test_bit (LTL_KERNEL_THREAD , mon -> atoms );
10594 bool futex_wait = test_bit (LTL_FUTEX_WAIT , mon -> atoms );
106- bool val9 = futex_wait || val18 ;
95+ bool futex_lock_pi = test_bit (LTL_FUTEX_LOCK_PI , mon -> atoms );
96+ bool epoll_wait = test_bit (LTL_EPOLL_WAIT , mon -> atoms );
97+ bool clock_nanosleep = test_bit (LTL_CLOCK_NANOSLEEP , mon -> atoms );
98+ bool block_on_rt_mutex = test_bit (LTL_BLOCK_ON_RT_MUTEX , mon -> atoms );
99+ bool abort_sleep = test_bit (LTL_ABORT_SLEEP , mon -> atoms );
100+ bool val42 = task_is_rcu || task_is_migration ;
101+ bool val43 = futex_lock_pi || val42 ;
102+ bool val5 = block_on_rt_mutex || val43 ;
103+ bool val34 = abort_sleep || kthread_should_stop ;
104+ bool val35 = woken_by_nmi || val34 ;
105+ bool val36 = woken_by_hardirq || val35 ;
106+ bool val14 = woken_by_equal_or_higher_prio || val36 ;
107+ bool val13 = !wake ;
108+ bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai ;
109+ bool val27 = nanosleep_timer_abstime && val26 ;
110+ bool val18 = clock_nanosleep && val27 ;
111+ bool val20 = val18 || epoll_wait ;
112+ bool val9 = futex_wait || val20 ;
107113 bool val11 = val9 || kernel_thread ;
108- bool sleep = test_bit (LTL_SLEEP , mon -> atoms );
109114 bool val2 = !sleep ;
110- bool rt = test_bit (LTL_RT , mon -> atoms );
111115 bool val1 = !rt ;
112116 bool val3 = val1 || val2 ;
113117
@@ -124,39 +128,41 @@ static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)
124128static void
125129ltl_possible_next_states (struct ltl_monitor * mon , unsigned int state , unsigned long * next )
126130{
127- bool task_is_migration = test_bit (LTL_TASK_IS_MIGRATION , mon -> atoms );
128- bool task_is_rcu = test_bit (LTL_TASK_IS_RCU , mon -> atoms );
129- bool val40 = task_is_rcu || task_is_migration ;
130- bool futex_lock_pi = test_bit (LTL_FUTEX_LOCK_PI , mon -> atoms );
131- bool val41 = futex_lock_pi || val40 ;
132- bool block_on_rt_mutex = test_bit (LTL_BLOCK_ON_RT_MUTEX , mon -> atoms );
133- bool val5 = block_on_rt_mutex || val41 ;
134- bool kthread_should_stop = test_bit (LTL_KTHREAD_SHOULD_STOP , mon -> atoms );
135- bool abort_sleep = test_bit (LTL_ABORT_SLEEP , mon -> atoms );
136- bool val32 = abort_sleep || kthread_should_stop ;
137131 bool woken_by_nmi = test_bit (LTL_WOKEN_BY_NMI , mon -> atoms );
138- bool val33 = woken_by_nmi || val32 ;
139132 bool woken_by_hardirq = test_bit (LTL_WOKEN_BY_HARDIRQ , mon -> atoms );
140- bool val34 = woken_by_hardirq || val33 ;
141133 bool woken_by_equal_or_higher_prio = test_bit (LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO ,
142134 mon -> atoms );
143- bool val14 = woken_by_equal_or_higher_prio || val34 ;
144135 bool wake = test_bit (LTL_WAKE , mon -> atoms );
145- bool val13 = !wake ;
146- bool kernel_thread = test_bit (LTL_KERNEL_THREAD , mon -> atoms );
136+ bool task_is_rcu = test_bit (LTL_TASK_IS_RCU , mon -> atoms );
137+ bool task_is_migration = test_bit (LTL_TASK_IS_MIGRATION , mon -> atoms );
138+ bool sleep = test_bit (LTL_SLEEP , mon -> atoms );
139+ bool rt = test_bit (LTL_RT , mon -> atoms );
140+ bool nanosleep_timer_abstime = test_bit (LTL_NANOSLEEP_TIMER_ABSTIME , mon -> atoms );
147141 bool nanosleep_clock_tai = test_bit (LTL_NANOSLEEP_CLOCK_TAI , mon -> atoms );
148142 bool nanosleep_clock_monotonic = test_bit (LTL_NANOSLEEP_CLOCK_MONOTONIC , mon -> atoms );
149- bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai ;
150- bool nanosleep_timer_abstime = test_bit (LTL_NANOSLEEP_TIMER_ABSTIME , mon -> atoms );
151- bool val25 = nanosleep_timer_abstime && val24 ;
152- bool clock_nanosleep = test_bit (LTL_CLOCK_NANOSLEEP , mon -> atoms );
153- bool val18 = clock_nanosleep && val25 ;
143+ bool kthread_should_stop = test_bit (LTL_KTHREAD_SHOULD_STOP , mon -> atoms );
144+ bool kernel_thread = test_bit (LTL_KERNEL_THREAD , mon -> atoms );
154145 bool futex_wait = test_bit (LTL_FUTEX_WAIT , mon -> atoms );
155- bool val9 = futex_wait || val18 ;
146+ bool futex_lock_pi = test_bit (LTL_FUTEX_LOCK_PI , mon -> atoms );
147+ bool epoll_wait = test_bit (LTL_EPOLL_WAIT , mon -> atoms );
148+ bool clock_nanosleep = test_bit (LTL_CLOCK_NANOSLEEP , mon -> atoms );
149+ bool block_on_rt_mutex = test_bit (LTL_BLOCK_ON_RT_MUTEX , mon -> atoms );
150+ bool abort_sleep = test_bit (LTL_ABORT_SLEEP , mon -> atoms );
151+ bool val42 = task_is_rcu || task_is_migration ;
152+ bool val43 = futex_lock_pi || val42 ;
153+ bool val5 = block_on_rt_mutex || val43 ;
154+ bool val34 = abort_sleep || kthread_should_stop ;
155+ bool val35 = woken_by_nmi || val34 ;
156+ bool val36 = woken_by_hardirq || val35 ;
157+ bool val14 = woken_by_equal_or_higher_prio || val36 ;
158+ bool val13 = !wake ;
159+ bool val26 = nanosleep_clock_monotonic || nanosleep_clock_tai ;
160+ bool val27 = nanosleep_timer_abstime && val26 ;
161+ bool val18 = clock_nanosleep && val27 ;
162+ bool val20 = val18 || epoll_wait ;
163+ bool val9 = futex_wait || val20 ;
156164 bool val11 = val9 || kernel_thread ;
157- bool sleep = test_bit (LTL_SLEEP , mon -> atoms );
158165 bool val2 = !sleep ;
159- bool rt = test_bit (LTL_RT , mon -> atoms );
160166 bool val1 = !rt ;
161167 bool val3 = val1 || val2 ;
162168
0 commit comments