152 and init_files_hung_valid: "\<And> f. f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files \<and> (\<exists> p fd. init_file_of_proc_fd p fd = Some f)" |
152 and init_files_hung_valid: "\<And> f. f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files \<and> (\<exists> p fd. init_file_of_proc_fd p fd = Some f)" |
153 and init_files_hung_valid': "\<And> f im. \<lbrakk>f \<in> init_files_hung_by_del; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> |
153 and init_files_hung_valid': "\<And> f im. \<lbrakk>f \<in> init_files_hung_by_del; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> |
154 init_itag_of_inum im = Some Tag_FILE \<or> (init_itag_of_inum im = Some Tag_DIR \<and> \<not> (\<exists> f'. f' \<in> init_files \<and> f \<prec> f'))" |
154 init_itag_of_inum im = Some Tag_FILE \<or> (init_itag_of_inum im = Some Tag_DIR \<and> \<not> (\<exists> f'. f' \<in> init_files \<and> f \<prec> f'))" |
155 |
155 |
156 and init_procfds_valid: "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)" |
156 and init_procfds_valid: "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)" |
157 and init_filefd_valid: "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)" |
157 and init_filefd_valid: "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags) \<and> (p, fd) \<notin> init_sockets" |
158 and init_fileflag_valid: "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f" |
158 and init_fileflag_valid: "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f" |
159 |
159 |
160 and init_procs_has_shm: "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms \<and> init_flag_of_proc_shm p h = Some flag" |
160 and init_procs_has_shm: "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms \<and> init_flag_of_proc_shm p h = Some flag" |
161 and init_shmflag_has_proc: "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h" |
161 and init_shmflag_has_proc: "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h" |
162 and init_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)" |
162 and init_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)" |
163 and init_msgs_valid: "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs" |
163 and init_msgs_valid: "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs" |
164 |
164 |
165 and init_socket_has_inode: "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p" |
165 and init_socket_has_inode: "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p \<and> init_file_of_proc_fd p fd = None" |
166 and inos_has_sock_tag: "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)" |
166 and inos_has_sock_tag: "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)" |
167 (* |
167 (* |
168 and init_netobj_has_state: "bidirect_in_init init_netobjs init_netobj_state" |
168 and init_netobj_has_state: "bidirect_in_init init_netobjs init_netobj_state" |
169 and init_netobj_has_socktype:"bidirect_in_init init_netobjs init_netobj_socktype" |
169 and init_netobj_has_socktype:"bidirect_in_init init_netobjs init_netobj_socktype" |
170 and init_netobj_has_laddr: "\<And> s. after_bind (init_netobj_state s) \<Longrightarrow> init_netobj_localaddr s \<noteq> None" |
170 and init_netobj_has_laddr: "\<And> s. after_bind (init_netobj_state s) \<Longrightarrow> init_netobj_localaddr s \<noteq> None" |
258 |
258 |
259 definition proc_fd_of_file :: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set" |
259 definition proc_fd_of_file :: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set" |
260 where |
260 where |
261 "proc_fd_of_file \<tau> f = {(p, fd) | p fd. file_of_proc_fd \<tau> p fd = Some f}" |
261 "proc_fd_of_file \<tau> f = {(p, fd) | p fd. file_of_proc_fd \<tau> p fd = Some f}" |
262 |
262 |
|
263 definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set" |
|
264 where |
|
265 "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}" |
|
266 |
|
267 definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set" |
|
268 where |
|
269 "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}" |
263 |
270 |
264 (****** files and directories ******) |
271 (****** files and directories ******) |
265 |
272 |
266 fun files_hung_by_del :: "t_state \<Rightarrow> t_file set" |
273 fun files_hung_by_del :: "t_state \<Rightarrow> t_file set" |
267 where |
274 where |
799 *) |
806 *) |
800 | "deleted obj (RemoveMsgq p q # s) = (obj = O_msgq q \<or> (\<exists> m. obj = O_msg q m) \<or> deleted obj s)" |
807 | "deleted obj (RemoveMsgq p q # s) = (obj = O_msgq q \<or> (\<exists> m. obj = O_msg q m) \<or> deleted obj s)" |
801 | "deleted obj (DeleteShM p h # s) = (obj = O_shm h \<or> deleted obj s)" |
808 | "deleted obj (DeleteShM p h # s) = (obj = O_shm h \<or> deleted obj s)" |
802 | "deleted obj (RecvMsg p q m # s) = (obj = O_msg q m \<or> deleted obj s)" |
809 | "deleted obj (RecvMsg p q m # s) = (obj = O_msg q m \<or> deleted obj s)" |
803 | "deleted obj (_ # s) = deleted obj s" |
810 | "deleted obj (_ # s) = deleted obj s" |
804 |
|
805 |
|
806 definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set" |
|
807 where |
|
808 "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}" |
|
809 |
|
810 |
|
811 definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set" |
|
812 where |
|
813 "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}" |
|
814 |
811 |
815 end |
812 end |
816 |
813 |
817 |
814 |
818 |
815 |