Re: Promela/spin model for NO_HZ_FULL_SYSIDLE code

[Mathieu Desnoyers]

----- Original Message -----
> From: "Paul E. McKenney" <paulmck@xxxxxxxxxxxxxxxxxx>
> To: "Mathieu Desnoyers" <mathieu.desnoyers@xxxxxxxxxxxx>
> Cc: fweisbec@xxxxxxxxx, peterz@xxxxxxxxxxxxx, linux-kernel@xxxxxxxxxxxxxxx
> Sent: Tuesday, April 1, 2014 10:50:44 PM
> Subject: Re: Promela/spin model for NO_HZ_FULL_SYSIDLE code
> 
[...]
> > Here is the experiment I did on this latest version: I just enabled the
> > safety checking (not progress). I commented these lines out (again):
> > 
> >                 /* If needed, wake up the timekeeper. */
> >                 if
> >                 //:: oldstate == RCU_SYSIDLE_FULL_NOTED ->
> >                 //      wakeup_timekeeper = 1;
> >                 :: else -> skip;
> >                 fi;
> > 
> > compile and run with:
> > 
> > spin -a sysidle.spin
> > gcc -o pan pan.c
> > ./pan -m1280000 -w22
> > 
> > My expectation would be to trigger some kind of assertion that the
> > timekeeper is not active while the worker is running. Unfortunately,
> > nothing triggers.
> 
> That is expected behavior.  Failure to wake up the timekeeper is set
> up as a progress criterion.
> 
> > I see 3 possible solutions: we could either add assertions into
> > other branches of the timekeeper, or add assertions into the worker
> > thread. Another way to do it would be to express the assertions as
> > negation of a LTL formula based on state variables.
> 
> I did try both a hand-coded "never" clause and LTL formulas without
> success. You have more experience with them, so perhaps you could make
> something work.  The need is that if all worker threads go non-idle
> indefinitely starting from the RCU_SYSIDLE_FULL_NOTED state, the
> wakeup_timekeeper must eventually be set to 1, and then the timekeeper
> must start running, for example, the wakeup_timekeeper value must revert
> to zero.
> 
> The problem I had is that the "never" claims seem set up to catch some
> finite behavior after a possibly-infinite prefix.  In this case, we
> instead need to catch some infinite behavior after a possibly-infinite
> prefix.
> 
> > Thoughts ?
> 
> Me, I eventually switched over to using progress detection.  Which might
> be a bit unconventional, but it did have the virtue of making the
> model complain when it should complain.  ;-)

Here is my attempt at simplifying the model. I use LTL formulas as checks
for the two things I think really matter here: having timekeeping eventually
active when threads are running, and having timekeeping eventually inactive
when threads are idle. Hopefully my Promela is not too rusty:

1) When, at any point in the trail, a worker is setup, then we want to
   be sure that at some point in the future the timer is necessarily
   running:

timer_active.ltl:
[] (am_setup_0 -> (<> timekeeper_is_running))

2) When, at any point in the trail, a worker is not setup, then we
   want to be sure that at some point in the future, either this
   thread is setup again, or the timekeeper reaches a not running
   state:

timer_inactive.ltl:
[] (!am_setup_0 -> (<> (!timekeeper_is_running || am_setup_0)))

sysidle.sh:
#!/bin/sh

spin -f "!(`cat timer_active.ltl`)" > pan.ltl
#spin -f "!(`cat timer_inactive.ltl`)" > pan.ltl
spin -a -X -N  pan.ltl sysidle.spin
#spin -DINJECT_MISSING_WAKEUP -a -X -N  pan.ltl sysidle.spin
gcc -o pan pan.c
./pan -f -a -m1280000 -w22

#view trail with:
# spin -v -t -N pan.ltl sysidle.spin

sysidle.spin:

/*
 * Promela model for CONFIG_NO_HZ_FULL_SYSIDLE=y in the Linux kernel.
 * This model assumes that the dyntick-idle bit manipulation works based
 * on long usage, and substitutes a per-thread boolean "am_busy[]" array
 * for the Linux kernel's dyntick-idle masks.  The focus of this model
 * is therefore on the state machine itself.  Models timekeeper "running"
 * state with respect to worker thread idle state.
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, you can access it online at
 * http://www.gnu.org/licenses/gpl-2.0.html.
 *
 * Copyright IBM Corporation, 2014
 * Copyright EfficiOS, 2014
 *
 * Author: Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx>
 *         Mathieu Desnoyers <mathieu.desnoyers@xxxxxxxxxxxx>
 */

// adapt LTL formulas before changing NUM_WORKERS
//#define NUM_WORKERS 2
#define NUM_WORKERS 1
/* Defines used because LTL formula interprets [] */
#define am_setup_0      am_setup[0]
#define am_setup_1      am_setup[1]

