47 "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)" |
47 "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)" |
48 using not_deleted_init_proc by auto |
48 using not_deleted_init_proc by auto |
49 |
49 |
50 lemma info_shm_flow_in_procs: |
50 lemma info_shm_flow_in_procs: |
51 "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s" |
51 "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s" |
52 by (auto simp:info_flow_shm_def intro:procs_of_shm_prop2) |
52 apply (induct rule:info_flow_shm.induct ) |
|
53 by (auto intro:procs_of_shm_prop2) |
|
54 |
|
55 (*********** simpset for info_flow_shm **************) |
|
56 |
|
57 lemma info_flow_shm_prop1: |
|
58 "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> |
|
59 \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'" |
|
60 by (induct rule: info_flow_shm.induct, auto) |
|
61 |
|
62 lemma info_flow_shm_cases: |
|
63 "\<lbrakk>info_flow_shm \<tau> pa pb; \<And>p s. \<lbrakk>s = \<tau> ; pa = p; pb = p; p \<in> current_procs s\<rbrakk> \<Longrightarrow> P; |
|
64 \<And>s p p' h p'' flag. \<lbrakk>s = \<tau>; pa = p; pb = p''; info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; |
|
65 (p'', flag) \<in> procs_of_shm s h\<rbrakk>\<Longrightarrow> P\<rbrakk> |
|
66 \<Longrightarrow> P" |
|
67 by (erule info_flow_shm.cases, auto) |
|
68 |
|
69 definition one_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
|
70 where |
|
71 "one_flow_shm s p p' \<equiv> p \<noteq> p' \<and> (\<exists> h flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h)" |
|
72 |
|
73 inductive flows_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
|
74 where |
|
75 "p \<in> current_procs s \<Longrightarrow> flows_shm s p p" |
|
76 | "\<lbrakk>flows_shm s p p'; one_flow_shm s p' p''\<rbrakk> \<Longrightarrow> flows_shm s p p''" |
|
77 |
|
78 definition attached_procs :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set" |
|
79 where |
|
80 "attached_procs s h \<equiv> {p. \<exists> flag. (p, flag) \<in> procs_of_shm s h}" |
|
81 |
|
82 definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set" |
|
83 where |
|
84 "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}" |
|
85 |
|
86 fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set" |
|
87 where |
|
88 "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})" |
|
89 | "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. if (p' = p) then {p''. \<exists> }" |
|
90 |
|
91 |
|
92 lemma info_flow_shm_attach: |
|
93 "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or> |
|
94 (if (pa = p) |
|
95 then (if (flag = SHM_RDWR) |
|
96 then (\<exists> flag. (pb, flag) \<in> procs_of_shm s h) |
|
97 else (pb = p)) |
|
98 else (if (pb = p) |
|
99 then (pa, SHM_RDWR) \<in> procs_of_shm s h |
|
100 else info_flow_shm s pa pb)) )" |
|
101 apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext) |
|
102 apply (case_tac "info_flow_shm s pa pb", simp) |
|
103 |
|
104 thm info_flow_shm.cases |
|
105 apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases) |
|
106 apply (erule info_flow_shm_cases, simp, simp split:if_splits) |
|
107 apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+) |
|
108 apply (rule notI, erule info_flow_shm.cases, simp+) |
|
109 pr 5 |
|
110 |
|
111 lemmas info_flow_shm_simps = info_flow_shm_other |
53 |
112 |
54 lemma has_same_inode_in_current: |
113 lemma has_same_inode_in_current: |
55 "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s" |
114 "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s" |
56 by (auto simp add:has_same_inode_def current_files_def) |
115 by (auto simp add:has_same_inode_def current_files_def) |
57 |
116 |