diff -r 2c56b20032a7 -r 0679a84b11ad prio/Paper/PrioGDef.tex --- a/prio/Paper/PrioGDef.tex Mon Dec 03 08:16:58 2012 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,488 +0,0 @@ -% -\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: