1 theory Implementation |
1 theory Implementation |
2 imports PIPBasics |
2 imports PIPBasics |
3 begin |
3 begin |
4 |
4 |
|
5 section {* |
|
6 This file contains lemmas used to guide the recalculation of current precedence |
|
7 after every step of execution (or system operation, or event), |
|
8 which is the most tricky part in the implementation of PIP. |
|
9 |
|
10 Following convention, lemmas are grouped into locales corresponding to |
|
11 system operations, each explained in a separate section. |
|
12 *} |
|
13 |
|
14 text {* |
|
15 The following two lemmas are general about any valid system state, |
|
16 but are used in the derivation in more specific system operations. |
|
17 *} |
5 |
18 |
6 context valid_trace |
19 context valid_trace |
7 begin |
20 begin |
8 |
21 |
9 lemma readys_root: |
22 lemma readys_root: |
37 show ?thesis by (auto simp:root_def) |
50 show ?thesis by (auto simp:root_def) |
38 qed |
51 qed |
39 qed |
52 qed |
40 |
53 |
41 end |
54 end |
42 |
|
43 section {* |
|
44 This file contains lemmas used to guide the recalculation of current precedence |
|
45 after every system call (or system operation) |
|
46 *} |
|
47 |
|
48 text {* (* ddd *) |
|
49 One beauty of our modelling is that we follow the definitional extension tradition of HOL. |
|
50 The benefit of such a concise and miniature model is that large number of intuitively |
|
51 obvious facts are derived as lemmas, rather than asserted as axioms. |
|
52 *} |
|
53 |
|
54 text {* |
|
55 However, the lemmas in the forthcoming several locales are no longer |
|
56 obvious. These lemmas show how the current precedences should be recalculated |
|
57 after every execution step (in our model, every step is represented by an event, |
|
58 which in turn, represents a system call, or operation). Each operation is |
|
59 treated in a separate locale. |
|
60 |
|
61 The complication of current precedence recalculation comes |
|
62 because the changing of RAG needs to be taken into account, |
|
63 in addition to the changing of precedence. |
|
64 |
|
65 The reason RAG changing affects current precedence is that, |
|
66 according to the definition, current precedence |
|
67 of a thread is the maximum of the precedences of every threads in its subtree, |
|
68 where the notion of sub-tree in RAG is defined in RTree.thy. |
|
69 |
|
70 Therefore, for each operation, lemmas about the change of precedences |
|
71 and RAG are derived first, on which lemmas about current precedence |
|
72 recalculation are based on. |
|
73 *} |
|
74 |
55 |
75 section {* The @{term Set} operation *} |
56 section {* The @{term Set} operation *} |
76 |
57 |
77 context valid_trace_set |
58 context valid_trace_set |
78 begin |
59 begin |