122 permission_check pctxt pctxt C_msgq P_create\<rbrakk> |
122 permission_check pctxt pctxt C_msgq P_create\<rbrakk> |
123 \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" |
123 \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" |
124 | s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
124 | s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
125 permission_check pctxt qctxt C_msgq P_enqueue; |
125 permission_check pctxt qctxt C_msgq P_enqueue; |
126 permission_check pctxt qctxt C_msgq P_write; |
126 permission_check pctxt qctxt C_msgq P_write; |
127 permission_check pctxt pctxt C_msg P_create\<rbrakk> |
127 permission_check pctxt pctxt C_msg P_create; length sms < max_queue\<rbrakk> |
128 \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) |
128 \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) |
129 (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static" |
129 (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static" |
130 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; |
130 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; |
131 S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss; |
131 S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss; |
132 permission_check pctxt qctxt C_msgq P_read; |
132 permission_check pctxt qctxt C_msgq P_read; |