[PATCH 00/17] Fixup `Formal Verification` chapter

[PATCH 00/17] Fixup `Formal Verification` chapter

[SeongJae Park]

This patchset contains fixups for files under formal/ directory.

SeongJae Park (17):
  formal: Rearrange promela sample code location
  formal/spinhint: Add missing NBSPs
  formal/spinhint: Fix typos
  formal/spinhint: Use \path{} for file name quotation
  formal/spinhint: Use \co{} for variable quotation consistently
  formal/spinhint: Reference figure
  formal/dyntickrcu: Add missing NBSPs
  formal/dyntickrcu: Append `()` to function name quotations
  formal/dyntickrcu: Fix typos
  formal/dyntickrcu: Fix wrong line number quotation
  formal/dyntickrcu: Fix wrong function name quotation
  formal/ppcmem: Fix typo for \co{}
  formal/ppcmem: Use \co{} for instruction quotation
  formal/ppcmem: Use P0 instead of thread 1
  formal/ppcmem: Substitute `paper` with `chapter`
  formal/ppcmem: Polish a sentence by removing unnecessary conjunction
  formal/dyntickrcu: Shorten too long code line length

 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
 formal/dyntickrcu.tex                              | 162 +++----
 formal/ppcmem.tex                                  |  12 +-
 formal/spinhint.tex                                |  18 +-
 29 files changed, 97 insertions(+), 2140 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%)

-- 
2.10.0

[PATCH 01/17] formal: Rearrange promela sample code location

[SeongJae Park]

