prio/Paper/Paper.thy
author urbanc
Tue, 14 Feb 2012 00:27:47 +0000
changeset 324 41e4b331ce08
parent 323 eee031cc9634
child 325 163cd8034e5b
permissions -rwxr-xr-x
fixed 1st paragraph
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
262
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
     1
(*<*)
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
     2
theory Paper
301
urbanc
parents: 300
diff changeset
     3
imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
262
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
     4
begin
266
800b0e3b4204 More explanations added by XY.
zhang
parents: 265
diff changeset
     5
ML {*
273
039711ba6cf9 slightly more on text
urbanc
parents: 272
diff changeset
     6
  open Printer;
272
ee4611c1e13c All comments added.
zhang
parents: 271
diff changeset
     7
  show_question_marks_default := false;
266
800b0e3b4204 More explanations added by XY.
zhang
parents: 265
diff changeset
     8
  *}
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
     9
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    10
notation (latex output)
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    11
  Cons ("_::_" [78,77] 73) and
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    12
  vt ("valid'_state") and
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    13
  runing ("running") and
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
    14
  birthtime ("last'_set") and
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    15
  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
    16
  Prc ("'(_, _')") and
287
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
    17
  holding ("holds") and
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
    18
  waiting ("waits") and
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
    19
  Th ("T") and
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
    20
  Cs ("C") and
287
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
    21
  readys ("ready") and
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
    22
  depend ("RAG") and 
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
    23
  preced ("prec") and
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
    24
  cpreced ("cprec") and
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
    25
  dependents ("dependants") and
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
    26
  cp ("cprec") and
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
    27
  holdents ("resources") and
299
4fcd802eba59 small polishing
urbanc
parents: 298
diff changeset
    28
  original_priority ("priority") and
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    29
  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
262
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    30
(*>*)
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    31
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    32
section {* Introduction *}
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    33
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    34
text {*
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    35
  Many real-time systems need to support threads involving priorities and
267
83fb18cadd2b added two paragraphs to the introduction
urbanc
parents: 266
diff changeset
    36
  locking of resources. Locking of resources ensures mutual exclusion
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    37
  when accessing shared data or devices that cannot be
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    38
  preempted. Priorities allow scheduling of threads that need to
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    39
  finish their work within deadlines.  Unfortunately, both features
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    40
  can interact in subtle ways leading to a problem, called
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    41
  \emph{Priority Inversion}. Suppose three threads having priorities
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    42
  $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    43
  $H$ blocks any other thread with lower priority and itself cannot
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    44
  be blocked by any thread with lower priority. Alas, in a naive
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    45
  implementation of resource looking and priorities this property can
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    46
  be violated. Even worse, $H$ can be delayed indefinitely by
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    47
  threads with lower priorities. For this let $L$ be in the
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    48
  possession of a lock for a resource that also $H$ needs. $H$ must
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    49
  therefore wait for $L$ to exit the critical section and release this
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    50
  lock. The problem is that $L$ might in turn be blocked by any
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    51
  thread with priority $M$, and so $H$ sits there potentially waiting
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    52
  indefinitely. Since $H$ is blocked by threads with lower
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    53
  priorities, the problem is called Priority Inversion. It was first
277
541bfdf1fa36 slight tuning
urbanc
parents: 276
diff changeset
    54
  described in \cite{Lampson80} in the context of the
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    55
  Mesa programming language designed for concurrent programming.
265
993068ce745f changed abstract, intro and IsaMakefile
urbanc
parents: 264
diff changeset
    56
273
039711ba6cf9 slightly more on text
urbanc
parents: 272
diff changeset
    57
  If the problem of Priority Inversion is ignored, real-time systems
267
83fb18cadd2b added two paragraphs to the introduction
urbanc
parents: 266
diff changeset
    58
  can become unpredictable and resulting bugs can be hard to diagnose.
83fb18cadd2b added two paragraphs to the introduction
urbanc
parents: 266
diff changeset
    59
  The classic example where this happened is the software that
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    60
  controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    61
  Once the spacecraft landed, the software shut down at irregular
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    62
  intervals leading to loss of project time as normal operation of the
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    63
  craft could only resume the next day (the mission and data already
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    64
  collected were fortunately not lost, because of a clever system
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    65
  design).  The reason for the shutdowns was that the scheduling
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    66
  software fell victim of Priority Inversion: a low priority thread
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    67
  locking a resource prevented a high priority thread from running in
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    68
  time leading to a system reset. Once the problem was found, it was
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    69
  rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    70
  \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
    71
  Inheritance Protocol} \cite{Sha90} and others sometimes also call it
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
    72
  \emph{Priority Boosting}.} in the scheduling software.
