137 |
137 |
138 and init_msgqs :: "t_msgq set" |
138 and init_msgqs :: "t_msgq set" |
139 and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list" |
139 and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list" |
140 and init_shms :: "t_shm set" |
140 and init_shms :: "t_shm set" |
141 and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" |
141 and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" |
|
142 and init_flag_of_proc_shm :: "t_process \<Rightarrow> t_shm \<rightharpoonup> t_shm_attach_flag" |
142 |
143 |
143 assumes |
144 assumes |
144 parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files" |
145 parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files" |
145 and root_is_dir: "\<exists> i. init_inum_of_file [] = Some i \<and> init_itag_of_inum i = Some Tag_DIR" |
146 and root_is_dir: "\<exists> i. init_inum_of_file [] = Some i \<and> init_itag_of_inum i = Some Tag_DIR" |
146 and init_file_has_inum: "\<And> f. f \<in> init_files \<Longrightarrow> \<exists> im. init_inum_of_file f = Some im" |
147 and init_file_has_inum: "\<And> f. f \<in> init_files \<Longrightarrow> \<exists> im. init_inum_of_file f = Some im" |
154 |
155 |
155 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)" |
156 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)" |
157 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" |
158 |
159 |
159 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" |
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_procshm_valid: "\<And> p h flag flag'. \<lbrakk>(p,flag) \<in> init_procs_of_shm h; (p, flag') \<in> init_procs_of_shm h\<rbrakk> \<Longrightarrow> flag = 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_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)" |
162 and init_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)" |
162 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" |
163 |
164 |
164 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" |
165 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)" |
425 "current_shms [] = init_shms" |
426 "current_shms [] = init_shms" |
426 | "current_shms (CreateShM p newshm # \<tau>) = insert newshm (current_shms \<tau>)" |
427 | "current_shms (CreateShM p newshm # \<tau>) = insert newshm (current_shms \<tau>)" |
427 | "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}" |
428 | "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}" |
428 | "current_shms (e # \<tau>) = current_shms \<tau> " |
429 | "current_shms (e # \<tau>) = current_shms \<tau> " |
429 |
430 |
430 fun procs_of_shm : "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" |
431 fun flag_of_proc_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag option" |
|
432 where |
|
433 "flag_of_proc_shm [] = init_flag_of_proc_shm" |
|
434 | "flag_of_proc_shm (Attach p h flag # s) = (\<lambda> p' h'. |
|
435 if (p' = p \<and> h' = h) then Some flag else flag_of_proc_shm s p' h')" |
|
436 | "flag_of_proc_shm (Detach p h # s) = (\<lambda> p' h'. |
|
437 if (p' = p \<and> h' = h) then None else flag_of_proc_shm s p' h')" |
|
438 | "flag_of_proc_shm (CreateShM p h # s) = (\<lambda> p' h'. |
|
439 if (h' = h) then None else flag_of_proc_shm s p' h')" |
|
440 | "flag_of_proc_shm (DeleteShM p h # s) = (\<lambda> p' h'. |
|
441 if (h' = h) then None else flag_of_proc_shm s p' h')" |
|
442 | "flag_of_proc_shm (Clone p p' fds shms # s) = (\<lambda> p'' h. |
|
443 if (p'' = p' \<and> h \<in> shms) then flag_of_proc_shm s p h |
|
444 else if (p'' = p') then None |
|
445 else flag_of_proc_shm s p'' h)" |
|
446 | "flag_of_proc_shm (Execve p f fds # s) = (\<lambda> p' h. |
|
447 if (p' = p) then None else flag_of_proc_shm s p' h)" |
|
448 | "flag_of_proc_shm (Kill p p' # s) = (\<lambda> p'' h. |
|
449 if (p'' = p') then None else flag_of_proc_shm s p'' h)" |
|
450 | "flag_of_proc_shm (Exit p # s) = (\<lambda> p' h. |
|
451 if (p' = p) then None else flag_of_proc_shm s p' h)" |
|
452 | "flag_of_proc_shm (e # s) = flag_of_proc_shm s" |
|
453 |
|
454 fun procs_of_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" |
431 where |
455 where |
432 "procs_of_shm [] = init_procs_of_shm" |
456 "procs_of_shm [] = init_procs_of_shm" |
433 | "procs_of_shm (CreateShM p h # \<tau>) = |
457 | "procs_of_shm (CreateShM p h # \<tau>) = |
434 (procs_of_shm \<tau>) (h := {})" (* creator may not be the sharer of the shm *) |
458 (procs_of_shm \<tau>) (h := {})" (* creator may not be the sharer of the shm *) |
435 | "procs_of_shm (Attach p h flag # \<tau>) = |
459 | "procs_of_shm (Attach p h flag # \<tau>) = |