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 (* |
476 inductive info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
477 inductive info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
477 where |
478 where |
478 "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p" |
479 "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 | "\<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 \<Longrightarrow> info_flow_shm s p p''" |
481 (* |
482 *) |
|
483 definition one_flow_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
|
484 where |
|
485 "one_flow_shm s h from to \<equiv> (from, SHM_RDWR) \<in> procs_of_shm s h \<and> (\<exists> flag. (to, flag) \<in> procs_of_shm s h)" |
|
486 |
|
487 fun self_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
|
488 where |
|
489 "self_shm s p p' = (p = p' \<and> p' \<in> current_procs s)" |
|
490 |
482 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
491 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
483 where |
492 where |
484 "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. |
493 "info_flow_shm s from to \<equiv> (self_shm s from to) \<or> (\<exists> h. one_flow_shm s h from to)" |
485 (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" |
494 |
486 *) |
|
487 |
495 |
488 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
496 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
489 where |
497 where |
490 "current_msgqs [] = init_msgqs" |
498 "current_msgqs [] = init_msgqs" |
491 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)" |
499 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)" |