Re: [PATCH v4 2/5] x86, traps: Track entry into and exit from IST context

["Paul E. McKenney" <paulmck@linux.vnet.ibm.com>]

On Mon, Nov 24, 2014 at 02:36:18PM -0800, Andy Lutomirski wrote:
> On Mon, Nov 24, 2014 at 2:34 PM, Paul E. McKenney
> <paulmck@linux.vnet.ibm.com> wrote:
> > On Mon, Nov 24, 2014 at 01:35:01PM -0800, Paul E. McKenney wrote:

[ . . . ]

> > And the following Promela model claims that your approach works.
> > Should I trust it?  ;-)
> >
> 
> I think so.
> 
> Want to write a patch?  If so, whose tree should it go in?  I can add
> it to my IST series, but that seems a bit odd.

Working on it.  ;-)

							Thanx, Paul

> --Andy
> 
> >                                                         Thanx, Paul
> >
> > ------------------------------------------------------------------------
> >
> > /*
> >  * Promela model for Andy Lutomirski's suggested change to rcu_nmi_enter()
> >  * that allows nesting.
> >  *
> >  * 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>
> >  */
> >
> > byte dynticks_nesting;
> > byte dynticks_nmi_nesting;
> > byte dynticks;
> > byte busy;
> >
> > /*
> >  * Promela verision of rcu_nmi_enter().
> >  */
> > inline rcu_nmi_enter()
> > {
> >         assert(dynticks_nmi_nesting >= 0);
> >         if
> >         :: (dynticks & 1) == 0 ->
> >                 atomic {
> >                         dynticks = dynticks + 1;
> >                 }
> >                 assert((dynticks & 1) == 1);
> >                 dynticks_nmi_nesting = dynticks_nmi_nesting + 1;
> >                 assert(dynticks_nmi_nesting >= 1);
> >         :: else ->
> >                 dynticks_nmi_nesting = dynticks_nmi_nesting + 2;
> >         fi;
> > }
> >
> > /*
> >  * Promela verision of rcu_nmi_exit().
> >  */
> > inline rcu_nmi_exit()
> > {
> >         assert(dynticks_nmi_nesting > 0);
> >         assert((dynticks & 1) != 0);
> >         if
> >         :: dynticks_nmi_nesting != 1 ->
> >                 dynticks_nmi_nesting = dynticks_nmi_nesting - 2;
> >         :: else ->
> >                 dynticks_nmi_nesting = 0;
> >                 atomic {
> >                         dynticks = dynticks + 1;
> >                 }
> >                 assert((dynticks & 1) == 0);
> >         fi;
> > }
> >
> > /*
> >  * Base-level NMI runs non-atomically.  Crudely emulates process-level
> >  * dynticks-idle entry/exit.
> >  */
> > proctype base_NMI()
> > {
> >         do
> >         ::      if
> >                 :: 1 -> atomic {
> >                                 dynticks = dynticks + 1;
> >                         }
> >                         busy = 0;
> >                 :: 1 -> skip;
> >                 fi;
> >                 rcu_nmi_enter();
> >                 assert((dynticks & 1) == 1);
> >                 rcu_nmi_exit();
> >                 if
> >                 :: busy -> skip;
> >                 :: !busy ->
> >                         atomic {
> >                                 dynticks = dynticks + 1;
> >                         }
> >                         busy = 1;
> >                 fi;
> >         od;
> > }
> >
> > /*
> >  * Nested NMI runs atomically to emulate interrupting base_level().
> >  */
> > proctype nested_NMI()
> > {
> >         do
> >         ::      atomic {
> >                         rcu_nmi_enter();
> >                         assert((dynticks & 1) == 1);
> >                         rcu_nmi_exit();
> >                 }
> >         od;
> > }
> >
> > init {
> >         dynticks_nesting = 0;
> >         dynticks_nmi_nesting = 0;
> >         dynticks = 0;
> >         busy = 0;
> >         run base_NMI();
> >         run nested_NMI();
> > }
> >
> 
> 
> 
> -- 
> Andy Lutomirski
> AMA Capital Management, LLC
>