On Wed, Sep 28, 2016 at 06:56:25AM +0900, SeongJae Park wrote:
> `Formal Verification` was a section in analysis chapter in initial
> version. After that, it changed to an appendix[1], then promoted to a
> chapter[2] now while the analysis chapter has merged into debugging
> chapter[3]. However, code samples for formal verification exist under
> `CodeSamples/appendix/formal/` and `CodeSamples/analysis/` directory.
> It is unnecessary duplicate and ambiguous directory hierarchy. This
> commit removes the unnecessarily dulicated files and changes the name of
> the directory.
>
> [1] commit 8a7e0cb902e9, ("Move the formal-verification sections to a
> new appendix.")
> [2] commit 87a645d2aa0b ("Promote formal-methods appendix to a
> chapter.")
> [3] commit e0c08f843331 ("Merge the analysis chapter into debugging.")
>
> Signed-off-by: SeongJae Park <sj38.park@xxxxxxxxx>
Applied, thank you!
Thanx, Paul
> ---
> CodeSamples/appendix/formal/dyntickRCU-base-s.spin | 196 --------
> .../appendix/formal/dyntickRCU-base-sl-busted.spin | 224 ---------
> .../appendix/formal/dyntickRCU-base-sl.spin | 220 ---------
> CodeSamples/appendix/formal/dyntickRCU-base.spin | 164 -------
> .../appendix/formal/dyntickRCU-irq-nmi-ssl.spin | 506 ---------------------
> .../appendix/formal/dyntickRCU-irq-ssl.spin | 356 ---------------
> .../appendix/formal/dyntickRCU-irqnn-ssl.spin | 330 --------------
> CodeSamples/appendix/formal/dyntickRCUtarball.sh | 18 -
> CodeSamples/appendix/formal/runspin.sh | 31 --
> .../{analysis => formal}/promela/.gitignore | 0
> .../promela/atomicincrement.spin | 0
> .../formal => formal/promela/dyntick}/.gitignore | 0
> .../promela/dyntick/dyntickRCU-base-s.spin | 0
> .../promela/dyntick/dyntickRCU-base-sl-busted.spin | 0
> .../dyntickRCU-base-sl-busted.spin.trail.txt | 0
> .../promela/dyntick/dyntickRCU-base-sl.spin | 0
> .../promela/dyntick/dyntickRCU-base.spin | 0
> .../promela/dyntick/dyntickRCU-irq-nmi-ssl.spin | 0
> .../promela/dyntick/dyntickRCU-irq-ssl.spin | 0
> .../promela/dyntick/dyntickRCU-irqnn-ssl.spin | 0
> .../promela/dyntick/dyntickRCUtarball.sh | 0
> .../promela/dyntick/runspin.sh | 0
> .../{analysis => formal}/promela/increment.spin | 0
> CodeSamples/{analysis => formal}/promela/lock.h | 0
> CodeSamples/{analysis => formal}/promela/lock.spin | 0
> CodeSamples/{analysis => formal}/promela/qrcu.spin | 0
> 26 files changed, 2045 deletions(-)
> delete mode 100644 CodeSamples/appendix/formal/dyntickRCU-base-s.spin
> delete mode 100644 CodeSamples/appendix/formal/dyntickRCU-base-sl-busted.spin
> delete mode 100644 CodeSamples/appendix/formal/dyntickRCU-base-sl.spin
> delete mode 100644 CodeSamples/appendix/formal/dyntickRCU-base.spin
> delete mode 100644 CodeSamples/appendix/formal/dyntickRCU-irq-nmi-ssl.spin
> delete mode 100644 CodeSamples/appendix/formal/dyntickRCU-irq-ssl.spin
> delete mode 100644 CodeSamples/appendix/formal/dyntickRCU-irqnn-ssl.spin
> delete mode 100644 CodeSamples/appendix/formal/dyntickRCUtarball.sh
> delete mode 100644 CodeSamples/appendix/formal/runspin.sh
> rename CodeSamples/{analysis => formal}/promela/.gitignore (100%)
> rename CodeSamples/{analysis => formal}/promela/atomicincrement.spin (100%)
> rename CodeSamples/{appendix/formal => formal/promela/dyntick}/.gitignore (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/dyntickRCU-base-s.spin (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/dyntickRCU-base-sl-busted.spin (100%)
> rename CodeSamples/{appendix/formal => formal/promela/dyntick}/dyntickRCU-base-sl-busted.spin.trail.txt (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/dyntickRCU-base-sl.spin (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/dyntickRCU-base.spin (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/dyntickRCU-irq-nmi-ssl.spin (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/dyntickRCU-irq-ssl.spin (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/dyntickRCU-irqnn-ssl.spin (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/dyntickRCUtarball.sh (100%)
> rename CodeSamples/{analysis => formal}/promela/dyntick/runspin.sh (100%)
> rename CodeSamples/{analysis => formal}/promela/increment.spin (100%)
> rename CodeSamples/{analysis => formal}/promela/lock.h (100%)
> rename CodeSamples/{analysis => formal}/promela/lock.spin (100%)
> rename CodeSamples/{analysis => formal}/promela/qrcu.spin (100%)
>
> diff --git a/CodeSamples/appendix/formal/dyntickRCU-base-s.spin b/CodeSamples/appendix/formal/dyntickRCU-base-s.spin
> deleted file mode 100644
> index 21aea11..0000000
> --- a/CodeSamples/appendix/formal/dyntickRCU-base-s.spin
> +++ /dev/null
> @@ -1,196 +0,0 @@
> -/*
> - * Tests a variation of RCU-dyntick interaction in the Linux 2.6.25-rc4
> - * kernel. Note that portions of this are derived from Linux kernel code,
> - * portions of which are licensed under a GPLv2-only license.
> - *
> - * This version omits irq/NMI handlers. It does not have liveness checks.
> - *
> - * 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 (c) 2008 IBM Corporation.
> - */
> -
> -/*
> - * Parameters:
> - *
> - * MAX_DYNTICK_LOOP_NOHZ: The number of non-idle process level bursts
> - * of work.
> - *
> - * Setting a given value for a given parameter covers all values up to
> - * and including the specified value. So, if MAX_DYNTICK_LOOP_NOHZ is
> - * set to "2", then the validation will cover 0, 1, and 2 loops.
> - */
> -
> -#define MAX_DYNTICK_LOOP_NOHZ 3
> -
> -/* Variables corresponding to the 2.6.25-rc4 per-CPU variables. */
> -
> -byte dynticks_progress_counter = 0;
> -byte rcu_update_flag = 0;
> -byte in_interrupt = 0;
> -
> -/*
> - * The grace_period() process uses this to track its progress through
> - * each phase, thus allowing the other processes to make sure that
> - * grace_period() does not advance prematurely.
> - */
> -
> -#define GP_IDLE 0
> -#define GP_WAITING 1
> -#define GP_DONE 2
> -byte grace_period_state = GP_DONE;
> -
> -/*
> - * Validation code for the slice of the preemptible-RCU code that
> - * interacts with the dynticks subsystem. This is set up to match
> - * the code in 2.6.25-rc4, namely dyntick_save_progress_counter(),
> - * rcu_try_flip_waitack_needed(), rcu_try_flip_waitmb_needed(),
> - * and portions of rcu_try_flip_waitack() and rcu_try_flip_waitmb().
> - */
> -
> -proctype grace_period()
> -{
> - byte curr;
> - byte snap;
> -
> - /*
> - * A little code from rcu_try_flip_idle() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. As noted earlier, the grace_period_state
> - * variable allows the other processes to scream if we jump
> - * the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - printf("MAX_DYNTICK_LOOP_NOHZ = %d\n", MAX_DYNTICK_LOOP_NOHZ);
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitack()
> - * and its call to rcu_try_flip_waitack_needed().
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - curr = dynticks_progress_counter;
> - if
> - :: (curr == snap) && ((curr & 1) == 0) ->
> - break;
> - :: (curr - snap) > 2 || (snap & 1) == 0 ->
> - break;
> - :: 1 -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -
> - /*
> - * A little code from rcu_try_flip_waitzero() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. As noted earlier, the grace_period_state
> - * variable allows the other processes to scream if we jump
> - * the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitmb()
> - * and its call to rcu_try_flip_waitmb_needed().
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - curr = dynticks_progress_counter;
> - if
> - :: (curr == snap) && ((curr & 1) == 0) ->
> - break;
> - :: (curr != snap) ->
> - break;
> - :: 1 -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -}
> -
> -/*
> - * Validation code for the rcu_enter_nohz() and rcu_exit_nohz()
> - * functions. Each pass through this process's loop corresponds
> - * to exiting nohz mode, then re-entering it. The old_gp_idle
> - * variable is used to verify that grace_period() does not incorrectly
> - * advance while this process is not in nohz mode. This code also
> - * includes assertions corresponding to the WARN_ON() calls in
> - * rcu_exit_nohz() and rcu_enter_nohz().
> - */
> -
> -proctype dyntick_nohz()
> -{
> - byte tmp;
> - byte i = 0;
> - bit old_gp_idle;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_NOHZ -> break;
> - :: i < MAX_DYNTICK_LOOP_NOHZ ->
> -
> - /*
> - * The following corresponds to rcu_exit_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - tmp = dynticks_progress_counter;
> - atomic {
> - dynticks_progress_counter = tmp + 1;
> - old_gp_idle = (grace_period_state == GP_IDLE);
> - assert((dynticks_progress_counter & 1) == 1);
> - }
> -
> - /*
> - * The following corresponds to rcu_enter_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - atomic {
> - tmp = dynticks_progress_counter;
> - assert(!old_gp_idle || grace_period_state != GP_DONE);
> - }
> - atomic {
> - dynticks_progress_counter = tmp + 1;
> - assert((dynticks_progress_counter & 1) == 0);
> - }
> - i++;
> - od;
> -}
> -
> -init {
> - atomic {
> - run dyntick_nohz();
> - run grace_period();
> - }
> -}
> diff --git a/CodeSamples/appendix/formal/dyntickRCU-base-sl-busted.spin b/CodeSamples/appendix/formal/dyntickRCU-base-sl-busted.spin
> deleted file mode 100644
> index 46e97fd..0000000
> --- a/CodeSamples/appendix/formal/dyntickRCU-base-sl-busted.spin
> +++ /dev/null
> @@ -1,224 +0,0 @@
> -/*
> - * Tests a variation of RCU-dyntick interaction in the Linux 2.6.25-rc4
> - * kernel. Note that portions of this are derived from Linux kernel code,
> - * portions of which are licensed under a GPLv2-only license.
> - *
> - * This version omits irq/NMI handlers.
> - *
> - * 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 (c) 2008 IBM Corporation.
> - */
> -
> -/*
> - * Parameters:
> - *
> - * MAX_DYNTICK_LOOP_NOHZ: The number of non-idle process level bursts
> - * of work.
> - *
> - * Setting a given value for a given parameter covers all values up to
> - * and including the specified value. So, if MAX_DYNTICK_LOOP_NOHZ is
> - * set to "2", then the validation will cover 0, 1, and 2 loops.
> - */
> -
> -#define MAX_DYNTICK_LOOP_NOHZ 3
> -
> -/* Variables corresponding to the 2.6.25-rc4 per-CPU variables. */
> -
> -byte dynticks_progress_counter = 0;
> -byte rcu_update_flag = 0;
> -byte in_interrupt = 0;
> -
> -/*
> - * The grace_period() process uses this to track its progress through
> - * each phase, thus allowing the other processes to make sure that
> - * grace_period() does not advance prematurely.
> - */
> -
> -#define GP_IDLE 0
> -#define GP_WAITING 1
> -#define GP_DONE 2
> -byte grace_period_state = GP_DONE;
> -
> -/*
> - * The following variables mark completion of the corresponding processes.
> - * This is used in grace_period() to check forward progress guarantees.
> - */
> -
> -bit dyntick_nohz_done = 0;
> -
> -/*
> - * Validation code for the slice of the preemptible-RCU code that
> - * interacts with the dynticks subsystem. This is set up to match
> - * the code in 2.6.25-rc4, namely dyntick_save_progress_counter(),
> - * rcu_try_flip_waitack_needed(), rcu_try_flip_waitmb_needed(),
> - * and portions of rcu_try_flip_waitack() and rcu_try_flip_waitmb().
> - *
> - * This code verifies forward progress: once all of the other processes
> - * have terminated, the grace_period() code must not block. In addition,
> - * this code maintains a progress indicator in the grace_period_state
> - * variable. It is an error for grace_period() to advance from GP_IDLE
> - * to GP_DONE unless all the other processes are simultaneously in nohz
> - * mode at some point during the transition.
> - */
> -
> -proctype grace_period()
> -{
> - byte curr;
> - byte snap;
> - bit shouldexit;
> -
> - /*
> - * A little code from rcu_try_flip_idle() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - printf("MAX_DYNTICK_LOOP_NOHZ = %d\n", MAX_DYNTICK_LOOP_NOHZ);
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitack()
> - * and its call to rcu_try_flip_waitack_needed(). The shouldexit
> - * check ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr == snap) && ((curr & 1) == 0) ->
> - break;
> - :: (curr - snap) > 2 || (snap & 1) == 0 ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -
> - /*
> - * A little code from rcu_try_flip_waitzero() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitmb()
> - * and its call to rcu_try_flip_waitmb_needed(). The shouldexit
> - * check again ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr == snap) && ((curr & 1) == 0) ->
> - break;
> - :: (curr != snap) ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -}
> -
> -/*
> - * Validation code for the rcu_enter_nohz() and rcu_exit_nohz()
> - * functions. Each pass through this process's loop corresponds
> - * to exiting nohz mode, then re-entering it. The old_gp_idle
> - * variable is used to verify that grace_period() does not incorrectly
> - * advance while this process is not in nohz mode. This code also
> - * includes assertions corresponding to the WARN_ON() calls in
> - * rcu_exit_nohz() and rcu_enter_nohz().
> - */
> -
> -proctype dyntick_nohz()
> -{
> - byte tmp;
> - byte i = 0;
> - bit old_gp_idle;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_NOHZ -> break;
> - :: i < MAX_DYNTICK_LOOP_NOHZ ->
> -
> - /*
> - * The following corresponds to rcu_exit_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - tmp = dynticks_progress_counter;
> - atomic {
> - dynticks_progress_counter = tmp + 1;
> - old_gp_idle = (grace_period_state == GP_IDLE);
> - assert((dynticks_progress_counter & 1) == 1);
> - }
> -
> - /*
> - * The following corresponds to rcu_enter_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - atomic {
> - tmp = dynticks_progress_counter;
> - assert(!old_gp_idle || grace_period_state != GP_DONE);
> - }
> - atomic {
> - dynticks_progress_counter = tmp + 1;
> - assert((dynticks_progress_counter & 1) == 0);
> - }
> - i++;
> - od;
> - dyntick_nohz_done = 1;
> -}
> -
> -init {
> - atomic {
> - run dyntick_nohz();
> - run grace_period();
> - }
> -}
> diff --git a/CodeSamples/appendix/formal/dyntickRCU-base-sl.spin b/CodeSamples/appendix/formal/dyntickRCU-base-sl.spin
> deleted file mode 100644
> index 3655e87..0000000
> --- a/CodeSamples/appendix/formal/dyntickRCU-base-sl.spin
> +++ /dev/null
> @@ -1,220 +0,0 @@
> -/*
> - * Tests a variation of RCU-dyntick interaction in the Linux 2.6.25-rc4
> - * kernel. Note that portions of this are derived from Linux kernel code,
> - * portions of which are licensed under a GPLv2-only license.
> - *
> - * This version omits irq/NMI handlers.
> - *
> - * 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 (c) 2008 IBM Corporation.
> - */
> -
> -/*
> - * Parameters:
> - *
> - * MAX_DYNTICK_LOOP_NOHZ: The number of non-idle process level bursts
> - * of work.
> - *
> - * Setting a given value for a given parameter covers all values up to
> - * and including the specified value. So, if MAX_DYNTICK_LOOP_NOHZ is
> - * set to "2", then the validation will cover 0, 1, and 2 loops.
> - */
> -
> -#define MAX_DYNTICK_LOOP_NOHZ 3
> -
> -/* Variables corresponding to the 2.6.25-rc4 per-CPU variables. */
> -
> -byte dynticks_progress_counter = 0;
> -byte rcu_update_flag = 0;
> -byte in_interrupt = 0;
> -
> -/*
> - * The grace_period() process uses this to track its progress through
> - * each phase, thus allowing the other processes to make sure that
> - * grace_period() does not advance prematurely.
> - */
> -
> -#define GP_IDLE 0
> -#define GP_WAITING 1
> -#define GP_DONE 2
> -byte grace_period_state = GP_DONE;
> -
> -/*
> - * The following variables mark completion of the corresponding processes.
> - * This is used in grace_period() to check forward progress guarantees.
> - */
> -
> -bit dyntick_nohz_done = 0;
> -
> -/*
> - * Validation code for the slice of the preemptible-RCU code that
> - * interacts with the dynticks subsystem. This is set up to match
> - * the code in 2.6.25-rc4, namely dyntick_save_progress_counter(),
> - * rcu_try_flip_waitack_needed(), rcu_try_flip_waitmb_needed(),
> - * and portions of rcu_try_flip_waitack() and rcu_try_flip_waitmb().
> - *
> - * This code verifies forward progress: once all of the other processes
> - * have terminated, the grace_period() code must not block. In addition,
> - * this code maintains a progress indicator in the grace_period_state
> - * variable. It is an error for grace_period() to advance from GP_IDLE
> - * to GP_DONE unless all the other processes are simultaneously in nohz
> - * mode at some point during the transition.
> - */
> -
> -proctype grace_period()
> -{
> - byte curr;
> - byte snap;
> - bit shouldexit;
> -
> - /*
> - * A little code from rcu_try_flip_idle() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - printf("MAX_DYNTICK_LOOP_NOHZ = %d\n", MAX_DYNTICK_LOOP_NOHZ);
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitack()
> - * and its call to rcu_try_flip_waitack_needed(). The shouldexit
> - * check ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr - snap) >= 2 || (curr & 1) == 0 ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -
> - /*
> - * A little code from rcu_try_flip_waitzero() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitmb()
> - * and its call to rcu_try_flip_waitmb_needed(). The shouldexit
> - * check again ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr != snap) || ((curr & 1) == 0) ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -}
> -
> -/*
> - * Validation code for the rcu_enter_nohz() and rcu_exit_nohz()
> - * functions. Each pass through this process's loop corresponds
> - * to exiting nohz mode, then re-entering it. The old_gp_idle
> - * variable is used to verify that grace_period() does not incorrectly
> - * advance while this process is not in nohz mode. This code also
> - * includes assertions corresponding to the WARN_ON() calls in
> - * rcu_exit_nohz() and rcu_enter_nohz().
> - */
> -
> -proctype dyntick_nohz()
> -{
> - byte tmp;
> - byte i = 0;
> - bit old_gp_idle;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_NOHZ -> break;
> - :: i < MAX_DYNTICK_LOOP_NOHZ ->
> -
> - /*
> - * The following corresponds to rcu_exit_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - tmp = dynticks_progress_counter;
> - atomic {
> - dynticks_progress_counter = tmp + 1;
> - old_gp_idle = (grace_period_state == GP_IDLE);
> - assert((dynticks_progress_counter & 1) == 1);
> - }
> -
> - /*
> - * The following corresponds to rcu_enter_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - atomic {
> - tmp = dynticks_progress_counter;
> - assert(!old_gp_idle || grace_period_state != GP_DONE);
> - }
> - atomic {
> - dynticks_progress_counter = tmp + 1;
> - assert((dynticks_progress_counter & 1) == 0);
> - }
> - i++;
> - od;
> - dyntick_nohz_done = 1;
> -}
> -
> -init {
> - atomic {
> - run dyntick_nohz();
> - run grace_period();
> - }
> -}
> diff --git a/CodeSamples/appendix/formal/dyntickRCU-base.spin b/CodeSamples/appendix/formal/dyntickRCU-base.spin
> deleted file mode 100644
> index 29f0345..0000000
> --- a/CodeSamples/appendix/formal/dyntickRCU-base.spin
> +++ /dev/null
> @@ -1,164 +0,0 @@
> -/*
> - * Tests a variation of RCU-dyntick interaction in the Linux 2.6.25-rc4
> - * kernel. Note that portions of this are derived from Linux kernel code,
> - * portions of which are licensed under a GPLv2-only license.
> - *
> - * This version omits irq/NMI handlers. It does not have either safety
> - * or liveness checks.
> - *
> - * 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 (c) 2008 IBM Corporation.
> - */
> -
> -/*
> - * Parameters:
> - *
> - * MAX_DYNTICK_LOOP_NOHZ: The number of non-idle process level bursts
> - * of work.
> - *
> - * Setting a given value for a given parameter covers all values up to
> - * and including the specified value. So, if MAX_DYNTICK_LOOP_NOHZ is
> - * set to "2", then the validation will cover 0, 1, and 2 loops.
> - */
> -
> -#define MAX_DYNTICK_LOOP_NOHZ 3
> -
> -/* Variables corresponding to the 2.6.25-rc4 per-CPU variables. */
> -
> -byte dynticks_progress_counter = 0;
> -byte rcu_update_flag = 0;
> -byte in_interrupt = 0;
> -
> -/*
> - * Validation code for the slice of the preemptible-RCU code that
> - * interacts with the dynticks subsystem. This is set up to match
> - * the code in 2.6.25-rc4, namely dyntick_save_progress_counter(),
> - * rcu_try_flip_waitack_needed(), rcu_try_flip_waitmb_needed(),
> - * and portions of rcu_try_flip_waitack() and rcu_try_flip_waitmb().
> - */
> -
> -proctype grace_period()
> -{
> - byte curr;
> - byte snap;
> -
> - /*
> - * A little code from rcu_try_flip_idle() and its call
> - * to dyntick_save_progress_counter().
> - */
> -
> - atomic {
> - printf("MAX_DYNTICK_LOOP_NOHZ = %d\n", MAX_DYNTICK_LOOP_NOHZ);
> - snap = dynticks_progress_counter;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitack()
> - * and its call to rcu_try_flip_waitack_needed().
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - curr = dynticks_progress_counter;
> - if
> - :: (curr == snap) && ((curr & 1) == 0) ->
> - break;
> - :: (curr - snap) > 2 || (snap & 1) == 0 ->
> - break;
> - :: 1 -> skip;
> - fi;
> - }
> - od;
> -
> - /*
> - * A little code from rcu_try_flip_waitzero() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code.
> - */
> -
> - snap = dynticks_progress_counter;
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitmb()
> - * and its call to rcu_try_flip_waitmb_needed().
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - curr = dynticks_progress_counter;
> - if
> - :: (curr == snap) && ((curr & 1) == 0) ->
> - break;
> - :: (curr != snap) ->
> - break;
> - :: 1 -> skip;
> - fi;
> - }
> - od;
> -}
> -
> -/*
> - * Validation code for the rcu_enter_nohz() and rcu_exit_nohz()
> - * functions. Each pass through this process's loop corresponds
> - * to exiting nohz mode, then re-entering it. This code also
> - * includes assertions corresponding to the WARN_ON() calls in
> - * rcu_exit_nohz() and rcu_enter_nohz().
> - */
> -
> -proctype dyntick_nohz()
> -{
> - byte tmp;
> - byte i = 0;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_NOHZ -> break;
> - :: i < MAX_DYNTICK_LOOP_NOHZ ->
> -
> - /*
> - * The following corresponds to rcu_exit_nohz().
> - */
> -
> - tmp = dynticks_progress_counter;
> - atomic {
> - dynticks_progress_counter = tmp + 1;
> - assert((dynticks_progress_counter & 1) == 1);
> - }
> -
> - /*
> - * The following corresponds to rcu_enter_nohz().
> - */
> -
> - tmp = dynticks_progress_counter;
> - atomic {
> - dynticks_progress_counter = tmp + 1;
> - assert((dynticks_progress_counter & 1) == 0);
> - }
> - i++;
> - od;
> -}
> -
> -init {
> - atomic {
> - run dyntick_nohz();
> - run grace_period();
> - }
> -}
> diff --git a/CodeSamples/appendix/formal/dyntickRCU-irq-nmi-ssl.spin b/CodeSamples/appendix/formal/dyntickRCU-irq-nmi-ssl.spin
> deleted file mode 100644
> index 9a01477..0000000
> --- a/CodeSamples/appendix/formal/dyntickRCU-irq-nmi-ssl.spin
> +++ /dev/null
> @@ -1,506 +0,0 @@
> -/*
> - * Tests a variation of RCU-dyntick interaction in the Linux 2.6.25-rc4
> - * kernel. Note that portions of this are derived from Linux kernel code,
> - * portions of which are licensed under a GPLv2-only license.
> - *
> - * 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 (c) 2008 IBM Corporation.
> - */
> -
> -/*
> - * Parameters:
> - *
> - * MAX_DYNTICK_LOOP_NOHZ: The number of non-idle process level bursts
> - * of work.
> - * MAX_DYNTICK_LOOP_IRQ: The number of interrupts (possibly arbitrarily
> - * nested) to be received.
> - * MAX_DYNTICK_LOOP_NMI: The number of NMIs (never nested) to be received.
> - *
> - * Setting a given value for a given parameter covers all values up to
> - * and including the specified value. So, if MAX_DYNTICK_LOOP_IRQ is
> - * set to "2", then the validation will cover 0, 1, and 2 interrupts,
> - * arbitrarily nested.
> - */
> -
> -#define MAX_DYNTICK_LOOP_NOHZ 1
> -#define MAX_DYNTICK_LOOP_IRQ 2
> -#define MAX_DYNTICK_LOOP_NMI 1
> -
> -/* Variables corresponding to the 2.6.25-rc4 per-CPU variables. */
> -
> -byte dynticks_progress_counter = 0;
> -byte rcu_update_flag = 0;
> -byte in_interrupt = 0;
> -
> -/* Set when IRQ code is running, to allow mainline code to lock itself out. */
> -
> -bit in_dyntick_irq = 0;
> -
> -/*
> - * Set when NMI code is running, to allow both mainline code and irq handler
> - * code to lock itself out.
> - */
> -
> -bit in_dyntick_nmi = 0;
> -
> -/*
> - * The grace_period() process uses this to track its progress through
> - * each phase, thus allowing the other processes to make sure that
> - * grace_period() does not advance prematurely.
> - */
> -
> -#define GP_IDLE 0
> -#define GP_WAITING 1
> -#define GP_DONE 2
> -byte grace_period_state = GP_DONE;
> -
> -/*
> - * The following variables mark completion of the corresponding processes.
> - * This is used in grace_period() to check forward progress guarantees.
> - */
> -
> -bit dyntick_nohz_done = 0;
> -bit dyntick_irq_done = 0;
> -bit dyntick_nmi_done = 0;
> -
> -/*
> - * Validation code for the slice of the preemptible-RCU code that
> - * interacts with the dynticks subsystem. This is set up to match
> - * the code in 2.6.25-rc4, namely dyntick_save_progress_counter(),
> - * rcu_try_flip_waitack_needed(), rcu_try_flip_waitmb_needed(),
> - * and portions of rcu_try_flip_waitack() and rcu_try_flip_waitmb().
> - *
> - * This code verifies forward progress: once all of the other processes
> - * have terminated, the grace_period() code must not block. In addition,
> - * this code maintains a progress indicator in the grace_period_state
> - * variable. It is an error for grace_period() to advance from GP_IDLE
> - * to GP_DONE unless all the other processes are simultaneously in nohz
> - * mode at some point during the transition.
> - */
> -
> -proctype grace_period()
> -{
> - byte curr;
> - byte snap;
> - bit shouldexit;
> -
> - /*
> - * A little code from rcu_try_flip_idle() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - printf("MAX_DYNTICK_LOOP_NOHZ = %d\n", MAX_DYNTICK_LOOP_NOHZ);
> - printf("MAX_DYNTICK_LOOP_IRQ = %d\n", MAX_DYNTICK_LOOP_IRQ);
> - printf("MAX_DYNTICK_LOOP_NMI = %d\n", MAX_DYNTICK_LOOP_NMI);
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitack()
> - * and its call to rcu_try_flip_waitack_needed(). The shouldexit
> - * check ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done &&
> - dyntick_irq_done &&
> - dyntick_nmi_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr - snap) >= 2 || (curr & 1) == 0 ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -
> - /*
> - * A little code from rcu_try_flip_waitzero() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitmb()
> - * and its call to rcu_try_flip_waitmb_needed(). The shouldexit
> - * check again ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done &&
> - dyntick_irq_done &&
> - dyntick_nmi_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr != snap) || ((curr & 1) == 0) ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -}
> -
> -/*
> - * Macro that allows dyntick_irq() and dyntick_nmi() code to run atomically
> - * with respect to dyntick_nohz(), but still allows dyntick_irq() and
> - * dyntick_nmi() to be interleaved with other processes.
> - */
> -
> -#define EXECUTE_MAINLINE(label, stmt) \
> -label: skip; \
> - atomic { \
> - if \
> - :: in_dyntick_irq || in_dyntick_nmi -> goto label; \
> - :: else -> stmt; \
> - fi; \
> - } \
> -
> -/*
> - * Validation code for the rcu_enter_nohz() and rcu_exit_nohz()
> - * functions. Each pass through this process's loop corresponds
> - * to exiting nohz mode, then re-entering it. The old_gp_idle
> - * variable is used to verify that grace_period() does not incorrectly
> - * advance while this process is not in nohz mode. This code also
> - * includes assertions corresponding to the WARN_ON() calls in
> - * rcu_exit_nohz() and rcu_enter_nohz().
> - */
> -
> -proctype dyntick_nohz()
> -{
> - byte tmp;
> - byte i = 0;
> - bit old_gp_idle;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_NOHZ -> break;
> - :: i < MAX_DYNTICK_LOOP_NOHZ ->
> -
> - /*
> - * The following corresponds to rcu_exit_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - EXECUTE_MAINLINE(stmt1, tmp = dynticks_progress_counter)
> - EXECUTE_MAINLINE(stmt2, dynticks_progress_counter = tmp + 1; old_gp_idle = (grace_period_state == GP_IDLE); assert((dynticks_progress_counter & 1) == 1))
> -
> - /*
> - * The following corresponds to rcu_enter_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - EXECUTE_MAINLINE(stmt3, tmp = dynticks_progress_counter; assert(!old_gp_idle || grace_period_state != GP_DONE))
> - EXECUTE_MAINLINE(stmt4, dynticks_progress_counter = tmp + 1; assert((dynticks_progress_counter & 1) == 0))
> - i++;
> - od;
> - dyntick_nohz_done = 1;
> -}
> -
> -/*
> - * Macro that allows dyntick_nmi() code to run atomically with respect
> - * to dyntick_irq(), but still allows dyntick_nmi() to be interleaved
> - * with other processes. This macro must be used when accessing
> - * external state, but statements that access state that is purely
> - * local to dyntick_irq() can be permitted to run in parallel with
> - * dyntick_nmi(). In addition, global state that is shared only
> - * with dyntick_nohz() may also be modified even when dyntick_nmi()
> - * is running.
> - */
> -
> -#define EXECUTE_IRQ(label, stmt) \
> -label: skip; \
> - atomic { \
> - if \
> - :: in_dyntick_nmi -> goto label; \
> - :: else -> stmt; \
> - fi; \
> - } \
> -
> -/*
> - * Validation code corresponding to rcu_irq_enter() and rcu_irq_exit().
> - */
> -
> -proctype dyntick_irq()
> -{
> - byte tmp;
> - byte i = 0;
> - byte j = 0;
> - bit old_gp_idle;
> - bit outermost;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_IRQ && j >= MAX_DYNTICK_LOOP_IRQ -> break;
> - :: i < MAX_DYNTICK_LOOP_IRQ ->
> -
> - /* Tell dyntick_nohz() that we are in interrupt handler. */
> -
> - atomic {
> - outermost = (in_dyntick_irq == 0);
> - in_dyntick_irq = 1;
> - }
> -
> - /* Validation code corresponding to rcu_irq_enter(). */
> -
> -stmt1: skip;
> - atomic {
> - if
> - :: in_dyntick_nmi -> goto stmt1;
> - :: !in_dyntick_nmi && rcu_update_flag ->
> - goto stmt1_then;
> - :: else -> goto stmt1_else;
> - fi;
> - }
> -stmt1_then: skip;
> - EXECUTE_IRQ(stmt1_1, tmp = rcu_update_flag)
> - EXECUTE_IRQ(stmt1_2, rcu_update_flag = tmp + 1)
> -stmt1_else: skip;
> -stmt2: skip; atomic {
> - if
> - :: in_dyntick_nmi -> goto stmt2;
> - :: !in_dyntick_nmi &&
> - !in_interrupt &&
> - (dynticks_progress_counter & 1) == 0 ->
> - goto stmt2_then;
> - :: else -> goto stmt2_else;
> - fi;
> - }
> -stmt2_then: skip;
> - EXECUTE_IRQ(stmt2_1, tmp = dynticks_progress_counter)
> - EXECUTE_IRQ(stmt2_2, dynticks_progress_counter = tmp + 1)
> - EXECUTE_IRQ(stmt2_3, tmp = rcu_update_flag)
> - EXECUTE_IRQ(stmt2_4, rcu_update_flag = tmp + 1)
> -stmt2_else: skip;
> -
> - /*
> - * And a snippet from __irq_enter() corresponding to
> - * the add_preempt_count().
> - */
> -
> - EXECUTE_IRQ(stmt3, tmp = in_interrupt)
> - EXECUTE_IRQ(stmt4, in_interrupt = tmp + 1)
> -
> - /* Capture state to see if grace_period() is behaving. */
> -
> -stmt5: skip;
> - atomic {
> - if
> - :: in_dyntick_nmi -> goto stmt4;
> - :: !in_dyntick_nmi && outermost ->
> - old_gp_idle = (grace_period_state == GP_IDLE);
> - :: else -> skip;
> - fi;
> - }
> -
> - /* Count the entry for termination and nesting. */
> -
> - i++;
> -
> - /* Note that we cannot exit a handler we have not yet entered! */
> -
> - :: j < i ->
> -
> - /* See if we can catch grace_period() misbehaving. */
> -
> -stmt6: skip;
> - atomic {
> - if
> - :: in_dyntick_nmi -> goto stmt6;
> - :: !in_dyntick_nmi && j + 1 == i ->
> - assert(!old_gp_idle ||
> - grace_period_state != GP_DONE);
> - :: else -> skip;
> - fi;
> - }
> -
> - /*
> - * Validation code corresponding to the sub_preempt_count()
> - * in __irq_exit().
> - */
> -
> - EXECUTE_IRQ(stmt7, tmp = in_interrupt);
> - EXECUTE_IRQ(stmt8, in_interrupt = tmp - 1);
> -
> - /* Validation code corresponding to rcu_irq_exit(). */
> -
> -stmt9: skip;
> - atomic {
> - if
> - :: in_dyntick_nmi -> goto stmt9;
> - :: !in_dyntick_nmi && rcu_update_flag != 0 ->
> - goto stmt9_then;
> - :: else -> goto stmt9_else;
> - fi;
> - }
> -stmt9_then: skip;
> - EXECUTE_IRQ(stmt9_1, tmp = rcu_update_flag)
> - EXECUTE_IRQ(stmt9_2, rcu_update_flag = tmp - 1)
> -stmt9_3: skip;
> - atomic {
> - if
> - :: in_dyntick_nmi -> goto stmt9_3;
> - :: !in_dyntick_nmi && rcu_update_flag == 0 ->
> - goto stmt9_3_then;
> - :: else -> goto stmt9_3_else;
> - fi;
> - }
> -stmt9_3_then: skip;
> - EXECUTE_IRQ(stmt9_3_1, tmp = dynticks_progress_counter)
> - EXECUTE_IRQ(stmt9_3_2, dynticks_progress_counter = tmp + 1)
> -stmt9_3_else:
> -stmt9_else: skip;
> -
> - /*
> - * Count the exit and let dyntick_nohz() know if we
> - * have completely exited a nested set of interrupts.
> - */
> -
> - atomic {
> - j++;
> - in_dyntick_irq = (i != j);
> - }
> - od;
> - dyntick_irq_done = 1;
> -}
> -
> -/*
> - * Validation code corresponding to rcu_irq_enter() and rcu_irq_exit().
> - * Similar to dyntick_irq(), but done atomically. This is a bit of
> - * a cheat, since the code would not really be atomic with respect
> - * to grace_period(), but one step at a time.
> - */
> -
> -proctype dyntick_nmi()
> -{
> - byte tmp;
> - byte i = 0;
> - bit old_gp_idle;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_NMI -> break;
> - :: i < MAX_DYNTICK_LOOP_NMI ->
> -
> - /* Tell dyntick_nohz() that we are in interrupt handler. */
> -
> - in_dyntick_nmi = 1;
> -
> - /* Validation code corresponding to rcu_irq_enter(). */
> -
> - if
> - :: rcu_update_flag > 0 ->
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp + 1;
> - :: else -> skip;
> - fi;
> - if
> - :: !in_interrupt && (dynticks_progress_counter & 1) == 0 ->
> - tmp = dynticks_progress_counter;
> - dynticks_progress_counter = tmp + 1;
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp + 1;
> - :: else -> skip;
> - fi;
> -
> - /*
> - * And a snippet from __irq_enter() corresponding to
> - * the add_preempt_count().
> - */
> -
> - tmp = in_interrupt;
> - in_interrupt = tmp + 1;
> -
> - /* Capture state to see if grace_period() is behaving. */
> -
> - old_gp_idle = (grace_period_state == GP_IDLE);
> -
> - /* See if we can catch grace_period() misbehaving. */
> -
> - assert(!old_gp_idle || grace_period_state != GP_DONE);
> -
> - /*
> - * Validation code corresponding to the sub_preempt_count()
> - * in __irq_exit().
> - */
> -
> - tmp = in_interrupt;
> - in_interrupt = tmp - 1;
> -
> - /* Validation code corresponding to rcu_irq_exit(). */
> -
> - if
> - :: rcu_update_flag != 0 ->
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp - 1;
> - if
> - :: rcu_update_flag == 0 ->
> - tmp = dynticks_progress_counter;
> - dynticks_progress_counter = tmp + 1;
> - :: else -> skip;
> - fi;
> - :: else -> skip;
> - fi;
> -
> - /*
> - * Count the exit and let dyntick_irq() and dyntick_nohz()
> - * know that we have exited the NMI.
> - */
> -
> - atomic {
> - i++;
> - in_dyntick_nmi = 0;
> - }
> - od;
> - dyntick_nmi_done = 1;
> -}
> -
> -init {
> - atomic {
> - run dyntick_nohz();
> - run dyntick_irq();
> - run dyntick_nmi();
> - run grace_period();
> - }
> -}
> diff --git a/CodeSamples/appendix/formal/dyntickRCU-irq-ssl.spin b/CodeSamples/appendix/formal/dyntickRCU-irq-ssl.spin
> deleted file mode 100644
> index 43ba53b..0000000
> --- a/CodeSamples/appendix/formal/dyntickRCU-irq-ssl.spin
> +++ /dev/null
> @@ -1,356 +0,0 @@
> -/*
> - * Tests a variation of RCU-dyntick interaction in the Linux 2.6.25-rc4
> - * kernel. Note that portions of this are derived from Linux kernel code,
> - * portions of which are licensed under a GPLv2-only license.
> - *
> - * This version omits NMI handlers.
> - *
> - * 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 (c) 2008 IBM Corporation.
> - */
> -
> -/*
> - * Parameters:
> - *
> - * MAX_DYNTICK_LOOP_NOHZ: The number of non-idle process level bursts
> - * of work.
> - * MAX_DYNTICK_LOOP_IRQ: The number of interrupts (possibly arbitrarily
> - * nested) to be received.
> - *
> - * Setting a given value for a given parameter covers all values up to
> - * and including the specified value. So, if MAX_DYNTICK_LOOP_IRQ is
> - * set to "2", then the validation will cover 0, 1, and 2 interrupts,
> - * arbitrarily nested.
> - */
> -
> -#define MAX_DYNTICK_LOOP_NOHZ 3
> -#define MAX_DYNTICK_LOOP_IRQ 3
> -
> -/* Variables corresponding to the 2.6.25-rc4 per-CPU variables. */
> -
> -byte dynticks_progress_counter = 0;
> -byte rcu_update_flag = 0;
> -byte in_interrupt = 0;
> -
> -/* Set when IRQ code is running, to allow mainline code to lock itself out. */
> -
> -bit in_dyntick_irq = 0;
> -
> -/*
> - * The grace_period() process uses this to track its progress through
> - * each phase, thus allowing the other processes to make sure that
> - * grace_period() does not advance prematurely.
> - */
> -
> -#define GP_IDLE 0
> -#define GP_WAITING 1
> -#define GP_DONE 2
> -byte grace_period_state = GP_DONE;
> -
> -/*
> - * The following variables mark completion of the corresponding processes.
> - * This is used in grace_period() to check forward progress guarantees.
> - */
> -
> -bit dyntick_nohz_done = 0;
> -bit dyntick_irq_done = 0;
> -
> -/*
> - * Validation code for the slice of the preemptible-RCU code that
> - * interacts with the dynticks subsystem. This is set up to match
> - * the code in 2.6.25-rc4, namely dyntick_save_progress_counter(),
> - * rcu_try_flip_waitack_needed(), rcu_try_flip_waitmb_needed(),
> - * and portions of rcu_try_flip_waitack() and rcu_try_flip_waitmb().
> - *
> - * This code verifies forward progress: once all of the other processes
> - * have terminated, the grace_period() code must not block. In addition,
> - * this code maintains a progress indicator in the grace_period_state
> - * variable. It is an error for grace_period() to advance from GP_IDLE
> - * to GP_DONE unless all the other processes are simultaneously in nohz
> - * mode at some point during the transition.
> - */
> -
> -proctype grace_period()
> -{
> - byte curr;
> - byte snap;
> - bit shouldexit;
> -
> - /*
> - * A little code from rcu_try_flip_idle() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - printf("MAX_DYNTICK_LOOP_NOHZ = %d\n", MAX_DYNTICK_LOOP_NOHZ);
> - printf("MAX_DYNTICK_LOOP_IRQ = %d\n", MAX_DYNTICK_LOOP_IRQ);
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitack()
> - * and its call to rcu_try_flip_waitack_needed(). The shouldexit
> - * check ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done && dyntick_irq_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr - snap) >= 2 || (curr & 1) == 0 ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -
> - /*
> - * A little code from rcu_try_flip_waitzero() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitmb()
> - * and its call to rcu_try_flip_waitmb_needed(). The shouldexit
> - * check again ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done && dyntick_irq_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr != snap) || ((curr & 1) == 0) ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -}
> -
> -/*
> - * Macro that allows dyntick_irq() code to run atomically with respect
> - * to dyntick_nohz(), but still allows dyntick_irq() to be interleaved
> - * with other processes.
> - */
> -
> -#define EXECUTE_MAINLINE(label, stmt) \
> -label: skip; \
> - atomic { \
> - if \
> - :: in_dyntick_irq -> goto label; \
> - :: else -> stmt; \
> - fi; \
> - } \
> -
> -/*
> - * Validation code for the rcu_enter_nohz() and rcu_exit_nohz()
> - * functions. Each pass through this process's loop corresponds
> - * to exiting nohz mode, then re-entering it. The old_gp_idle
> - * variable is used to verify that grace_period() does not incorrectly
> - * advance while this process is not in nohz mode. This code also
> - * includes assertions corresponding to the WARN_ON() calls in
> - * rcu_exit_nohz() and rcu_enter_nohz().
> - */
> -
> -proctype dyntick_nohz()
> -{
> - byte tmp;
> - byte i = 0;
> - bit old_gp_idle;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_NOHZ -> break;
> - :: i < MAX_DYNTICK_LOOP_NOHZ ->
> -
> - /*
> - * The following corresponds to rcu_exit_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - EXECUTE_MAINLINE(stmt1, tmp = dynticks_progress_counter)
> - EXECUTE_MAINLINE(stmt2,
> - dynticks_progress_counter = tmp + 1;
> - old_gp_idle = (grace_period_state == GP_IDLE);
> - assert((dynticks_progress_counter & 1) == 1))
> -
> - /*
> - * The following corresponds to rcu_enter_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - EXECUTE_MAINLINE(stmt3,
> - tmp = dynticks_progress_counter;
> - assert(!old_gp_idle || grace_period_state != GP_DONE))
> - EXECUTE_MAINLINE(stmt4,
> - dynticks_progress_counter = tmp + 1;
> - assert((dynticks_progress_counter & 1) == 0))
> - i++;
> - od;
> - dyntick_nohz_done = 1;
> -}
> -
> -/*
> - * Validation code corresponding to rcu_irq_enter() and rcu_irq_exit().
> - */
> -
> -proctype dyntick_irq()
> -{
> - byte tmp;
> - byte i = 0;
> - byte j = 0;
> - bit old_gp_idle;
> - bit outermost;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_IRQ && j >= MAX_DYNTICK_LOOP_IRQ -> break;
> - :: i < MAX_DYNTICK_LOOP_IRQ ->
> -
> - /* Tell dyntick_nohz() that we are in interrupt handler. */
> -
> - atomic {
> - outermost = (in_dyntick_irq == 0);
> - in_dyntick_irq = 1;
> - }
> -
> - /* Validation code corresponding to rcu_irq_enter(). */
> -
> - if
> - :: rcu_update_flag > 0 ->
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp + 1;
> - :: else -> skip;
> - fi;
> - if
> - :: !in_interrupt && (dynticks_progress_counter & 1) == 0 ->
> - tmp = dynticks_progress_counter;
> - dynticks_progress_counter = tmp + 1;
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp + 1;
> - :: else -> skip;
> - fi;
> -
> - /*
> - * And a snippet from __irq_enter() corresponding to
> - * the add_preempt_count().
> - */
> -
> - tmp = in_interrupt;
> - in_interrupt = tmp + 1;
> -
> - /* Capture state to see if grace_period() is behaving. */
> -
> - atomic {
> - if
> - :: outermost ->
> - old_gp_idle = (grace_period_state == GP_IDLE);
> - :: else -> skip;
> - fi;
> - }
> -
> - /* Count the entry for termination and nesting. */
> -
> - i++;
> -
> - /* Note that we cannot exit a handler we have not yet entered! */
> -
> - :: j < i ->
> -
> - /* See if we can catch grace_period() misbehaving. */
> -
> - atomic {
> - if
> - :: j + 1 == i ->
> - assert(!old_gp_idle ||
> - grace_period_state != GP_DONE);
> - :: else -> skip;
> - fi;
> - }
> -
> - /*
> - * Validation code corresponding to the sub_preempt_count()
> - * in __irq_exit().
> - */
> -
> - tmp = in_interrupt;
> - in_interrupt = tmp - 1;
> -
> - /* Validation code corresponding to rcu_irq_exit(). */
> -
> - if
> - :: rcu_update_flag != 0 ->
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp - 1;
> - if
> - :: rcu_update_flag == 0 ->
> - tmp = dynticks_progress_counter;
> - dynticks_progress_counter = tmp + 1;
> - :: else -> skip;
> - fi;
> - :: else -> skip;
> - fi;
> -
> - /*
> - * Count the exit and let dyntick_nohz() know if we
> - * have completely exited a nested set of interrupts.
> - */
> -
> - atomic {
> - j++;
> - in_dyntick_irq = (i != j);
> - }
> - od;
> - dyntick_irq_done = 1;
> -}
> -
> -init {
> - atomic {
> - run dyntick_nohz();
> - run dyntick_irq();
> - run grace_period();
> - }
> -}
> diff --git a/CodeSamples/appendix/formal/dyntickRCU-irqnn-ssl.spin b/CodeSamples/appendix/formal/dyntickRCU-irqnn-ssl.spin
> deleted file mode 100644
> index 8157a9f..0000000
> --- a/CodeSamples/appendix/formal/dyntickRCU-irqnn-ssl.spin
> +++ /dev/null
> @@ -1,330 +0,0 @@
> -/*
> - * Tests a variation of RCU-dyntick interaction in the Linux 2.6.25-rc4
> - * kernel. Note that portions of this are derived from Linux kernel code,
> - * portions of which are licensed under a GPLv2-only license.
> - *
> - * This version omits NMI handlers, and disallows nested irq handlers.
> - *
> - * 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 (c) 2008 IBM Corporation.
> - */
> -
> -/*
> - * Parameters:
> - *
> - * MAX_DYNTICK_LOOP_NOHZ: The number of non-idle process level bursts
> - * of work.
> - * MAX_DYNTICK_LOOP_IRQ: The number of interrupts (possibly arbitrarily
> - * nested) to be received.
> - *
> - * Setting a given value for a given parameter covers all values up to
> - * and including the specified value. So, if MAX_DYNTICK_LOOP_IRQ is
> - * set to "2", then the validation will cover 0, 1, and 2 interrupts.
> - */
> -
> -#define MAX_DYNTICK_LOOP_NOHZ 3
> -#define MAX_DYNTICK_LOOP_IRQ 3
> -
> -/* Variables corresponding to the 2.6.25-rc4 per-CPU variables. */
> -
> -byte dynticks_progress_counter = 0;
> -byte rcu_update_flag = 0;
> -byte in_interrupt = 0;
> -
> -/* Set when IRQ code is running, to allow mainline code to lock itself out. */
> -
> -bit in_dyntick_irq = 0;
> -
> -/*
> - * The grace_period() process uses this to track its progress through
> - * each phase, thus allowing the other processes to make sure that
> - * grace_period() does not advance prematurely.
> - */
> -
> -#define GP_IDLE 0
> -#define GP_WAITING 1
> -#define GP_DONE 2
> -byte grace_period_state = GP_DONE;
> -
> -/*
> - * The following variables mark completion of the corresponding processes.
> - * This is used in grace_period() to check forward progress guarantees.
> - */
> -
> -bit dyntick_nohz_done = 0;
> -bit dyntick_irq_done = 0;
> -
> -/*
> - * Validation code for the slice of the preemptible-RCU code that
> - * interacts with the dynticks subsystem. This is set up to match
> - * the code in 2.6.25-rc4, namely dyntick_save_progress_counter(),
> - * rcu_try_flip_waitack_needed(), rcu_try_flip_waitmb_needed(),
> - * and portions of rcu_try_flip_waitack() and rcu_try_flip_waitmb().
> - *
> - * This code verifies forward progress: once all of the other processes
> - * have terminated, the grace_period() code must not block. In addition,
> - * this code maintains a progress indicator in the grace_period_state
> - * variable. It is an error for grace_period() to advance from GP_IDLE
> - * to GP_DONE unless all the other processes are simultaneously in nohz
> - * mode at some point during the transition.
> - */
> -
> -proctype grace_period()
> -{
> - byte curr;
> - byte snap;
> - bit shouldexit;
> -
> - /*
> - * A little code from rcu_try_flip_idle() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - printf("MAX_DYNTICK_LOOP_NOHZ = %d\n", MAX_DYNTICK_LOOP_NOHZ);
> - printf("MAX_DYNTICK_LOOP_IRQ = %d\n", MAX_DYNTICK_LOOP_IRQ);
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitack()
> - * and its call to rcu_try_flip_waitack_needed(). The shouldexit
> - * check ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done && dyntick_irq_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr - snap) >= 2 || (curr & 1) == 0 ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -
> - /*
> - * A little code from rcu_try_flip_waitzero() and its call
> - * to dyntick_save_progress_counter(), plus a bunch of
> - * validation code. The shouldexit variable is for the
> - * later liveness checks. As noted earlier, the
> - * grace_period_state variable allows the other processes
> - * to scream if we jump the gun here.
> - */
> -
> - grace_period_state = GP_IDLE;
> - atomic {
> - shouldexit = 0;
> - snap = dynticks_progress_counter;
> - grace_period_state = GP_WAITING;
> - }
> -
> - /*
> - * Each pass through the following loop corresponds to an
> - * invocation of the scheduling-clock interrupt handler,
> - * specifically a little code from rcu_try_flip_waitmb()
> - * and its call to rcu_try_flip_waitmb_needed(). The shouldexit
> - * check again ensures that we scream if we cannot immediately exit
> - * the loop after all other proceses have completed.
> - */
> -
> - do
> - :: 1 ->
> - atomic {
> - assert(!shouldexit);
> - shouldexit = dyntick_nohz_done && dyntick_irq_done;
> - curr = dynticks_progress_counter;
> - if
> - :: (curr != snap) || ((curr & 1) == 0) ->
> - break;
> - :: else -> skip;
> - fi;
> - }
> - od;
> - grace_period_state = GP_DONE;
> -}
> -
> -/*
> - * Macro that allows dyntick_irq() code to run atomically with respect
> - * to dyntick_nohz(), but still allows dyntick_irq() to be interleaved
> - * with other processes.
> - */
> -
> -#define EXECUTE_MAINLINE(label, stmt) \
> -label: skip; \
> - atomic { \
> - if \
> - :: in_dyntick_irq -> goto label; \
> - :: else -> stmt; \
> - fi; \
> - } \
> -
> -/*
> - * Validation code for the rcu_enter_nohz() and rcu_exit_nohz()
> - * functions. Each pass through this process's loop corresponds
> - * to exiting nohz mode, then re-entering it. The old_gp_idle
> - * variable is used to verify that grace_period() does not incorrectly
> - * advance while this process is not in nohz mode. This code also
> - * includes assertions corresponding to the WARN_ON() calls in
> - * rcu_exit_nohz() and rcu_enter_nohz().
> - */
> -
> -proctype dyntick_nohz()
> -{
> - byte tmp;
> - byte i = 0;
> - bit old_gp_idle;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_NOHZ -> break;
> - :: i < MAX_DYNTICK_LOOP_NOHZ ->
> -
> - /*
> - * The following corresponds to rcu_exit_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - EXECUTE_MAINLINE(stmt1, tmp = dynticks_progress_counter)
> - EXECUTE_MAINLINE(stmt2,
> - dynticks_progress_counter = tmp + 1;
> - old_gp_idle = (grace_period_state == GP_IDLE);
> - assert((dynticks_progress_counter & 1) == 1))
> -
> - /*
> - * The following corresponds to rcu_enter_nohz(), along
> - * with code to check for grace_period() jumping the gun.
> - */
> -
> - EXECUTE_MAINLINE(stmt3,
> - tmp = dynticks_progress_counter;
> - assert(!old_gp_idle || grace_period_state != GP_DONE))
> - EXECUTE_MAINLINE(stmt4,
> - dynticks_progress_counter = tmp + 1;
> - assert((dynticks_progress_counter & 1) == 0))
> - i++;
> - od;
> - dyntick_nohz_done = 1;
> -}
> -
> -/*
> - * Validation code corresponding to rcu_irq_enter() and rcu_irq_exit().
> - */
> -
> -proctype dyntick_irq()
> -{
> - byte tmp;
> - byte i = 0;
> - bit old_gp_idle;
> -
> - do
> - :: i >= MAX_DYNTICK_LOOP_IRQ -> break;
> - :: i < MAX_DYNTICK_LOOP_IRQ ->
> -
> - /* Tell dyntick_nohz() that we are in interrupt handler. */
> -
> - in_dyntick_irq = 1;
> -
> - /* Validation code corresponding to rcu_irq_enter(). */
> -
> - if
> - :: rcu_update_flag > 0 ->
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp + 1;
> - :: else -> skip;
> - fi;
> - if
> - :: !in_interrupt && (dynticks_progress_counter & 1) == 0 ->
> - tmp = dynticks_progress_counter;
> - dynticks_progress_counter = tmp + 1;
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp + 1;
> - :: else -> skip;
> - fi;
> -
> - /*
> - * And a snippet from __irq_enter() corresponding to
> - * the add_preempt_count().
> - */
> -
> - tmp = in_interrupt;
> - in_interrupt = tmp + 1;
> -
> - /* Capture state to see if grace_period() is behaving. */
> -
> - old_gp_idle = (grace_period_state == GP_IDLE);
> -
> - /* See if we can catch grace_period() misbehaving. */
> -
> - assert(!old_gp_idle || grace_period_state != GP_DONE);
> -
> - /*
> - * Validation code corresponding to the sub_preempt_count()
> - * in __irq_exit().
> - */
> -
> - tmp = in_interrupt;
> - in_interrupt = tmp - 1;
> -
> - /* Validation code corresponding to rcu_irq_exit(). */
> -
> - if
> - :: rcu_update_flag != 0 ->
> - tmp = rcu_update_flag;
> - rcu_update_flag = tmp - 1;
> - if
> - :: rcu_update_flag == 0 ->
> - tmp = dynticks_progress_counter;
> - dynticks_progress_counter = tmp + 1;
> - :: else -> skip;
> - fi;
> - :: else -> skip;
> - fi;
> -
> - /*
> - * Count the exit and let dyntick_nohz() know if we
> - * have completely exited a nested set of interrupts.
> - * Count the irq handler for termination. */
> - */
> -
> - atomic {
> - in_dyntick_irq = 0;
> - i++;
> - }
> - od;
> - dyntick_irq_done = 1;
> -}
> -
> -init {
> - atomic {
> - run dyntick_nohz();
> - run dyntick_irq();
> - run grace_period();
> - }
> -}
> diff --git a/CodeSamples/appendix/formal/dyntickRCUtarball.sh b/CodeSamples/appendix/formal/dyntickRCUtarball.sh
> deleted file mode 100644
> index ee6b104..0000000
> --- a/CodeSamples/appendix/formal/dyntickRCUtarball.sh
> +++ /dev/null
> @@ -1,18 +0,0 @@
> -rm -rf dyntickRCU
> -mkdir dyntickRCU
> -cp dyntickRCU-base-sl-busted.spin.trail.txt \
> - dyntickRCU-base-s.spin \
> - dyntickRCU-irq-ssl.spin \
> - RCUpreemptStates.fig \
> - dyntickRCU-irqnn-ssl.spin \
> - dyntickRCU-irq-nmi-ssl.spin \
> - runspin.sh \
> - dyntickRCU-base-sl.spin \
> - dyntickRCU-base-sl-busted.spin.trail \
> - dyntickRCU-base-sl-busted.spin \
> - RCUpreemptStates.png \
> - dyntickRCU-base.spin \
> - RCUpreemptStates.eps \
> - dyntickRCU.$1.html \
> - dyntickRCU
> -tar -czf dyntickRCU.$1.tgz dyntickRCU
> diff --git a/CodeSamples/appendix/formal/runspin.sh b/CodeSamples/appendix/formal/runspin.sh
> deleted file mode 100644
> index 0978f4c..0000000
> --- a/CodeSamples/appendix/formal/runspin.sh
> +++ /dev/null
> @@ -1,31 +0,0 @@
> -#!/bin/sh
> -#
> -# Run a test. Specify the test type as the first argument, for example:
> -#
> -# sh runtest.sh base
> -#
> -# will run the "dyntickRCU-base.spin model". Be sure to edit the
> -# MAX_DYNTICK_LOOP_* parameters as needed to fit your needs and
> -# memory size.
> -#
> -# 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 (c) 2008 Paul E. McKenney, IBM Corporation.
> -
> -type=${1-irq-nmi-ssl}
> -spin -a dyntickRCU-$type.spin
> -cc -DSAFETY -o pan pan.c
> -grep '^#.*DYN' dyntickRCU-$type.spin
> -./pan
> diff --git a/CodeSamples/analysis/promela/.gitignore b/CodeSamples/formal/promela/.gitignore
> similarity index 100%
> rename from CodeSamples/analysis/promela/.gitignore
> rename to CodeSamples/formal/promela/.gitignore
> diff --git a/CodeSamples/analysis/promela/atomicincrement.spin b/CodeSamples/formal/promela/atomicincrement.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/atomicincrement.spin
> rename to CodeSamples/formal/promela/atomicincrement.spin
> diff --git a/CodeSamples/appendix/formal/.gitignore b/CodeSamples/formal/promela/dyntick/.gitignore
> similarity index 100%
> rename from CodeSamples/appendix/formal/.gitignore
> rename to CodeSamples/formal/promela/dyntick/.gitignore
> diff --git a/CodeSamples/analysis/promela/dyntick/dyntickRCU-base-s.spin b/CodeSamples/formal/promela/dyntick/dyntickRCU-base-s.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/dyntickRCU-base-s.spin
> rename to CodeSamples/formal/promela/dyntick/dyntickRCU-base-s.spin
> diff --git a/CodeSamples/analysis/promela/dyntick/dyntickRCU-base-sl-busted.spin b/CodeSamples/formal/promela/dyntick/dyntickRCU-base-sl-busted.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/dyntickRCU-base-sl-busted.spin
> rename to CodeSamples/formal/promela/dyntick/dyntickRCU-base-sl-busted.spin
> diff --git a/CodeSamples/appendix/formal/dyntickRCU-base-sl-busted.spin.trail.txt b/CodeSamples/formal/promela/dyntick/dyntickRCU-base-sl-busted.spin.trail.txt
> similarity index 100%
> rename from CodeSamples/appendix/formal/dyntickRCU-base-sl-busted.spin.trail.txt
> rename to CodeSamples/formal/promela/dyntick/dyntickRCU-base-sl-busted.spin.trail.txt
> diff --git a/CodeSamples/analysis/promela/dyntick/dyntickRCU-base-sl.spin b/CodeSamples/formal/promela/dyntick/dyntickRCU-base-sl.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/dyntickRCU-base-sl.spin
> rename to CodeSamples/formal/promela/dyntick/dyntickRCU-base-sl.spin
> diff --git a/CodeSamples/analysis/promela/dyntick/dyntickRCU-base.spin b/CodeSamples/formal/promela/dyntick/dyntickRCU-base.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/dyntickRCU-base.spin
> rename to CodeSamples/formal/promela/dyntick/dyntickRCU-base.spin
> diff --git a/CodeSamples/analysis/promela/dyntick/dyntickRCU-irq-nmi-ssl.spin b/CodeSamples/formal/promela/dyntick/dyntickRCU-irq-nmi-ssl.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/dyntickRCU-irq-nmi-ssl.spin
> rename to CodeSamples/formal/promela/dyntick/dyntickRCU-irq-nmi-ssl.spin
> diff --git a/CodeSamples/analysis/promela/dyntick/dyntickRCU-irq-ssl.spin b/CodeSamples/formal/promela/dyntick/dyntickRCU-irq-ssl.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/dyntickRCU-irq-ssl.spin
> rename to CodeSamples/formal/promela/dyntick/dyntickRCU-irq-ssl.spin
> diff --git a/CodeSamples/analysis/promela/dyntick/dyntickRCU-irqnn-ssl.spin b/CodeSamples/formal/promela/dyntick/dyntickRCU-irqnn-ssl.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/dyntickRCU-irqnn-ssl.spin
> rename to CodeSamples/formal/promela/dyntick/dyntickRCU-irqnn-ssl.spin
> diff --git a/CodeSamples/analysis/promela/dyntick/dyntickRCUtarball.sh b/CodeSamples/formal/promela/dyntick/dyntickRCUtarball.sh
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/dyntickRCUtarball.sh
> rename to CodeSamples/formal/promela/dyntick/dyntickRCUtarball.sh
> diff --git a/CodeSamples/analysis/promela/dyntick/runspin.sh b/CodeSamples/formal/promela/dyntick/runspin.sh
> similarity index 100%
> rename from CodeSamples/analysis/promela/dyntick/runspin.sh
> rename to CodeSamples/formal/promela/dyntick/runspin.sh
> diff --git a/CodeSamples/analysis/promela/increment.spin b/CodeSamples/formal/promela/increment.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/increment.spin
> rename to CodeSamples/formal/promela/increment.spin
> diff --git a/CodeSamples/analysis/promela/lock.h b/CodeSamples/formal/promela/lock.h
> similarity index 100%
> rename from CodeSamples/analysis/promela/lock.h
> rename to CodeSamples/formal/promela/lock.h
> diff --git a/CodeSamples/analysis/promela/lock.spin b/CodeSamples/formal/promela/lock.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/lock.spin
> rename to CodeSamples/formal/promela/lock.spin
> diff --git a/CodeSamples/analysis/promela/qrcu.spin b/CodeSamples/formal/promela/qrcu.spin
> similarity index 100%
> rename from CodeSamples/analysis/promela/qrcu.spin
> rename to CodeSamples/formal/promela/qrcu.spin
> --
> 2.10.0
>
> --
> To unsubscribe from this list: send the line "unsubscribe perfbook" in
> the body of a message to majordomo@xxxxxxxxxxxxxxx
> More majordomo info at http://vger.kernel.org/majordomo-info.html
>
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
