equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 type_synonym thread = nat -- {* Type for thread identifiers. *} |
5 type_synonym thread = nat -- {* Type for thread identifiers. *} |
6 type_synonym priority = nat -- {* Type for priorities. *} |
6 type_synonym priority = nat -- {* Type for priorities. *} |
7 type_synonym cs = nat -- {* Type for critical sections (or resources). *} |
7 type_synonym cs = nat -- {* Type for critical sections (or resources). *} |
|
8 |
|
9 -- {* Schedulling Events *} |
8 |
10 |
9 datatype event = |
11 datatype event = |
10 Create thread priority |
12 Create thread priority |
11 | Exit thread |
13 | Exit thread |
12 | P thread cs |
14 | P thread cs |
34 "last_set th [] = 0" |
36 "last_set th [] = 0" |
35 | "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)" |
37 | "last_set th ((Create th' prio)#s) = (if (th = th') then length s else last_set th s)" |
36 | "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" |
38 | "last_set th ((Set th' prio)#s) = (if (th = th') then length s else last_set th s)" |
37 | "last_set th (_#s) = last_set th s" |
39 | "last_set th (_#s) = last_set th s" |
38 |
40 |
|
41 |
39 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence" |
42 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence" |
40 where "preced th s \<equiv> Prc (priority th s) (last_set th s)" |
43 where "preced th s \<equiv> Prc (priority th s) (last_set th s)" |
41 |
44 |
42 abbreviation |
45 abbreviation |
43 "preceds s ths \<equiv> {preced th s | th. th \<in> ths}" |
46 "preceds s ths \<equiv> {preced th s | th. th \<in> ths}" |
46 "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)" |
49 "holds wq th cs \<equiv> th \<in> set (wq cs) \<and> th = hd (wq cs)" |
47 |
50 |
48 definition |
51 definition |
49 "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)" |
52 "waits wq th cs \<equiv> th \<in> set (wq cs) \<and> th \<noteq> hd (wq cs)" |
50 |
53 |
|
54 --{* Nodes in Resource Graph *} |
51 datatype node = |
55 datatype node = |
52 Th "thread" |
56 Th "thread" |
53 | Cs "cs" |
57 | Cs "cs" |
54 |
58 |
55 definition |
59 definition |
81 "(SOME q. distinct q \<and> q = []) = []" |
85 "(SOME q. distinct q \<and> q = []) = []" |
82 by auto |
86 by auto |
83 |
87 |
84 lemma [simp]: |
88 lemma [simp]: |
85 "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)" |
89 "(x \<in> set (SOME q. distinct q \<and> set q = set p)) = (x \<in> set p)" |
86 apply(auto) |
90 apply(rule iffI) |
87 apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) |
91 apply (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex)+ |
88 by (metis (mono_tags, lifting) List.finite_set finite_distinct_list some_eq_ex) |
92 done |
89 |
93 |
90 abbreviation |
94 abbreviation |
91 "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)" |
95 "next_to_run ths \<equiv> hd (SOME q::thread list. distinct q \<and> set q = set ths)" |
92 |
96 |
93 |
97 |