360 |
358 |
361 \begin{isabelle}\ \ \ \ \ %%% |
359 \begin{isabelle}\ \ \ \ \ %%% |
362 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"} |
360 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"} |
363 \end{isabelle} |
361 \end{isabelle} |
364 |
362 |
|
363 \noindent |
|
364 We have the usual getter and setter methods for such records. |
|
365 |
365 In the initial state, the scheduler starts with all resources unlocked and the |
366 In the initial state, the scheduler starts with all resources unlocked and the |
366 precedence of every thread is initialised with @{term "Prc 0 0"}. |
367 precedence of every thread is initialised with @{term "Prc 0 0"}. |
367 |
368 |
368 \begin{isabelle}\ \ \ \ \ %%% |
369 \begin{isabelle}\ \ \ \ \ %%% |
369 \begin{tabular}{@ {}l} |
370 \begin{tabular}{@ {}l} |
370 @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ |
371 @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ |
371 \hspace{5mm}@{term "(|waiting_queue = all_unlocked, cur_preced = (\<lambda>_::thread. Prc 0 0)|)"} |
372 \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"} |
372 \end{tabular} |
373 \end{tabular} |
373 \end{isabelle} |
374 \end{isabelle} |
374 |
375 |
375 \noindent |
376 \noindent |
376 The cases for @{term Create}, @{term Exit} and @{term Set} are straightforward: |
377 The cases for @{term Create}, @{term Exit} and @{term Set} are straightforward: |
380 This gives the following clauses: |
381 This gives the following clauses: |
381 |
382 |
382 \begin{isabelle}\ \ \ \ \ %%% |
383 \begin{isabelle}\ \ \ \ \ %%% |
383 \begin{tabular}{@ {}l} |
384 \begin{tabular}{@ {}l} |
384 @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ |
385 @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ |
385 \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ |
386 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
386 \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Create th prio # s)|)"}\\ |
387 \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\\ |
387 @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\ |
388 @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\ |
388 \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ |
389 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
389 \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\ |
390 \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\ |
390 @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ |
391 @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ |
391 \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ |
392 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
392 \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Set th prio # s)|)"} |
393 \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"} |
393 \end{tabular} |
394 \end{tabular} |
394 \end{isabelle} |
395 \end{isabelle} |
395 |
396 |
396 \noindent |
397 \noindent |
397 More interesting are the cases when a resource, say @{text cs}, is locked or relaesed. In this case |
398 More interesting are the cases when a resource, say @{text cs}, is locked or relaesed. In this case |
401 resource). |
402 resource). |
402 |
403 |
403 \begin{isabelle}\ \ \ \ \ %%% |
404 \begin{isabelle}\ \ \ \ \ %%% |
404 \begin{tabular}{@ {}l} |
405 \begin{tabular}{@ {}l} |
405 @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ |
406 @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ |
406 \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ |
407 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
407 \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\ |
408 \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\ |
408 \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|)"} |
409 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"} |
409 \end{tabular} |
410 \end{tabular} |
410 \end{isabelle} |
411 \end{isabelle} |
411 |
412 |
412 \noindent |
413 \noindent |
413 The case for @{term V} is similarly, except that we update the waiting queue function |
414 The case for @{term V} is similarly, except that we update the waiting queue function |
421 This gives for @{term schs} the clause: |
422 This gives for @{term schs} the clause: |
422 |
423 |
423 \begin{isabelle}\ \ \ \ \ %%% |
424 \begin{isabelle}\ \ \ \ \ %%% |
424 \begin{tabular}{@ {}l} |
425 \begin{tabular}{@ {}l} |
425 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\ |
426 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\ |
426 \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\ |
427 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
427 \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\ |
428 \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\ |
428 \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|)"} |
429 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"} |
429 \end{tabular} |
430 \end{tabular} |
430 \end{isabelle} |
431 \end{isabelle} |
431 |
432 |
432 |
433 |
433 TODO |
434 TODO |