Re: Promela/spin model for NO_HZ_FULL_SYSIDLE code

[Paul E. McKenney]

On Mon, Mar 31, 2014 at 08:38:13AM -0700, Paul E. McKenney wrote:
> On Mon, Mar 31, 2014 at 02:02:23PM +0000, Mathieu Desnoyers wrote:
> > ----- Original Message -----
> > > From: "Paul E. McKenney" <paulmck@xxxxxxxxxxxxxxxxxx>
> > > To: "Mathieu Desnoyers" <mathieu.desnoyers@xxxxxxxxxxxx>
> > > Cc: fweisbec@xxxxxxxxx, peterz@xxxxxxxxxxxxx, linux-kernel@xxxxxxxxxxxxxxx
> > > Sent: Sunday, March 30, 2014 11:54:58 PM
> > > Subject: Re: Promela/spin model for NO_HZ_FULL_SYSIDLE code
> > > 
> > > On Mon, Mar 31, 2014 at 03:29:25AM +0000, Mathieu Desnoyers wrote:
> > > > ----- Original Message -----
> > > > > From: "Paul E. McKenney" <paulmck@xxxxxxxxxxxxxxxxxx>
> > > > > To: fweisbec@xxxxxxxxx, "mathieu desnoyers"
> > > > > <mathieu.desnoyers@xxxxxxxxxxxx>, peterz@xxxxxxxxxxxxx
> > > > > Cc: linux-kernel@xxxxxxxxxxxxxxx
> > > > > Sent: Sunday, March 30, 2014 7:08:56 PM
> > > > > Subject: Promela/spin model for NO_HZ_FULL_SYSIDLE code
> > > > > 
> > > > > For whatever it is worth, the following model claims safety and progress
> > > > > for the sysidle state machine.
> > > > > 
> > > > > Thoughts?
> > > > 
> > > > Hi Paul,
> > > > 
> > > > Please keep in mind that it's been a while since I've looked at Promela
> > > > proofs, but a couple of questions come to mind. First, how is the execution
> > > > script below checking for progress in any way ? I remember that we used
> > > > the negation of a "_np" LTL claim to check for progress in the past.
> > > > Moreover, I'd be much more comfortable seeing ifdefs in the code that
> > > > inject
> > > > known failures, and let them be triggered by error-triggering runs in the
> > > > scripts (with e.g. -DINJECT_ERROR_XYZ), to confirm that this model actually
> > > > catches known issues.
> > > 
> > > Well, if I comment out the four "progress_" labels, it complains about
> > > a non-progress cycle.  So at least spin does pay attention to these.  ;-)
> > > 
> > > If I put the "progress_" labels back in, but change the check so as to
> > > prevent the state machine from ever entering RCU_SYSIDLE_FULL_NOTED,
> > > it cranks through 14M states before complaining about a non-progress cycle,
> > > as expected.
> > > 
> > > If I revert back to pristine state, and then comment out the statements
> > > that reverts state back to RCU_SYSIDLE_NOT when exiting idle, an assert()
> > > triggers, as expected.
> > > 
> > > > If we can show that the model can detect a few failure modes, both for
> > > > safety
> > > > and progress, then my confidence level in the model will start to improve.
> > > > ;-)
> > > 
> > > Well, there probably is a bug in there somewhere, Murphy being who he is.
> > > ;-)
> > 
> > One failure mode your model seems to miss is when I comment the wakeup:
> > 
> >                 /* If needed, wake up the timekeeper. */
> >                 if
> > #ifndef INJECT_NO_WAKEUP
> >                 :: oldstate == RCU_SYSIDLE_FULL_NOTED ->
> >                         wakeup_timekeeper = 1;
> > #endif /* #ifndef INJECT_NO_WAKEUP */
> >                 :: else -> skip;
> >                 fi;
> > 
> > Somehow, I feel I am doing something very nasty to the algorithm,
> > but the model checker fails to find any kind of progress or safety
> > issue. Any idea why ?
> 
> Hmmm...  One reason is because I am not modeling the timekeeper thread
> as waiting for the wakeup.  Let me see what I can do about that...

And here is an updated model.  I now make it loop waiting for the
wakeup_timekeeper variable to transition to 1.  And I learned that
Promela ignores "progress" labels within atomic statements...

The previous error injections still trigger asserts.

							Thanx, Paul

------------------------------------------------------------------------

/*
 * 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@xxxxxxxxxxxxxxxxxx>
 */

#define NUM_WORKERS 2

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;
			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:
			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;
			}
		:: 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. */
		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 ->
			do
			:: full_sysidle_state == RCU_SYSIDLE_FULL_NOTED &&
			   wakeup_timekeeper == 0 ->
				/*
				 * We are asleep, so all workers better
				 * be idle.
				 */
progress_full_system_idle_2:
				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);
				}
			:: full_sysidle_state != RCU_SYSIDLE_FULL_NOTED &&
			   wakeup_timekeeper == 0 ->
				skip; /* No progress, should be awakened. */
			:: wakeup_timekeeper != 0 ->
				break;
			od;
		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();
}

--
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/