%
\begin{isabellebody}%
\def\isabellecontext{PrioGDef}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
In this section, the formal model of Priority Inheritance is presented. First, the identifiers of {\em threads},
  {\em priority} and {\em critical resources } (abbreviated as \isa{cs}) are all represented as natural numbers,
  i.e. standard Isabelle/HOL type \isa{nat}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
\ thread\ {\isaliteral{3D}{\isacharequal}}\ nat\ %
\isamarkupcmt{Type for thread identifiers.%
}
\isanewline
\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
\ priority\ {\isaliteral{3D}{\isacharequal}}\ nat\ \ %
\isamarkupcmt{Type for priorities.%
}
\isanewline
\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
\ cs\ {\isaliteral{3D}{\isacharequal}}\ nat\ %
\isamarkupcmt{Type for critical sections (or critical resources).%
}
%
\begin{isamarkuptext}%
Priority Inheritance protocol is modeled as an event driven system, where every event represents an 
  system call. Event format is given by the following type definition:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
\ event\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
\ \ Create\ thread\ priority\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{Thread \isa{thread} is created with priority \isa{priority}.%
}
\isanewline
\ \ Exit\ thread\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{Thread \isa{thread} finishing its execution.%
}
\isanewline
\ \ P\ thread\ cs\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{Thread \isa{thread} requesting critical resource \isa{cs}.%
}
\isanewline
\ \ V\ thread\ cs\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{Thread \isa{thread}  releasing critical resource \isa{cs}.%
}
\isanewline
\ \ Set\ thread\ priority\ %
\isamarkupcmt{Thread \isa{thread} resets its priority to \isa{priority}.%
}
%
\begin{isamarkuptext}%
Resource Allocation Graph (RAG for short) is used extensively in the analysis of Priority Inheritance. 
  The following type \isa{node} is used to model nodes in RAG.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\isamarkupfalse%
