Re: Promela/spin model for NO_HZ_FULL_SYSIDLE code

[Paul E. McKenney]

On Mon, Apr 07, 2014 at 08:54:52PM +0200, Frederic Weisbecker wrote:
> On Mon, Apr 07, 2014 at 11:11:55AM -0700, Paul E. McKenney wrote:
> > > 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.
> 
> Right but the very first read that checks if full_sysidle_state is > RCU_SYSIDLE_SHORT
> is done in a non-atomic way. Only when it verifies the condition do we use cmpxchg()
> 
>        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;
>        }
> 
> Now the way you wrote it PROMELA looked like we use cmpxchg() (or some close relative)
> right away from the first read. It's hard to translate with real world operations so I'm
> inventing cmpxchg_if_above() which has the same atomic and full barrier properties
> than cmpxchg() expect that it only exchanges old value with new value if old is
> above the last parameter:
> 
>         oldstate = cmpxchg_if_above(oldstate, RCU_SYSIDLE_NOT, RCU_SYSIDLE_SHORT);
>         if (oldstate == RCU_SYSIDLE_FULL_NOTED)
>                 rcu_kick_nohz_cpu(tick_do_timer_cpu);
>                 return; /* We cleared it, done! */
> 
> 
> > If the value is different at the time of the cmpxchg(), the cmpxchg() fails.
> 
> Right but it might not do a cmpxchg() if oldval is <= SHORT.
> 
> > 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
> 
> Ok if they have the same result and implement the first read in a non atomic
> way then it's all good. The PROMELA syntax has just been confusing to me in
> this regard.

Actually, my first attempt above wasn't quite right.  This one is better.
So, yes, Promela can be confusing.  ;-)

		/* 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;
				:: oldstate > RCU_SYSIDLE_SHORT &&
				   oldstate != full_sysidle_state ->
					oldstate = full_sysidle_state;
				:: oldstate <= RCU_SYSIDLE_SHORT -> break;
				fi;
			}
		od;

And this passes as well.

> > > > 			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.
> 
> Ah ok.
> 
> > 
> > > > 		:: 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?
> 
> Hmm, the loop above is the code of !timekeeper side. I'm referring to the timekeeper side (which
> is what this PROMELA chunck represents, unless I'm utterly confused).

Yep, we are in the timekeeper part of the model.

> And the timekeeper side resets full_sysidle_state when it detects a non-idle CPU:
> 
> rcu_sys_is_idle() -> rcu_sysidle_report -> rcu_sysidle_cancel()
> 
> So the PROMELA code suggests that when we find a non idle CPU, we only reset
> full_sysidle_state when is it >= RCU_SYSIDLE_LONG:
> 
>                   :: idle == 0 && full_sysidle_state >= RCU_SYSIDLE_LONG ->
>                         /* Non-idle and state advanced, revert to base state. */
>                         full_sysidle_state = RCU_SYSIDLE_NOT;
> 
> ...but actually the condition upstream seems to be full_sysidle_state >= RCU_SYSIDLE_SHORT.
> 
> For example we loop in rcu_sys_is_idle() (case of NR_CPUS < 8), and we detect a round of full-idle CPUs, so we
> set full_sysidle_state to RCU_SYSIDLE_SHORT. Then we do another pass in the loop but this
> time we detect a CPU is not idle, so we reset to RCU_SYSIDLE_NOT instead of advancing to RCU_SYSIDLE_LONG.
> 
> Right?

So rcu_sys_is_idle() invokes rcu_sysidle_report() after each scan.
If rcu_sysidle_report() sees that there was a nonidle CPU, it invokes
rcu_sysidle_cancel().  Which does indeed set the state back to
RCU_SYSIDLE_NOT, as you say.  Who wrote this code, anyway?  ;-)

IIRC, the rationale was that hitting the state hard and often on
small systems should not be a problem.  But there will probably
soon be some system out there that will not like this sort of
treatment.

I am tempted to modify the kernel to make it easier to model by putting a
check for full_sysidle_state >= RCU_SYSIDLE_LONG in rcu_sysidle_cancel(),
and I might at some point do just that.  For the moment, I just made
the model check both ways.  It does work either way.  (Whew!)

Seems like it would be simpler if the state machines for both large
and small systems operated the same, though.  And the extra check
certainly shouldn't hurt small systems.  So I will change the kernel!

							Thanx, Paul

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