`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@gmail.com>
---
 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

[PATCH 02/17] formal/spinhint: Add missing NBSPs

[SeongJae Park]

This commit adds missing non-breakable spaces.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/spinhint.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 10f6263..7787ed8 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -738,7 +738,7 @@ havelock array entry on line~26, starts the current locker on
 line~27, and advances to the next locker on line~28.
 Once all locker processes are spawned, the do-od loop
 moves to line~29, which checks the assertion.
-Lines 30 and 31 initialize the control variables,
+Lines~30 and~31 initialize the control variables,
 lines~32-40 atomically sum the havelock array entries,
 line~41 is the assertion, and line~42 exits the loop.

@@ -1009,7 +1009,7 @@ of the pair and sums them.
 The atomic block consists of a single do-od statement.
 This do-od statement (spanning lines~3-12) is unusual in that
 it contains two unconditional
-branches with guards on lines 4 and 8, which causes Promela to
+branches with guards on lines~4 and~8, which causes Promela to
 non-deterministically choose one of the two (but again, the full
 state-space search causes Promela to eventually make all possible
 choices in each applicable situation).
@@ -1107,7 +1107,7 @@ re-invoke \co{sum_unordered} if the fastpath is potentially
 usable.

 Lines~28-40 execute the slowpath code if need be, with
-lines 30 and 38 acquiring and releasing the update-side lock,
+lines~30 and~38 acquiring and releasing the update-side lock,
 lines~31-33 flipping the index, and lines~34-37 waiting for
 all pre-existing readers to complete.

@@ -1374,7 +1374,7 @@ Is QRCU really correct?
 We have a Promela-based mechanical proof and a by-hand proof that both
 say that it is.
 However, a recent paper by Alglave et al.~\cite{JadeAlglave2013-cav}
-says otherwise (see Section 5.1 of the paper at the bottom of page 12).
+says otherwise (see Section~5.1 of the paper at the bottom of page~12).
 Which is it?

 I do not know, as I never have been able to track down the code in which
-- 
2.10.0

[PATCH 03/17] formal/spinhint: Fix typos

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/spinhint.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 7787ed8..e91d458 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -422,7 +422,7 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
 	you.

 	Don't forget to capture the output, especially
-	if you are working on a remote machine,
+	if you are working on a remote machine.

 	If your model includes forward-progress checks, you will likely
 	need to enable ``weak fairness'' via the \co{-f} command-line
@@ -594,7 +594,7 @@ The following tricks can help you to abuse Promela safely:
 	Because each statement contributes to state, we can reduce
 	the number of useless states by enclosing it in an \co{atomic}
 	block as shown in
-	Figure~\ref{fig:analysis:Atomic Block for Complex Promela Assertion}
+	Figure~\ref{fig:analysis:Atomic Block for Complex Promela Assertion}.

 \item	Promela does not provide functions.
 	You must instead use C preprocessor macros.
-- 
2.10.0

[PATCH 04/17] formal/spinhint: Use \path{} for file name quotation

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/spinhint.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index e91d458..73ebe8e 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -409,7 +409,7 @@ Given a source file \path{qrcu.spin}, one can use the following commands:
 	This actually searches the state space.  The number of states
 	can reach into the tens of millions with very small state
 	machines, so you will need a machine with large memory.
-	For example, qrcu.spin with 3 readers and 2 updaters required
+	For example, \path{qrcu.spin} with 3 readers and 2 updaters required
 	2.7GB of memory.

 	If you aren't sure whether your machine has enough memory,
-- 
2.10.0

[PATCH 05/17] formal/spinhint: Use \co{} for variable quotation consistently

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/spinhint.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 73ebe8e..878fa61 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -921,7 +921,7 @@ allows an assertion to determine when all the readers are finished
 (since a QRCU update cannot be permitted to complete until all
 pre-existing readers have completed their QRCU read-side critical
 sections).
-The readerprogress array elements have values as follows,
+The \co{readerprogress} array elements have values as follows,
 indicating the state of the corresponding reader:

 \begin{enumerate}
-- 
2.10.0

[PATCH 06/17] formal/spinhint: Reference figure

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/spinhint.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/spinhint.tex b/formal/spinhint.tex
index 878fa61..ec53a7f 100644
--- a/formal/spinhint.tex
+++ b/formal/spinhint.tex
@@ -1096,7 +1096,7 @@ to 0 (so that line~14 will fetch the second counter).

 With the \co{sum_unordered} macro in place, we can now proceed
 to the update-side process shown in
-Figure.
+Figure~\ref{fig:analysis:QRCU Updater Process}.
 The update-side process repeats indefinitely, with the corresponding
 do-od loop ranging over lines~7-57.
 Each pass through the loop first snapshots the global {\tt readerprogress}
-- 
2.10.0

[PATCH 07/17] formal/dyntickrcu: Add missing NBSPs

[SeongJae Park]

This commit adds missed non-breakable spaces for line numbers.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 64 +++++++++++++++++++++++++--------------------------
 1 file changed, 32 insertions(+), 32 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 4d27d6c..3aa79f9 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -209,7 +209,7 @@ shown below:
 \end{verbatim}
 }

-Line~3 fetches the current CPU's number, while lines~5 and 6
+Line~3 fetches the current CPU's number, while lines~5 and~6
 increment the \co{rcu_update_flag} nesting counter if it
 is already non-zero.
 Lines~7-9 check to see whether we are the outermost level of
@@ -282,13 +282,13 @@ Line~3 fetches the current CPU's number, as before.
 Line~5 checks to see if the \co{rcu_update_flag} is
 non-zero, returning immediately (via falling off the end of the
 function) if not.
-Otherwise, lines~6 through 12 come into play.
+Otherwise, lines~6 through~12 come into play.
 Line~6 decrements \co{rcu_update_flag}, returning
 if the result is not zero.
 Line~8 verifies that we are indeed leaving the outermost
 level of nested interrupts, line~9 executes a memory barrier,
 line~10 increments \co{dynticks_progress_counter},
-and lines~11 and 12 verify that this variable is now even.
+and lines~11 and~12 verify that this variable is now even.
 As with \co{rcu_enter_nohz()}, the memory barrier ensures that
 any other CPU that sees the increment of
 \co{dynticks_progress_counter}
@@ -362,15 +362,15 @@ The \co{rcu_try_flip_waitack_state()} state invokes
 \end{verbatim}
 }

-Lines~7 and 8 pick up current and snapshot versions of
+Lines~7 and~8 pick up current and snapshot versions of
 \co{dynticks_progress_counter}, respectively.
 The memory barrier on line~9 ensures that the counter checks
 in the later \co{rcu_try_flip_waitzero_state} follow
 the fetches of these counters.
-Lines~10 and 11 return zero (meaning no communication with the
+Lines~10 and~11 return zero (meaning no communication with the
 specified CPU is required) if that CPU has remained in dynticks-idle
 state since the time that the snapshot was taken.
-Similarly, lines~12 and 13 return zero if that CPU was initially
+Similarly, lines~12 and~13 return zero if that CPU was initially
 in dynticks-idle state or if it has completely passed through a
 dynticks-idle state.
 In both these cases, there is no way that that CPU could have retained
@@ -402,7 +402,7 @@ invokes \co{rcu_try_flip_waitmb_needed()}, shown below:
 }

 This is quite similar to \co{rcu_try_flip_waitack_needed},
-the difference being in lines~12 and 13, because any transition
+the difference being in lines~12 and~13, because any transition
 either to or from dynticks-idle state executes the memory barrier
 needed by the \co{rcu_try_flip_waitmb_state()} state.

@@ -463,17 +463,17 @@ a loop as follows:
 \end{verbatim}
 }

-Lines~6 and 20 define a loop.
+Lines~6 and~20 define a loop.
 Line~7 exits the loop once the loop counter \co{i}
 has exceeded the limit \co{MAX_DYNTICK_LOOP_NOHZ}.
 Line~8 tells the loop construct to execute lines~9-19
 for each pass through the loop.
-Because the conditionals on lines~7 and 8 are exclusive of
+Because the conditionals on lines~7 and~8 are exclusive of
 each other, the normal Promela random selection of true conditions
 is disabled.
-Lines~9 and 11 model \co{rcu_exit_nohz()}'s non-atomic
+Lines~9 and~11 model \co{rcu_exit_nohz()}'s non-atomic
 increment of \co{dynticks_progress_counter}, while
-line 12 models the \co{WARN_ON()}.
+line~12 models the \co{WARN_ON()}.
 The \co{atomic} construct simply reduces the Promela state space,
 given that the \co{WARN_ON()} is not strictly speaking part
 of the algorithm.
@@ -687,7 +687,7 @@ progresses through the grace-period phases, as shown below:
 \end{verbatim}
 }

-Lines~6, 10, 25, 26, 29, and 44 update this variable (combining
+Lines~6, 10, 25, 26, 29, and~44 update this variable (combining
 atomically with algorithmic operations where feasible) to
 allow the \co{dyntick_nohz()} process to verify the basic
 RCU safety property.
@@ -698,7 +698,7 @@ over which RCU readers could plausibly persist.

 \QuickQuiz{}
 	Given there are a pair of back-to-back changes to
-	\co{gp_state} on lines~25 and 26,
+	\co{gp_state} on lines~25 and~26,
 	how can we be sure that line~25's changes won't be lost?
 \QuickQuizAnswer{
 	Recall that Promela and spin trace out
@@ -747,7 +747,7 @@ this verification as shown below:
 Line~13 sets a new \co{old_gp_idle} flag if the
 value of the \co{gp_state} variable is
 \co{GP_IDLE} at the beginning of task execution,
-and the assertion at lines~18 and 19 fire if the \co{gp_state}
+and the assertion at lines~18 and~19 fire if the \co{gp_state}
 variable has advanced to \co{GP_DONE} during task execution,
 which would be illegal given that a single RCU read-side critical
 section could span the entire intervening time period.
@@ -877,7 +877,7 @@ any more state changes to force us out of the loop, so going through twice
 in this state means an infinite loop, which in turn means no end to the
 grace period.

-Lines~32, 39, and 40 operate in a similar manner for the
+Lines~32, 39, and~40 operate in a similar manner for the
 second (memory-barrier) loop.

 However, running this
@@ -1216,7 +1216,7 @@ to model an interrupt handler:
 }

 The loop from lines~7-48 models up to \co{MAX_DYNTICK_LOOP_IRQ}
-interrupts, with lines~8 and 9 forming the loop condition and line~45
+interrupts, with lines~8 and~9 forming the loop condition and line~45
 incrementing the control variable.
 Line~10 tells \co{dyntick_nohz()} that an interrupt handler
 is running, and line~45 tells \co{dyntick_nohz()} that this
@@ -1225,7 +1225,7 @@ Line~49 is used for liveness verification, just like the corresponding
 line of \co{dyntick_nohz()}.

 \QuickQuiz{}
-	Why are lines~45 and 46 (the \co{in_dyntick_irq = 0;}
+	Why are lines~45 and~46 (the \co{in_dyntick_irq = 0;}
 	and the \co{i++;}) executed atomically?
 \QuickQuizAnswer{
 	These lines of code pertain to controlling the
@@ -1236,10 +1236,10 @@ line of \co{dyntick_nohz()}.
 } \QuickQuizEnd

 Lines~11-25 model \co{rcu_irq_enter()}, and
-lines~26 and 27 model the relevant snippet of \co{__irq_enter()}.
-Lines~28 and 29 verifies safety in much the same manner as do the
+lines~26 and~27 model the relevant snippet of \co{__irq_enter()}.
+Lines~28 and~29 verifies safety in much the same manner as do the
 corresponding lines of \co{dynticks_nohz()}.
-Lines~30 and 31 model the relevant snippet of \co{__irq_exit()},
+Lines~30 and~31 model the relevant snippet of \co{__irq_exit()},
 and finally lines~32-43 model \co{rcu_irq_exit()}.

 \QuickQuiz{}
@@ -1309,9 +1309,9 @@ The \co{grace_period} process then becomes as follows:
 The implementation of \co{grace_period()} is very similar
 to the earlier one.
 The only changes are the addition of line~10 to add the new
-interrupt-count parameter, changes to lines~19 and 39 to
+interrupt-count parameter, changes to lines~19 and~39 to
 add the new \co{dyntick_irq_done} variable to the liveness
-checks, and of course the optimizations on lines~22 and 42.
+checks, and of course the optimizations on lines~22 and~42.

 This model (\path{dyntickRCU-irqnn-ssl.spin})
 results in a correct verification with roughly half a million
@@ -1409,7 +1409,7 @@ counts exits.
 The \co{outermost} variable on line~7 helps determine
 when the \co{gp_state} variable needs to be sampled
 for the safety checks.
-The loop-exit check on lines~10 and 11 is updated to require that the
+The loop-exit check on lines~10 and~11 is updated to require that the
 specified number of interrupt handlers are exited as well as entered,
 and the increment of \co{i} is moved to line~41, which is
 the end of the interrupt-entry model.
@@ -1719,7 +1719,7 @@ Finally, \co{grace_period()} requires only a few changes:
 We have added the \co{printf()} for the new
 \co{MAX_DYNTICK_LOOP_NMI} parameter on line~11 and
 added \co{dyntick_nmi_done} to the \co{shouldexit}
-assignments on lines~22 and 44.
+assignments on lines~22 and~44.

 The model (\path{dyntickRCU-irq-nmi-ssl.spin})
 results in a correct verification with several hundred million
@@ -1985,7 +1985,7 @@ These two functions are invoked from process context.
 Line~6 ensures that any prior memory accesses (which might
 include accesses from RCU read-side critical sections) are seen
 by other CPUs before those marking entry to dynticks-idle mode.
-Lines~7 and 12 disable and reenable irqs.
+Lines~7 and~12 disable and reenable irqs.
 Line~8 acquires a pointer to the current CPU's \co{rcu_dynticks}
 structure, and
 line~9 increments the current CPU's \co{dynticks} counter, which
@@ -2040,13 +2040,13 @@ which inform RCU of NMI entry and exit, respectively, from dynticks-idle
 mode.
 However, if the NMI arrives during an irq handler, then RCU will already
 be on the lookout for RCU read-side critical sections from this CPU,
-so lines~6 and 7 of \co{rcu_nmi_enter} and lines~18 and 19
+so lines~6 and~7 of \co{rcu_nmi_enter} and lines~18 and~19
 of \co{rcu_nmi_exit} silently return if \co{dynticks} is odd.
 Otherwise, the two functions increment \co{dynticks_nmi}, with
 \co{rcu_nmi_enter()} leaving it with an odd value and \co{rcu_nmi_exit()}
 leaving it with an even value.
 Both functions execute memory barriers between this increment
-and possible RCU read-side critical sections on lines~11 and 21,
+and possible RCU read-side critical sections on lines~11 and~21,
 respectively.

 \subsubsection{Interrupts From Dynticks-Idle Mode}
@@ -2150,18 +2150,18 @@ Figure~\ref{fig:formal:Saving Dyntick Progress Counters}
 shows \co{dyntick_save_progress_counter()}, which takes a snapshot
 of the specified CPU's \co{dynticks} and \co{dynticks_nmi}
 counters.
-Lines~8 and 9 snapshot these two variables to locals, line~10
+Lines~8 and~9 snapshot these two variables to locals, line~10
 executes a memory barrier to pair with the memory barriers in
 the functions in
 Figures~\ref{fig:formal:Entering and Exiting Dynticks-Idle Mode},
 \ref{fig:formal:NMIs From Dynticks-Idle Mode}, and
 \ref{fig:formal:Interrupts From Dynticks-Idle Mode}.
-Lines~11 and 12 record the snapshots for later calls to
+Lines~11 and~12 record the snapshots for later calls to
 \co{rcu_implicit_dynticks_qs},
 and lines~13 and~14 check to see if the CPU is in dynticks-idle mode with
 neither irqs nor NMIs in progress (in other words, both snapshots
 have even values), hence in an extended quiescent state.
-If so, lines~15 and 16 count this event, and line~17 returns
+If so, lines~15 and~16 count this event, and line~17 returns
 true if the CPU was in a quiescent state.

 \begin{figure}[tbp]
@@ -2200,8 +2200,8 @@ Figure~\ref{fig:formal:Checking Dyntick Progress Counters}
 shows \co{dyntick_save_progress_counter}, which is called to check
 whether a CPU has entered dyntick-idle mode subsequent to a call
 to \co{dynticks_save_progress_counter()}.
-Lines~9 and 11 take new snapshots of the corresponding CPU's
-\co{dynticks} and \co{dynticks_nmi} variables, while lines~10 and 12
+Lines~9 and~11 take new snapshots of the corresponding CPU's
+\co{dynticks} and \co{dynticks_nmi} variables, while lines~10 and~12
 retrieve the snapshots saved earlier by
 \co{dynticks_save_progress_counter()}.
 Line~13 then
-- 
2.10.0

[PATCH 08/17] formal/dyntickrcu: Append `()` to function name quotations

[SeongJae Park]

Few sentences do not append `()` to function name quotations while
others do.  This commit let them append `()` to function name quotations
consistently.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 3aa79f9..5ede587 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -147,7 +147,7 @@ of any prior RCU read-side critical sections.

 Similarly, when a CPU that is in dynticks-idle mode prepares to
 start executing a newly runnable task, it invokes
-\co{rcu_exit_nohz}:
+\co{rcu_exit_nohz()}:

 { \scriptsize
 \begin{verbatim}
@@ -169,7 +169,7 @@ then that other CPU will also see the incremented value of
 Finally, \co{rcu_exit_nohz()} checks that the result of the
 increment is an odd value.

-The \co{rcu_enter_nohz()} and \co{rcu_exit_nohz}
+The \co{rcu_enter_nohz()} and \co{rcu_exit_nohz()}
 functions handle the case where a CPU enters and exits dynticks-idle
 mode due to task execution, but does not handle interrupts, which are
 covered in the following section.
@@ -187,7 +187,7 @@ and is decremented upon exit (in \co{rcu_irq_exit()}).
 In addition, the pre-existing \co{in_interrupt()} primitive is
 used to distinguish between an outermost or a nested interrupt/NMI.

-Interrupt entry is handled by the \co{rcu_irq_enter}
+Interrupt entry is handled by the \co{rcu_irq_enter()}
 shown below:

 { \scriptsize
@@ -327,7 +327,7 @@ the preceding state takes a snapshot of each CPU's
 snapshot in another per-CPU variable,
 \co{rcu_dyntick_snapshot}.
 This is accomplished by invoking
-\co{dyntick_save_progress_counter}, shown below:
+\co{dyntick_save_progress_counter()}, shown below:

 { \scriptsize
 \begin{verbatim}
@@ -365,7 +365,7 @@ The \co{rcu_try_flip_waitack_state()} state invokes
 Lines~7 and~8 pick up current and snapshot versions of
 \co{dynticks_progress_counter}, respectively.
 The memory barrier on line~9 ensures that the counter checks
-in the later \co{rcu_try_flip_waitzero_state} follow
+in the later \co{rcu_try_flip_waitzero_state()} follow
 the fetches of these counters.
 Lines~10 and~11 return zero (meaning no communication with the
 specified CPU is required) if that CPU has remained in dynticks-idle
@@ -378,7 +378,7 @@ the old value of the grace-period counter.
 If neither of these conditions hold, line~14 returns one, meaning
 that the CPU needs to explicitly respond.

-For its part, the \co{rcu_try_flip_waitmb_state} state
+For its part, the \co{rcu_try_flip_waitmb_state()} state
 invokes \co{rcu_try_flip_waitmb_needed()}, shown below:

 { \scriptsize
@@ -401,7 +401,7 @@ invokes \co{rcu_try_flip_waitmb_needed()}, shown below:
 \end{verbatim}
 }

-This is quite similar to \co{rcu_try_flip_waitack_needed},
+This is quite similar to \co{rcu_try_flip_waitack_needed()},
 the difference being in lines~12 and~13, because any transition
 either to or from dynticks-idle state executes the memory barrier
 needed by the \co{rcu_try_flip_waitmb_state()} state.
@@ -966,7 +966,7 @@ The corrected C code is as follows:
 Lines~10-13 can now be combined and simplified,
 resulting in the following.
 A similar simplification can be applied to
-\co{rcu_try_flip_waitmb_needed}.
+\co{rcu_try_flip_waitmb_needed()}.

 { \scriptsize
 \begin{verbatim}
@@ -1250,7 +1250,7 @@ and finally lines~32-43 model \co{rcu_irq_exit()}.
 	which are handled in the following section.
 } \QuickQuizEnd

-The \co{grace_period} process then becomes as follows:
+The \co{grace_period()} process then becomes as follows:

 { \scriptsize
 \begin{verbatim}
@@ -2040,8 +2040,8 @@ which inform RCU of NMI entry and exit, respectively, from dynticks-idle
 mode.
 However, if the NMI arrives during an irq handler, then RCU will already
 be on the lookout for RCU read-side critical sections from this CPU,
-so lines~6 and~7 of \co{rcu_nmi_enter} and lines~18 and~19
-of \co{rcu_nmi_exit} silently return if \co{dynticks} is odd.
+so lines~6 and~7 of \co{rcu_nmi_enter()} and lines~18 and~19
+of \co{rcu_nmi_exit()} silently return if \co{dynticks} is odd.
 Otherwise, the two functions increment \co{dynticks_nmi}, with
 \co{rcu_nmi_enter()} leaving it with an odd value and \co{rcu_nmi_exit()}
 leaving it with an even value.
@@ -2102,7 +2102,7 @@ the increment of \co{dynticks} is seen before any
 RCU read-side critical sections that the subsequent irq handler
 might execute.

-Line~18 of \co{rcu_irq_exit} decrements \co{dynticks_nesting}, and
+Line~18 of \co{rcu_irq_exit()} decrements \co{dynticks_nesting}, and
 if the result is non-zero, line~19 silently returns.
 Otherwise, line~20 executes a memory barrier to ensure that the
 increment of \co{dynticks} on line~21 is seen after any RCU
@@ -2157,7 +2157,7 @@ Figures~\ref{fig:formal:Entering and Exiting Dynticks-Idle Mode},
 \ref{fig:formal:NMIs From Dynticks-Idle Mode}, and
 \ref{fig:formal:Interrupts From Dynticks-Idle Mode}.
 Lines~11 and~12 record the snapshots for later calls to
-\co{rcu_implicit_dynticks_qs},
+\co{rcu_implicit_dynticks_qs()},
 and lines~13 and~14 check to see if the CPU is in dynticks-idle mode with
 neither irqs nor NMIs in progress (in other words, both snapshots
 have even values), hence in an extended quiescent state.
-- 
2.10.0

[PATCH 09/17] formal/dyntickrcu: Fix typos

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 5ede587..1d3e155 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -213,7 +213,7 @@ Line~3 fetches the current CPU's number, while lines~5 and~6
 increment the \co{rcu_update_flag} nesting counter if it
 is already non-zero.
 Lines~7-9 check to see whether we are the outermost level of
-interrupt, and, if so, whether \co{dynticks_progress_counter}
+interrupt, and, if so, \co{dynticks_progress_counter}
 needs to be incremented.
 If so, line~10 increments \co{dynticks_progress_counter},
 line~11 executes a memory barrier, and line~12 increments
@@ -887,9 +887,9 @@ is even.
 Upon failure, \co{spin} writes out a
 ``trail'' file
 (\path{dyntickRCU-base-sl-busted.spin.trail})
-file, which records the sequence of states that lead to the failure.
+, which records the sequence of states that lead to the failure.
 Use the {\tt spin -t -p -g -l dyntickRCU-base-sl-busted.spin}
-command to cause \co{spin} to retrace this sequence of state,
+command to cause \co{spin} to retrace this sequence of states,
 printing the statements executed and the values of variables
 (\path{dyntickRCU-base-sl-busted.spin.trail.txt}).
 Note that the line numbers do not match the listing above due to
-- 
2.10.0

[PATCH 10/17] formal/dyntickrcu: Fix wrong line number quotation

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 1d3e155..a36901e 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -1098,7 +1098,7 @@ The first step is to convert \co{dyntick_nohz()} to
 }

 It is important to note that when a group of statements is passed
-to \co{EXECUTE_MAINLINE()}, as in lines~11-14, all
+to \co{EXECUTE_MAINLINE()}, as in lines~12-15, all
 statements in that group execute atomically.

 \QuickQuiz{}
@@ -1216,7 +1216,7 @@ to model an interrupt handler:
 }

 The loop from lines~7-48 models up to \co{MAX_DYNTICK_LOOP_IRQ}
-interrupts, with lines~8 and~9 forming the loop condition and line~45
+interrupts, with lines~8 and~9 forming the loop condition and line~46
 incrementing the control variable.
 Line~10 tells \co{dyntick_nohz()} that an interrupt handler
 is running, and line~45 tells \co{dyntick_nohz()} that this
@@ -2046,7 +2046,7 @@ Otherwise, the two functions increment \co{dynticks_nmi}, with
 \co{rcu_nmi_enter()} leaving it with an odd value and \co{rcu_nmi_exit()}
 leaving it with an even value.
 Both functions execute memory barriers between this increment
-and possible RCU read-side critical sections on lines~11 and~21,
+and possible RCU read-side critical sections on lines~10 and~20,
 respectively.

 \subsubsection{Interrupts From Dynticks-Idle Mode}
-- 
2.10.0

[PATCH 11/17] formal/dyntickrcu: Fix wrong function name quotation

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index a36901e..e31996d 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -2197,7 +2197,7 @@ true if the CPU was in a quiescent state.
 \end{figure}

 Figure~\ref{fig:formal:Checking Dyntick Progress Counters}
-shows \co{dyntick_save_progress_counter}, which is called to check
+shows \co{rcu_implicit_dynticks_qs()}, which is called to check
 whether a CPU has entered dyntick-idle mode subsequent to a call
 to \co{dynticks_save_progress_counter()}.
 Lines~9 and~11 take new snapshots of the corresponding CPU's
-- 
2.10.0

[PATCH 12/17] formal/ppcmem: Fix typo for \co{}

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 9e0392a..c18cb9a 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -165,7 +165,7 @@ exclusive'' in ARM parlance and ``load reserve'' in Power parlance)
 and store-conditional (``store register exclusive'' in ARM parlance),
 respectively. When these are used together, they form an atomic
 instruction sequence, roughly similar to the compare-and-swap sequences
-exemplified by the x86 co{lock;cmpxchg} instruction. Moving to a higher
+exemplified by the x86 \co{lock;cmpxchg} instruction. Moving to a higher
 level of abstraction, the sequence from lines~10-15 is equivalent to
 the Linux kernel's \co{atomic_add_return(&z, 0)}. Finally, line~16 is
 roughly equivalent to the C statement \co{r3=y}.
-- 
2.10.0

[PATCH 13/17] formal/ppcmem: Use \co{} for instruction quotation

[SeongJae Park]

Sentences about PPCMEM litmus test uses \co{} for machine instruction
quotations but missed it for `bne`.  This commit uses \co{} for `bne`
quotation.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index c18cb9a..5dfddd8 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -182,7 +182,7 @@ and line~11 is equivalent to the C statement \co{r3=x}.
 	The implementation of powerpc version of \co{atomic_add_return()}
 	loops when the \co{stwcx} instruction fails, which it communicates
 	by setting non-zero status in the condition-code register,
-	which in turn is tested by the bne instruction. Because actually
+	which in turn is tested by the \co{bne} instruction. Because actually
 	modeling the loop would result in state-space explosion, we
 	instead branch to the Fail: label, terminating the model with
 	the initial value of 2 in thread~1's \co{r3} register, which
-- 
2.10.0

[PATCH 14/17] formal/ppcmem: Use P0 instead of thread 1

[SeongJae Park]

There is a sentence that uses term `thread 1` to point `P0` in sample
PPCMEM litmus test.  Because all other sentences uses term `P0` for the
thread, it would be natural to use the term consistently.  This commit
fixes the sentence to use the consistent term.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 5dfddd8..e33ba2f 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -185,7 +185,7 @@ and line~11 is equivalent to the C statement \co{r3=x}.
 	which in turn is tested by the \co{bne} instruction. Because actually
 	modeling the loop would result in state-space explosion, we
 	instead branch to the Fail: label, terminating the model with
-	the initial value of 2 in thread~1's \co{r3} register, which
+	the initial value of 2 in P0's \co{r3} register, which
 	will not trigger the exists assertion.

 	There is some debate about whether this trick is universally
-- 
2.10.0

[PATCH 15/17] formal/ppcmem: Substitute `paper` with `chapter`

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index e33ba2f..743a891 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -391,10 +391,10 @@ It is worth repeating that formal methods and tools are no substitute for
 testing. The fact is that producing large reliable concurrent software
 artifacts, the Linux kernel for example, is quite difficult. Developers
 must therefore be prepared to apply every tool at their disposal towards
-this goal. The tools presented in this paper are able to locate bugs that
+this goal. The tools presented in this chapter are able to locate bugs that
 are quite difficult to produce (let alone track down) via testing. On the
 other hand, testing can be applied to far larger bodies of software than
-the tools presented in this paper are ever likely to handle. As always,
+the tools presented in this chapter are ever likely to handle. As always,
 use the right tools for the job!

 Of course, it is always best to avoid the need to work at this level
-- 
2.10.0

[PATCH 16/17] formal/ppcmem: Polish a sentence by removing unnecessary conjunction

[SeongJae Park]

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/ppcmem.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 743a891..7dc9675 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -233,7 +233,7 @@ The next section describes how to run this litmus test.
 \subsection{Running a Litmus Test}
 \label{sec:formal:Running a Litmus Test}

-Although litmus tests may be run interactively via
+Litmus tests may be run interactively via
 \url{http://www.cl.cam.ac.uk/~pes20/ppcmem/}, which can help build an
 understanding of the memory model.
 However, this approach requires that the user manually carry out the
-- 
2.10.0

[PATCH 17/17] formal/dyntickrcu: Shorten too long code line length

[SeongJae Park]

Lines 19 and 39 of dyntickRCU-irqnn-ssl.spin is too long.  This commit
shortens the lines.

Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 68 ++++++++++++++++++++++++++-------------------------
 1 file changed, 35 insertions(+), 33 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index e31996d..922e556 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -1272,46 +1272,48 @@ The \co{grace_period()} process then becomes as follows:
  16   :: 1 ->
  17     atomic {
  18       assert(!shouldexit);
- 19       shouldexit = dyntick_nohz_done && dyntick_irq_done;
- 20       curr = dynticks_progress_counter;
- 21       if
- 22       :: (curr - snap) >= 2 || (curr & 1) == 0 ->
- 23         break;
- 24       :: else -> skip;
- 25       fi;
- 26     }
- 27   od;
- 28   gp_state = GP_DONE;
- 29   gp_state = GP_IDLE;
- 30   atomic {
- 31     shouldexit = 0;
- 32     snap = dynticks_progress_counter;
- 33     gp_state = GP_WAITING;
- 34   }
- 35   do
- 36   :: 1 ->
- 37     atomic {
- 38       assert(!shouldexit);
- 39       shouldexit = dyntick_nohz_done && dyntick_irq_done;
- 40       curr = dynticks_progress_counter;
- 41       if
- 42       :: (curr != snap) || ((curr & 1) == 0) ->
- 43         break;
- 44       :: else -> skip;
- 45       fi;
- 46     }
- 47   od;
- 48   gp_state = GP_DONE;
- 49 }
+ 19       shouldexit = dyntick_nohz_done &&
+ 20                        dyntick_irq_done;
+ 21       curr = dynticks_progress_counter;
+ 22       if
+ 23       :: (curr - snap) >= 2 || (curr & 1) == 0 ->
+ 24         break;
+ 25       :: else -> skip;
+ 26       fi;
+ 27     }
+ 28   od;
+ 29   gp_state = GP_DONE;
+ 30   gp_state = GP_IDLE;
+ 31   atomic {
+ 32     shouldexit = 0;
+ 33     snap = dynticks_progress_counter;
+ 34     gp_state = GP_WAITING;
+ 35   }
+ 36   do
+ 37   :: 1 ->
+ 38     atomic {
+ 39       assert(!shouldexit);
+ 40       shouldexit = dyntick_nohz_done &&
+ 41                        dyntick_irq_done;
+ 42       curr = dynticks_progress_counter;
+ 43       if
+ 44       :: (curr != snap) || ((curr & 1) == 0) ->
+ 45         break;
+ 46       :: else -> skip;
+ 47       fi;
+ 48     }
+ 49   od;
+ 50   gp_state = GP_DONE;
+ 51 }
 \end{verbatim}
 }

 The implementation of \co{grace_period()} is very similar
 to the earlier one.
 The only changes are the addition of line~10 to add the new
-interrupt-count parameter, changes to lines~19 and~39 to
+interrupt-count parameter, changes to lines~19-20 and~40-41 to
 add the new \co{dyntick_irq_done} variable to the liveness
-checks, and of course the optimizations on lines~22 and~42.
+checks, and of course the optimizations on lines~23 and~44.

 This model (\path{dyntickRCU-irqnn-ssl.spin})
 results in a correct verification with roughly half a million
-- 
2.10.0

Re: [PATCH 09/17] formal/dyntickrcu: Fix typos

[Akira Yokosawa]

Hi,

I have a few comments regarding this patch.

On 2016/09/21 11:44:40 +0900, SeongJae Park wrote:
> Signed-off-by: SeongJae Park <sj38.park@gmail.com>
> ---
>  formal/dyntickrcu.tex | 6 +++---
>  1 file changed, 3 insertions(+), 3 deletions(-)
> 
> diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
> index 5ede587..1d3e155 100644
> --- a/formal/dyntickrcu.tex
> +++ b/formal/dyntickrcu.tex
> @@ -213,7 +213,7 @@ Line~3 fetches the current CPU's number, while lines~5 and~6
>  increment the \co{rcu_update_flag} nesting counter if it
>  is already non-zero.
>  Lines~7-9 check to see whether we are the outermost level of
> -interrupt, and, if so, whether \co{dynticks_progress_counter}
> +interrupt, and, if so, \co{dynticks_progress_counter}
>  needs to be incremented.
>  If so, line~10 increments \co{dynticks_progress_counter},
>  line~11 executes a memory barrier, and line~12 increments

I think this change is unnecessary.  The original sentence makes
sense for me.

> @@ -887,9 +887,9 @@ is even.
>  Upon failure, \co{spin} writes out a
>  ``trail'' file
>  (\path{dyntickRCU-base-sl-busted.spin.trail})
> -file, which records the sequence of states that lead to the failure.
> +, which records the sequence of states that lead to the failure.
>  Use the {\tt spin -t -p -g -l dyntickRCU-base-sl-busted.spin}
> -command to cause \co{spin} to retrace this sequence of state,
> +command to cause \co{spin} to retrace this sequence of states,
>  printing the statements executed and the values of variables
>  (\path{dyntickRCU-base-sl-busted.spin.trail.txt}).
>  Note that the line numbers do not match the listing above due to
> 

Well, if you put the "," at the beginning of the line, there would be
an extra space (or even a line break) between the ")" and the ",".
A better hunk would be as the following;

> @@ -886,10 +886,10 @@ results in failure, as line~23 is checking that the wrong 
>  is even.
>  Upon failure, \co{spin} writes out a
>  ``trail'' file
> -(\path{dyntickRCU-base-sl-busted.spin.trail})
> -file, which records the sequence of states that lead to the failure.
> +(\path{dyntickRCU-base-sl-busted.spin.trail}),
> +which records the sequence of states that lead to the failure.
>  Use the {\tt spin -t -p -g -l dyntickRCU-base-sl-busted.spin}
> -command to cause \co{spin} to retrace this sequence of state,
> +command to cause \co{spin} to retrace this sequence of states,
>  printing the statements executed and the values of variables
>  (\path{dyntickRCU-base-sl-busted.spin.trail.txt}).
>  Note that the line numbers do not match the listing above due to

                                                  Thanks, Akira

Re: [PATCH 17/17] formal/dyntickrcu: Shorten too long code line length

[Akira Yokosawa]

Hi,

On 2016/09/21 11:44:48 +0900, SeongJae Park wrote:
> Lines 19 and 39 of dyntickRCU-irqnn-ssl.spin is too long.  This commit
> shortens the lines.
> 
> Signed-off-by: SeongJae Park <sj38.park@gmail.com>
> ---
>  formal/dyntickrcu.tex | 68 ++++++++++++++++++++++++++-------------------------
>  1 file changed, 35 insertions(+), 33 deletions(-)
> 
> diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
> index e31996d..922e556 100644
> --- a/formal/dyntickrcu.tex
> +++ b/formal/dyntickrcu.tex
> @@ -1272,46 +1272,48 @@ The \co{grace_period()} process then becomes as follows:
>   16   :: 1 ->
>   17     atomic {
>   18       assert(!shouldexit);
> - 19       shouldexit = dyntick_nohz_done && dyntick_irq_done;
> - 20       curr = dynticks_progress_counter;
> - 21       if
> - 22       :: (curr - snap) >= 2 || (curr & 1) == 0 ->
> - 23         break;
> - 24       :: else -> skip;
> - 25       fi;
> - 26     }
> - 27   od;
> - 28   gp_state = GP_DONE;
> - 29   gp_state = GP_IDLE;
> - 30   atomic {
> - 31     shouldexit = 0;
> - 32     snap = dynticks_progress_counter;
> - 33     gp_state = GP_WAITING;
> - 34   }
> - 35   do
> - 36   :: 1 ->
> - 37     atomic {
> - 38       assert(!shouldexit);
> - 39       shouldexit = dyntick_nohz_done && dyntick_irq_done;
> - 40       curr = dynticks_progress_counter;
> - 41       if
> - 42       :: (curr != snap) || ((curr & 1) == 0) ->
> - 43         break;
> - 44       :: else -> skip;
> - 45       fi;
> - 46     }
> - 47   od;
> - 48   gp_state = GP_DONE;
> - 49 }
> + 19       shouldexit = dyntick_nohz_done &&
> + 20                        dyntick_irq_done;
> + 21       curr = dynticks_progress_counter;
> + 22       if
> + 23       :: (curr - snap) >= 2 || (curr & 1) == 0 ->
> + 24         break;
> + 25       :: else -> skip;
> + 26       fi;
> + 27     }
> + 28   od;
> + 29   gp_state = GP_DONE;
> + 30   gp_state = GP_IDLE;
> + 31   atomic {
> + 32     shouldexit = 0;
> + 33     snap = dynticks_progress_counter;
> + 34     gp_state = GP_WAITING;
> + 35   }
> + 36   do
> + 37   :: 1 ->
> + 38     atomic {
> + 39       assert(!shouldexit);
> + 40       shouldexit = dyntick_nohz_done &&
> + 41                        dyntick_irq_done;
> + 42       curr = dynticks_progress_counter;
> + 43       if
> + 44       :: (curr != snap) || ((curr & 1) == 0) ->
> + 45         break;
> + 46       :: else -> skip;
> + 47       fi;
> + 48     }
> + 49   od;
> + 50   gp_state = GP_DONE;
> + 51 }
>  \end{verbatim}
>  }
>  
>  The implementation of \co{grace_period()} is very similar
>  to the earlier one.
>  The only changes are the addition of line~10 to add the new
> -interrupt-count parameter, changes to lines~19 and~39 to
> +interrupt-count parameter, changes to lines~19-20 and~40-41 to
>  add the new \co{dyntick_irq_done} variable to the liveness
> -checks, and of course the optimizations on lines~22 and~42.
> +checks, and of course the optimizations on lines~23 and~44.
>  
>  This model (\path{dyntickRCU-irqnn-ssl.spin})
>  results in a correct verification with roughly half a million
> 

Instead of modifying the code, you can specify a proper font size
for this instance, e.g.,

> @@ -1252,7 +1252,7 @@ and finally lines~32-43 model \co{rcu_irq_exit()}.
>  
>  The \co{grace_period} process then becomes as follows:
>  
> -{ \scriptsize
> +{ \fontsize{6.7pt}{8pt}\selectfont
>  \begin{verbatim}
>    1 proctype grace_period()
>    2 {

I once did a similar tweak in commit bc0fd9d40035 ("after: Tweak font
size of Figure A.2").

                                           Thanks, Akira

Re: [PATCH 09/17] formal/dyntickrcu: Fix typos

[SeongJae Park]

[-- Attachment #1: Type: text/plain, Size: 2983 bytes --]

Hi,


Thanks for all your comments and agree!  Will send next patches as reply to
this mail soon.


Thanks,
SeongJae Park

On Wed, Sep 21, 2016 at 7:57 PM, Akira Yokosawa <akiyks@gmail.com> wrote:

> Hi,
>
> I have a few comments regarding this patch.
>
> On 2016/09/21 11:44:40 +0900, SeongJae Park wrote:
> > Signed-off-by: SeongJae Park <sj38.park@gmail.com>
> > ---
> >  formal/dyntickrcu.tex | 6 +++---
> >  1 file changed, 3 insertions(+), 3 deletions(-)
> >
> > diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
> > index 5ede587..1d3e155 100644
> > --- a/formal/dyntickrcu.tex
> > +++ b/formal/dyntickrcu.tex
> > @@ -213,7 +213,7 @@ Line~3 fetches the current CPU's number, while
> lines~5 and~6
> >  increment the \co{rcu_update_flag} nesting counter if it
> >  is already non-zero.
> >  Lines~7-9 check to see whether we are the outermost level of
> > -interrupt, and, if so, whether \co{dynticks_progress_counter}
> > +interrupt, and, if so, \co{dynticks_progress_counter}
> >  needs to be incremented.
> >  If so, line~10 increments \co{dynticks_progress_counter},
> >  line~11 executes a memory barrier, and line~12 increments
>
> I think this change is unnecessary.  The original sentence makes
> sense for me.
>
> > @@ -887,9 +887,9 @@ is even.
> >  Upon failure, \co{spin} writes out a
> >  ``trail'' file
> >  (\path{dyntickRCU-base-sl-busted.spin.trail})
> > -file, which records the sequence of states that lead to the failure.
> > +, which records the sequence of states that lead to the failure.
> >  Use the {\tt spin -t -p -g -l dyntickRCU-base-sl-busted.spin}
> > -command to cause \co{spin} to retrace this sequence of state,
> > +command to cause \co{spin} to retrace this sequence of states,
> >  printing the statements executed and the values of variables
> >  (\path{dyntickRCU-base-sl-busted.spin.trail.txt}).
> >  Note that the line numbers do not match the listing above due to
> >
>
> Well, if you put the "," at the beginning of the line, there would be
> an extra space (or even a line break) between the ")" and the ",".
> A better hunk would be as the following;
>
> > @@ -886,10 +886,10 @@ results in failure, as line~23 is checking that
> the wrong
> >  is even.
> >  Upon failure, \co{spin} writes out a
> >  ``trail'' file
> > -(\path{dyntickRCU-base-sl-busted.spin.trail})
> > -file, which records the sequence of states that lead to the failure.
> > +(\path{dyntickRCU-base-sl-busted.spin.trail}),
> > +which records the sequence of states that lead to the failure.
> >  Use the {\tt spin -t -p -g -l dyntickRCU-base-sl-busted.spin}
> > -command to cause \co{spin} to retrace this sequence of state,
> > +command to cause \co{spin} to retrace this sequence of states,
> >  printing the statements executed and the values of variables
> >  (\path{dyntickRCU-base-sl-busted.spin.trail.txt}).
> >  Note that the line numbers do not match the listing above due to
>
>                                                   Thanks, Akira
>

[-- Attachment #2: Type: text/html, Size: 4618 bytes --]

[PATCH v2] formal/dyntickrcu: Fix typos

[SeongJae Park]

Suggested-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index 5ede587..bbbdb18 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -886,10 +886,10 @@ results in failure, as line~23 is checking that the wrong variable
 is even.
 Upon failure, \co{spin} writes out a
 ``trail'' file
-(\path{dyntickRCU-base-sl-busted.spin.trail})
-file, which records the sequence of states that lead to the failure.
+(\path{dyntickRCU-base-sl-busted.spin.trail}),
+which records the sequence of states that lead to the failure.
 Use the {\tt spin -t -p -g -l dyntickRCU-base-sl-busted.spin}
-command to cause \co{spin} to retrace this sequence of state,
+command to cause \co{spin} to retrace this sequence of states,
 printing the statements executed and the values of variables
 (\path{dyntickRCU-base-sl-busted.spin.trail.txt}).
 Note that the line numbers do not match the listing above due to
-- 
2.10.0

Re: [PATCH 17/17] formal/dyntickrcu: Shorten too long code line length

[SeongJae Park]

Hi,

On Wed, Sep 21, 2016 at 8:30 PM, Akira Yokosawa <akiyks@gmail.com> wrote:
>
> Hi,
>
> On 2016/09/21 11:44:48 +0900, SeongJae Park wrote:
> > Lines 19 and 39 of dyntickRCU-irqnn-ssl.spin is too long.  This commit
> > shortens the lines.
> >
> > Signed-off-by: SeongJae Park <sj38.park@gmail.com>
> > ---
> >  formal/dyntickrcu.tex | 68 ++++++++++++++++++++++++++-------------------------
> >  1 file changed, 35 insertions(+), 33 deletions(-)
> >
> > diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
> > index e31996d..922e556 100644
> > --- a/formal/dyntickrcu.tex
> > +++ b/formal/dyntickrcu.tex
> > @@ -1272,46 +1272,48 @@ The \co{grace_period()} process then becomes as follows:
> >   16   :: 1 ->
> >   17     atomic {
> >   18       assert(!shouldexit);
> > - 19       shouldexit = dyntick_nohz_done && dyntick_irq_done;
> > - 20       curr = dynticks_progress_counter;
> > - 21       if
> > - 22       :: (curr - snap) >= 2 || (curr & 1) == 0 ->
> > - 23         break;
> > - 24       :: else -> skip;
> > - 25       fi;
> > - 26     }
> > - 27   od;
> > - 28   gp_state = GP_DONE;
> > - 29   gp_state = GP_IDLE;
> > - 30   atomic {
> > - 31     shouldexit = 0;
> > - 32     snap = dynticks_progress_counter;
> > - 33     gp_state = GP_WAITING;
> > - 34   }
> > - 35   do
> > - 36   :: 1 ->
> > - 37     atomic {
> > - 38       assert(!shouldexit);
> > - 39       shouldexit = dyntick_nohz_done && dyntick_irq_done;
> > - 40       curr = dynticks_progress_counter;
> > - 41       if
> > - 42       :: (curr != snap) || ((curr & 1) == 0) ->
> > - 43         break;
> > - 44       :: else -> skip;
> > - 45       fi;
> > - 46     }
> > - 47   od;
> > - 48   gp_state = GP_DONE;
> > - 49 }
> > + 19       shouldexit = dyntick_nohz_done &&
> > + 20                        dyntick_irq_done;
> > + 21       curr = dynticks_progress_counter;
> > + 22       if
> > + 23       :: (curr - snap) >= 2 || (curr & 1) == 0 ->
> > + 24         break;
> > + 25       :: else -> skip;
> > + 26       fi;
> > + 27     }
> > + 28   od;
> > + 29   gp_state = GP_DONE;
> > + 30   gp_state = GP_IDLE;
> > + 31   atomic {
> > + 32     shouldexit = 0;
> > + 33     snap = dynticks_progress_counter;
> > + 34     gp_state = GP_WAITING;
> > + 35   }
> > + 36   do
> > + 37   :: 1 ->
> > + 38     atomic {
> > + 39       assert(!shouldexit);
> > + 40       shouldexit = dyntick_nohz_done &&
> > + 41                        dyntick_irq_done;
> > + 42       curr = dynticks_progress_counter;
> > + 43       if
> > + 44       :: (curr != snap) || ((curr & 1) == 0) ->
> > + 45         break;
> > + 46       :: else -> skip;
> > + 47       fi;
> > + 48     }
> > + 49   od;
> > + 50   gp_state = GP_DONE;
> > + 51 }
> >  \end{verbatim}
> >  }
> >
> >  The implementation of \co{grace_period()} is very similar
> >  to the earlier one.
> >  The only changes are the addition of line~10 to add the new
> > -interrupt-count parameter, changes to lines~19 and~39 to
> > +interrupt-count parameter, changes to lines~19-20 and~40-41 to
> >  add the new \co{dyntick_irq_done} variable to the liveness
> > -checks, and of course the optimizations on lines~22 and~42.
> > +checks, and of course the optimizations on lines~23 and~44.
> >
> >  This model (\path{dyntickRCU-irqnn-ssl.spin})
> >  results in a correct verification with roughly half a million
> >
>
> Instead of modifying the code, you can specify a proper font size
> for this instance, e.g.,
>
> > @@ -1252,7 +1252,7 @@ and finally lines~32-43 model \co{rcu_irq_exit()}.
> >
> >  The \co{grace_period} process then becomes as follows:
> >
> > -{ \scriptsize
> > +{ \fontsize{6.7pt}{8pt}\selectfont
> >  \begin{verbatim}
> >    1 proctype grace_period()
> >    2 {
>
> I once did a similar tweak in commit bc0fd9d40035 ("after: Tweak font
> size of Figure A.2").


Yes, it would be much better.  Thanks for your comment!
I will send the patch again in reply to this mail.


Thanks,
SeongJae Park

>
>
>                                            Thanks, Akira

[PATCH v2] formal/dyntickrcu: Adjust font size of sample code

[SeongJae Park]

Code for `dyntickRCU-irqnn-ssl.spin` has a too long line.  Because the
line breaks the layout, this commit reduces font size of the sample code
for better layout.

Suggested-by: Akira Yokosawa <akiyks@gmail.com>
Signed-off-by: SeongJae Park <sj38.park@gmail.com>
---
 formal/dyntickrcu.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
index d0b2c6e..a63d324 100644
--- a/formal/dyntickrcu.tex
+++ b/formal/dyntickrcu.tex
@@ -1252,7 +1252,7 @@ and finally lines~32-43 model \co{rcu_irq_exit()}.

 The \co{grace_period()} process then becomes as follows:

-{ \scriptsize
+{ \fontsize{6.7pt}{8pt}\selectfont
 \begin{verbatim}
   1 proctype grace_period()
   2 {
-- 
2.10.0

Re: [PATCH v2] formal/dyntickrcu: Adjust font size of sample code

[Paul E. McKenney]

On Wed, Sep 21, 2016 at 10:05:48PM +0900, SeongJae Park wrote:
> Code for `dyntickRCU-irqnn-ssl.spin` has a too long line.  Because the
> line breaks the layout, this commit reduces font size of the sample code
> for better layout.
> 
> Suggested-by: Akira Yokosawa <akiyks@gmail.com>
> Signed-off-by: SeongJae Park <sj38.park@gmail.com>

Thank you both!

SeongJae, could you please resend the series?  Sorry to be so picky,
but you might be underestimating my ability to apply the wrong patch
at the wrong time.  ;-)

							Thanx, Paul

> ---
>  formal/dyntickrcu.tex | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
> index d0b2c6e..a63d324 100644
> --- a/formal/dyntickrcu.tex
> +++ b/formal/dyntickrcu.tex
> @@ -1252,7 +1252,7 @@ and finally lines~32-43 model \co{rcu_irq_exit()}.
> 
>  The \co{grace_period()} process then becomes as follows:
> 
> -{ \scriptsize
> +{ \fontsize{6.7pt}{8pt}\selectfont
>  \begin{verbatim}
>    1 proctype grace_period()
>    2 {
> -- 
> 2.10.0
> 

Re: [PATCH v2] formal/dyntickrcu: Adjust font size of sample code

[SeongJae Park]

On Wed, Sep 28, 2016 at 1:14 AM, Paul E. McKenney
<paulmck@linux.vnet.ibm.com> wrote:
> On Wed, Sep 21, 2016 at 10:05:48PM +0900, SeongJae Park wrote:
>> Code for `dyntickRCU-irqnn-ssl.spin` has a too long line.  Because the
>> line breaks the layout, this commit reduces font size of the sample code
>> for better layout.
>>
>> Suggested-by: Akira Yokosawa <akiyks@gmail.com>
>> Signed-off-by: SeongJae Park <sj38.park@gmail.com>
>
> Thank you both!
>
> SeongJae, could you please resend the series?  Sorry to be so picky,
> but you might be underestimating my ability to apply the wrong patch
> at the wrong time.  ;-)

Of course I will :)  I will send the series again in reply to this mail.


Thanks, SeongJae Park

>
>                                                         Thanx, Paul
>
>> ---
>>  formal/dyntickrcu.tex | 2 +-
>>  1 file changed, 1 insertion(+), 1 deletion(-)
>>
>> diff --git a/formal/dyntickrcu.tex b/formal/dyntickrcu.tex
>> index d0b2c6e..a63d324 100644
>> --- a/formal/dyntickrcu.tex
>> +++ b/formal/dyntickrcu.tex
>> @@ -1252,7 +1252,7 @@ and finally lines~32-43 model \co{rcu_irq_exit()}.
>>
>>  The \co{grace_period()} process then becomes as follows:
>>
>> -{ \scriptsize
>> +{ \fontsize{6.7pt}{8pt}\selectfont
>>  \begin{verbatim}
>>    1 proctype grace_period()
>>    2 {
>> --
>> 2.10.0
>>
>