byte wakeup_timekeeper = 0; /* Models rcu_kick_nohz_cpu(). */

#define RCU_SYSIDLE_NOT         0       /* Some CPU is not idle. */
#define RCU_SYSIDLE_SHORT       1       /* All CPUs idle for brief period. */
#define RCU_SYSIDLE_LONG        2       /* All CPUs idle for long enough. */
#define RCU_SYSIDLE_FULL        3       /* All CPUs idle, ready for sysidle. */
#define RCU_SYSIDLE_FULL_NOTED  4       /* Actually entered sysidle state. */

byte full_sysidle_state = RCU_SYSIDLE_NOT;

byte am_busy[NUM_WORKERS];  /* Busy is similar to "not dyntick-idle". */
byte am_setup[NUM_WORKERS]; /* Setup means timekeeper knows I am not idle. */

byte timekeeper_is_running = 1; /* Timekeeper initially running */

/*
 * Non-timekeeping CPU going into and out of dyntick-idle state.
 */
proctype worker(byte me)
{
        byte oldstate;

        do
        :: 1 ->
                /* Go idle. */
                am_setup[me] = 0;
                am_busy[me] = 0;

                /* Dyntick-idle in the following loop. */
                do
                :: 1 -> skip;
                :: 1 -> break;
                od;

                /* Exit idle loop, model getting out of dyntick idle state. */
                am_busy[me] = 1;

                /* Get state out of full-system idle states. */
                atomic {
                        oldstate = full_sysidle_state;
                        if
                        :: oldstate > RCU_SYSIDLE_SHORT ->
                                full_sysidle_state = RCU_SYSIDLE_NOT;
                        :: else -> skip;
                        fi;
                }

                /* If needed, wake up the timekeeper. */
                if
                :: oldstate == RCU_SYSIDLE_FULL_NOTED ->
#ifndef INJECT_MISSING_WAKEUP
                        wakeup_timekeeper = 1;
#else
                        skip;
#endif
                :: else -> skip;
                fi;

                /* Mark ourselves fully awake and operational. */
                am_setup[me] = 1;

                /* We are fully awake, so timekeeper must not be asleep. */
                assert(full_sysidle_state < RCU_SYSIDLE_FULL);

                /* Running in kernel in the following loop. */
                do
                :: 1 -> skip;
                :: 1 -> break;
                od;
        od
}

/*
 * Are all the workers in dyntick-idle state?
 */
#define check_idle() \
        i = 0; \
        idle = 1; \
        do \
        :: i < NUM_WORKERS -> \
                if \
                :: am_busy[i] == 1 -> idle = 0; \
                :: else -> skip; \
                fi; \
                i++; \
        :: i >= NUM_WORKERS -> break; \
        od

/*
 * Timekeeping CPU.
 */
proctype timekeeper()
{
        byte i;
        byte idle;
        byte curstate;
        byte newstate;

        do
        :: 1 ->
                /* Capture current state. */
                check_idle();
                curstate = full_sysidle_state;
                newstate = curstate;

                /* Manage state... */
                if
                :: idle == 1 && curstate < RCU_SYSIDLE_FULL_NOTED ->
                        /* Idle, advance to next state. */
                        atomic {
                                if
                                :: full_sysidle_state == curstate ->
                                        newstate = curstate + 1;
                                        full_sysidle_state = newstate;
                                :: else -> skip;
                                fi;
                        }
                :: idle == 0 && full_sysidle_state >= RCU_SYSIDLE_LONG ->
                        /* Non-idle and state advanced, revert to base state. */
                        full_sysidle_state = RCU_SYSIDLE_NOT;
                :: else -> skip;
                fi;

                /* If in RCU_SYSIDLE_FULL_NOTED, wait to be awakened. */
                if
                :: newstate != RCU_SYSIDLE_FULL_NOTED ->
                        skip;
                :: newstate == RCU_SYSIDLE_FULL_NOTED ->
                        timekeeper_is_running = 0;
                        do
                        :: wakeup_timekeeper == 0 ->
                                skip; /* Awaiting wake up */
                        :: else ->
                                timekeeper_is_running = 1;
                                wakeup_timekeeper = 0;
                                break; /* awakened */
                        od;
                fi;
                assert(full_sysidle_state <= RCU_SYSIDLE_FULL_NOTED);
        od;
}

init {
        byte i = 0;

        do
        :: i < NUM_WORKERS ->
                am_busy[i] = 1;
                am_setup[i] = 1;
                run worker(i);
                i++;
        :: i >= NUM_WORKERS -> break;
        od;
        run timekeeper();
}

-- 
Mathieu Desnoyers
EfficiOS Inc.
http://www.efficios.com
--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/