262
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
    73
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    74
  The idea behind PIP is to let the thread $L$ temporarily inherit
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
    75
  the high priority from $H$ until $L$ leaves the critical section
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    76
  unlocking the resource. This solves the problem of $H$ having to
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    77
  wait indefinitely, because $L$ cannot be blocked by threads having
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    78
  priority $M$. While a few other solutions exist for the Priority
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    79
  Inversion problem, PIP is one that is widely deployed and
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    80
  implemented. This includes VxWorks (a proprietary real-time OS used
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    81
  in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    82
  ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    83
  example in libraries for FreeBSD, Solaris and Linux.
274
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
    84
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    85
  One advantage of PIP is that increasing the priority of a thread
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
    86
  can be dynamically calculated by the scheduler. This is in contrast
277
541bfdf1fa36 slight tuning
urbanc
parents: 276
diff changeset
    87
  to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
541bfdf1fa36 slight tuning
urbanc
parents: 276
diff changeset
    88
  solution to the Priority Inversion problem, which requires static
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    89
  analysis of the program in order to prevent Priority
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    90
  Inversion. However, there has also been strong criticism against
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    91
  PIP. For instance, PIP cannot prevent deadlocks when lock
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    92
  dependencies are circular, and also blocking times can be
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    93
  substantial (more than just the duration of a critical section).
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    94
  Though, most criticism against PIP centres around unreliable
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    95
  implementations and PIP being too complicated and too inefficient.
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
    96
  For example, Yodaiken writes in \cite{Yodaiken02}:
274
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
    97
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
    98
  \begin{quote}
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
    99
  \it{}``Priority inheritance is neither efficient nor reliable. Implementations
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   100
  are either incomplete (and unreliable) or surprisingly complex and intrusive.''
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   101
  \end{quote}
273
039711ba6cf9 slightly more on text
urbanc
parents: 272
diff changeset
   102
274
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   103
  \noindent
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
   104
  He suggests to avoid PIP altogether by not allowing critical
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   105
  sections to be preempted. Unfortunately, this solution does not
304
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   106
  help in real-time systems with hard deadlines for high-priority 
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   107
  threads.
278
3e2c006e7d6c a bit more on the introduction
urbanc
parents: 277
diff changeset
   108
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   109
  In our opinion, there is clearly a need for investigating correct
278
3e2c006e7d6c a bit more on the introduction
urbanc
parents: 277
diff changeset
   110
  algorithms for PIP. A few specifications for PIP exist (in English)
3e2c006e7d6c a bit more on the introduction
urbanc
parents: 277
diff changeset
   111
  and also a few high-level descriptions of implementations (e.g.~in
3e2c006e7d6c a bit more on the introduction
urbanc
parents: 277
diff changeset
   112
  the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
3e2c006e7d6c a bit more on the introduction
urbanc
parents: 277
diff changeset
   113
  with actual implementations. That this is a problem in practise is
283
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   114
  proved by an email from Baker, who wrote on 13 July 2009 on the Linux
278
3e2c006e7d6c a bit more on the introduction
urbanc
parents: 277
diff changeset
   115
  Kernel mailing list:
274
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   116
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   117
  \begin{quote}
275
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
   118
  \it{}``I observed in the kernel code (to my disgust), the Linux PIP
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
   119
  implementation is a nightmare: extremely heavy weight, involving
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
   120
  maintenance of a full wait-for graph, and requiring updates for a
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
   121
  range of events, including priority changes and interruptions of
22b6bd498419 more on intro
urbanc
parents: 274
diff changeset
   122
  wait operations.''
274
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   123
  \end{quote}
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   124
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   125
  \noindent
277
541bfdf1fa36 slight tuning
urbanc
parents: 276
diff changeset
   126
  The criticism by Yodaiken, Baker and others suggests to us to look
541bfdf1fa36 slight tuning
urbanc
parents: 276
diff changeset
   127
  again at PIP from a more abstract level (but still concrete enough
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   128
  to inform an implementation), and makes PIP an ideal candidate for a
277
541bfdf1fa36 slight tuning
urbanc
parents: 276
diff changeset
   129
  formal verification. One reason, of course, is that the original
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   130
  presentation of PIP~\cite{Sha90}, despite being informally
283
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   131
  ``proved'' correct, is actually \emph{flawed}. 
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   132
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   133
  Yodaiken \cite{Yodaiken02} points to a subtlety that had been
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   134
  overlooked in the informal proof by Sha et al. They specify in
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   135
  \cite{Sha90} that after the thread (whose priority has been raised)
283
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   136
  completes its critical section and releases the lock, it ``returns
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   137
  to its original priority level.'' This leads them to believe that an
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   138
  implementation of PIP is ``rather straightforward''~\cite{Sha90}.
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   139
  Unfortunately, as Yodaiken points out, this behaviour is too
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   140
  simplistic.  Consider the case where the low priority thread $L$
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   141
  locks \emph{two} resources, and two high-priority threads $H$ and
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   142
  $H'$ each wait for one of them.  If $L$ releases one resource
283
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   143
  so that $H$, say, can proceed, then we still have Priority Inversion
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   144
  with $H'$ (which waits for the other resource). The correct
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   145
  behaviour for $L$ is to revert to the highest remaining priority of
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   146
  the threads that it blocks. The advantage of formalising the
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   147
  correctness of a high-level specification of PIP in a theorem prover
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   148
  is that such issues clearly show up and cannot be overlooked as in
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   149
  informal reasoning (since we have to analyse all possible behaviours
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   150
  of threads, i.e.~\emph{traces}, that could possibly happen).\medskip
274
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   151
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   152
  \noindent
301
urbanc
parents: 300
diff changeset
   153
  {\bf Contributions:} There have been earlier formal investigations
304
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   154
  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   155
  checking techniques. This paper presents a formalised and
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   156
  mechanically checked proof for the correctness of PIP (to our
305
463bed130705 some polishing
urbanc
parents: 304
diff changeset
   157
  knowledge the first one; the earlier informal proof by Sha et
304
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   158
  al.~\cite{Sha90} is flawed).  In contrast to model checking, our
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   159
  formalisation provides insight into why PIP is correct and allows us
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   160
  to prove stronger properties that, as we will show, can inform an
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   161
  efficient implementation.  For example, we found by ``playing'' with the formalisation
304
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   162
  that the choice of the next thread to take over a lock when a
305
463bed130705 some polishing
urbanc
parents: 304
diff changeset
   163
  resource is released is irrelevant for PIP being correct. Something
463bed130705 some polishing
urbanc
parents: 304
diff changeset
   164
  which has not been mentioned in the relevant literature.
280
c91c2dd08599 updated
urbanc
parents: 279
diff changeset
   165
*}
278
3e2c006e7d6c a bit more on the introduction
urbanc
parents: 277
diff changeset
   166
283
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   167
section {* Formal Model of the Priority Inheritance Protocol *}
267
83fb18cadd2b added two paragraphs to the introduction
urbanc
parents: 266
diff changeset
   168
280
c91c2dd08599 updated
urbanc
parents: 279
diff changeset
   169
text {*
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   170
  The Priority Inheritance Protocol, short PIP, is a scheduling
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   171
  algorithm for a single-processor system.\footnote{We shall come back
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   172
  later to the case of PIP on multi-processor systems.} Our model of
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   173
  PIP is based on Paulson's inductive approach to protocol
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   174
  verification \cite{Paulson98}, where the \emph{state} of a system is
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   175
  given by a list of events that happened so far.  \emph{Events} of PIP fall
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   176
  into five categories defined as the datatype:
283
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   177
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   178
  \begin{isabelle}\ \ \ \ \ %%%
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   179
  \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   180
  \isacommand{datatype} event 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   181
  & @{text "="} & @{term "Create thread priority"}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   182
  & @{text "|"} & @{term "Exit thread"} \\
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   183
  & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the priority for} @{text thread}\\
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   184
  & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   185
  & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   186
  \end{tabular}}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   187
  \end{isabelle}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   188
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   189
  \noindent
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   190
  whereby threads, priorities and (critical) resources are represented
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   191
  as natural numbers. The event @{term Set} models the situation that
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   192
  a thread obtains a new priority given by the programmer or
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   193
  user (for example via the {\tt nice} utility under UNIX).  As in Paulson's work, we
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   194
  need to define functions that allow us to make some observations
297
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   195
  about states.  One, called @{term threads}, calculates the set of
