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