\ node\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
\ \ \ Th\ {\isaliteral{22}{\isachardoublequoteopen}}thread{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{Node for thread.%
}
\isanewline
\ \ \ Cs\ {\isaliteral{22}{\isachardoublequoteopen}}cs{\isaliteral{22}{\isachardoublequoteclose}}\ %
\isamarkupcmt{Node for critical resource.%
}
%
\begin{isamarkuptext}%
The protocol is analyzed using Paulson's inductive protocol verification method, where 
  the state of the system is modelled as the list of events happened so far with the latest 
  event at the head. Therefore, the state of the system is represented by the following
  type \isa{state}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
\ state\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}event\ list{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The following \isa{threads} is used to calculate the set of live threads (\isa{threads\ s})
  in state \isa{s}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ threads\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ \isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{At the start of the system, the set of threads is empty.%
}
\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}Create\ thread\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}thread{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ threads\ s{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{New thread is added to the \isa{threads}.%
}
\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}Exit\ thread\ {\isaliteral{23}{\isacharhash}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}threads\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{7B}{\isacharbraceleft}}thread{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{Finished thread is removed.%
}
\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ threads\ s{\isaliteral{22}{\isachardoublequoteclose}}\ %
\isamarkupcmt{other kind of events does not affect the value of \isa{threads}.%
}
%
\begin{isamarkuptext}%
Functions such as \isa{threads}, which extract information out of system states, are called
  {\em observing functions}. A series of observing functions will be defined in the sequel in order to 
  model the protocol. 
  Observing function \isa{original{\isaliteral{5F}{\isacharunderscore}}priority} calculates 
  the {\em original priority} of thread \isa{th} in state \isa{s}, expressed as
  : \isa{original{\isaliteral{5F}{\isacharunderscore}}priority\ th\ s}. The {\em original priority} is the priority 
  assigned to a thread when it is created or when it is reset by system call \isa{Set\ thread\ priority}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ original{\isaliteral{5F}{\isacharunderscore}}priority\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ priority{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
\isamarkupcmt{\isa{{\isadigit{0}}} is assigned to threads which have never been created.%
}
\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}Create\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ thread{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ thread\ then\ prio\ else\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}Set\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ thread{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ thread\ then\ prio\ else\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\isa{birthtime\ th\ s} is the time when thread \isa{th} is created, observed from state \isa{s}.
  The time in the system is measured by the number of events happened so far since the very beginning.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ birthtime\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Create\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{3D}{\isacharequal}}\ thread{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ then\ length\ s\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Set\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{3D}{\isacharequal}}\ thread{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ then\ length\ s\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ birthtime\ thread\ s{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of 
  a thread is the combination of its {\em original priority} and {\em birth time}. The intention is
  to discriminate threads with the same priority by giving threads with the earlier assigned priority
  higher precedence in scheduling. This explains the following definition:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ preced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}preced\ thread\ s\ {\isaliteral{3D}{\isacharequal}}\ Prc\ {\isaliteral{28}{\isacharparenleft}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
A number of important notions are defined here:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
\ \isanewline
\ \ holding\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isanewline
\ \ \ \ \ \ \ waiting\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \ depend\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}node\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ node{\isaliteral{29}{\isacharparenright}}\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \ dependents\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The definition of the following several functions, it is supposed that
  the waiting queue of every critical resource is given by a waiting queue 
  function \isa{wq}, which servers as arguments of these functions.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{defs}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{overloaded}{\isaliteral{29}{\isacharparenright}}\ \isanewline
\ \ %
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
  We define that the thread which is at the head of waiting queue of resource \isa{cs}
  is holding the resource. This definition is slightly different from tradition where
  all threads in the waiting queue are considered as waiting for the resource.
  This notion is reflected in the definition of \isa{holding\ wq\ th\ cs} as follows:
  \end{minipage}%
}
\isanewline
\ \ cs{\isaliteral{5F}{\isacharunderscore}}holding{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}holding\ wq\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ %
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
  In accordance with the definition of \isa{holding\ wq\ th\ cs}, 
  a thread \isa{th} is considered waiting for \isa{cs} if 
  it is in the {\em waiting queue} of critical resource \isa{cs}, but not at the head.
  This is reflected in the definition of \isa{waiting\ wq\ th\ cs} as follows:
  \end{minipage}%
}
\isanewline
\ \ cs{\isaliteral{5F}{\isacharunderscore}}waiting{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}waiting\ wq\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ %
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
  \isa{depend\ wq} represents the Resource Allocation Graph of the system under the waiting 
  queue function \isa{wq}.
  \end{minipage}%
}
\isanewline
\ \ cs{\isaliteral{5F}{\isacharunderscore}}depend{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}depend\ {\isaliteral{28}{\isacharparenleft}}wq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Th\ t{\isaliteral{2C}{\isacharcomma}}\ Cs\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ t\ c{\isaliteral{2E}{\isachardot}}\ waiting\ wq\ t\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Cs\ c{\isaliteral{2C}{\isacharcomma}}\ Th\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ c\ t{\isaliteral{2E}{\isachardot}}\ holding\ wq\ t\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ %
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
  \isa{dependents\ wq\ th} represents the set of threads which are depending on
  thread \isa{th} in Resource Allocation Graph \isa{depend\ wq}:
  \end{minipage}%
}
\isanewline
\ \ cs{\isaliteral{5F}{\isacharunderscore}}dependents{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dependents\ {\isaliteral{28}{\isacharparenleft}}wq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ th\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ wq{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The data structure used by the operating system for scheduling is referred to as 
  {\em schedule state}. It is represented as a record consisting of 
  a function assigning waiting queue to resources and a function assigning precedence to 
  threads:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{record}\isamarkupfalse%
\ schedule{\isaliteral{5F}{\isacharunderscore}}state\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
\ \ \ \ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{22}{\isachardoublequoteclose}}\ %
\isamarkupcmt{The function assigning waiting queue.%
}
\isanewline
\ \ \ \ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\ %
\isamarkupcmt{The function assigning precedence.%
}
%
\begin{isamarkuptext}%
\isa{cpreced\ s\ th} gives the {\em current precedence} of thread \isa{th} under
  state \isa{s}. The definition of \isa{cpreced} reflects the basic idea of 
  Priority Inheritance that the {\em current precedence} of a thread is the precedence 
  inherited from the maximum of all its dependents, i.e. the threads which are waiting 
  directly or indirectly waiting for some resources from it. If no such thread exits, 
  \isa{th}'s {\em current precedence} equals its original precedence, i.e. 
  \isa{preced\ th\ s}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ cpreced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cpreced\ s\ wq\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ th{\isaliteral{2E}{\isachardot}}\ Max\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ th{\isaliteral{2E}{\isachardot}}\ preced\ th\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ dependents\ wq\ th{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The following function \isa{schs} is used to calculate the schedule state \isa{schs\ s}.
  It is the key function to model Priority Inheritance:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ schs\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ schedule{\isaliteral{5F}{\isacharunderscore}}state{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\isanewline
\ \ \ {\isaliteral{22}{\isachardoublequoteopen}}schs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3D}{\isacharequal}}\ cpreced\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ %
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
  \begin{enumerate}
  \item \isa{ps} is the schedule state of last moment.
  \item \isa{pwq} is the waiting queue function of last moment.
  \item \isa{pcp} is the precedence function of last moment. 
  \item \isa{nwq} is the new waiting queue function. It is calculated using a \isa{case} statement:
  \begin{enumerate}
      \item If the happening event is \isa{P\ thread\ cs}, \isa{thread} is added to 
            the end of \isa{cs}'s waiting queue.
      \item If the happening event is \isa{V\ thread\ cs} and \isa{s} is a legal state,
            \isa{th{\isaliteral{27}{\isacharprime}}} must equal to \isa{thread}, 
            because \isa{thread} is the one currently holding \isa{cs}. 
            The case \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} may never be executed in a legal state.
            the \isa{{\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ qs{\isaliteral{29}{\isacharparenright}}} is used to choose arbitrarily one 
            thread in waiting to take over the released resource \isa{cs}. In our representation,
            this amounts to rearrange elements in waiting queue, so that one of them is put at the head.
      \item For other happening event, the schedule state just does not change.
  \end{enumerate}
  \item \isa{ncp} is new precedence function, it is calculated from the newly updated waiting queue 
        function. The dependency of precedence function on waiting queue function is the reason to 
        put them in the same record so that they can evolve together.
  \end{enumerate}
  \end{minipage}%
}
\isanewline
\ \ \ {\isaliteral{22}{\isachardoublequoteopen}}schs\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}let\ ps\ {\isaliteral{3D}{\isacharequal}}\ schs\ s\ in\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ pwq\ {\isaliteral{3D}{\isacharequal}}\ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ ps\ in\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ pcp\ {\isaliteral{3D}{\isacharequal}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ ps\ in\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ nwq\ {\isaliteral{3D}{\isacharequal}}\ case\ e\ of\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ P\ thread\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ \ pwq{\isaliteral{28}{\isacharparenleft}}cs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}pwq\ cs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}thread{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ V\ thread\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ let\ nq\ {\isaliteral{3D}{\isacharequal}}\ case\ {\isaliteral{28}{\isacharparenleft}}pwq\ cs{\isaliteral{29}{\isacharparenright}}\ of\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}th{\isaliteral{27}{\isacharprime}}{\isaliteral{23}{\isacharhash}}qs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ qs{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ pwq{\isaliteral{28}{\isacharparenleft}}cs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}nq{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ pwq\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ let\ ncp\ {\isaliteral{3D}{\isacharequal}}\ cpreced\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ nwq\ in\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3D}{\isacharequal}}\ nwq{\isaliteral{2C}{\isacharcomma}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3D}{\isacharequal}}\ ncp{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\isa{wq} is a shorthand for \isa{waiting{\isaliteral{5F}{\isacharunderscore}}queue}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ wq\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}wq\ s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{28}{\isacharparenleft}}schs\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\isa{cp} is a shorthand for \isa{cur{\isaliteral{5F}{\isacharunderscore}}preced}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ cp\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cp\ s\ {\isaliteral{3D}{\isacharequal}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{28}{\isacharparenleft}}schs\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
Functions \isa{holding}, \isa{waiting}, \isa{depend} and \isa{dependents} still have the 
  same meaning, but redefined so that they no longer depend on the fictitious {\em waiting queue function}
  \isa{wq}, but on system state \isa{s}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{defs}\isamarkupfalse%
