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

Paul E. McKenney
2014-11-24T22:58:03Z

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
>