590 (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static" |
590 (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static" |
591 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
591 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
592 S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss; |
592 S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss; |
593 permission_check pctxt qctxt C_msgq P_read; |
593 permission_check pctxt qctxt C_msgq P_read; |
594 permission_check pctxt mctxt C_msg P_receive\<rbrakk> |
594 permission_check pctxt mctxt C_msg P_receive\<rbrakk> |
595 \<Longrightarrow> (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) \<in> static" |
595 \<Longrightarrow> (update_ss (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) |
|
596 (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms)) |
|
597 (S_msgq (qi, qctxt, sms))) \<in> static" |
596 | s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
598 | s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
597 permission_check pctxt qctxt C_msgq P_destroy\<rbrakk> |
599 permission_check pctxt qctxt C_msgq P_destroy\<rbrakk> |
598 \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static" |
600 \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static" |
599 | s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
601 | s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
600 permission_check pctxt pctxt C_shm P_associate; |
602 permission_check pctxt pctxt C_shm P_associate; |
784 | _ \<Rightarrow> None)" |
786 | _ \<Rightarrow> None)" |
785 | "co2sobj s (O_shm h) = |
787 | "co2sobj s (O_shm h) = |
786 (case (ch2sshm s h) of |
788 (case (ch2sshm s h) of |
787 Some sh \<Rightarrow> Some (S_shm sh) |
789 Some sh \<Rightarrow> Some (S_shm sh) |
788 | _ \<Rightarrow> None)" |
790 | _ \<Rightarrow> None)" |
|
791 (* |
789 | "co2sobj s (O_msg q m) = |
792 | "co2sobj s (O_msg q m) = |
790 (case (cq2smsgq s q, cm2smsg s q m) of |
793 (case (cq2smsgq s q, cm2smsg s q m) of |
791 (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm) |
794 (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm) |
792 | _ \<Rightarrow> None)" |
795 | _ \<Rightarrow> None)" |
|
796 *) |
793 | "co2sobj s _ = None" |
797 | "co2sobj s _ = None" |
794 |
798 |
795 |
799 |
796 (***************** for backward proof when Instancing static objects ******************) |
800 (***************** for backward proof when Instancing static objects ******************) |
797 |
801 |