lkml.org 
[lkml]   [2014]   [Apr]   [7]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    From
    SubjectRe: Promela/spin model for NO_HZ_FULL_SYSIDLE code
    On Fri, Apr 04, 2014 at 01:43:16AM +0200, Frederic Weisbecker wrote:
    > On Sun, Mar 30, 2014 at 04:08:56PM -0700, Paul E. McKenney wrote:
    > > For whatever it is worth, the following model claims safety and progress
    > > for the sysidle state machine.
    > >
    > > Thoughts?
    >
    > I'm going to get fun of myself by risking a review of this. Warning,
    > I don't speak promelian, so I may well write non-sense :)

    Actually, you did find one real mismatch and one arguable one. ;-)

    > > Thanx, Paul
    > >
    > > ------------------------------------------------------------------------
    > > sysidle.sh
    > > ------------------------------------------------------------------------
    > > spin -a sysidle.spin
    > > cc -DNP -o pan pan.c
    > > # Fair scheduling to focus progress checks in timekeeper.
    > > ./pan -f -l -m1280000 -w22
    > >
    > > ------------------------------------------------------------------------
    > > 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. Checks for both safety and
    > > * forward progress.
    > > *
    > > * 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
    > > *
    > > * Author: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
    > > */
    > >
    > > #define NUM_WORKERS 3
    > >
    > > 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. */
    > >
    > > /*
    > > * 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;
    >
    > On the upstream code, the first read of full_sysidle_state after exiting idle is not
    > performed by an atomic operation. So I wonder if this is right to put this
    > in the atomic section.
    >
    > I don't know the language enough to tell if it has no effect but I'm just
    > worried that it gets badly intepreted. Like the above read plus the below
    > conditional write in the same atomic section gets packed in a kind of cmpxchg_if_above() ?
    >
    > Which is what we want to avoid if the value is not above RCU_SYSIDLE_SHORT after
    > a non atomic read.

    Given that cmpxchg() is being used to emulate exactly that atomic
    operation, I feel good about this Promela translation. If the value is
    different at the time of the cmpxchg(), the cmpxchg() fails. I suppose
    I could write it as follows instead:

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

    Here the "if" emulates the cmpxchg() instruction and the rest emulates
    the loop. Both representations get the same result when

    > > 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 ->
    > > wakeup_timekeeper = 1;
    > > :: 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;
    > >
    > > /* Check for acceptance state. */
    > > if
    > > :: idle == 0 ->
    > > progress_idle:
    >
    > Is this some kind of label? I can't find the target anywhere.

    It is a marker. If you specify -DNP and if there is any cycle of
    states that does not pass through a label beginning with "progress",
    the verification will fail. So it is useful for finding livelocks.

    Mathieu posted another way of getting this same effect.

    > > skip;
    > > :: curstate == RCU_SYSIDLE_NOT ->
    > > progress_idle_reset:
    > > skip;
    > > :: else -> skip;
    > > fi;
    > >
    > > /* 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;
    > > }
    >
    > It looks good but just one thing about the transition from FULL -> FULL_NOTED.
    > At least in the case of CONFIG_NO_HZ_FULL_SYSIDLE_SMALL (which is usually the
    > scenario I refer to, but I'll check further the grace-period driven way as well),
    > we switch from FULL to FULL_NOTED without checking a new round of the dynticks counters.
    >
    > But this timekeeper() proc doesn't seem to care and does a check_idle() no matter
    > the current state.
    >
    > There should probably be a special case to handle that otherwise we add a new
    > round of dynticks counters read between FULL and FULL_NOTED transition and this is an
    > entirely different scenario than what we run.

    Good catch! I changed the above RCU_SYSIDLE_FULL_NOTED to RCU_SYSIDLE_FULL
    and added an atomic block to move to RCU_SYSIDLE_FULL_NOTED. Still verifies
    (whew!).

    > > :: idle == 0 && full_sysidle_state >= RCU_SYSIDLE_LONG ->
    > > /* Non-idle and state advanced, revert to base state. */
    > > full_sysidle_state = RCU_SYSIDLE_NOT;
    >
    > Looking at the upstream code, I think we reset also when state == RCU_SYSIDLE_SHORT
    > once we detect a non-idle state. If it's not a mistyping, I'm probably missing something.

    I don't see this. The resetting happens in rcu_sysidle_force_exit(),
    which contains the following:

    while (oldstate > RCU_SYSIDLE_SHORT) {
    newoldstate = cmpxchg(&full_sysidle_state,
    oldstate, RCU_SYSIDLE_NOT);
    if (oldstate == newoldstate &&
    oldstate == RCU_SYSIDLE_FULL_NOTED) {
    rcu_kick_nohz_cpu(tick_do_timer_cpu);
    return; /* We cleared it, done! */
    }
    oldstate = newoldstate;
    }

    If the state is RCU_SYSIDLE_SHORT, we skip the body of the "if" thus
    declining to reset back to RCU_SYSIDLE_NOT. Or am I confused?

    Thanx, Paul

    > Thanks.
    >
    > > :: else -> skip;
    > > fi;
    > >
    > > /* If in RCU_SYSIDLE_FULL_NOTED, wait to be awakened. */
    > > do
    > > :: newstate != RCU_SYSIDLE_FULL_NOTED &&
    > > wakeup_timekeeper == 1 ->
    > > assert(0); /* Should never get here. */
    > > :: newstate != RCU_SYSIDLE_FULL_NOTED &&
    > > wakeup_timekeeper == 0 ->
    > > break;
    > > :: newstate == RCU_SYSIDLE_FULL_NOTED &&
    > > wakeup_timekeeper == 1 ->
    > > progress_full_system_idle_1:
    > > assert(full_sysidle_state == RCU_SYSIDLE_NOT);
    > > wakeup_timekeeper = 0;
    > > break;
    > > :: newstate == RCU_SYSIDLE_FULL_NOTED &&
    > > wakeup_timekeeper == 0 ->
    > > progress_full_system_idle_2:
    > >
    > > /* We are asleep, so all workers better be idle. */
    > > atomic {
    > > i = 0;
    > > idle = 1;
    > > do
    > > :: i < NUM_WORKERS ->
    > > if
    > > :: am_setup[i] -> idle = 0;
    > > :: else -> skip;
    > > fi;
    > > i++;
    > > :: i >= NUM_WORKERS -> break;
    > > od;
    > > assert(idle == 1 ||
    > > full_sysidle_state < RCU_SYSIDLE_FULL);
    > > }
    > > od;
    > > 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();
    > > }
    > >
    >



    \
     
     \ /
      Last update: 2014-04-07 20:41    [W:4.483 / U:0.016 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site