1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7chapter "Abstract Specification Instantiations" 8 9theory Deterministic_A 10imports 11 Structures_A 12 "Lib.List_Lib" 13 14begin 15 16text \<open> 17\label{c:ext-spec} 18 19The kernel specification operates over states of type @{typ "'a state"}, which 20includes all of the abstract kernel state plus an extra field, @{term exst} 21of type @{typ "'a"}. By choosing an appropriate concrete type for @{typ "'a"}, 22we obtain different \emph{instantiations} of this specification, at differing 23levels of abstraction. The abstract specification is thus \emph{extensible}. 24The basic technique, and its motivation, are described in~\cite{Matichuk_Murray_12}. 25 26Here, we define two such instantiations. The first yields a 27largely-deterministic specification by instantiating @{typ "'a"} with 28a record that includes concrete scheduler state and 29information about sibling ordering in the capability derivation tree (CDT). 30We call the resulting 31specification the \emph{deterministic abstract specification} and it is 32defined below in \autoref{s:det-spec}. 33 34The second instantiation uses the type @{typ unit} for @{typ 'a}, yielding 35a specification that is far more nondeterministic. In particular, the 36scheduling behaviour and the order in which capabilities are deleted during 37a \emph{revoke} system call both become completely nondeterministic. 38We call this second instantiation the 39\emph{nondeterministic abstract specification} and it is defined below in 40\autoref{s:nondet-spec}. 41\<close> 42 43text \<open>Translate a state of type @{typ "'a state"} to one of type @{typ "'b state"} 44 via a function @{term t} from @{typ "'a"} to @{typ "'b"}. 45\<close> 46definition trans_state :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a state \<Rightarrow> 'b state" where 47"trans_state t s = \<lparr>kheap = kheap s, cdt = cdt s, is_original_cap = is_original_cap s, 48 cur_thread = cur_thread s, idle_thread = idle_thread s, 49 machine_state = machine_state s, 50 interrupt_irq_node = interrupt_irq_node s, 51 interrupt_states = interrupt_states s, arch_state = arch_state s, 52 exst = t(exst s)\<rparr>" 53 54(*<*) 55lemma trans_state[simp]: "kheap (trans_state t s) = kheap s" 56 "cdt (trans_state t s) = cdt s" 57 "is_original_cap (trans_state t s) = is_original_cap s" 58 "cur_thread (trans_state t s) = cur_thread s" 59 "idle_thread (trans_state t s) = idle_thread s" 60 "machine_state (trans_state t s) = machine_state s" 61 "interrupt_irq_node (trans_state t s) = interrupt_irq_node s" 62 "interrupt_states (trans_state t s) = interrupt_states s" 63 "arch_state (trans_state t s) = arch_state s" 64 "exst (trans_state t s) = (t (exst s))" 65 "exst (trans_state (\<lambda>_. e) s) = e" 66 apply (simp add: trans_state_def)+ 67 done 68 69lemma trans_state_update[simp]: 70 "trans_state t (kheap_update f s) = kheap_update f (trans_state t s)" 71 "trans_state t (cdt_update g s) = cdt_update g (trans_state t s)" 72 "trans_state t (is_original_cap_update h s) = is_original_cap_update h (trans_state t s)" 73 "trans_state t (cur_thread_update i s) = cur_thread_update i (trans_state t s)" 74 "trans_state t (idle_thread_update j s) = idle_thread_update j (trans_state t s)" 75 "trans_state t (machine_state_update k s) = machine_state_update k (trans_state t s)" 76 "trans_state t (interrupt_irq_node_update l s) = interrupt_irq_node_update l (trans_state t s)" 77 "trans_state t (arch_state_update m s) = arch_state_update m (trans_state t s)" 78 "trans_state t (interrupt_states_update p s) = interrupt_states_update p (trans_state t s)" 79 apply (simp add: trans_state_def)+ 80 done 81 82 83lemma trans_state_update': 84 "trans_state f = exst_update f" 85 apply (rule ext) 86 apply simp 87 done 88 89lemma trans_state_update''[simp]: 90 "trans_state t' (trans_state t s) = trans_state (\<lambda>e. t' (t e)) s" 91 apply simp 92 done 93(*>*) 94 95text \<open>Truncate an extended state of type @{typ "'a state"} 96 by effectively throwing away all the @{typ "'a"} information. 97\<close> 98abbreviation "truncate_state \<equiv> trans_state (\<lambda>_. ())" 99 100section "Deterministic Abstract Specification" 101 102text \<open>\label{s:det-spec} 103 The deterministic abstract specification tracks the state of the scheduler 104and ordering information about sibling nodes in the CDT.\<close> 105 106text \<open>The current scheduler action, 107 which is part of the scheduling state.\<close> 108datatype scheduler_action = 109 resume_cur_thread 110 | switch_thread obj_ref 111 | choose_new_thread 112 113type_synonym domain = word8 114 115record etcb = 116 tcb_priority :: "priority" 117 tcb_time_slice :: "nat" 118 tcb_domain :: "domain" 119 120definition num_domains :: nat where 121 "num_domains \<equiv> 16" 122 123definition time_slice :: "nat" where 124 "time_slice \<equiv> 5" 125 126definition default_priority :: "priority" where 127 "default_priority \<equiv> minBound" 128 129definition default_domain :: "domain" where 130 "default_domain \<equiv> minBound" 131 132definition default_etcb :: "etcb" where 133 "default_etcb \<equiv> \<lparr>tcb_priority = default_priority, tcb_time_slice = time_slice, tcb_domain = default_domain\<rparr>" 134 135type_synonym ready_queue = "obj_ref list" 136 137text \<open> 138 For each entry in the CDT, we record an ordered list of its children. 139 This encodes the order of sibling nodes in the CDT. 140\<close> 141type_synonym cdt_list = "cslot_ptr \<Rightarrow> cslot_ptr list" 142 143definition work_units_limit :: "machine_word" where 144 "work_units_limit = 0x64" 145text \<open> 146 The extended state of the deterministic abstract specification. 147\<close> 148record det_ext = 149 work_units_completed_internal :: "machine_word" 150 scheduler_action_internal :: scheduler_action 151 ekheap_internal :: "obj_ref \<Rightarrow> etcb option" 152 domain_list_internal :: "(domain \<times> machine_word) list" 153 domain_index_internal :: nat 154 cur_domain_internal :: domain 155 domain_time_internal :: "machine_word" 156 ready_queues_internal :: "domain \<Rightarrow> priority \<Rightarrow> ready_queue" 157 cdt_list_internal :: cdt_list 158 159text \<open> 160 The state of the deterministic abstract specification extends the 161 abstract state with the @{typ det_ext} record. 162\<close> 163type_synonym det_state = "det_ext state" 164 165text \<open>Accessor and update functions for the extended state of the 166 deterministic abstract specification. 167\<close> 168abbreviation 169 "work_units_completed (s::det_state) \<equiv> work_units_completed_internal (exst s)" 170 171abbreviation 172 "work_units_completed_update f (s::det_state) \<equiv> trans_state (work_units_completed_internal_update f) s" 173 174abbreviation 175 "scheduler_action (s::det_state) \<equiv> scheduler_action_internal (exst s)" 176 177abbreviation 178 "scheduler_action_update f (s::det_state) \<equiv> trans_state (scheduler_action_internal_update f) s" 179 180abbreviation 181 "ekheap (s::det_state) \<equiv> ekheap_internal (exst s)" 182 183abbreviation 184 "ekheap_update f (s::det_state) \<equiv> trans_state (ekheap_internal_update f) s" 185 186abbreviation 187 "domain_list (s::det_state) \<equiv> domain_list_internal (exst s)" 188 189abbreviation 190 "domain_list_update f (s::det_state) \<equiv> trans_state (domain_list_internal_update f) s" 191 192abbreviation 193 "domain_index (s::det_state) \<equiv> domain_index_internal (exst s)" 194 195abbreviation 196 "domain_index_update f (s::det_state) \<equiv> trans_state (domain_index_internal_update f) s" 197 198abbreviation 199 "cur_domain (s::det_state) \<equiv> cur_domain_internal (exst s)" 200 201abbreviation 202 "cur_domain_update f (s::det_state) \<equiv> trans_state (cur_domain_internal_update f) s" 203 204abbreviation 205 "domain_time (s::det_state) \<equiv> domain_time_internal (exst s)" 206 207abbreviation 208 "domain_time_update f (s::det_state) \<equiv> trans_state (domain_time_internal_update f) s" 209 210abbreviation 211 "ready_queues (s::det_state) \<equiv> ready_queues_internal (exst s)" 212 213abbreviation 214 "ready_queues_update f (s::det_state) \<equiv> trans_state (ready_queues_internal_update f) s" 215 216abbreviation 217 "cdt_list (s::det_state) \<equiv> cdt_list_internal (exst s)" 218 219abbreviation 220 "cdt_list_update f (s::det_state) \<equiv> trans_state (cdt_list_internal_update f) s" 221 222type_synonym 'a det_ext_monad = "(det_state,'a) nondet_monad" 223 224text \<open> 225 Basic monadic functions for operating on the extended state of the 226 deterministic abstract specification. 227\<close> 228definition 229 get_etcb :: "obj_ref \<Rightarrow> det_state \<Rightarrow> etcb option" 230where 231 "get_etcb tcb_ref es \<equiv> ekheap es tcb_ref" 232 233definition 234 ethread_get :: "(etcb \<Rightarrow> 'a) \<Rightarrow> obj_ref \<Rightarrow> 'a det_ext_monad" 235where 236 "ethread_get f tptr \<equiv> do 237 tcb \<leftarrow> gets_the $ get_etcb tptr; 238 return $ f tcb 239 od" 240 241(* For infoflow, we want to avoid certain read actions, such as reading the priority of the 242 current thread when it could be idle. Then we need to make sure we do not rely on the result. 243 undefined is the closest we have to a result that can't be relied on *) 244definition 245 ethread_get_when :: "bool \<Rightarrow> (etcb \<Rightarrow> 'a) \<Rightarrow> obj_ref \<Rightarrow> 'a det_ext_monad" 246where 247 "ethread_get_when b f tptr \<equiv> if b then (ethread_get f tptr) else return undefined" 248 249definition set_eobject :: "obj_ref \<Rightarrow> etcb \<Rightarrow> unit det_ext_monad" 250 where 251 "set_eobject ptr obj \<equiv> 252 do es \<leftarrow> get; 253 ekh \<leftarrow> return $ ekheap es(ptr \<mapsto> obj); 254 put (es\<lparr>ekheap := ekh\<rparr>) 255 od" 256 257definition 258 ethread_set :: "(etcb \<Rightarrow> etcb) \<Rightarrow> obj_ref \<Rightarrow> unit det_ext_monad" 259where 260 "ethread_set f tptr \<equiv> do 261 tcb \<leftarrow> gets_the $ get_etcb tptr; 262 set_eobject tptr $ f tcb 263 od" 264 265definition 266 set_scheduler_action :: "scheduler_action \<Rightarrow> unit det_ext_monad" where 267 "set_scheduler_action action \<equiv> 268 modify (\<lambda>es. es\<lparr>scheduler_action := action\<rparr>)" 269 270definition 271 thread_set_priority :: "obj_ref \<Rightarrow> priority \<Rightarrow> unit det_ext_monad" where 272 "thread_set_priority tptr prio \<equiv> ethread_set (\<lambda>tcb. tcb\<lparr>tcb_priority := prio\<rparr>) tptr" 273 274definition 275 thread_set_time_slice :: "obj_ref \<Rightarrow> nat \<Rightarrow> unit det_ext_monad" where 276 "thread_set_time_slice tptr time \<equiv> ethread_set (\<lambda>tcb. tcb\<lparr>tcb_time_slice := time\<rparr>) tptr" 277 278definition 279 thread_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where 280 "thread_set_domain tptr domain \<equiv> ethread_set (\<lambda>tcb. tcb\<lparr>tcb_domain := domain\<rparr>) tptr" 281 282 283definition 284 get_tcb_queue :: "domain \<Rightarrow> priority \<Rightarrow> ready_queue det_ext_monad" where 285 "get_tcb_queue d prio \<equiv> do 286 queues \<leftarrow> gets ready_queues; 287 return (queues d prio) 288 od" 289 290definition 291 set_tcb_queue :: "domain \<Rightarrow> priority \<Rightarrow> ready_queue \<Rightarrow> unit det_ext_monad" where 292 "set_tcb_queue d prio queue \<equiv> 293 modify (\<lambda>es. es\<lparr> ready_queues := 294 (\<lambda>d' p. if d' = d \<and> p = prio then queue else ready_queues es d' p)\<rparr>)" 295 296 297definition 298 tcb_sched_action :: "(obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list) \<Rightarrow> obj_ref \<Rightarrow> unit det_ext_monad" where 299 "tcb_sched_action action thread \<equiv> do 300 d \<leftarrow> ethread_get tcb_domain thread; 301 prio \<leftarrow> ethread_get tcb_priority thread; 302 queue \<leftarrow> get_tcb_queue d prio; 303 set_tcb_queue d prio (action thread queue) 304 od" 305 306definition 307 tcb_sched_enqueue :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where 308 "tcb_sched_enqueue thread queue \<equiv> if (thread \<notin> set queue) then thread # queue else queue" 309 310definition 311 tcb_sched_append :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where 312 "tcb_sched_append thread queue \<equiv> if (thread \<notin> set queue) then queue @ [thread] else queue" 313 314definition 315 tcb_sched_dequeue :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where 316 "tcb_sched_dequeue thread queue \<equiv> filter (\<lambda>x. x \<noteq> thread) queue" 317 318 319definition reschedule_required :: "unit det_ext_monad" where 320 "reschedule_required \<equiv> do 321 action \<leftarrow> gets scheduler_action; 322 case action of switch_thread t \<Rightarrow> tcb_sched_action (tcb_sched_enqueue) t | _ \<Rightarrow> return (); 323 set_scheduler_action choose_new_thread 324 od" 325 326definition 327 possible_switch_to :: "obj_ref \<Rightarrow> unit det_ext_monad" where 328 "possible_switch_to target \<equiv> do 329 cur_dom \<leftarrow> gets cur_domain; 330 target_dom \<leftarrow> ethread_get tcb_domain target; 331 action \<leftarrow> gets scheduler_action; 332 333 if (target_dom \<noteq> cur_dom) then 334 tcb_sched_action tcb_sched_enqueue target 335 else if (action \<noteq> resume_cur_thread) then 336 do 337 reschedule_required; 338 tcb_sched_action tcb_sched_enqueue target 339 od 340 else 341 set_scheduler_action $ switch_thread target 342 od" 343 344definition 345 next_domain :: "unit det_ext_monad" where 346 "next_domain \<equiv> 347 modify (\<lambda>s. 348 let domain_index' = (domain_index s + 1) mod length (domain_list s) in 349 let next_dom = (domain_list s)!domain_index' 350 in s\<lparr> domain_index := domain_index', 351 cur_domain := fst next_dom, 352 domain_time := snd next_dom, 353 work_units_completed := 0\<rparr>)" 354 355definition 356 dec_domain_time :: "unit det_ext_monad" where 357 "dec_domain_time = modify (\<lambda>s. s\<lparr>domain_time := domain_time s - 1\<rparr>)" 358 359definition set_cdt_list :: "cdt_list \<Rightarrow> (det_state, unit) nondet_monad" where 360 "set_cdt_list t \<equiv> do 361 s \<leftarrow> get; 362 put $ s\<lparr> cdt_list := t \<rparr> 363 od" 364 365definition 366 update_cdt_list :: "(cdt_list \<Rightarrow> cdt_list) \<Rightarrow> (det_state, unit) nondet_monad" 367where 368 "update_cdt_list f \<equiv> do 369 t \<leftarrow> gets cdt_list; 370 set_cdt_list (f t) 371 od" 372 373 374text \<open>The CDT in the implementation is stored in prefix traversal order. 375 The following functions traverse its abstract representation here to 376 yield corresponding information. 377\<close> 378definition next_child :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cslot_ptr option" where 379 "next_child slot t \<equiv> case (t slot) of [] \<Rightarrow> None | 380 x # xs \<Rightarrow> Some x" 381 382definition next_sib :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cdt \<Rightarrow> cslot_ptr option" where 383 "next_sib slot t m \<equiv> case m slot of None \<Rightarrow> None | 384 Some p \<Rightarrow> after_in_list (t p) slot" 385 386 387function (domintros) next_not_child :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cdt \<Rightarrow> cslot_ptr option" where 388 "next_not_child slot t m = (if next_sib slot t m = None 389 then (case m slot of 390 None \<Rightarrow> None | 391 Some p \<Rightarrow> next_not_child p t m) 392 else next_sib slot t m)" 393 by auto 394 395(* next_slot traverses the cdt, replicating mdb_next in the Haskell spec. 396 The cdt is traversed child first, by next_child 397 going to a nodes first child when it exists, 398 otherwise next_not_child looks up the tree until it finds 399 a new node to visit as a sibling of its self or some ancestor *) 400 401definition next_slot :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cdt \<Rightarrow> cslot_ptr option" where 402 "next_slot slot t m \<equiv> if t slot \<noteq> [] 403 then next_child slot t 404 else next_not_child slot t m" 405 406text \<open>\emph{Extended operations} for the deterministic abstract specification.\<close> 407 408definition max_non_empty_queue :: "(priority \<Rightarrow> ready_queue) \<Rightarrow> ready_queue" where 409 "max_non_empty_queue queues \<equiv> queues (Max {prio. queues prio \<noteq> []})" 410 411 412definition default_ext :: "apiobject_type \<Rightarrow> domain \<Rightarrow> etcb option" where 413 "default_ext type cdom \<equiv> 414 case type of TCBObject \<Rightarrow> Some (default_etcb\<lparr>tcb_domain := cdom\<rparr>) 415 | _ \<Rightarrow> None" 416 417definition retype_region_ext :: "obj_ref list \<Rightarrow> apiobject_type \<Rightarrow> unit det_ext_monad" where 418 "retype_region_ext ptrs type \<equiv> do 419 ekh \<leftarrow> gets ekheap; 420 cdom \<leftarrow> gets cur_domain; 421 ekh' \<leftarrow> return $ foldr (\<lambda>p ekh. (ekh(p := default_ext type cdom))) ptrs ekh; 422 modify (\<lambda>s. s\<lparr>ekheap := ekh'\<rparr>) 423 od" 424 425definition cap_swap_ext where 426"cap_swap_ext \<equiv> (\<lambda> slot1 slot2 slot1_op slot2_op. 427 do 428 update_cdt_list (\<lambda>list. list(slot1 := list slot2, slot2 := list slot1)); 429 update_cdt_list 430 (\<lambda>list. case if slot2_op = Some slot1 then Some slot2 431 else if slot2_op = Some slot2 then Some slot1 else slot2_op of 432 None \<Rightarrow> (case if slot1_op = Some slot1 then Some slot2 433 else if slot1_op = Some slot2 then Some slot1 else slot1_op of 434 None \<Rightarrow> list 435 | Some slot2_p \<Rightarrow> list(slot2_p := list_replace (list slot2_p) slot1 slot2)) 436 | Some slot1_p \<Rightarrow> 437 (case if slot1_op = Some slot1 then Some slot2 438 else if slot1_op = Some slot2 then Some slot1 else slot1_op of 439 None \<Rightarrow> list(slot1_p := list_replace (list slot1_p) slot2 slot1) 440 | Some slot2_p \<Rightarrow> 441 if slot1_p = slot2_p 442 then list(slot1_p := list_swap (list slot1_p) slot1 slot2) 443 else list(slot1_p := list_replace (list slot1_p) slot2 slot1, 444 slot2_p := list_replace (list slot2_p) slot1 slot2))) 445 od)" 446 447definition cap_move_ext where 448"cap_move_ext \<equiv> (\<lambda> src_slot dest_slot src_p dest_p. 449 do 450 451 update_cdt_list (\<lambda>list. case (dest_p) of 452 None \<Rightarrow> list | 453 Some p \<Rightarrow> list (p := list_remove (list p) dest_slot)); 454 455 if (src_slot = dest_slot) then return () else 456 457 (do 458 update_cdt_list (\<lambda>list. case (src_p) of 459 None \<Rightarrow> list | 460 Some p \<Rightarrow> list (p := list_replace (list p) src_slot dest_slot)); 461 462 update_cdt_list (\<lambda>list. list (src_slot := [], dest_slot := (list src_slot) @ (list dest_slot))) 463 od) 464 465 od)" 466 467 468definition cap_insert_ext where 469"cap_insert_ext \<equiv> (\<lambda> src_parent src_slot dest_slot src_p dest_p. 470 do 471 472 update_cdt_list (\<lambda>list. case (dest_p) of 473 None \<Rightarrow> list | 474 Some p \<Rightarrow> (list (p := list_remove (list p) dest_slot))); 475 476 update_cdt_list (\<lambda>list. case (src_p) of 477 None \<Rightarrow> list ( 478 src_slot := if src_parent then [dest_slot] @ (list src_slot) else list src_slot) | 479 Some p \<Rightarrow> list ( 480 src_slot := if src_parent then [dest_slot] @ (list src_slot) else list src_slot, 481 p := if (src_parent \<and> p \<noteq> src_slot) then (list p) else if (src_slot \<noteq> dest_slot) then (list_insert_after (list p) src_slot dest_slot) else (dest_slot # (list p)))) 482 od)" 483 484definition empty_slot_ext where 485"empty_slot_ext \<equiv> (\<lambda> slot slot_p. 486 487 update_cdt_list (\<lambda>list. case slot_p of None \<Rightarrow> list (slot := []) | 488 Some p \<Rightarrow> if (p = slot) then list(p := list_remove (list p) slot) else list (p := list_replace_list (list p) slot (list slot), slot := [])))" 489 490definition create_cap_ext where 491"create_cap_ext \<equiv> (\<lambda> untyped dest dest_p. do 492 493 update_cdt_list (\<lambda>list. case dest_p of 494 None \<Rightarrow> list | 495 Some p \<Rightarrow> (list (p := list_remove (list p) dest))); 496 497 update_cdt_list (\<lambda>list. list (untyped := [dest] @ (list untyped))) 498 od)" 499 500definition next_revoke_cap where 501"next_revoke_cap \<equiv> (\<lambda>slot ext. the (next_child slot (cdt_list ext)))" 502 503definition 504 free_asid_select :: "(asid_high_index \<rightharpoonup> 'a) \<Rightarrow> asid_high_index" 505where 506 "free_asid_select \<equiv> \<lambda>asid_table. fst (hd (filter (\<lambda>(x,y). x \<le> 2 ^ asid_high_bits - 1 \<and> y = None) (assocs asid_table)))" 507 508definition 509 free_asid_pool_select :: "(asid_low_index \<rightharpoonup> 'a) \<Rightarrow> asid \<Rightarrow> asid_low_index" 510where 511 "free_asid_pool_select \<equiv> (\<lambda>pool base. 512 fst (hd ((filter (\<lambda> (x,y). ucast x + base \<noteq> 0 \<and> y = None) (assocs pool)))))" 513 514definition update_work_units where 515 "update_work_units \<equiv> 516 modify (\<lambda>s. s\<lparr>work_units_completed := work_units_completed s + 1\<rparr>)" 517 518definition reset_work_units where 519 "reset_work_units \<equiv> 520 modify (\<lambda>s. s\<lparr>work_units_completed := 0\<rparr>)" 521 522definition work_units_limit_reached where 523 "work_units_limit_reached \<equiv> do 524 work_units \<leftarrow> gets work_units_completed; 525 return (work_units_limit \<le> work_units) 526 od" 527 528text \<open> 529 A type class for all instantiations of the abstract specification. In 530 practice, this is restricted to basically allow only two sensible 531 implementations at present: the deterministic abstract specification and 532 the nondeterministic one. 533\<close> 534class state_ext = 535 fixes unwrap_ext :: "'a state \<Rightarrow> det_ext state" 536 fixes wrap_ext :: "(det_ext \<Rightarrow> det_ext) \<Rightarrow> ('a \<Rightarrow> 'a)" 537 fixes wrap_ext_op :: "unit det_ext_monad \<Rightarrow> ('a state,unit) nondet_monad" 538 fixes wrap_ext_bool :: "bool det_ext_monad \<Rightarrow> ('a state,bool) nondet_monad" 539 fixes select_switch :: "'a \<Rightarrow> bool" 540 fixes ext_init :: "'a" 541 542definition detype_ext :: "obj_ref set \<Rightarrow> 'z::state_ext \<Rightarrow> 'z" where 543 "detype_ext S \<equiv> wrap_ext (\<lambda>s. s\<lparr>ekheap_internal := (\<lambda>x. if x \<in> S then None else ekheap_internal s x)\<rparr>)" 544 545instantiation det_ext_ext :: (type) state_ext 546begin 547 548definition "unwrap_ext_det_ext_ext == (\<lambda>x. x) :: det_ext state \<Rightarrow> det_ext state" 549 550definition "wrap_ext_det_ext_ext == (\<lambda>x. x) :: 551 (det_ext \<Rightarrow> det_ext) \<Rightarrow> det_ext \<Rightarrow> det_ext" 552 553definition "wrap_ext_op_det_ext_ext == (\<lambda>x. x) :: 554 (det_ext state \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool) 555 \<Rightarrow> det_ext state \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool" 556 557definition "wrap_ext_bool_det_ext_ext == (\<lambda>x. x) :: 558 (det_ext state \<Rightarrow> ((bool \<times> det_ext state) set) \<times> bool) 559 \<Rightarrow> det_ext state \<Rightarrow> ((bool \<times> det_ext state) set) \<times> bool" 560 561definition "select_switch_det_ext_ext == (\<lambda>_. True) :: det_ext\<Rightarrow> bool" 562 563(* this probably doesn't satisfy the invariants *) 564definition "ext_init_det_ext_ext \<equiv> 565 \<lparr>work_units_completed_internal = 0, 566 scheduler_action_internal = resume_cur_thread, 567 ekheap_internal = Map.empty (idle_thread_ptr \<mapsto> default_etcb), 568 domain_list_internal = [(0,15)], 569 domain_index_internal = 0, 570 cur_domain_internal = 0, 571 domain_time_internal = 15, 572 ready_queues_internal = const (const []), 573 cdt_list_internal = const []\<rparr> :: det_ext" 574 575instance .. 576 577end 578 579section "Nondeterministic Abstract Specification" 580 581text \<open>\label{s:nondet-spec} 582The nondeterministic abstract specification instantiates the extended state 583with the unit type -- i.e. it doesn't have any meaningful extended state. 584\<close> 585 586instantiation unit :: state_ext 587begin 588 589 590definition "unwrap_ext_unit == (\<lambda>_. undefined) :: unit state \<Rightarrow> det_ext state" 591 592definition "wrap_ext_unit == (\<lambda>f s. ()) :: (det_ext \<Rightarrow> det_ext) \<Rightarrow> unit \<Rightarrow> unit" 593 594 595definition "wrap_ext_op_unit == (\<lambda>m. return ()) :: 596 (det_ext state \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool) \<Rightarrow> unit state \<Rightarrow> ((unit \<times> unit state) set) \<times> bool" 597 598definition "wrap_ext_bool_unit == (\<lambda>m. select UNIV) :: 599 (det_ext state \<Rightarrow> ((bool \<times> det_ext state ) set) \<times> bool) \<Rightarrow> unit state \<Rightarrow> ((bool \<times> unit state) set) \<times> bool" 600 601definition "select_switch_unit == (\<lambda>s. False) :: unit \<Rightarrow> bool" 602 603definition "ext_init_unit \<equiv> () :: unit" 604 605instance .. 606 607end 608 609text \<open>Run an extended operation over the extended state without 610 modifying it and use the return value to choose between two computations 611 to run. 612\<close> 613lemmas ext_init_def = ext_init_det_ext_ext_def ext_init_unit_def 614 615definition OR_choice :: "bool det_ext_monad \<Rightarrow> ('z::state_ext state,'a) nondet_monad \<Rightarrow> ('z state,'a) nondet_monad \<Rightarrow> ('z state,'a) nondet_monad" where 616"OR_choice c f g \<equiv> 617 do 618 ex \<leftarrow> get; 619 (rv,_) \<leftarrow> select_f (mk_ef ((wrap_ext_bool c) ex)); 620 if rv then f else g 621 od" 622 623definition OR_choiceE :: "bool det_ext_monad \<Rightarrow> ('z::state_ext state,'e + 'a) nondet_monad \<Rightarrow> ('z state,'e + 'a) nondet_monad \<Rightarrow> ('z state,'e + 'a) nondet_monad" where 624"OR_choiceE c f g \<equiv> 625 doE 626 ex \<leftarrow> liftE get; 627 (rv,_) \<leftarrow> liftE $ select_f (mk_ef ((wrap_ext_bool c) ex)); 628 if rv then f else g 629 odE" 630 631text \<open>Run an extended operation over the extended state to update the 632 extended state, ignoring any return value that the extended operation might 633 yield. 634\<close> 635 636definition do_extended_op :: "unit det_ext_monad \<Rightarrow> ('z::state_ext state,unit) nondet_monad" where 637 "do_extended_op eop \<equiv> do 638 ex \<leftarrow> get; 639 (_,es') \<leftarrow> select_f (mk_ef ((wrap_ext_op eop) ex)); 640 modify (\<lambda> state. state\<lparr>exst := (exst es')\<rparr>) 641 od" 642 643text \<open> 644 Use the extended state to choose a value from a bounding set @{term S} when 645 @{term select_switch} is true. Otherwise just select from @{term S}. 646\<close> 647definition select_ext :: "(det_ext state \<Rightarrow> 'd) \<Rightarrow> ('d set) \<Rightarrow> ('a::state_ext state,'d) nondet_monad" where 648 "select_ext a S \<equiv> do 649 s \<leftarrow> get; 650 x \<leftarrow> if (select_switch (exst s)) then (return (a (unwrap_ext s))) 651 else (select S); 652 assert (x \<in> S); 653 return x 654 od" 655 656(*Defined here because it's asserted before empty_slot*) 657definition valid_list_2 :: "cdt_list \<Rightarrow> cdt \<Rightarrow> bool" where 658 "valid_list_2 t m \<equiv> (\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p))" 659 660abbreviation valid_list :: "det_ext state \<Rightarrow> bool" where 661 "valid_list s \<equiv> valid_list_2 (cdt_list s) (cdt s)" 662 663end 664