471 (\<lambda> h. (procs_of_shm s h) - {(p', flag) | flag. (p', flag) \<in> procs_of_shm s h})" |
471 (\<lambda> h. (procs_of_shm s h) - {(p', flag) | flag. (p', flag) \<in> procs_of_shm s h})" |
472 | "procs_of_shm (Exit p # s) = |
472 | "procs_of_shm (Exit p # s) = |
473 (\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})" |
473 (\<lambda> h. (procs_of_shm s h) - {(p, flag) | flag. (p, flag) \<in> procs_of_shm s h})" |
474 | "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>" |
474 | "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>" |
475 |
475 |
|
476 inductive info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
|
477 where |
|
478 "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p" |
|
479 | "\<lbrakk>info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h; p' \<noteq> p''\<rbrakk> |
|
480 \<Longrightarrow> info_flow_shm s p p''" |
|
481 (* |
476 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
482 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
477 where |
483 where |
478 "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. |
484 "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. |
479 (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" |
485 (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" |
|
486 *) |
480 |
487 |
481 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
488 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
482 where |
489 where |
483 "current_msgqs [] = init_msgqs" |
490 "current_msgqs [] = init_msgqs" |
484 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)" |
491 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)" |