293
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   196
  ``live'' threads that we have seen so far:
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   197
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   198
  \begin{isabelle}\ \ \ \ \ %%%
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   199
  \mbox{\begin{tabular}{lcl}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   200
  @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   201
    @{thm (rhs) threads.simps(1)}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   202
  @{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   203
    @{thm (rhs) threads.simps(2)[where thread="th"]}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   204
  @{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   205
    @{thm (rhs) threads.simps(3)[where thread="th"]}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   206
  @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   207
  \end{tabular}}
283
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   208
  \end{isabelle}
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   209
7d2bab099b89 paper updatated
urbanc
parents: 280
diff changeset
   210
  \noindent
299
4fcd802eba59 small polishing
urbanc
parents: 298
diff changeset
   211
  In this definition @{term "DUMMY # DUMMY"} stands for list-cons.
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   212
  Another function calculates the priority for a thread @{text "th"}, which is 
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   213
  defined as
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   214
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   215
  \begin{isabelle}\ \ \ \ \ %%%
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   216
  \mbox{\begin{tabular}{lcl}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   217
  @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   218
    @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   219
  @{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   220
    @{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   221
  @{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   222
    @{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   223
  @{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   224
  \end{tabular}}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   225
  \end{isabelle}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   226
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   227
  \noindent
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   228
  In this definition we set @{text 0} as the default priority for
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   229
  threads that have not (yet) been created. The last function we need 
285
5920649c5a22 more on paper
urbanc
parents: 284
diff changeset
   230
  calculates the ``time'', or index, at which time a process had its 
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   231
  priority last set.
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   232
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   233
  \begin{isabelle}\ \ \ \ \ %%%
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   234
  \mbox{\begin{tabular}{lcl}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   235
  @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   236
    @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   237
  @{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   238
    @{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   239
  @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   240
    @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   241
  @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   242
  \end{tabular}}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   243
  \end{isabelle}
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   244
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   245
  \noindent
287
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   246
  In this definition @{term "length s"} stands for the length of the list
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   247
  of events @{text s}. Again the default value in this function is @{text 0}
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   248
  for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a 
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   249
  state @{text s} is the pair of natural numbers defined as
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   250
  
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   251
  \begin{isabelle}\ \ \ \ \ %%%
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   252
  @{thm preced_def[where thread="th"]}
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   253
  \end{isabelle}
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   254
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   255
  \noindent
287
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   256
  The point of precedences is to schedule threads not according to priorities (because what should
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   257
  we do in case two threads have the same priority), but according to precedences. 
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   258
  Precedences allow us to always discriminate between two threads with equal priority by 
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   259
  taking into account the time when the priority was last set. We order precedences so 
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   260
  that threads with the same priority get a higher precedence if their priority has been 
293
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   261
  set earlier, since for such threads it is more urgent to finish their work. In an implementation
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   262
  this choice would translate to a quite natural FIFO-scheduling of processes with 
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   263
  the same priority.
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   264
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   265
  Next, we introduce the concept of \emph{waiting queues}. They are
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   266
  lists of threads associated with every resource. The first thread in
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   267
  this list (i.e.~the head, or short @{term hd}) is chosen to be the one 
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   268
  that is in possession of the
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   269
  ``lock'' of the corresponding resource. We model waiting queues as
293
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   270
  functions, below abbreviated as @{text wq}. They take a resource as
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   271
  argument and return a list of threads.  This allows us to define
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   272
  when a thread \emph{holds}, respectively \emph{waits} for, a
293
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   273
  resource @{text cs} given a waiting queue function @{text wq}.
287
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   274
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   275
  \begin{isabelle}\ \ \ \ \ %%%
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   276
  \begin{tabular}{@ {}l}
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   277
  @{thm cs_holding_def[where thread="th"]}\\
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   278
  @{thm cs_waiting_def[where thread="th"]}
287
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   279
  \end{tabular}
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   280
  \end{isabelle}
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   281
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   282
  \noindent
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   283
  In this definition we assume @{text "set"} converts a list into a set.
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   284
  At the beginning, that is in the state where no thread is created yet, 
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   285
  the waiting queue function will be the function that returns the
293
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   286
  empty list for every resource.
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   287
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   288
  \begin{isabelle}\ \ \ \ \ %%%
301
urbanc
parents: 300
diff changeset
   289
  @{abbrev all_unlocked}\hfill\numbered{allunlocked}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   290
  \end{isabelle}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   292
  \noindent
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   293
  Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} 
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   294
  (RAG), which represent the dependencies between threads and resources.
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   295
  We represent RAGs as relations using pairs of the form
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   296
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   297
  \begin{isabelle}\ \ \ \ \ %%%
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   298
  @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   299
  @{term "(Cs cs, Th th)"}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   300
  \end{isabelle}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   301
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   302
  \noindent
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   303
  where the first stands for a \emph{waiting edge} and the second for a 
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   304
  \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a 
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   305
  datatype for vertices). Given a waiting queue function, a RAG is defined 
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   306
  as the union of the sets of waiting and holding edges, namely
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   307
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   308
  \begin{isabelle}\ \ \ \ \ %%%
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   309
  @{thm cs_depend_def}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   310
  \end{isabelle}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   311
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   312
  \noindent
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   313
  Given three threads and three resources, an instance of a RAG can be pictured 
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   314
  as follows:
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   315
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   316
  \begin{center}
297
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   317
  \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   318
  \begin{tikzpicture}[scale=1]
297
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   319
  %%\draw[step=2mm] (-3,2) grid (1,-1);
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   320
297
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   321
  \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   322
  \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   323
  \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   324
  \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   325
  \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   326
  \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
297
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   327
  \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   328
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   329
  \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (B);
297
0a4be67ea7f8 added picture
urbanc
parents: 296
diff changeset
   330
  \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   331
  \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting}  (B);
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   332
  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (E);
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   333
  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (E1);
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   334
  \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (E);
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   335
  \end{tikzpicture}
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   336
  \end{center}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   337
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   338
  \noindent
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   339
  The use of relations for representing RAGs allows us to conveniently define
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   340
  the notion of the \emph{dependants} of a thread using the transitive closure
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   341
  operation for relations. This gives
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   342
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   343
  \begin{isabelle}\ \ \ \ \ %%%
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   344
  @{thm cs_dependents_def}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   345
  \end{isabelle}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   346
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   347
  \noindent
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   348
  This definition needs to account for all threads that wait for a thread to
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   349
  release a resource. This means we need to include threads that transitively
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   350
  wait for a resource being released (in the picture above this means the dependants
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   351
  of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"}, 
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   352
  but also @{text "th\<^isub>3"}, 
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   353
  which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   354
  in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle in a RAG, then clearly
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   355
  we have a deadlock. Therefore when a thread requests a resource,
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   356
  we must ensure that the resulting RAG is not circular. 
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   357
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   358
  Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   359
  state @{text s}. It is defined as
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   360
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   361
  \begin{isabelle}\ \ \ \ \ %%%
299
4fcd802eba59 small polishing
urbanc
parents: 298
diff changeset
   362
  @{thm cpreced_def2}\hfill\numbered{cpreced}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   363
  \end{isabelle}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   364
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   365
  \noindent
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   366
  where the dependants of @{text th} are given by the waiting queue function.
293
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   367
  While the precedence @{term prec} of a thread is determined by the programmer 
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   368
  (for example when the thread is
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   369
  created), the point of the current precedence is to let the scheduler increase this
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   370
  precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   371
  given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   372
  threads that are dependants of @{text th}. Since the notion @{term "dependants"} is
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   373
  defined as the transitive closure of all dependent threads, we deal correctly with the 
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   374
  problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   375
  lowered prematurely.
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   376
  
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   377
  The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   378
  by recursion on the state (a list of events); this function returns a \emph{schedule state}, which 
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   379
  we represent as a record consisting of two
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   380
  functions:
293
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   381
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   382
  \begin{isabelle}\ \ \ \ \ %%%
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   383
  @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
cab43c4a96d2 some polishing
urbanc
parents: 292
diff changeset
   384
  \end{isabelle}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   385
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   386
  \noindent
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   387
  The first function is a waiting queue function (that is, it takes a
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   388
  resource @{text "cs"} and returns the corresponding list of threads
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   389
  that lock, respectively wait for, it); the second is a function that
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   390
  takes a thread and returns its current precedence (see
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   391
  \eqref{cpreced}). We assume the usual getter and setter methods for
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   392
  such records.
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   393
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   394
  In the initial state, the scheduler starts with all resources unlocked (the corresponding 
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   395
  function is defined in \eqref{allunlocked}) and the
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   396
  current precedence of every thread is initialised with @{term "Prc 0 0"}; that means 
299
4fcd802eba59 small polishing
urbanc
parents: 298
diff changeset
   397
  \mbox{@{abbrev initial_cprec}}. Therefore
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   398
  we have for the initial state
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   399
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   400
  \begin{isabelle}\ \ \ \ \ %%%
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   401
  \begin{tabular}{@ {}l}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   402
  @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ 
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   403
  \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   404
  \end{tabular}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   405
  \end{isabelle}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   406
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   407
  \noindent
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   408
  The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   409
  we calculate the waiting queue function of the (previous) state @{text s}; 
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   410
  this waiting queue function @{text wq} is unchanged in the next schedule state---because
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   411
  none of these events lock or release any resource; 
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   412
  for calculating the next @{term "cprec_fun"}, we use @{text wq} and 
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   413
  @{term cpreced}. This gives the following three clauses for @{term schs}:
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   414
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   415
  \begin{isabelle}\ \ \ \ \ %%%
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   416
  \begin{tabular}{@ {}l}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   417
  @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ 
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   418
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   419
  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\smallskip\\
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   420
  @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   421
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   422
  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   423
  @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ 
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   424
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   425
  \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   426
  \end{tabular}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   427
  \end{isabelle}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   428
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   429
  \noindent 
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   430
  More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   431
  we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   432
  the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th} 
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   433
  appended to the end of that list (remember the head of this list is assigned to be in the possession of this
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   434
  resource). This gives the clause
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   435
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   436
  \begin{isabelle}\ \ \ \ \ %%%
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   437
  \begin{tabular}{@ {}l}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   438
  @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ 
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   439
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   440
  \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   441
  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   442
  \end{tabular}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   443
  \end{isabelle}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   444
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   445
  \noindent
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   446
  The clause for event @{term "V th cs"} is similar, except that we need to update the waiting queue function
301
urbanc
parents: 300
diff changeset
   447
  so that the thread that possessed the lock is deleted from the corresponding thread list. For this 
urbanc
parents: 300
diff changeset
   448
  list transformation, we use
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   449
  the auxiliary function @{term release}. A simple version of @{term release} would
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   450
  just delete this thread and return the remaining threads, namely
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   451
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   452
  \begin{isabelle}\ \ \ \ \ %%%
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   453
  \begin{tabular}{@ {}lcl}
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   454
  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   455
  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   456
  \end{tabular}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   457
  \end{isabelle}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   458
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   459
  \noindent
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   460
  In practice, however, often the thread with the highest precedence in the list will get the
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   461
  lock next. We have implemented this choice, but later found out that the choice 
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   462
  of which thread is chosen next is actually irrelevant for the correctness of PIP.
296
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   463
  Therefore we prove the stronger result where @{term release} is defined as
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   464
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   465
  \begin{isabelle}\ \ \ \ \ %%%
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   466
  \begin{tabular}{@ {}lcl}
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   467
  @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   468
  @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   469
  \end{tabular}
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   470
  \end{isabelle}
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   471
2c8dcf010567 spell check; release
urbanc
parents: 294
diff changeset
   472
  \noindent
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   473
  where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   474
  choice for the next waiting list. It just has to be a list of distinctive threads and
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   475
  contain the same elements as @{text "qs"}. This gives for @{term V} the clause:
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   476
 
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   477
  \begin{isabelle}\ \ \ \ \ %%%
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   478
  \begin{tabular}{@ {}l}
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   479
  @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   480
  \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   481
  \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
294
bc5bf9e9ada2 renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
urbanc
parents: 293
diff changeset
   482
  \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
291
5ef9f6ebe827 more on paper; modified schs functions; it is still compatible with the old definition
urbanc
parents: 290
diff changeset
   483
  \end{tabular}
290
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   484
  \end{isabelle}
6a6d0bd16035 more on paper
urbanc
parents: 287
diff changeset
   485
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   486
  Having the scheduler function @{term schs} at our disposal, we can ``lift'', or
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   487
  overload, the notions
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   488
  @{term waiting}, @{term holding}, @{term depend} and @{term cp} to operate on states only.
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   489
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   490
  \begin{isabelle}\ \ \ \ \ %%%
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   491
  \begin{tabular}{@ {}rcl}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   492
  @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   493
  @{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   494
  @{thm (lhs) s_depend_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_depend_abv}\\
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   495
  @{thm (lhs) cp_def}        & @{text "\<equiv>"} & @{thm (rhs) cp_def}
287
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   496
  \end{tabular}
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   497
  \end{isabelle}
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   498
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   499
  \noindent
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   500
  With these abbreviations we can introduce 
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
   501
  the notion of threads being @{term readys} in a state (i.e.~threads
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   502
  that do not wait for any resource) and the running thread.
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   503
287
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   504
  \begin{isabelle}\ \ \ \ \ %%%
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   505
  \begin{tabular}{@ {}l}
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   506
  @{thm readys_def}\\
440382eb6427 more on the specification section
urbanc
parents: 286
diff changeset
   507
  @{thm runing_def}\\
286
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   508
  \end{tabular}
572f202659ff corrections by Xingyuan
urbanc
parents: 285
diff changeset
   509
  \end{isabelle}
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   510
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   511
  \noindent
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   512
  In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   513
  Note that in the initial state, that is where the list of events is empty, the set 
309
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   514
  @{term threads} is empty and therefore there is neither a thread ready nor running.
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   515
  If there is one or more threads ready, then there can only be \emph{one} thread
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   516
  running, namely the one whose current precedence is equal to the maximum of all ready 
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   517
  threads. We use sets to capture both possibilities.
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   518
  We can now also conveniently define the set of resources that are locked by a thread in a
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   519
  given state.
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   520
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   521
  \begin{isabelle}\ \ \ \ \ %%%
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   522
  @{thm holdents_def}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   523
  \end{isabelle}
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   524
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   525
  Finally we can define what a \emph{valid state} is in our model of PIP. For
304
bd05c5011c0f contribution section
urbanc
parents: 301
diff changeset
   526
  example we cannot expect to be able to exit a thread, if it was not
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   527
  created yet. These validity constraints on states are characterised by the
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   528
  inductive predicate @{term "step"} and @{term vt}. We first give five inference rules
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   529
  for @{term step} relating a state and an event that can happen next.
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   530
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   531
  \begin{center}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   532
  \begin{tabular}{c}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   533
  @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   534
  @{thm[mode=Rule] thread_exit[where thread=th]}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   535
  \end{tabular}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   536
  \end{center}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   537
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   538
  \noindent
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   539
  The first rule states that a thread can only be created, if it does not yet exists.
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   540
  Similarly, the second rule states that a thread can only be terminated if it was
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   541
  running and does not lock any resources anymore (this simplifies slightly our model;
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   542
  in practice we would expect the operating system releases all locks held by a
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   543
  thread that is about to exit). The event @{text Set} can happen
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   544
  if the corresponding thread is running. 
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   545
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   546
  \begin{center}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   547
  @{thm[mode=Rule] thread_set[where thread=th]}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   548
  \end{center}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   549
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   550
  \noindent
301
urbanc
parents: 300
diff changeset
   551
  If a thread wants to lock a resource, then the thread needs to be
urbanc
parents: 300
diff changeset
   552
  running and also we have to make sure that the resource lock does
urbanc
parents: 300
diff changeset
   553
  not lead to a cycle in the RAG. In practice, ensuring the latter is
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   554
  the responsibility of the programmer.  In our formal
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   555
  model we brush aside these problematic cases in order to be able to make
301
urbanc
parents: 300
diff changeset
   556
  some meaningful statements about PIP.\footnote{This situation is
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   557
  similar to the infamous occurs check in Prolog: In order to say
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   558
  anything meaningful about unification, one needs to perform an occurs
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   559
  check. But in practice the occurs check is ommited and the
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   560
  responsibility for avoiding problems rests with the programmer.}
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   561
 
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   562
  \begin{center}
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   563
  @{thm[mode=Rule] thread_P[where thread=th]}
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   564
  \end{center}
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   565
 
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   566
  \noindent
301
urbanc
parents: 300
diff changeset
   567
  Similarly, if a thread wants to release a lock on a resource, then
urbanc
parents: 300
diff changeset
   568
  it must be running and in the possession of that lock. This is
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   569
  formally given by the last inference rule of @{term step}.
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   570
 
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   571
  \begin{center}
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   572
  @{thm[mode=Rule] thread_V[where thread=th]}
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   573
  \end{center}
306
5113aa1ae69a some polishing
urbanc
parents: 305
diff changeset
   574
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   575
  \noindent
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   576
  A valid state of PIP can then be conveniently be defined as follows:
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   577
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   578
  \begin{center}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   579
  \begin{tabular}{c}
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   580
  @{thm[mode=Axiom] vt_nil}\hspace{1cm}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   581
  @{thm[mode=Rule] vt_cons}
284
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   582
  \end{tabular}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   583
  \end{center}
d296cb127fcb more on paper
urbanc
parents: 283
diff changeset
   584
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   585
  \noindent
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   586
  This completes our formal model of PIP. In the next section we present
309
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   587
  properties that show our model of PIP is correct.
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   588
*}
274
83b0317370c2 more on intro
urbanc
parents: 273
diff changeset
   589
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   590
section {* The Correctness Proof *}
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   591
301
urbanc
parents: 300
diff changeset
   592
(*<*)
urbanc
parents: 300
diff changeset
   593
context extend_highest_gen
urbanc
parents: 300
diff changeset
   594
begin
urbanc
parents: 300
diff changeset
   595
print_locale extend_highest_gen
urbanc
parents: 300
diff changeset
   596
thm extend_highest_gen_def
urbanc
parents: 300
diff changeset
   597
thm extend_highest_gen_axioms_def
urbanc
parents: 300
diff changeset
   598
thm highest_gen_def
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   599
(*>*)
301
urbanc
parents: 300
diff changeset
   600
text {* 
322
c37b387110d0 1st paragraph
urbanc
parents: 321
diff changeset
   601
  Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
c37b387110d0 1st paragraph
urbanc
parents: 321
diff changeset
   602
  for PIP in terms of the number of critical resources: if there are
c37b387110d0 1st paragraph
urbanc
parents: 321
diff changeset
   603
  @{text m} critical resources, then a blocked job with high priority
324
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   604
  can only be blocked @{text m} times---that is a \emph{bounded}
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   605
  number of times. This result on its own, strictly speaking, does
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   606
  \emph{not} prevent indefinite, or unbounded, Priority Inversion,
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   607
  because if one low-priority thread does not give up its critical
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   608
  resource (the one the high-priority thread is waiting for), then the
322
c37b387110d0 1st paragraph
urbanc
parents: 321
diff changeset
   609
  high-priority thread can never run.  The argument of Sha et al.~is
c37b387110d0 1st paragraph
urbanc
parents: 321
diff changeset
   610
  that \emph{if} threads release locked resources in a finite amount
324
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   611
  of time, then indefinite Priority Inversion cannot occur---the high-priority
322
c37b387110d0 1st paragraph
urbanc
parents: 321
diff changeset
   612
  thread is guaranteed to run eventually. The assumption is that
c37b387110d0 1st paragraph
urbanc
parents: 321
diff changeset
   613
  programmers always ensure that this is the case.  However, even
324
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   614
  taking this assumption into account, ther correctness property is
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   615
  \emph{not} true for their version of PIP. As Yodaiken
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   616
  \cite{Yodaiken02} pointed out: If a low-priority thread possesses
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   617
  locks to two resources for which two high-priority threads are
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   618
  waiting for, then lowering the priority prematurely after giving up
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   619
  only one lock, can cause indefinite Priority Inversion for one of the
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   620
  high-priority threads, invalidating their bound.
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   621
323
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   622
  Even when fixed, their proof idea does not seem to go through for
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   623
  us, because of the way we have set up our formal model of PIP.  The
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   624
  reason is that we allow that critical sections can intersect
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   625
  (something Sha et al.~explicitly exclude).  Therefore we have a 
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   626
  different correctness criterion for PIP. The idea behind our
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   627
  criterion is as follows: for all states @{text
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   628
  s}, we know the corresponding thread @{text th} with the highest
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   629
  precedence; we show that in every future state (denoted by @{text
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   630
  "s' @ s"}) in which @{text th} is still alive, either @{text th} is
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   631
  running or it is blocked by a thread that was alive in the state
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   632
  @{text s}. Since in @{text s}, as in every state, the set of alive
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   633
  threads is finite, @{text th} can only be blocked a finite number of
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   634
  times. We will actually prove a stricter bound below. However, this
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   635
  correctness criterion hinges upon a number of assumptions about the
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   636
  states @{text s} and @{text "s' @ s"}, the thread @{text th} and the
eee031cc9634 1st paragraph
urbanc
parents: 322
diff changeset
   637
  events happening in @{text s'}. We list them next:
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   638
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   639
  \begin{quote}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   640
  {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make 
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   641
  any meaningful statement, we need to require that @{text "s"} and 
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   642
  @{text "s' @ s"} are valid states, namely
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   643
  \begin{isabelle}\ \ \ \ \ %%%
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   644
  \begin{tabular}{l}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   645
  @{term "vt s"}\\
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   646
  @{term "vt (s' @ s)"} 
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   647
  \end{tabular}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   648
  \end{isabelle}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   649
  \end{quote}
301
urbanc
parents: 300
diff changeset
   650
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   651
  \begin{quote}
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   652
  {\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be alive in @{text s} and 
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   653
  has the highest precedence of all alive threads in @{text s}. Furthermore the
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   654
  priority of @{text th} is @{text prio} (we need this in the next assumptions).
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   655
  \begin{isabelle}\ \ \ \ \ %%%
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   656
  \begin{tabular}{l}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   657
  @{term "th \<in> threads s"}\\
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   658
  @{term "prec th s = Max (cprec s ` threads s)"}\\
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   659
  @{term "prec th s = (prio, DUMMY)"}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   660
  \end{tabular}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   661
  \end{isabelle}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   662
  \end{quote}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   663
  
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   664
  \begin{quote}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   665
  {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot
309
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   666
  be blocked indefinitely. Of course this can happen if threads with higher priority
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   667
  than @{text th} are continously created in @{text s'}. Therefore we have to assume that  
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   668
  events in @{text s'} can only create (respectively set) threads with equal or lower 
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   669
  priority than @{text prio} of @{text th}. We also need to assume that the
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   670
  priority of @{text "th"} does not get reset and also that @{text th} does
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   671
  not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications. 
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   672
  \begin{isabelle}\ \ \ \ \ %%%
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   673
  \begin{tabular}{l}
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   674
  {If}~~@{text "Create th' prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   675
  {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   676
  {If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   677
  \end{tabular}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   678
  \end{isabelle}
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   679
  \end{quote}
301
urbanc
parents: 300
diff changeset
   680
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   681
  \noindent
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   682
  Under these assumptions we will prove the following correctness property:
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   683
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   684
  \begin{theorem}\label{mainthm}
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   685
  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   686
  the thread @{text th} and the events in @{text "s'"},
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   687
  if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   688
  @{text "th' \<in> threads s"}.
307
a2d4450b4bf3 assumptions
urbanc
parents: 306
diff changeset
   689
  \end{theorem}
301
urbanc
parents: 300
diff changeset
   690
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   691
  \noindent
324
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   692
  This theorem ensures that the thread @{text th}, which has the
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   693
  highest precedence in the state @{text s}, can only be blocked in
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   694
  the state @{text "s' @ s"} by a thread @{text th'} that already
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   695
  existed in @{text s}. As we shall see shortly, that means by only
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   696
  finitely many threads. Like in the argument by Sha et al.~this
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   697
  finite bound does not guarantee absence of indefinite Priority
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   698
  Inversion. For this we further have to assume that every thread
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   699
  gives up its resources after a finite amount of time. We found that
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   700
  this assumption is awkward to formalise in our model. Therefore we
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   701
  leave it out and let the programmer assume the responsibility to
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   702
  program threads in such a benign manner. In this detail, we do not
41e4b331ce08 fixed 1st paragraph
urbanc
parents: 323
diff changeset
   703
  make any progress in comparison with the work by Sha et al.
309
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   704
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   705
  In what follows we will describe properties of PIP that allow us to prove 
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   706
  Theorem~\ref{mainthm}. It is relatively easily to see that
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   707
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   708
  \begin{isabelle}\ \ \ \ \ %%%
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   709
  \begin{tabular}{@ {}l}
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   710
  @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   711
  @{thm[mode=IfThen]  finite_threads}
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   712
  \end{tabular}
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   713
  \end{isabelle}
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   714
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   715
  \noindent
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   716
  where the second property is by induction of @{term vt}. The next three
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   717
  properties are 
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   718
309
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   719
  \begin{isabelle}\ \ \ \ \ %%%
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   720
  \begin{tabular}{@ {}l}
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   721
  @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   722
  @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   723
  @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   724
  \end{tabular}
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   725
  \end{isabelle}
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   726
309
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   727
  \noindent
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   728
  The first one states that every waiting thread can only wait for a single
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   729
  resource (because it gets suspended after requesting that resource and having
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   730
  to wait for it); the second that every resource can only be held by a single thread; 
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   731
  the third property establishes that in every given valid state, there is
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   732
  at most one running thread. We can also show the following properties 
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   733
  about the RAG in @{text "s"}.
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   734
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   735
  \begin{isabelle}\ \ \ \ \ %%%
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   736
  \begin{tabular}{@ {}l}
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   737
  @{text If}~@{thm (prem 1) acyclic_depend}~@{text "then"}:\\
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   738
  \hspace{5mm}@{thm (concl) acyclic_depend},
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   739
  @{thm (concl) finite_depend} and
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   740
  @{thm (concl) wf_dep_converse},\\
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   741
  \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}\\
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   742
  \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}
310
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   743
  \end{tabular}
4d93486cb302 polished
urbanc
parents: 309
diff changeset
   744
  \end{isabelle}
309
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   745
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   746
  TODO
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   747
e44c4055d430 more on the paper
urbanc
parents: 308
diff changeset
   748
  \noindent
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   749
  The following lemmas show how RAG is changed with the execution of events:
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   750
  \begin{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   751
  \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   752
    @{thm[display] depend_set_unchanged}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   753
  \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   754
    @{thm[display] depend_create_unchanged}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   755
  \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   756
    @{thm[display] depend_exit_unchanged}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   757
  \item Execution of @{term "P"} (@{text "step_depend_p"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   758
    @{thm[display] step_depend_p}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   759
  \item Execution of @{term "V"} (@{text "step_depend_v"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   760
    @{thm[display] step_depend_v}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   761
  \end{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   762
  *}
301
urbanc
parents: 300
diff changeset
   763
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   764
text {* \noindent
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   765
  These properties are used to derive the following important results about RAG:
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   766
  \begin{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   767
  \item RAG is loop free (@{text "acyclic_depend"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   768
  @{thm [display] acyclic_depend}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   769
  \item RAGs are finite (@{text "finite_depend"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   770
  @{thm [display] finite_depend}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   771
  \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   772
  @{thm [display] wf_dep_converse}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   773
  \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   774
  @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   775
  \item All threads in RAG are living threads 
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   776
    (@{text "dm_depend_threads"} and @{text "range_in"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   777
    @{thm [display] dm_depend_threads range_in}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   778
  \end{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   779
  *}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   780
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   781
text {* \noindent
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   782
  The following lemmas show how every node in RAG can be chased to ready threads:
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   783
  \begin{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   784
  \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   785
    @{thm [display] chain_building[rule_format]}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   786
  \item The ready thread chased to is unique (@{text "dchain_unique"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   787
    @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   788
  \end{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   789
  *}
301
urbanc
parents: 300
diff changeset
   790
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   791
text {* \noindent
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   792
  Properties about @{term "next_th"}:
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   793
  \begin{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   794
  \item The thread taking over is different from the thread which is releasing
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   795
  (@{text "next_th_neq"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   796
  @{thm [display] next_th_neq}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   797
  \item The thread taking over is unique
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   798
  (@{text "next_th_unique"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   799
  @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}  
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   800
  \end{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   801
  *}
301
urbanc
parents: 300
diff changeset
   802
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   803
text {* \noindent
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   804
  Some deeper results about the system:
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   805
  \begin{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   806
  \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   807
  @{thm [display] max_cp_eq}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   808
  \item There must be one ready thread having the max @{term "cp"}-value 
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   809
  (@{text "max_cp_readys_threads"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   810
  @{thm [display] max_cp_readys_threads}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   811
  \end{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   812
  *}
301
urbanc
parents: 300
diff changeset
   813
308
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   814
text {* \noindent
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   815
  The relationship between the count of @{text "P"} and @{text "V"} and the number of 
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   816
  critical resources held by a thread is given as follows:
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   817
  \begin{enumerate}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   818
  \item The @{term "V"}-operation decreases the number of critical resources 
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   819
    one thread holds (@{text "cntCS_v_dec"})
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   820
     @{thm [display]  cntCS_v_dec}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   821
  \item The number of @{text "V"} never exceeds the number of @{text "P"} 
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   822
    (@{text "cnp_cnv_cncs"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   823
    @{thm [display]  cnp_cnv_cncs}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   824
  \item The number of @{text "V"} equals the number of @{text "P"} when 
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   825
    the relevant thread is not living:
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   826
    (@{text "cnp_cnv_eq"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   827
    @{thm [display]  cnp_cnv_eq}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   828
  \item When a thread is not living, it does not hold any critical resource 
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   829
    (@{text "not_thread_holdents"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   830
    @{thm [display] not_thread_holdents}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   831
  \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   832
    thread does not hold any critical resource, therefore no thread can depend on it
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   833
    (@{text "count_eq_dependents"}):
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   834
    @{thm [display] count_eq_dependents}
a401d2dff7d0 more on the paper
urbanc
parents: 307
diff changeset
   835
  \end{enumerate}
301
urbanc
parents: 300
diff changeset
   836
*}
urbanc
parents: 300
diff changeset
   837
urbanc
parents: 300
diff changeset
   838
(*<*)
urbanc
parents: 300
diff changeset
   839
end
urbanc
parents: 300
diff changeset
   840
(*>*)
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
   841
313
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   842
subsection {* Proof idea *}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   843
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   844
(*<*)
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   845
context extend_highest_gen
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   846
begin
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   847
print_locale extend_highest_gen
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   848
thm extend_highest_gen_def
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   849
thm extend_highest_gen_axioms_def
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   850
thm highest_gen_def
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   851
(*>*)
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   852
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   853
text {*
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   854
The reason that only threads which already held some resoures
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   855
can be runing and block @{text "th"} is that if , otherwise, one thread 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   856
does not hold any resource, it may never have its prioirty raised
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   857
and will not get a chance to run. This fact is supported by 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   858
lemma @{text "moment_blocked"}:
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   859
@{thm [display] moment_blocked}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   860
When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   861
resource in state @{text "s"} will not have a change to run latter. Rephrased, it means 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   862
any thread which is running after @{text "th"} became the highest must have already held
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   863
some resource at state @{text "s"}.
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   864
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   865
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   866
  When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   867
  if a thread releases all its resources at some moment in @{text "t"}, after that, 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   868
  it may never get a change to run. If every thread releases its resource in finite duration,
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   869
  then after a while, only thread @{text "th"} is left running. This shows how indefinite 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   870
  priority inversion can be avoided. 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   871
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   872
  So, the key of the proof is to establish the correctness of @{text "moment_blocked"}.
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   873
  We are going to show how this lemma is proved. At the heart of this proof, is 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   874
  lemma @{text "pv_blocked"}:
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   875
  @{thm [display] pv_blocked}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   876
  This lemma says: for any @{text "s"}-extension {text "t"}, if thread @{text "th'"}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   877
  does not hold any resource, it can not be running at @{text "t@s"}.
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   878
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   879
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   880
  \noindent Proof: 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   881
  \begin{enumerate}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   882
  \item Since thread @{text "th'"} does not hold any resource, no thread may depend on it, 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   883
    so its current precedence @{text "cp (t@s) th'"} equals to its own precedence
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   884
   @{text "preced th' (t@s)"}.  \label{arg_1}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   885
  \item Since @{text "th"} has the highest precedence in the system and 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   886
    precedences are distinct among threads, we have
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   887
    @{text "preced th' (t@s) < preced th (t@s)"}. From this and item \ref{arg_1}, 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   888
    we have @{text "cp (t@s) th' < preced th (t@s)"}.
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   889
  \item Since @{text "preced th (t@s)"} is already the highest in the system, 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   890
    @{text "cp (t@s) th"} can not be higher than this and can not be lower neither (by 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   891
    the definition of @{text "cp"}), we have @{text "preced th (t@s) = cp (t@s) th"}.
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   892
  \item Finally we have @{text "cp (t@s) th' < cp (t@s) th"}.
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   893
  \item By defintion of @{text "running"}, @{text "th'"} can not be runing at 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   894
    @{text "t@s"}.
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   895
  \end{enumerate}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   896
  Since @{text "th'"} is not able to run at state @{text "t@s"}, it is not able to 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   897
  make either {text "P"} or @{text "V"} action, so if @{text "t@s"} is extended
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   898
  one step further, @{text "th'"} still does not hold any resource. 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   899
  The situation will not unchanged in further extensions as long as 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   900
  @{text "th"} holds the highest precedence. Since this @{text "t"} is arbitarily chosen 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   901
  except being constrained by predicate @{text "extend_highest_gen"} and 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   902
  this predicate has the property that if it holds for @{text "t"}, it also holds
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   903
  for any moment @{text "i"} inside @{text "t"}, as shown by lemma @{text "red_moment"}:
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   904
@{thm [display] "extend_highest_gen.red_moment"}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   905
  so @{text "pv_blocked"} can be applied to any @{text "moment i t"}. 
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   906
  From this, lemma @{text "moment_blocked"} follows.
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   907
*}
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   908
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   909
(*<*)
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   910
end
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   911
(*>*)
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   912
3d154253d5fe proof idea
urbanc
parents: 312
diff changeset
   913
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
   914
section {* Properties for an Implementation\label{implement} *}
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
   915
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
   916
text {*
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   917
  While a formal correctness proof for our model of PIP is certainly
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   918
  attractive (especially in light of the flawed proof by Sha et
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   919
  al.~\cite{Sha90}), we found that the formalisation can even help us
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   920
  with efficiently implementing PIP.
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
   921
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   922
  For example Baker complained that calculating the current precedence
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   923
  in PIP is quite ``heavy weight'' in Linux (see the Introduction).
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   924
  In our model of PIP the current precedence of a thread in a state s
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   925
  depends on all its dependants---a ``global'' transitive notion,
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   926
  which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   927
  We can however improve upon this. For this let us define the notion
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   928
  of @{term children} of a thread @{text th} in a state @{text s} as
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   929
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   930
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   931
  \begin{tabular}{@ {}l}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   932
  @{thm children_def2}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   933
  \end{tabular}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   934
  \end{isabelle}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   935
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   936
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   937
  where a child is a thread that is one ``hop'' away from the tread
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   938
  @{text th} in the @{term RAG} (and waiting for @{text th} to release
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   939
  a resource). We can prove that
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
   940
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   941
  \begin{lemma}\label{childrenlem}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   942
  @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   943
  \begin{center}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   944
  @{thm (concl) cp_rec}.
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   945
  \end{center}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   946
  \end{lemma}
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
   947
  
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   948
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   949
  That means the current precedence of a thread @{text th} can be
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   950
  computed locally by considering only the children of @{text th}. In
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   951
  effect, it only needs to be recomputed for @{text th} when one of
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   952
  its children changes its current precedence.  Once the current 
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   953
  precedence is computed in this more efficient manner, the selection
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   954
  of the thread with highest precedence from a set of ready threads is
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   955
  a standard scheduling operation implemented in most operating
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   956
  systems.
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
   957
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   958
  Of course the main implementation work for PIP involves the
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   959
  scheduler and coding how it should react to events.  Below we
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   960
  outline how our formalisation guides this implementation for each
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   961
  kind of event.\smallskip
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   962
*}
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
   963
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
   964
(*<*)
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   965
context step_create_cps
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   966
begin
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   967
(*>*)
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   968
text {*
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   969
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   970
  \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and 
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   971
  the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   972
  is allowed to occur). In this situation we can show that
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   973
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   974
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   975
  \begin{tabular}{@ {}l}
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   976
  @{thm eq_dep},\\
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   977
  @{thm eq_cp_th}, and\\
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   978
  @{thm[mode=IfThen] eq_cp}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   979
  \end{tabular}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   980
  \end{isabelle}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   981
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   982
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   983
  This means we do not have recalculate the @{text RAG} and also none of the
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   984
  current precedences of the other threads. The current precedence of the created
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   985
  thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   986
  \smallskip
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   987
  *}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   988
(*<*)
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   989
end
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   990
context step_exit_cps
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   991
begin
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   992
(*>*)
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   993
text {*
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   994
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
   995
  \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and 
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   996
  the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   997
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   998
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
   999
  \begin{tabular}{@ {}l}
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1000
  @{thm eq_dep}, and\\
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1001
  @{thm[mode=IfThen] eq_cp}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1002
  \end{tabular}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1003
  \end{isabelle}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1004
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1005
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1006
  This means again we do not have to recalculate the @{text RAG} and
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1007
  also not the current precedences for the other threads. Since @{term th} is not
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1008
  alive anymore in state @{term "s"}, there is no need to calculate its
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1009
  current precedence.
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1010
  \smallskip
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1011
*}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1012
(*<*)
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1013
end
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1014
context step_set_cps
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1015
begin
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1016
(*>*)
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1017
text {*
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1018
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1019
  \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and 
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1020
  @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1021
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1022
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1023
  \begin{tabular}{@ {}l}
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1024
  @{thm[mode=IfThen] eq_dep}, and\\
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1025
  @{thm[mode=IfThen] eq_cp}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1026
  \end{tabular}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1027
  \end{isabelle}
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1028
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1029
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1030
  The first property is again telling us we do not need to change the @{text RAG}. The second
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1031
  however states that only threads that are \emph{not} dependants of @{text th} have their
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1032
  current precedence unchanged. For the others we have to recalculate the current
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1033
  precedence. To do this we can start from @{term "th"} 
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1034
  and follow the @{term "depend"}-chains to recompute the @{term "cp"} of every 
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1035
  thread encountered on the way using Lemma~\ref{childrenlem}. Since the @{term "depend"}
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1036
  is loop free, this procedure will always stop. The following two lemmas show, however, 
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1037
  that this procedure can actually stop often earlier without having to consider all
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1038
  dependants.
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1039
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1040
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1041
  \begin{tabular}{@ {}l}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1042
  @{thm[mode=IfThen] eq_up_self}\\
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1043
  @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1044
  @{text "then"} @{thm (concl) eq_up}.
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1045
  \end{tabular}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1046
  \end{isabelle}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1047
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1048
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1049
  The first states that if the current precedence of @{text th} is unchanged,
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1050
  then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1051
  The second states that if an intermediate @{term cp}-value does not change, then
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1052
  the procedure can also stop, because none of its dependent threads will
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1053
  have their current precedence changed.
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1054
  \smallskip
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1055
  *}
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1056
(*<*)
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1057
end
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1058
context step_v_cps_nt
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1059
begin
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1060
(*>*)
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1061
text {*
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1062
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1063
  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and 
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1064
  @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1065
  subcases: one where there is a thread to ``take over'' the released
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1066
  resource @{text cs}, and one where there is not. Let us consider them
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1067
  in turn. Suppose in state @{text s}, the thread @{text th'} takes over
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1068
  resource @{text cs} from thread @{text th}. We can show
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1069
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1070
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1071
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1072
  @{thm depend_s}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1073
  \end{isabelle}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1074
  
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1075
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1076
  which shows how the @{text RAG} needs to be changed. This also suggests
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1077
  how the current precedences need to be recalculated. For threads that are
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1078
  not @{text "th"} and @{text "th'"} nothing needs to be changed, since we
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1079
  can show
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1080
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1081
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1082
  @{thm[mode=IfThen] cp_kept}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1083
  \end{isabelle}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1084
  
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1085
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1086
  For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1087
  recalculate their current prcedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1088
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1089
  In the other case where there is no thread that takes over @{text cs}, we can show how
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1090
  to recalculate the @{text RAG} and also show that no current precedence needs
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1091
  to be recalculated.
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1092
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1093
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1094
  \begin{tabular}{@ {}l}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1095
  @{thm depend_s}\\
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1096
  @{thm eq_cp}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1097
  \end{tabular}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1098
  \end{isabelle}
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1099
  *}
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1100
(*<*)
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1101
end
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1102
context step_P_cps_e
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1103
begin
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1104
(*>*)
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1105
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1106
text {*
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1107
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1108
  \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and 
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1109
  @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1110
  the one where @{text cs} is locked, and where it is not. We treat the second case
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1111
  first by showing that
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1112
  
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1113
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1114
  \begin{tabular}{@ {}l}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1115
  @{thm depend_s}\\
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1116
  @{thm eq_cp}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1117
  \end{tabular}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1118
  \end{isabelle}
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1119
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1120
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1121
  This means we do not need to add a holding edge to the @{text RAG} and no
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1122
  current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1123
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1124
  In the second case we know that resouce @{text cs} is locked. We can show that
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1125
  
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1126
  \begin{isabelle}\ \ \ \ \ %%%
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1127
  \begin{tabular}{@ {}l}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1128
  @{thm depend_s}\\
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1129
  @{thm[mode=IfThen] eq_cp}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1130
  \end{tabular}
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1131
  \end{isabelle}
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1132
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1133
  \noindent
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1134
  That means we have to add a waiting edge to the @{text RAG}. Furthermore
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1135
  the current precedence for all threads that are not dependants of @{text th}
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1136
  are unchanged. For the others we need to follow the edges 
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1137
  in the @{text RAG} and recompute the @{term "cp"}. However, like in the 
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1138
  @case of {text Set}, this operation can stop often earlier, namely when intermediate
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1139
  values do not change.
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1140
  *}
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1141
(*<*)
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1142
end
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1143
(*>*)
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1144
text {*
312
09281ccb31bd added implementation section
urbanc
parents: 311
diff changeset
  1145
  \noindent
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1146
  A pleasing result of our formalisation is that the properties in
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1147
  this section closely inform an implementation of PIP:  Whether the
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1148
  @{text RAG} needs to be reconfigured or current precedences need to
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1149
  recalculated for an event is given by a lemma we proved.
311
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1150
*}
23632f329e10 merged Xingyuan's changes
urbanc
parents: 310
diff changeset
  1151
298
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
  1152
section {* Conclusion *}
f2e0d031a395 completed model section; vt has only state as argument
urbanc
parents: 297
diff changeset
  1153
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
  1154
text {* 
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
  1155
  The Priority Inheritance Protocol (PIP) is a classic textbook
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1156
  algorithm used in real-time operating systems in order to avoid the problem of
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1157
  Priority Inversion.  Although classic and widely used, PIP does have
317
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1158
  its faults: for example it does not prevent deadlocks in cases where threads
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1159
  have circular lock dependencies.
300
8524f94d251b correct RAG
urbanc
parents: 299
diff changeset
  1160
317
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1161
  We had two goals in mind with our formalisation of PIP: One is to
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1162
  make the notions in the correctness proof by Sha et al.~\cite{Sha90}
317
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1163
  precise so that they can be processed by a theorem prover. The reason is
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1164
  that a mechanically checked proof avoids the flaws that crept into their
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1165
  informal reasoning. We achieved this goal: The correctness of PIP now
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1166
  only hinges on the assumptions behind our formal model. The reasoning, which is
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
  1167
  sometimes quite intricate and tedious, has been checked beyond any
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1168
  reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1169
  inductive method for protocol verification~\cite{Paulson98} is quite
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1170
  suitable for our formal model and proof. The traditional application
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1171
  area of this method is security protocols.  The only other
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1172
  application of Paulson's method we know of outside this area is
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1173
  \cite{Wang09}.
301
urbanc
parents: 300
diff changeset
  1174
317
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1175
  The second goal of our formalisation is to provide a specification for actually
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1176
  implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1177
  explain how to use various implementations of PIP and abstractly
317
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1178
  discuss their properties, but surprisingly lack most details for a
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1179
  programmer who wants to implement PIP.  That this is an issue in practice is illustrated by the
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1180
  email from Baker we cited in the Introduction. We achieved also this
317
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1181
  goal: The formalisation gives the first author enough data to enable
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1182
  his undergraduate students to implement PIP (as part of their OS course)
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1183
  on top of PINTOS, a small operating system for teaching
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1184
  purposes. A byproduct of our formalisation effort is that nearly all
314
ccb6c0601614 some parts of the conclusion
urbanc
parents: 313
diff changeset
  1185
  design choices for the PIP scheduler are backed up with a proved
317
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1186
  lemma. We were also able to establish the property that the choice of
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1187
  the next thread which takes over a lock is irrelevant for the correctness
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1188
  of PIP. Earlier model checking approaches which verified implementations
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1189
  of PIP \cite{Faria08,Jahier09,Wellings07} cannot
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1190
  provide this kind of ``deep understanding'' about the principles behind 
2d268a0afc07 more conclusion
urbanc
parents: 316
diff changeset
  1191
  PIP and its correctness.
315
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1192
f05f6aeb32f4 more conclusion
urbanc
parents: 314
diff changeset
  1193
  PIP is a scheduling algorithm for single-processor systems. We are
316
0423e4d7c77b more conclusion
urbanc
parents: 315
diff changeset
  1194
  now living in a multi-processor world. So the question naturally
318
b1c3be7ab341 more conclusion
urbanc
parents: 317
diff changeset
  1195
  arises whether PIP has any relevance in such a world beyond
b1c3be7ab341 more conclusion
urbanc
parents: 317
diff changeset
  1196
  teaching. Priority Inversion certainly occurs also in
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1197
  multi-processor systems.  However, the surprising answer, according
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1198
  to \cite{Steinberg10}, is that except for one unsatisfactory
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1199
  proposal nobody has a good idea for how PIP should be modified to
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1200
  work correctly on multi-processor systems. The difficulties become
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1201
  clear when considering that locking and releasing a resource always
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1202
  requires a small amount of time. If processes work independently,
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1203
  then a low priority process can ``steal'' in such an unguarded
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1204
  moment a lock for a resource that was supposed allow a high-priority
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1205
  process to run next. Thus the problem of Priority Inversion is not
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1206
  really prevented. It seems difficult to design a PIP-algorithm with
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1207
  a meaningful correctness property on a multi-processor systems where
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1208
  processes work independently.  We can imagine PIP to be of use in
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1209
  situations where processes are \emph{not} independent, but
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1210
  coordinated via a master process that distributes work over some
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1211
  slave processes. However, a formal investigation of this is beyond
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1212
  the scope of this paper.  We are not aware of any proofs in this
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1213
  area, not even informal ones.
265
993068ce745f changed abstract, intro and IsaMakefile
urbanc
parents: 264
diff changeset
  1214
321
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1215
  The most closely related work to ours is the formal verification in
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1216
  PVS for Priority Ceiling done by Dutertre \cite{dutertre99b}. His formalisation
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1217
  consists of 407 lemmas and 2500 lines of ``specification'' (we do not
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1218
  know whether this includes also code for proofs).  Our formalisation
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1219
  consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1220
  code with a few apply-scripts interspersed. The formal model of PIP
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1221
  is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1222
  definitions and proofs took 770 lines of code. The properties relevant
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1223
  for an implementation took 2000 lines.  Our code can be downloaded from
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1224
  ...
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1225
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1226
  \bibliographystyle{plain}
6a4249608ad0 polished implementation
urbanc
parents: 320
diff changeset
  1227
  \bibliography{root}
262
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
  1228
*}
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
  1229
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
  1230
section {* Key properties \label{extension} *}
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
  1231
264
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1232
(*<*)
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1233
context extend_highest_gen
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1234
begin
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1235
(*>*)
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1236
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1237
text {*
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1238
  The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1239
  purpose, we need to investigate what happens after one thread takes the highest precedence. 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1240
  A locale is used to describe such a situation, which assumes:
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1241
  \begin{enumerate}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1242
  \item @{term "s"} is a valid state (@{text "vt_s"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1243
    @{thm  vt_s}.
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1244
  \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1245
    @{thm threads_s}.
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1246
  \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1247
    @{thm highest}.
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1248
  \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1249
    @{thm preced_th}.
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1250
  \end{enumerate}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1251
  *}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1252
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1253
text {* \noindent
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1254
  Under these assumptions, some basic priority can be derived for @{term "th"}:
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1255
  \begin{enumerate}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1256
  \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1257
    @{thm [display] eq_cp_s_th}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1258
  \item The current precedence of @{term "th"} is the highest precedence in 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1259
    the system (@{text "highest_cp_preced"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1260
    @{thm [display] highest_cp_preced}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1261
  \item The precedence of @{term "th"} is the highest precedence 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1262
    in the system (@{text "highest_preced_thread"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1263
    @{thm [display] highest_preced_thread}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1264
  \item The current precedence of @{term "th"} is the highest current precedence 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1265
    in the system (@{text "highest'"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1266
    @{thm [display] highest'}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1267
  \end{enumerate}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1268
  *}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1269
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1270
text {* \noindent
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1271
  To analysis what happens after state @{term "s"} a sub-locale is defined, which 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1272
  assumes:
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1273
  \begin{enumerate}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1274
  \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1275
  \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1276
    its precedence can not be higher than @{term "th"},  therefore
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1277
    @{term "th"} remain to be the one with the highest precedence
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1278
    (@{text "create_low"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1279
    @{thm [display] create_low}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1280
  \item Any adjustment of priority in 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1281
    @{term "t"} does not happen to @{term "th"} and 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1282
    the priority set is no higher than @{term "prio"}, therefore
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1283
    @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1284
    @{thm [display] set_diff_low}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1285
  \item Since we are investigating what happens to @{term "th"}, it is assumed 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1286
    @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1287
    @{thm [display] exit_diff}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1288
  \end{enumerate}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1289
*}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1290
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1291
text {* \noindent
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1292
  All these assumptions are put into a predicate @{term "extend_highest_gen"}. 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1293
  It can be proved that @{term "extend_highest_gen"} holds 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1294
  for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1295
  @{thm [display] red_moment}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1296
  
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1297
  From this, an induction principle can be derived for @{text "t"}, so that 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1298
  properties already derived for @{term "t"} can be applied to any prefix 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1299
  of @{text "t"} in the proof of new properties 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1300
  about @{term "t"} (@{text "ind"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1301
  \begin{center}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1302
  @{thm[display] ind}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1303
  \end{center}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1304
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1305
  The following properties can be proved about @{term "th"} in @{term "t"}:
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1306
  \begin{enumerate}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1307
  \item In @{term "t"}, thread @{term "th"} is kept live and its 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1308
    precedence is preserved as well
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1309
    (@{text "th_kept"}): 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1310
    @{thm [display] th_kept}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1311
  \item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1312
    all living threads
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1313
    (@{text "max_preced"}): 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1314
    @{thm [display] max_preced}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1315
  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1316
    among all living threads
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1317
    (@{text "th_cp_max_preced"}): 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1318
    @{thm [display] th_cp_max_preced}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1319
  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1320
    precedence among all living threads
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1321
    (@{text "th_cp_max"}): 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1322
    @{thm [display] th_cp_max}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1323
  \item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1324
    @{term "s"}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1325
    (@{text "th_cp_preced"}): 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1326
    @{thm [display] th_cp_preced}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1327
  \end{enumerate}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1328
  *}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1329
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1330
text {* \noindent
266
800b0e3b4204 More explanations added by XY.
zhang
parents: 265
diff changeset
  1331
  The main theorem of this part is to characterizing the running thread during @{term "t"} 
264
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1332
  (@{text "runing_inversion_2"}):
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1333
  @{thm [display] runing_inversion_2}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1334
  According to this, if a thread is running, it is either @{term "th"} or was
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1335
  already live and held some resource 
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1336
  at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1337
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1338
  Since there are only finite many threads live and holding some resource at any moment,
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1339
  if every such thread can release all its resources in finite duration, then after finite
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1340
  duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1341
  then.
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1342
  *}
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1343
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1344
(*<*)
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1345
end
24199eb2c423 Newer version.
zhang
parents: 262
diff changeset
  1346
262
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
  1347
end
4190df6f4488 initial version of the PIP formalisation
urbanc
parents:
diff changeset
  1348
(*>*)