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 > <paul...@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 <paul...@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 > -- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majord...@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/