\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{overloaded}{\isaliteral{29}{\isacharparenright}}\ \isanewline
\ \ s{\isaliteral{5F}{\isacharunderscore}}holding{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}holding\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ s{\isaliteral{5F}{\isacharunderscore}}waiting{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}waiting\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ s{\isaliteral{5F}{\isacharunderscore}}depend{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}depend\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Th\ t{\isaliteral{2C}{\isacharcomma}}\ Cs\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ t\ c{\isaliteral{2E}{\isachardot}}\ waiting\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}\ t\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Cs\ c{\isaliteral{2C}{\isacharcomma}}\ Th\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ c\ t{\isaliteral{2E}{\isachardot}}\ holding\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}\ t\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ s{\isaliteral{5F}{\isacharunderscore}}dependents{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dependents\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ th\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The following function \isa{readys} calculates the set of ready threads. A thread is {\em ready} 
  for running if it is a live thread and it is not waiting for any critical resource.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ readys\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\isanewline
\ \ {\isaliteral{22}{\isachardoublequoteopen}}readys\ s\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
\ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}thread\ {\isaliteral{2E}{\isachardot}}\ thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ threads\ s\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ waiting\ s\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The following function \isa{runing} calculates the set of running thread, which is the ready 
  thread with the highest precedence.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ runing\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}runing\ s\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th\ {\isaliteral{2E}{\isachardot}}\ th\ {\isaliteral{5C3C696E3E}{\isasymin}}\ readys\ s\ {\isaliteral{5C3C616E643E}{\isasymand}}\ cp\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ Max\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}cp\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{28}{\isacharparenleft}}readys\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The following function \isa{holdents\ s\ th} returns the set of resources held by thread 
  \isa{th} in state \isa{s}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ holdents\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}holdents\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}cs\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ depend\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\isa{cntCS\ s\ th} returns the number of resources held by thread \isa{th} in
  state \isa{s}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ cntCS\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntCS\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ card\ {\isaliteral{28}{\isacharparenleft}}holdents\ s\ th{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The fact that event \isa{e} is eligible to happen next in state \isa{s} 
  is expressed as \isa{step\ s\ e}. The predicate \isa{step} is inductively defined as 
  follows:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{inductive}\isamarkupfalse%
\ step\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ event\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\isanewline
\ \ %
\isamarkupcmt{A thread can be created if it is not a live thread:%
}
\isanewline
\ \ thread{\isaliteral{5F}{\isacharunderscore}}create{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ threads\ s{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Create\ thread\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ %
\isamarkupcmt{A thread can exit if it no longer hold any resource:%
}
\isanewline
\ \ thread{\isaliteral{5F}{\isacharunderscore}}exit{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ holdents\ s\ thread\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Exit\ thread{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ %
\isamarkupcmt{A thread can request for an critical resource \isa{cs}, if it is running and 
  the request does not form a loop in the current RAG. The latter condition 
  is set up to avoid deadlock. The condition also reflects our assumption all threads are 
  carefully programmed so that deadlock can not happen.%
}
\isanewline
\ \ thread{\isaliteral{5F}{\isacharunderscore}}P{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ \ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{2C}{\isacharcomma}}\ Th\ thread{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}P\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ %
\isamarkupcmt{A thread can release a critical resource \isa{cs} if it is running and holding that resource.%
}
\isanewline
\ \ thread{\isaliteral{5F}{\isacharunderscore}}V{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ \ holding\ s\ thread\ cs{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}V\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ %
\isamarkupcmt{A thread can adjust its own priority as long as it is current running.%
}
\ \ \isanewline
\ \ thread{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Set\ thread\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
With predicate \isa{step}, the fact that \isa{s} is a legal state in 
  Priority Inheritance protocol can be expressed as: \isa{vt\ step\ s}, where
  the predicate \isa{vt} can be defined as the following:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{inductive}\isamarkupfalse%
\ vt\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ event\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \isakeyword{for}\ cs\ %
\isamarkupcmt{\isa{cs} is an argument representing any step predicate.%
}
\isanewline
\isakeyword{where}\isanewline
\ \ %
\isamarkupcmt{Empty list \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is a legal state in any protocol:%
}
\isanewline
\ \ vt{\isaliteral{5F}{\isacharunderscore}}nil{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}vt\ cs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
\ \ %
\isamarkupcmt{If \isa{s} a legal state, and event \isa{e} is eligible to happen
        in state \isa{s}, then \isa{e{\isaliteral{23}{\isacharhash}}{\isaliteral{23}{\isacharhash}}s} is a legal state as well:%
}
\isanewline
\ \ vt{\isaliteral{5F}{\isacharunderscore}}cons{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}vt\ cs\ s{\isaliteral{3B}{\isacharsemicolon}}\ cs\ s\ e{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ vt\ cs\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
It is easy to see that the definition of \isa{vt} is generic. It can be applied to 
  any step predicate to get the set of legal states.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\begin{isamarkuptext}%
The following two functions \isa{the{\isaliteral{5F}{\isacharunderscore}}cs} and \isa{the{\isaliteral{5F}{\isacharunderscore}}th} are used to extract
  critical resource and thread respectively out of RAG nodes.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{fun}\isamarkupfalse%
\ the{\isaliteral{5F}{\isacharunderscore}}cs\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}node\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}the{\isaliteral{5F}{\isacharunderscore}}cs\ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ cs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isanewline
\isacommand{fun}\isamarkupfalse%
\ the{\isaliteral{5F}{\isacharunderscore}}th\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}node\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}the{\isaliteral{5F}{\isacharunderscore}}th\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ th{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The following predicate \isa{next{\isaliteral{5F}{\isacharunderscore}}th} describe the next thread to 
  take over when a critical resource is released. In \isa{next{\isaliteral{5F}{\isacharunderscore}}th\ s\ th\ cs\ t}, 
  \isa{th} is the thread to release, \isa{t} is the one to take over.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ next{\isaliteral{5F}{\isacharunderscore}}th{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}next{\isaliteral{5F}{\isacharunderscore}}th\ s\ th\ cs\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}\ rest{\isaliteral{2E}{\isachardot}}\ wq\ s\ cs\ {\isaliteral{3D}{\isacharequal}}\ th{\isaliteral{23}{\isacharhash}}rest\ {\isaliteral{5C3C616E643E}{\isasymand}}\ rest\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ rest{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The function \isa{count\ Q\ l} is used to count the occurrence of situation \isa{Q}
  in list \isa{l}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ count\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}count\ Q\ l\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{28}{\isacharparenleft}}filter\ Q\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\isa{cntP\ s} returns the number of operation \isa{P} happened 
  before reaching state \isa{s}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ cntP\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntP\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ count\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ e{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}\ cs{\isaliteral{2E}{\isachardot}}\ e\ {\isaliteral{3D}{\isacharequal}}\ P\ th\ cs{\isaliteral{29}{\isacharparenright}}\ s{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\isa{cntV\ s} returns the number of operation \isa{V} happened 
  before reaching state \isa{s}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
\ cntV\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntV\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ count\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ e{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}\ cs{\isaliteral{2E}{\isachardot}}\ e\ {\isaliteral{3D}{\isacharequal}}\ V\ th\ cs{\isaliteral{29}{\isacharparenright}}\ s{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
\isanewline
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: