--- a/Journal/Paper.thy	Wed Sep 09 11:24:19 2015 +0100
+++ b/Journal/Paper.thy	Sun Oct 04 23:02:57 2015 +0100
@@ -170,10 +170,15 @@
   computing the priority to be restored solely from this log is  not explained in
   \cite{Liu00} but left as an ``{\it excercise}'' to the reader.
   Of course, a correct version of PIP does not need to maintain
-  this (potentially expensive) data structure at all. 
+  this (potentially expensive) data structure at all. Surprisingly
+  also the widely read and frequently updated textbook \cite{Silberschatz13} gives
+  the wrong specification. For example on Page 254 the
+  authors write: ``{\it Upon releasing the lock, the [low-priority] thread
+  will revert to its original priority.}'' The same error is also repeated
+  later in this textbook.
 
   
-  While \cite{Laplante11,Liu00,book,Sha90} are the only formal publications we have 
+  While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have 
   found that specify the incorrect behaviour, it seems also many
   informal descriptions of PIP overlook the possibility that another
   high-priority might wait for a low-priority process to finish.

--- a/Journal/document/root.bib	Wed Sep 09 11:24:19 2015 +0100
+++ b/Journal/document/root.bib	Sun Oct 04 23:02:57 2015 +0100
@@ -1,4 +1,11 @@
 
+@Book{Silberschatz13,
+  author =    {A.~Silberschatz and P.~B.~Galvin and G.~Gagne},
+  title =        {Operating System Concepts},
+  publisher =    {John Wiley \& Sons},
+  year =         {2013},
+  edition =   {9th}
+}
 
 @Book{liu00,
   author =    {J.~W.~S.~Liu},

--- a/Test.thy	Wed Sep 09 11:24:19 2015 +0100
+++ b/Test.thy	Sun Oct 04 23:02:57 2015 +0100
@@ -6,6 +6,8 @@
 type_synonym priority = nat  -- {* Type for priorities. *}
 type_synonym cs = nat -- {* Type for critical sections (or resources). *}
 
+-- {* Schedulling Events *}
+
 datatype event = 
   Create thread priority 
 | Exit thread 
@@ -36,6 +38,7 @@
 | "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" 
 | "last_set th (_#s) = last_set th s"
 
+
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
   where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
 
@@ -48,6 +51,7 @@
 definition
   "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)"
 
+--{* Nodes in Resource Graph *}
 datatype node = 
   Th "thread" 
 | Cs "cs" 
@@ -83,9 +87,9 @@
 
 lemma [simp]: 
   "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)"
-apply(auto)
-apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
-by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)
+apply(rule iffI)
+apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)+
+done
 
 abbreviation
   "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)"

Binary file journal.pdf has changed