From 933079cd4120cc739f1ec7317622ce23c6e8f816 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Mon, 28 Oct 2024 17:45:35 +1100
Subject: [PATCH] aspec: refactor det_ext to remove scheduler state

The scheduler is now fully part of the extensible abstract specification,
because we are increasingly finding properties that are not able to be
reasonably specified without it. This means that there is now no
non-deterministic scheduler specification and that the only slots for
non-determinism are now CDT and preemption operations.

This came up due to some properties currently being proved not being true for
all execution paths of the previous non-deterministic specification. Options
that were considered were:
1 - move the minimal state (the current domain and tcb's domain) required for
the properties currently being considered  to the extensible abstract
specification.
2 - move all of the scheduler state to the extensible abstract specification,
the same as what has been done on the rt branch.
3 - move all state and remove the non-deterministic specification completely.
4 - add ghost state to sidestep the specific problem that we are currently
encountering (it is unclear whether this would actually work).

Option 2 was chosen because it is the least blocking (although may be more
annoying than some of the others), will result in the smallest diff to the rt
branch, and we don't think it will be significantly more work than the other
options. If we want to reason about threads in the future (e.g. liveness), we
will require that this information about the scheduler state is accessible.

We are really not sure about whether moving specifically the scheduler action is
the right decision, but we are moving it across because the correctness of the
ready queues depends on it and any alternatives that we have thought of would be
a lot of work that we do not want to do at this time.

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 spec/abstract/AARCH64/Init_A.thy  |   9 +
 spec/abstract/Deterministic_A.thy | 487 ++++++++----------------------
 spec/abstract/Interrupt_A.thy     |  12 +-
 spec/abstract/IpcCancel_A.thy     |  14 +-
 spec/abstract/Ipc_A.thy           |  12 +-
 spec/abstract/KHeap_A.thy         | 153 +++++++---
 spec/abstract/Retype_A.thy        |  14 +-
 spec/abstract/Schedule_A.thy      | 108 +++----
 spec/abstract/Structures_A.thy    |  35 ++-
 spec/abstract/Syscall_A.thy       |   8 +-
 spec/abstract/Tcb_A.thy           |  22 +-
 11 files changed, 371 insertions(+), 503 deletions(-)

diff --git a/spec/abstract/AARCH64/Init_A.thy b/spec/abstract/AARCH64/Init_A.thy
index 9182f606e2..e8cd649fe8 100644
--- a/spec/abstract/AARCH64/Init_A.thy
+++ b/spec/abstract/AARCH64/Init_A.thy
@@ -79,6 +79,9 @@ definition init_kheap :: kheap where
          tcb_fault = None,
          tcb_bound_notification = None,
          tcb_mcpriority = minBound,
+         tcb_priority = 0,
+         tcb_time_slice = timeSlice,
+         tcb_domain = 0,
          tcb_arch = init_arch_tcb
          \<rparr>,
      arm_global_pt_ptr \<mapsto> ArchObj global_pt_obj
@@ -100,6 +103,12 @@ definition init_A_st :: "'z::state_ext state"
     is_original_cap = init_ioc,
     cur_thread = idle_thread_ptr,
     idle_thread = idle_thread_ptr,
+    scheduler_action = resume_cur_thread,
+    domain_list = [(0,15)],
+    domain_index = 0,
+    cur_domain = 0,
+    domain_time = 15,
+    ready_queues = const (const []),
     machine_state = init_machine_state,
     interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (ucast irq << cte_level_bits),
     interrupt_states = \<lambda>_. IRQInactive,
diff --git a/spec/abstract/Deterministic_A.thy b/spec/abstract/Deterministic_A.thy
index f84aa166b8..81241e8785 100644
--- a/spec/abstract/Deterministic_A.thy
+++ b/spec/abstract/Deterministic_A.thy
@@ -25,7 +25,7 @@ The basic technique, and its motivation, are described in~\cite{Matichuk_Murray_
 
 Here, we define two such instantiations. The first yields a
 largely-deterministic specification by instantiating @{typ "'a"} with
-a record that includes concrete scheduler state and
+a record that includes
 information about sibling ordering in the capability derivation tree (CDT).
 We call the resulting
 specification the \emph{deterministic abstract specification} and it is
@@ -33,8 +33,8 @@ defined below in \autoref{s:det-spec}.
 
 The second instantiation uses the type @{typ unit} for @{typ 'a}, yielding
 a specification that is far more nondeterministic. In particular, the
-scheduling behaviour and the order in which capabilities are deleted during
-a \emph{revoke} system call both become completely nondeterministic.
+order in which capabilities are deleted during
+a \emph{revoke} system call becomes completely nondeterministic.
 We call this second instantiation the
 \emph{nondeterministic abstract specification} and it is defined below in
 \autoref{s:nondet-spec}.
@@ -44,52 +44,54 @@ text \<open>Translate a state of type @{typ "'a state"} to one of type @{typ "'b
   via a function @{term t} from @{typ "'a"} to @{typ "'b"}.
 \<close>
 definition trans_state :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a state \<Rightarrow> 'b state" where
-"trans_state t s = \<lparr>kheap = kheap s, cdt = cdt s, is_original_cap = is_original_cap s,
-                     cur_thread = cur_thread s, idle_thread = idle_thread s,
-                     machine_state = machine_state s,
-                     interrupt_irq_node = interrupt_irq_node s,
-                     interrupt_states = interrupt_states s, arch_state = arch_state s,
-                     exst = t(exst s)\<rparr>"
+  "trans_state t s = abstract_state.extend (abstract_state.truncate s) (state.fields (t (exst s)))"
 
 (*<*)
-lemma trans_state[simp]: "kheap (trans_state t s) = kheap s"
-                            "cdt (trans_state t s) = cdt s"
-                            "is_original_cap (trans_state t s) = is_original_cap s"
-                            "cur_thread (trans_state t s) = cur_thread s"
-                            "idle_thread (trans_state t s) = idle_thread s"
-                            "machine_state (trans_state t s) = machine_state s"
-                            "interrupt_irq_node (trans_state t s) = interrupt_irq_node s"
-                           "interrupt_states (trans_state t s) = interrupt_states s"
-                            "arch_state (trans_state t s) = arch_state s"
-                            "exst (trans_state t s) = (t (exst s))"
-                            "exst (trans_state (\<lambda>_. e) s) = e"
-  apply (simp add: trans_state_def)+
-  done
+lemma trans_state[simp]:
+  "kheap (trans_state t s) = kheap s"
+  "cdt (trans_state t s) = cdt s"
+  "is_original_cap (trans_state t s) = is_original_cap s"
+  "cur_thread (trans_state t s) = cur_thread s"
+  "idle_thread (trans_state t s) = idle_thread s"
+  "machine_state (trans_state t s) = machine_state s"
+  "interrupt_irq_node (trans_state t s) = interrupt_irq_node s"
+  "interrupt_states (trans_state t s) = interrupt_states s"
+  "arch_state (trans_state t s) = arch_state s"
+  "scheduler_action (trans_state t s) = scheduler_action s"
+  "domain_list (trans_state t s) = domain_list s"
+  "domain_index (trans_state t s) = domain_index s"
+  "cur_domain (trans_state t s) = cur_domain s"
+  "domain_time (trans_state t s) = domain_time s"
+  "ready_queues (trans_state t s) = ready_queues s"
+  "exst (trans_state t s) = (t (exst s))"
+  "exst (trans_state (\<lambda>_. e) s) = e"
+  by (simp add: trans_state_def abstract_state.defs state.defs)+
 
 lemma trans_state_update[simp]:
- "trans_state t (kheap_update f s) = kheap_update f (trans_state t s)"
- "trans_state t (cdt_update g s) = cdt_update g (trans_state t s)"
- "trans_state t (is_original_cap_update h s) = is_original_cap_update h (trans_state t s)"
- "trans_state t (cur_thread_update i s) = cur_thread_update i (trans_state t s)"
- "trans_state t (idle_thread_update j s) = idle_thread_update j (trans_state t s)"
- "trans_state t (machine_state_update k s) = machine_state_update k (trans_state t s)"
- "trans_state t (interrupt_irq_node_update l s) = interrupt_irq_node_update l (trans_state t s)"
- "trans_state t (arch_state_update m s) = arch_state_update m (trans_state t s)"
- "trans_state t (interrupt_states_update p s) = interrupt_states_update p (trans_state t s)"
-  apply (simp add: trans_state_def)+
-  done
+  "trans_state t (kheap_update f s) = kheap_update f (trans_state t s)"
+  "trans_state t (cdt_update g s) = cdt_update g (trans_state t s)"
+  "trans_state t (is_original_cap_update h s) = is_original_cap_update h (trans_state t s)"
+  "trans_state t (cur_thread_update i s) = cur_thread_update i (trans_state t s)"
+  "trans_state t (idle_thread_update j s) = idle_thread_update j (trans_state t s)"
+  "trans_state t (machine_state_update k s) = machine_state_update k (trans_state t s)"
+  "trans_state t (interrupt_irq_node_update l s) = interrupt_irq_node_update l (trans_state t s)"
+  "trans_state t (arch_state_update m s) = arch_state_update m (trans_state t s)"
+  "trans_state t (scheduler_action_update b s) = scheduler_action_update b (trans_state t s)"
+  "trans_state t (domain_list_update c s) = domain_list_update c (trans_state t s)"
+  "trans_state t (domain_index_update d s) = domain_index_update d (trans_state t s)"
+  "trans_state t (cur_domain_update e s) = cur_domain_update e (trans_state t s)"
+  "trans_state t (domain_time_update f2 s) = domain_time_update f2 (trans_state t s)"
+  "trans_state t (ready_queues_update g2 s) = ready_queues_update g2 (trans_state t s)"
+  by (simp add: trans_state_def abstract_state.defs)+
 
 
 lemma trans_state_update':
   "trans_state f = exst_update f"
-  apply (rule ext)
-  apply simp
-  done
+  by (rule ext) simp
 
 lemma trans_state_update''[simp]:
   "trans_state t' (trans_state t s) = trans_state (\<lambda>e. t' (t e)) s"
-  apply simp
-  done
+  by simp
 (*>*)
 
 text \<open>Truncate an extended state of type @{typ "'a state"}
@@ -100,33 +102,8 @@ abbreviation "truncate_state \<equiv> trans_state (\<lambda>_. ())"
 section "Deterministic Abstract Specification"
 
 text \<open>\label{s:det-spec}
-  The deterministic abstract specification tracks the state of the scheduler
-and ordering information about sibling nodes in the CDT.\<close>
-
-text \<open>The current scheduler action,
-  which is part of the scheduling state.\<close>
-datatype scheduler_action =
-    resume_cur_thread
-  | switch_thread (sch_act_target : obj_ref)
-  | choose_new_thread
-
-type_synonym domain = word8
-
-record etcb =
- tcb_priority :: "priority"
- tcb_time_slice :: "nat"
- tcb_domain :: "domain"
-
-definition default_priority :: "priority" where
-  "default_priority \<equiv> minBound"
-
-definition default_domain :: "domain" where
-  "default_domain \<equiv> minBound"
-
-definition default_etcb :: "etcb" where
-  "default_etcb \<equiv> \<lparr>tcb_priority = default_priority, tcb_time_slice = timeSlice, tcb_domain = default_domain\<rparr>"
-
-type_synonym ready_queue = "obj_ref list"
+  The deterministic abstract specification tracks
+  ordering information about sibling nodes in the CDT.\<close>
 
 text \<open>
   For each entry in the CDT, we record an ordered list of its children.
@@ -141,13 +118,6 @@ text \<open>
 \<close>
 record det_ext =
    work_units_completed_internal :: "machine_word"
-   scheduler_action_internal :: scheduler_action
-   ekheap_internal :: "obj_ref \<Rightarrow> etcb option"
-   domain_list_internal :: "(domain \<times> machine_word) list"
-   domain_index_internal :: nat
-   cur_domain_internal :: domain
-   domain_time_internal :: "machine_word"
-   ready_queues_internal :: "domain \<Rightarrow> priority \<Rightarrow> ready_queue"
    cdt_list_internal :: cdt_list
 
 text \<open>
@@ -166,189 +136,92 @@ abbreviation
   "work_units_completed_update f (s::det_state) \<equiv>  trans_state (work_units_completed_internal_update f) s"
 
 abbreviation
-  "scheduler_action (s::det_state) \<equiv> scheduler_action_internal (exst s)"
-
-abbreviation
-  "scheduler_action_update f (s::det_state) \<equiv>  trans_state (scheduler_action_internal_update f) s"
-
-abbreviation
-  "ekheap (s::det_state) \<equiv> ekheap_internal (exst s)"
-
-abbreviation
-  "ekheap_update f (s::det_state) \<equiv> trans_state (ekheap_internal_update f) s"
-
-abbreviation
-  "domain_list (s::det_state) \<equiv> domain_list_internal (exst s)"
-
-abbreviation
-  "domain_list_update f (s::det_state) \<equiv> trans_state (domain_list_internal_update f) s"
-
-abbreviation
-  "domain_index (s::det_state) \<equiv> domain_index_internal (exst s)"
+  "cdt_list (s::det_state) \<equiv> cdt_list_internal (exst s)"
 
 abbreviation
-  "domain_index_update f (s::det_state) \<equiv> trans_state (domain_index_internal_update f) s"
+  "cdt_list_update f (s::det_state) \<equiv> trans_state (cdt_list_internal_update f) s"
 
-abbreviation
-  "cur_domain (s::det_state) \<equiv> cur_domain_internal (exst s)"
+type_synonym 'a det_ext_monad = "(det_state,'a) nondet_monad"
 
-abbreviation
-  "cur_domain_update f (s::det_state) \<equiv> trans_state (cur_domain_internal_update f) s"
 
-abbreviation
-  "domain_time (s::det_state) \<equiv> domain_time_internal (exst s)"
+section \<open>Type Class\<close>
 
-abbreviation
-  "domain_time_update f (s::det_state) \<equiv> trans_state (domain_time_internal_update f) s"
+text \<open>
+  A type class for all instantiations of the abstract specification. In
+  practice, this is restricted to basically allow only two sensible
+  implementations at present: the deterministic abstract specification and
+  the nondeterministic one.
+\<close>
+class state_ext =
+ fixes unwrap_ext :: "'a state \<Rightarrow> det_ext state"
+ fixes wrap_ext :: "(det_ext \<Rightarrow> det_ext) \<Rightarrow> ('a \<Rightarrow> 'a)"
+ fixes wrap_ext_op :: "unit det_ext_monad \<Rightarrow> ('a state,unit) nondet_monad"
+ fixes wrap_ext_bool :: "bool det_ext_monad \<Rightarrow> ('a state,bool) nondet_monad"
+ fixes select_switch :: "'a \<Rightarrow> bool"
+ fixes ext_init :: "'a"
 
-abbreviation
-  "ready_queues (s::det_state) \<equiv> ready_queues_internal (exst s)"
 
-abbreviation
-  "ready_queues_update f (s::det_state) \<equiv> trans_state (ready_queues_internal_update f) s"
+section \<open>Type Class Instances\<close>
 
-abbreviation
-  "cdt_list (s::det_state) \<equiv> cdt_list_internal (exst s)"
+subsection "Deterministic Abstract Specification"
 
-abbreviation
-  "cdt_list_update f (s::det_state) \<equiv> trans_state (cdt_list_internal_update f) s"
+instantiation  det_ext_ext :: (type) state_ext
+begin
 
-type_synonym 'a det_ext_monad = "(det_state,'a) nondet_monad"
+definition "unwrap_ext_det_ext_ext == (\<lambda>x. x) :: det_ext state \<Rightarrow> det_ext state"
 
-text \<open>
-  Basic monadic functions for operating on the extended state of the
-  deterministic abstract specification.
-\<close>
-definition
-  get_etcb :: "obj_ref \<Rightarrow> det_state \<Rightarrow> etcb option"
-where
-  "get_etcb tcb_ref es \<equiv> ekheap es tcb_ref"
+definition "wrap_ext_det_ext_ext == (\<lambda>x. x) ::
+  (det_ext \<Rightarrow> det_ext) \<Rightarrow> det_ext \<Rightarrow> det_ext"
 
-definition
-  ethread_get :: "(etcb \<Rightarrow> 'a) \<Rightarrow> obj_ref \<Rightarrow> 'a det_ext_monad"
-where
-  "ethread_get f tptr \<equiv> do
-     tcb \<leftarrow> gets_the $ get_etcb tptr;
-     return $ f tcb
-   od"
+definition "wrap_ext_op_det_ext_ext == (\<lambda>x. x) ::
+  (det_ext state \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool)
+  \<Rightarrow> det_ext state  \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool"
 
-(* For infoflow, we want to avoid certain read actions, such as reading the priority of the
-   current thread when it could be idle. Then we need to make sure we do not rely on the result.
-   undefined is the closest we have to a result that can't be relied on *)
-definition
-  ethread_get_when :: "bool \<Rightarrow> (etcb \<Rightarrow> 'a) \<Rightarrow> obj_ref \<Rightarrow> 'a det_ext_monad"
-where
-  "ethread_get_when b f tptr \<equiv> if b then (ethread_get f tptr) else return undefined"
-
-definition set_eobject :: "obj_ref \<Rightarrow> etcb \<Rightarrow> unit det_ext_monad"
-  where
- "set_eobject ptr obj \<equiv>
-  do es \<leftarrow> get;
-    ekh \<leftarrow> return $ (ekheap es)(ptr \<mapsto> obj);
-    put (es\<lparr>ekheap := ekh\<rparr>)
-  od"
+definition "wrap_ext_bool_det_ext_ext == (\<lambda>x. x) ::
+  (det_ext state \<Rightarrow> ((bool \<times> det_ext state) set) \<times> bool)
+  \<Rightarrow> det_ext state \<Rightarrow> ((bool \<times> det_ext state) set) \<times> bool"
 
-definition
-  ethread_set :: "(etcb \<Rightarrow> etcb) \<Rightarrow> obj_ref \<Rightarrow> unit det_ext_monad"
-where
-  "ethread_set f tptr \<equiv> do
-     tcb \<leftarrow> gets_the $ get_etcb tptr;
-     set_eobject tptr $ f tcb
-   od"
+definition "select_switch_det_ext_ext == (\<lambda>_. True)  :: det_ext\<Rightarrow> bool"
 
-definition
-  set_scheduler_action :: "scheduler_action \<Rightarrow> unit det_ext_monad" where
-  "set_scheduler_action action \<equiv>
-     modify (\<lambda>es. es\<lparr>scheduler_action := action\<rparr>)"
+definition "ext_init_det_ext_ext \<equiv>
+     \<lparr>work_units_completed_internal = 0,
+      cdt_list_internal = const [] \<rparr> :: det_ext"
 
-definition
-  thread_set_priority :: "obj_ref \<Rightarrow> priority \<Rightarrow> unit det_ext_monad" where
-  "thread_set_priority tptr prio \<equiv> ethread_set (\<lambda>tcb. tcb\<lparr>tcb_priority := prio\<rparr>) tptr"
+instance ..
 
-definition
-  thread_set_time_slice :: "obj_ref \<Rightarrow> nat \<Rightarrow> unit det_ext_monad" where
-  "thread_set_time_slice tptr time \<equiv> ethread_set (\<lambda>tcb. tcb\<lparr>tcb_time_slice := time\<rparr>) tptr"
+end
 
-definition
-  thread_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
-  "thread_set_domain tptr domain \<equiv> ethread_set (\<lambda>tcb. tcb\<lparr>tcb_domain := domain\<rparr>) tptr"
+subsection "Nondeterministic Abstract Specification"
 
+text \<open>\label{s:nondet-spec}
+The nondeterministic abstract specification instantiates the extended state
+with the unit type -- i.e. it doesn't have any meaningful extended state.
+\<close>
 
-definition
-  get_tcb_queue :: "domain \<Rightarrow> priority \<Rightarrow> ready_queue det_ext_monad" where
-  "get_tcb_queue d prio \<equiv> do
-     queues \<leftarrow> gets ready_queues;
-     return (queues d prio)
-   od"
+instantiation unit :: state_ext
+begin
 
-definition
-  set_tcb_queue :: "domain \<Rightarrow> priority \<Rightarrow> ready_queue \<Rightarrow> unit det_ext_monad" where
-  "set_tcb_queue d prio queue \<equiv>
-     modify (\<lambda>es. es\<lparr> ready_queues :=
-      (\<lambda>d' p. if d' = d \<and> p = prio then queue else ready_queues es d' p)\<rparr>)"
+definition "unwrap_ext_unit == (\<lambda>_. undefined) :: unit state \<Rightarrow> det_ext state"
 
+definition "wrap_ext_unit == (\<lambda>f s. ()) :: (det_ext \<Rightarrow> det_ext) \<Rightarrow> unit \<Rightarrow> unit"
 
-definition
-  tcb_sched_action :: "(obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list) \<Rightarrow> obj_ref  \<Rightarrow> unit det_ext_monad" where
-  "tcb_sched_action action thread \<equiv> do
-     d \<leftarrow> ethread_get tcb_domain thread;
-     prio \<leftarrow> ethread_get tcb_priority thread;
-     queue \<leftarrow> get_tcb_queue d prio;
-     set_tcb_queue d prio (action thread queue)
-   od"
 
-definition
-  tcb_sched_enqueue :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where
-  "tcb_sched_enqueue thread queue \<equiv> if (thread \<notin> set queue) then thread # queue else queue"
+definition "wrap_ext_op_unit == (\<lambda>m. return ()) ::
+  (det_ext state \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool) \<Rightarrow> unit state \<Rightarrow> ((unit \<times> unit state) set) \<times> bool"
 
-definition
-  tcb_sched_append :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where
-  "tcb_sched_append thread queue \<equiv> if (thread \<notin> set queue) then queue @ [thread] else queue"
+definition "wrap_ext_bool_unit == (\<lambda>m. select UNIV) ::
+  (det_ext state \<Rightarrow> ((bool \<times> det_ext state ) set) \<times> bool) \<Rightarrow> unit state \<Rightarrow> ((bool \<times> unit state) set) \<times> bool"
 
-definition
-  tcb_sched_dequeue :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where
-  "tcb_sched_dequeue thread queue \<equiv> filter (\<lambda>x. x \<noteq> thread) queue"
+definition "select_switch_unit == (\<lambda>s. False) :: unit \<Rightarrow> bool"
 
+definition "ext_init_unit \<equiv> () :: unit"
 
-definition reschedule_required :: "unit det_ext_monad" where
-  "reschedule_required \<equiv> do
-     action \<leftarrow> gets scheduler_action;
-     case action of switch_thread t \<Rightarrow> tcb_sched_action (tcb_sched_enqueue) t | _ \<Rightarrow> return ();
-     set_scheduler_action choose_new_thread
-   od"
+instance ..
 
-definition
-  possible_switch_to :: "obj_ref \<Rightarrow> unit det_ext_monad" where
-  "possible_switch_to target \<equiv> do
-     cur_dom \<leftarrow> gets cur_domain;
-     target_dom \<leftarrow> ethread_get tcb_domain target;
-     action \<leftarrow> gets scheduler_action;
-
-     if (target_dom \<noteq> cur_dom) then
-       tcb_sched_action tcb_sched_enqueue target
-     else if (action \<noteq> resume_cur_thread) then
-       do
-         reschedule_required;
-         tcb_sched_action tcb_sched_enqueue target
-       od
-     else
-       set_scheduler_action $ switch_thread target
-   od"
+end
 
-definition
-  next_domain :: "unit det_ext_monad" where
-  "next_domain \<equiv>
-    modify (\<lambda>s.
-      let domain_index' = (domain_index s + 1) mod length (domain_list s) in
-      let next_dom = (domain_list s)!domain_index'
-      in s\<lparr> domain_index := domain_index',
-            cur_domain := fst next_dom,
-            domain_time := snd next_dom,
-            work_units_completed := 0\<rparr>)"
 
-definition
-  dec_domain_time :: "unit det_ext_monad" where
-  "dec_domain_time = modify (\<lambda>s. s\<lparr>domain_time := domain_time s - 1\<rparr>)"
+section \<open>Basic Deterministic Monadic Accessors\<close>
 
 definition set_cdt_list :: "cdt_list \<Rightarrow> (det_state, unit) nondet_monad" where
   "set_cdt_list t \<equiv> do
@@ -369,9 +242,9 @@ text \<open>The CDT in the implementation is stored in prefix traversal order.
   The following functions traverse its abstract representation here to
   yield corresponding information.
 \<close>
+(* FIXME: use Lib.hd_opt instead *)
 definition next_child :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cslot_ptr option" where
-  "next_child slot t \<equiv> case (t slot) of [] \<Rightarrow> None |
-                                        x # xs \<Rightarrow> Some x"
+  "next_child slot t \<equiv> case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x"
 
 definition next_sib :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cdt \<Rightarrow> cslot_ptr option" where
   "next_sib slot t m \<equiv> case m slot of None \<Rightarrow> None |
@@ -380,10 +253,10 @@ definition next_sib :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cdt \<Rig
 
 function (domintros) next_not_child :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cdt \<Rightarrow> cslot_ptr option" where
   "next_not_child slot t m = (if next_sib slot t m = None
-                             then (case m slot of
-                               None \<Rightarrow> None |
-                               Some p \<Rightarrow> next_not_child p t m)
-                             else next_sib slot t m)"
+                              then case m slot of
+                                      None \<Rightarrow> None
+                                    | Some p \<Rightarrow> next_not_child p t m
+                              else next_sib slot t m)"
   by auto
 
 (* next_slot traverses the cdt, replicating mdb_next in the Haskell spec.
@@ -397,24 +270,8 @@ definition next_slot :: "cslot_ptr \<Rightarrow> cdt_list \<Rightarrow> cdt \<Ri
                         then next_child slot t
                         else next_not_child slot t m"
 
-text \<open>\emph{Extended operations} for the deterministic abstract specification.\<close>
-
-definition max_non_empty_queue :: "(priority \<Rightarrow> ready_queue) \<Rightarrow> ready_queue" where
-  "max_non_empty_queue queues \<equiv> queues (Max {prio. queues prio \<noteq> []})"
-
-
-definition default_ext :: "apiobject_type \<Rightarrow> domain \<Rightarrow> etcb option" where
-  "default_ext type cdom \<equiv>
-      case type of TCBObject \<Rightarrow> Some (default_etcb\<lparr>tcb_domain := cdom\<rparr>)
-                         | _ \<Rightarrow> None"
 
-definition retype_region_ext :: "obj_ref list \<Rightarrow> apiobject_type \<Rightarrow> unit det_ext_monad" where
-  "retype_region_ext ptrs type \<equiv>  do
-                                     ekh \<leftarrow> gets ekheap;
-                                     cdom \<leftarrow> gets cur_domain;
-                                     ekh' \<leftarrow> return $ foldr (\<lambda>p ekh. (ekh(p := default_ext type cdom))) ptrs ekh;
-                                     modify (\<lambda>s. s\<lparr>ekheap := ekh'\<rparr>)
-                                  od"
+text \<open>\emph{Extended operations} for the deterministic abstract specification.\<close>
 
 definition cap_swap_ext where
 "cap_swap_ext \<equiv> (\<lambda> slot1 slot2 slot1_op slot2_op.
@@ -442,44 +299,44 @@ definition cap_move_ext where
 "cap_move_ext \<equiv> (\<lambda> src_slot dest_slot src_p dest_p.
  do
 
-    update_cdt_list (\<lambda>list. case (dest_p) of
+    update_cdt_list (\<lambda>list. case dest_p of
       None \<Rightarrow> list |
       Some p \<Rightarrow> list (p := list_remove (list p) dest_slot));
 
-   if (src_slot = dest_slot) then return () else
+   if src_slot = dest_slot then return () else
 
     (do
-    update_cdt_list (\<lambda>list. case (src_p) of
+    update_cdt_list (\<lambda>list. case src_p of
       None \<Rightarrow> list |
       Some p \<Rightarrow> list (p := list_replace (list p) src_slot dest_slot));
 
-    update_cdt_list (\<lambda>list. list (src_slot := [], dest_slot := (list src_slot) @ (list dest_slot)))
+    update_cdt_list (\<lambda>list. list (src_slot := [], dest_slot := list src_slot @ list dest_slot))
     od)
 
   od)"
 
 
 definition cap_insert_ext where
-"cap_insert_ext \<equiv> (\<lambda> src_parent src_slot dest_slot src_p dest_p.
- do
-
- update_cdt_list (\<lambda>list. case (dest_p) of
-      None \<Rightarrow> list |
-      Some p \<Rightarrow> (list (p := list_remove (list p) dest_slot)));
-
-    update_cdt_list (\<lambda>list. case (src_p) of
-      None \<Rightarrow> list (
-        src_slot := if src_parent then [dest_slot] @ (list src_slot) else list src_slot) |
-      Some p \<Rightarrow> list (
-        src_slot := if src_parent then [dest_slot] @ (list src_slot) else list src_slot,
-        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))))
- od)"
+  "cap_insert_ext \<equiv> \<lambda>src_parent src_slot dest_slot src_p dest_p. do
+     update_cdt_list (\<lambda>list. case dest_p of
+       None \<Rightarrow> list
+     | Some p \<Rightarrow> list (p := list_remove (list p) dest_slot));
+     update_cdt_list (\<lambda>list. case src_p of
+       None \<Rightarrow> list (src_slot := if src_parent then [dest_slot] @ list src_slot else list src_slot)
+     | Some p \<Rightarrow> list (src_slot := if src_parent then [dest_slot] @ list src_slot else list src_slot,
+                       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))
+   od"
 
 definition empty_slot_ext where
-"empty_slot_ext \<equiv> (\<lambda> slot slot_p.
-
+"empty_slot_ext \<equiv> \<lambda> slot slot_p.
     update_cdt_list (\<lambda>list. case slot_p of None \<Rightarrow> list (slot := []) |
-      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 := [])))"
+      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 := []))"
 
 definition create_cap_ext where
 "create_cap_ext \<equiv> (\<lambda> untyped dest dest_p. do
@@ -519,86 +376,6 @@ definition work_units_limit_reached where
      return (work_units_limit \<le> work_units)
    od"
 
-text \<open>
-  A type class for all instantiations of the abstract specification. In
-  practice, this is restricted to basically allow only two sensible
-  implementations at present: the deterministic abstract specification and
-  the nondeterministic one.
-\<close>
-class state_ext =
- fixes unwrap_ext :: "'a state \<Rightarrow> det_ext state"
- fixes wrap_ext :: "(det_ext \<Rightarrow> det_ext) \<Rightarrow> ('a \<Rightarrow> 'a)"
- fixes wrap_ext_op :: "unit det_ext_monad \<Rightarrow> ('a state,unit) nondet_monad"
- fixes wrap_ext_bool :: "bool det_ext_monad \<Rightarrow> ('a state,bool) nondet_monad"
- fixes select_switch :: "'a \<Rightarrow> bool"
- fixes ext_init :: "'a"
-
-definition detype_ext :: "obj_ref set \<Rightarrow> 'z::state_ext \<Rightarrow> 'z" where
- "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>)"
-
-instantiation  det_ext_ext :: (type) state_ext
-begin
-
-definition "unwrap_ext_det_ext_ext == (\<lambda>x. x) :: det_ext state \<Rightarrow> det_ext state"
-
-definition "wrap_ext_det_ext_ext == (\<lambda>x. x) ::
-  (det_ext \<Rightarrow> det_ext) \<Rightarrow> det_ext \<Rightarrow> det_ext"
-
-definition "wrap_ext_op_det_ext_ext == (\<lambda>x. x) ::
-  (det_ext state \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool)
-  \<Rightarrow> det_ext state  \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool"
-
-definition "wrap_ext_bool_det_ext_ext == (\<lambda>x. x) ::
-  (det_ext state \<Rightarrow> ((bool \<times> det_ext state) set) \<times> bool)
-  \<Rightarrow> det_ext state \<Rightarrow> ((bool \<times> det_ext state) set) \<times> bool"
-
-definition "select_switch_det_ext_ext == (\<lambda>_. True)  :: det_ext\<Rightarrow> bool"
-
-(* this probably doesn't satisfy the invariants *)
-definition "ext_init_det_ext_ext \<equiv>
-     \<lparr>work_units_completed_internal = 0,
-      scheduler_action_internal = resume_cur_thread,
-      ekheap_internal = Map.empty (idle_thread_ptr \<mapsto> default_etcb),
-      domain_list_internal = [(0,15)],
-      domain_index_internal = 0,
-      cur_domain_internal = 0,
-      domain_time_internal = 15,
-      ready_queues_internal = const (const []),
-      cdt_list_internal = const []\<rparr> :: det_ext"
-
-instance ..
-
-end
-
-section "Nondeterministic Abstract Specification"
-
-text \<open>\label{s:nondet-spec}
-The nondeterministic abstract specification instantiates the extended state
-with the unit type -- i.e. it doesn't have any meaningful extended state.
-\<close>
-
-instantiation unit :: state_ext
-begin
-
-
-definition "unwrap_ext_unit == (\<lambda>_. undefined) :: unit state \<Rightarrow> det_ext state"
-
-definition "wrap_ext_unit == (\<lambda>f s. ()) :: (det_ext \<Rightarrow> det_ext) \<Rightarrow> unit \<Rightarrow> unit"
-
-
-definition "wrap_ext_op_unit == (\<lambda>m. return ()) ::
-  (det_ext state \<Rightarrow> ((unit \<times> det_ext state) set) \<times> bool) \<Rightarrow> unit state \<Rightarrow> ((unit \<times> unit state) set) \<times> bool"
-
-definition "wrap_ext_bool_unit == (\<lambda>m. select UNIV) ::
-  (det_ext state \<Rightarrow> ((bool \<times> det_ext state ) set) \<times> bool) \<Rightarrow> unit state \<Rightarrow> ((bool \<times> unit state) set) \<times> bool"
-
-definition "select_switch_unit == (\<lambda>s. False) :: unit \<Rightarrow> bool"
-
-definition "ext_init_unit \<equiv> () :: unit"
-
-instance ..
-
-end
 
 text \<open>Run an extended operation over the extended state without
   modifying it and use the return value to choose between two computations
@@ -638,14 +415,16 @@ text \<open>
   Use the extended state to choose a value from a bounding set @{term S} when
   @{term select_switch} is true. Otherwise just select from @{term S}.
 \<close>
-definition select_ext :: "(det_ext state \<Rightarrow> 'd) \<Rightarrow> ('d set) \<Rightarrow> ('a::state_ext state,'d) nondet_monad" where
+definition select_ext ::
+  "(det_ext state \<Rightarrow> 'd) \<Rightarrow> 'd set \<Rightarrow> ('a::state_ext state,'d) nondet_monad" where
   "select_ext a S \<equiv> do
-                      s \<leftarrow> get;
-                      x \<leftarrow> if (select_switch (exst s)) then (return (a (unwrap_ext s)))
-                          else (select S);
-                      assert (x \<in> S);
-                      return x
-                    od"
+     s \<leftarrow> get;
+     x \<leftarrow> if select_switch (exst s)
+          then return (a (unwrap_ext s))
+          else select S;
+     assert (x \<in> S);
+     return x
+   od"
 
 (*Defined here because it's asserted before empty_slot*)
 definition valid_list_2 :: "cdt_list \<Rightarrow> cdt \<Rightarrow> bool" where
diff --git a/spec/abstract/Interrupt_A.thy b/spec/abstract/Interrupt_A.thy
index 082c55869e..23515d177d 100644
--- a/spec/abstract/Interrupt_A.thy
+++ b/spec/abstract/Interrupt_A.thy
@@ -56,12 +56,12 @@ included in this model, so no scheduling action needs to be taken on timer
 ticks. If the IRQ has a valid Notification cap loaded a message is
 delivered.\<close>
 
-definition timer_tick :: "unit det_ext_monad" where
+definition timer_tick :: "(unit, 'z::state_ext) s_monad" where
   "timer_tick \<equiv> do
      cur \<leftarrow> gets cur_thread;
      state \<leftarrow> get_thread_state cur;
      case state of Running \<Rightarrow> do
-       ts \<leftarrow> ethread_get tcb_time_slice cur;
+       ts \<leftarrow> thread_get tcb_time_slice cur;
        let ts' = ts - 1 in
        if (ts' > 0) then thread_set_time_slice cur ts' else do
          thread_set_time_slice cur timeSlice;
@@ -78,12 +78,12 @@ definition timer_tick :: "unit det_ext_monad" where
    od"
 
 definition
-  handle_interrupt :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad" where
+  handle_interrupt :: "irq \<Rightarrow> (unit, 'z::state_ext) s_monad" where
  "handle_interrupt irq \<equiv>
    if irq > maxIRQ then do_machine_op $ do
     maskInterrupt True irq;
     ackInterrupt irq
-    od
+   od
   else do
    st \<leftarrow> get_irq_state irq;
    case st of
@@ -95,12 +95,12 @@ definition
        arch_mask_irq_signal irq
      od
    | IRQTimer \<Rightarrow> do
-       do_extended_op timer_tick;
+       timer_tick;
        do_machine_op resetTimer
      od
    | IRQInactive \<Rightarrow> fail \<comment> \<open>not meant to be able to get IRQs from inactive lines\<close>
    | IRQReserved \<Rightarrow> handle_reserved_irq irq;
    do_machine_op $ ackInterrupt irq
-   od"
+  od"
 
 end
diff --git a/spec/abstract/IpcCancel_A.thy b/spec/abstract/IpcCancel_A.thy
index f33ff6867c..4607ef52d9 100644
--- a/spec/abstract/IpcCancel_A.thy
+++ b/spec/abstract/IpcCancel_A.thy
@@ -55,8 +55,8 @@ where
                         queue \<leftarrow> get_ep_queue ep;
                         set_endpoint epptr IdleEP;
                         mapM_x (\<lambda>t. do set_thread_state t Restart;
-                                       do_extended_op (tcb_sched_action (tcb_sched_enqueue) t) od) $ queue;
-                        do_extended_op (reschedule_required)
+                                       tcb_sched_action (tcb_sched_enqueue) t od) $ queue;
+                        reschedule_required
                      od
    od"
 
@@ -82,7 +82,7 @@ where
                 st \<leftarrow> get_thread_state t;
                 if blocking_ipc_badge st = badge then do
                   set_thread_state t Restart;
-                  do_extended_op (tcb_sched_action (tcb_sched_enqueue) t);
+                  tcb_sched_action (tcb_sched_enqueue) t;
                   return False od
                 else return True
             od);
@@ -90,7 +90,7 @@ where
                            [] \<Rightarrow> IdleEP
                          | _ \<Rightarrow> SendEP queue');
             set_endpoint epptr ep';
-            do_extended_op (reschedule_required)
+            reschedule_required
         od
   od"
 
@@ -137,8 +137,8 @@ where
      case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> do
                       _ \<leftarrow> set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn;
                       mapM_x (\<lambda>t. do set_thread_state t Restart;
-                                     do_extended_op (tcb_sched_action tcb_sched_enqueue t) od) queue;
-                      do_extended_op (reschedule_required)
+                                     tcb_sched_action tcb_sched_enqueue t od) queue;
+                      reschedule_required
                      od
                | _ \<Rightarrow> return ()
    od"
@@ -372,7 +372,7 @@ where
      state \<leftarrow> get_thread_state thread;
      (if state = Running then update_restart_pc thread else return ());
      set_thread_state thread Inactive;
-     do_extended_op (tcb_sched_action (tcb_sched_dequeue) thread)
+     tcb_sched_action (tcb_sched_dequeue) thread
    od"
 
 end
diff --git a/spec/abstract/Ipc_A.thy b/spec/abstract/Ipc_A.thy
index 6ba07151dd..c90e98fc97 100644
--- a/spec/abstract/Ipc_A.thy
+++ b/spec/abstract/Ipc_A.thy
@@ -251,7 +251,7 @@ where
          do_ipc_transfer sender None 0 grant receiver;
          cap_delete_one slot;
          set_thread_state receiver Running;
-         do_extended_op (possible_switch_to receiver)
+         possible_switch_to receiver
       od
     | Some f \<Rightarrow> do
          cap_delete_one slot;
@@ -261,7 +261,7 @@ where
          restart \<leftarrow> handle_fault_reply f receiver (mi_label mi) mrs;
          thread_set (\<lambda>tcb. tcb \<lparr> tcb_fault := None \<rparr>) receiver;
          set_thread_state receiver (if restart then Restart else Inactive);
-         when restart $ do_extended_op (possible_switch_to receiver);
+         when restart $ possible_switch_to receiver;
          return ()
        od
   od"
@@ -330,7 +330,7 @@ where
                            od
                   | _ \<Rightarrow> fail;
                 set_thread_state dest Running;
-                do_extended_op (possible_switch_to dest);
+                possible_switch_to dest;
                 when call $
                   if (can_grant \<or> can_grant_reply)
                   then setup_caller_cap thread dest reply_can_grant
@@ -420,7 +420,7 @@ where
                 else set_thread_state sender Inactive
               else do
                 set_thread_state sender Running;
-                do_extended_op (possible_switch_to sender)
+                possible_switch_to sender
               od
             od
    od"
@@ -441,7 +441,7 @@ where
          ntfn_bound_tcb = bound_tcb \<rparr>;
      set_thread_state dest Running;
      as_user dest $ setRegister badge_register badge;
-     do_extended_op (possible_switch_to dest)
+     possible_switch_to dest
 
    od"
 
@@ -470,7 +470,7 @@ where
                       cancel_ipc tcb;
                       set_thread_state tcb Running;
                       as_user tcb $ setRegister badge_register badge;
-                      do_extended_op (possible_switch_to tcb)
+                      possible_switch_to tcb
                     od
                   else set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge)
             od
diff --git a/spec/abstract/KHeap_A.thy b/spec/abstract/KHeap_A.thy
index 3d9a4542e1..f4647f53b8 100644
--- a/spec/abstract/KHeap_A.thy
+++ b/spec/abstract/KHeap_A.thy
@@ -101,39 +101,6 @@ where
      set_object ref (TCB (tcb \<lparr> tcb_bound_notification := ntfn \<rparr>))
    od"
 
-definition set_thread_state_ext :: "obj_ref \<Rightarrow> unit det_ext_monad" where
-  "set_thread_state_ext t \<equiv> do
-     ts \<leftarrow> get_thread_state t;
-     cur \<leftarrow> gets cur_thread;
-     action \<leftarrow> gets scheduler_action;
-     when (\<not> (runnable ts) \<and> cur = t \<and> action = resume_cur_thread) (set_scheduler_action choose_new_thread)
-   od"
-
-definition
-  set_thread_state :: "obj_ref \<Rightarrow> thread_state \<Rightarrow> (unit,'z::state_ext) s_monad"
-where
-  "set_thread_state ref ts \<equiv> do
-     tcb \<leftarrow> gets_the $ get_tcb ref;
-     set_object ref (TCB (tcb \<lparr> tcb_state := ts \<rparr>));
-     do_extended_op (set_thread_state_ext ref)
-   od"
-
-definition
-  set_priority :: "obj_ref \<Rightarrow> priority \<Rightarrow> unit det_ext_monad" where
-  "set_priority tptr prio \<equiv> do
-     tcb_sched_action tcb_sched_dequeue tptr;
-     thread_set_priority tptr prio;
-     ts \<leftarrow> get_thread_state tptr;
-     when (runnable ts) $ do
-       cur \<leftarrow> gets cur_thread;
-       if tptr = cur then reschedule_required else possible_switch_to tptr
-     od
-   od"
-
-definition
-  set_mcpriority :: "obj_ref \<Rightarrow> priority \<Rightarrow> (unit, 'z::state_ext) s_monad"  where
-  "set_mcpriority ref mcp \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_mcpriority:=mcp\<rparr>) ref "
-
 
 section "simple kernel objects"
 (* to be used for abstraction unifying kernel objects other than TCB and CNode *)
@@ -158,10 +125,11 @@ lemma proj_ko_type_ntfn[simp]:
   "(\<exists>v. partial_inv Notification  ko = Some (v::notification)) = (a_type ko = ANTFN)"
   by (cases ko; auto simp: partial_inv_def a_type_def)
 
-
 abbreviation
   "is_simple_type \<equiv> (\<lambda>ob. a_type ob \<in> {AEndpoint, ANTFN})"
 
+section "getters/setters for simple kernel objects"
+(* to be used for abstraction unifying kernel objects other than TCB and CNode*)
 
 definition
   get_simple_ko :: "('a \<Rightarrow> kernel_object) \<Rightarrow> obj_ref \<Rightarrow> ('a,'z::state_ext) s_monad"
@@ -184,7 +152,6 @@ where
    od"
 
 
-
 section \<open>Synchronous and Asyncronous Endpoints\<close>
 
 
@@ -235,6 +202,122 @@ definition
   is_irq_active :: "irq \<Rightarrow> (bool,'z::state_ext) s_monad" where
  "is_irq_active irq \<equiv> liftM (\<lambda>st. st \<noteq> IRQInactive) $ get_irq_state irq"
 
+
+definition
+  get_tcb_queue :: "domain \<Rightarrow> priority \<Rightarrow> (ready_queue, 'z::state_ext) s_monad" where
+  "get_tcb_queue d prio \<equiv> do
+     queues \<leftarrow> gets ready_queues;
+     return (queues d prio)
+   od"
+
+definition
+  set_tcb_queue :: "domain \<Rightarrow> priority \<Rightarrow> ready_queue \<Rightarrow> (unit, 'z::state_ext) s_monad" where
+  "set_tcb_queue d prio queue \<equiv>
+     modify (\<lambda>es. es\<lparr> ready_queues :=
+      (\<lambda>d' p. if d' = d \<and> p = prio then queue else ready_queues es d' p)\<rparr>)"
+
+definition
+  tcb_sched_action :: "(obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list) \<Rightarrow> obj_ref
+                        \<Rightarrow> (unit, 'z::state_ext) s_monad"
+where
+  "tcb_sched_action action thread \<equiv> do
+     d \<leftarrow> thread_get tcb_domain thread;
+     prio \<leftarrow> thread_get tcb_priority thread;
+     queue \<leftarrow> get_tcb_queue d prio;
+     set_tcb_queue d prio (action thread queue)
+   od"
+
+definition
+  tcb_sched_enqueue :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where
+  "tcb_sched_enqueue thread queue \<equiv> if thread \<notin> set queue then thread # queue else queue"
+
+definition
+  tcb_sched_append :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where
+  "tcb_sched_append thread queue \<equiv> if thread \<notin> set queue then queue @ [thread] else queue"
+
+definition
+  tcb_sched_dequeue :: "obj_ref \<Rightarrow> obj_ref list \<Rightarrow> obj_ref list" where
+  "tcb_sched_dequeue thread queue \<equiv> filter ((\<noteq>) thread) queue"
+
+definition
+  set_scheduler_action :: "scheduler_action \<Rightarrow> (unit, 'z::state_ext) s_monad" where
+  "set_scheduler_action action \<equiv>
+     modify (\<lambda>es. es\<lparr>scheduler_action := action\<rparr>)"
+
+definition
+  thread_set_priority :: "obj_ref \<Rightarrow> priority \<Rightarrow> (unit, 'z::state_ext) s_monad" where
+  "thread_set_priority tptr prio \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_priority := prio\<rparr>) tptr"
+
+definition
+  thread_set_time_slice :: "obj_ref \<Rightarrow> nat \<Rightarrow> (unit, 'z::state_ext) s_monad" where
+  "thread_set_time_slice tptr time \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_time_slice := time\<rparr>) tptr"
+
+definition
+  thread_set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> (unit, 'z::state_ext) s_monad" where
+  "thread_set_domain tptr domain \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_domain := domain\<rparr>) tptr"
+
+definition reschedule_required :: "(unit, 'z::state_ext) s_monad" where
+  "reschedule_required \<equiv> do
+     action \<leftarrow> gets scheduler_action;
+     case action of
+       switch_thread t \<Rightarrow> tcb_sched_action (tcb_sched_enqueue) t | _ \<Rightarrow> return ();
+     set_scheduler_action choose_new_thread
+   od"
+
+definition
+  possible_switch_to :: "obj_ref \<Rightarrow> (unit, 'z::state_ext) s_monad" where
+  "possible_switch_to target \<equiv> do
+     cur_dom \<leftarrow> gets cur_domain;
+     target_dom \<leftarrow> thread_get tcb_domain target;
+     action \<leftarrow> gets scheduler_action;
+
+     if (target_dom \<noteq> cur_dom) then
+       tcb_sched_action tcb_sched_enqueue target
+     else if (action \<noteq> resume_cur_thread) then do
+         reschedule_required;
+         tcb_sched_action tcb_sched_enqueue target
+       od
+     else set_scheduler_action $ switch_thread target
+   od"
+
+definition
+  set_thread_state_act :: "obj_ref \<Rightarrow> (unit, 'z::state_ext) s_monad"
+where
+  "set_thread_state_act tcb_ptr \<equiv> do
+    ts \<leftarrow> get_thread_state tcb_ptr;
+    cur \<leftarrow> gets cur_thread;
+    sched_act \<leftarrow> gets scheduler_action;
+    when (tcb_ptr = cur \<and> sched_act = resume_cur_thread \<and> \<not> runnable ts) $ set_scheduler_action choose_new_thread
+  od"
+
+(***)
+
+definition
+  set_thread_state :: "obj_ref \<Rightarrow> thread_state \<Rightarrow> (unit,'z::state_ext) s_monad"
+where
+  "set_thread_state ref ts \<equiv> do
+     tcb \<leftarrow> gets_the $ get_tcb ref;
+     set_object ref (TCB (tcb \<lparr> tcb_state := ts \<rparr>));
+     set_thread_state_act ref
+   od"
+
+definition
+  set_priority :: "obj_ref \<Rightarrow> priority \<Rightarrow> (unit,'z::state_ext) s_monad" where
+  "set_priority tptr prio \<equiv> do
+     tcb_sched_action tcb_sched_dequeue tptr;
+     thread_set_priority tptr prio;
+     ts \<leftarrow> get_thread_state tptr;
+     when (runnable ts) $ do
+       cur \<leftarrow> gets cur_thread;
+       if tptr = cur then reschedule_required else possible_switch_to tptr
+     od
+   od"
+
+definition
+  set_mcpriority :: "obj_ref \<Rightarrow> priority \<Rightarrow> (unit, 'z::state_ext) s_monad"  where
+  "set_mcpriority ref mcp \<equiv> thread_set (\<lambda>tcb. tcb\<lparr>tcb_mcpriority:=mcp\<rparr>) ref "
+
+
 section "User Context"
 
 text \<open>
diff --git a/spec/abstract/Retype_A.thy b/spec/abstract/Retype_A.thy
index 9a6e6ede7f..d0eba76db9 100644
--- a/spec/abstract/Retype_A.thy
+++ b/spec/abstract/Retype_A.thy
@@ -62,11 +62,11 @@ definition
 
 text \<open>The initial state objects of various types are in when created.\<close>
 definition
-  default_object :: "apiobject_type \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> kernel_object" where
-  "default_object api dev n \<equiv> case api of
+  default_object :: "apiobject_type \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> domain \<Rightarrow> kernel_object" where
+  "default_object api dev n d \<equiv> case api of
            Untyped \<Rightarrow> undefined
          | CapTableObject \<Rightarrow> CNode n (empty_cnode n)
-         | TCBObject \<Rightarrow> TCB default_tcb
+         | TCBObject \<Rightarrow> TCB (default_tcb d)
          | EndpointObject \<Rightarrow> Endpoint default_ep
          | NotificationObject \<Rightarrow> Notification default_notification
          | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev n)"
@@ -78,7 +78,7 @@ definition
   "obj_bits_api type obj_size_bits \<equiv> case type of
            Untyped \<Rightarrow> obj_size_bits
          | CapTableObject \<Rightarrow> obj_size_bits + slot_bits
-         | TCBObject \<Rightarrow> obj_bits (TCB default_tcb)
+         | TCBObject \<Rightarrow> obj_bits (TCB (default_tcb default_domain))
          | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined)
          | NotificationObject \<Rightarrow> obj_bits (Notification undefined)
          | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False obj_size_bits"
@@ -99,8 +99,8 @@ where
     ptrs \<leftarrow> return $ map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..< numObjects];
     when (type \<noteq> Untyped) (do
       kh \<leftarrow> gets kheap;
-      kh' \<leftarrow> return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) ptrs kh;
-      do_extended_op (retype_region_ext ptrs type);
+      cd \<leftarrow> gets cur_domain;
+      kh' \<leftarrow> return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits cd)) ptrs kh;
       modify $ kheap_update (K kh')
     od);
     return $ ptrs
@@ -113,7 +113,7 @@ abbreviation (input) "extended_state_update \<equiv> trans_state"
 text \<open>Remove objects from a region of the heap.\<close>
 definition
   detype :: "(obj_ref set) \<Rightarrow> 'z::state_ext state \<Rightarrow> 'z::state_ext state" where
- "detype S s \<equiv> s \<lparr> kheap := (\<lambda>x. if x \<in> S then None else kheap s x), extended_state := detype_ext S (exst s)\<rparr>"
+ "detype S s \<equiv> s \<lparr> kheap := (\<lambda>x. if x \<in> S then None else kheap s x)\<rparr>"
 
 text \<open>Delete objects within a specified region.\<close>
 definition
diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy
index a541a1dc88..d95124a9e8 100644
--- a/spec/abstract/Schedule_A.thy
+++ b/spec/abstract/Schedule_A.thy
@@ -4,10 +4,6 @@
  * SPDX-License-Identifier: GPL-2.0-only
  *)
 
-(*
-Non-deterministic scheduler functionality.
-*)
-
 chapter "Scheduler"
 
 theory Schedule_A
@@ -46,16 +42,17 @@ definition
      state \<leftarrow> get;
      assert (get_tcb t state \<noteq> None);
      arch_switch_to_thread t;
-     do_extended_op (tcb_sched_action (tcb_sched_dequeue) t);
+     tcb_sched_action (tcb_sched_dequeue) t;
      modify (\<lambda>s. s \<lparr> cur_thread := t \<rparr>)
    od"
 
 text \<open>Asserts that a thread is runnable before switching to it.\<close>
-definition guarded_switch_to :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
-"guarded_switch_to thread \<equiv> do ts \<leftarrow> get_thread_state thread;
-                    assert (runnable ts);
-                    switch_to_thread thread
-                 od"
+definition guarded_switch_to :: "obj_ref \<Rightarrow> (unit, 'z::state_ext) s_monad" where
+  "guarded_switch_to thread \<equiv> do
+     ts \<leftarrow> get_thread_state thread;
+     assert (runnable ts);
+     switch_to_thread thread
+    od"
 
 text \<open>Switches to the idle thread.\<close>
 definition
@@ -66,36 +63,47 @@ definition
      modify (\<lambda>s. s \<lparr> cur_thread := thread \<rparr>)
    od"
 
-class state_ext_sched = state_ext +
-  fixes schedule :: "(unit,'a) s_monad"
+definition
+  next_domain :: "(unit, 'z::state_ext) s_monad" where
+  "next_domain \<equiv> do
+    modify (\<lambda>s.
+      let domain_index' = (domain_index s + 1) mod length (domain_list s) in
+      let next_dom = (domain_list s)!domain_index'
+      in s\<lparr> domain_index := domain_index',
+            cur_domain := fst next_dom,
+            domain_time := snd next_dom\<rparr>);
+    do_extended_op $ modify (\<lambda>s. s \<lparr>work_units_completed := 0\<rparr>)
+  od"
 
-definition choose_thread :: "det_ext state \<Rightarrow> (unit \<times> det_ext state) set \<times> bool" where
-"choose_thread \<equiv>
-      do
-        d \<leftarrow> gets cur_domain;
-        queues \<leftarrow> gets (\<lambda>s. ready_queues s d);
-        if (\<forall>prio. queues prio = []) then (switch_to_idle_thread)
-        else (guarded_switch_to (hd (max_non_empty_queue queues)))
-      od"
+definition
+  dec_domain_time :: "(unit, 'z::state_ext) s_monad" where
+  "dec_domain_time = modify (\<lambda>s. s\<lparr>domain_time := domain_time s - 1\<rparr>)"
+
+definition max_non_empty_queue :: "(priority \<Rightarrow> ready_queue) \<Rightarrow> ready_queue" where
+  "max_non_empty_queue queues \<equiv> queues (Max {prio. queues prio \<noteq> []})"
+
+definition choose_thread :: "(unit, 'z::state_ext) s_monad" where
+  "choose_thread \<equiv> do
+     d \<leftarrow> gets cur_domain;
+     queues \<leftarrow> gets (\<lambda>s. ready_queues s d);
+     if \<forall>prio. queues prio = []
+     then switch_to_idle_thread
+     else guarded_switch_to (hd (max_non_empty_queue queues))
+   od"
 
 text \<open>
   Determine whether given priority is highest among queued ready threads in given domain.
   Trivially true if no threads are ready.\<close>
 definition
-  is_highest_prio :: "domain \<Rightarrow> priority \<Rightarrow> det_ext state \<Rightarrow> bool"
+  is_highest_prio :: "domain \<Rightarrow> priority \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
 where
   "is_highest_prio d p s \<equiv>
     (\<forall>prio. ready_queues s d prio = [])
     \<or> p \<ge> Max {prio. ready_queues s d prio \<noteq> []}"
 
-instantiation  det_ext_ext :: (type) state_ext_sched
-begin
-
 definition
   "schedule_switch_thread_fastfail ct it ct_prio target_prio \<equiv>
-     if ct \<noteq> it
-     then return (target_prio < ct_prio)
-     else return True"
+     return $ ct \<noteq> it \<longrightarrow> target_prio < ct_prio"
 
 definition
   "schedule_choose_new_thread \<equiv> do
@@ -106,7 +114,7 @@ definition
    od"
 
 definition
-  "schedule_det_ext_ext \<equiv> do
+  "schedule \<equiv> do
      ct \<leftarrow> gets cur_thread;
      ct_st \<leftarrow> get_thread_state ct;
      ct_runnable \<leftarrow> return $ runnable ct_st;
@@ -125,10 +133,10 @@ definition
            when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
 
            it \<leftarrow> gets idle_thread;
-           target_prio \<leftarrow> ethread_get tcb_priority candidate;
+           target_prio \<leftarrow> thread_get tcb_priority candidate;
 
            \<comment> \<open>Infoflow does not like asking about the idle thread's priority or domain.\<close>
-           ct_prio \<leftarrow> ethread_get_when (ct \<noteq> it) tcb_priority ct;
+           ct_prio \<leftarrow> if ct \<noteq> it then thread_get tcb_priority ct else return 0;
            \<comment> \<open>When to look at the bitmaps. This optimisation is used in the C fast path,
               but there we know @{text cur_thread} is not idle.\<close>
            fastfail \<leftarrow> schedule_switch_thread_fastfail ct it ct_prio target_prio;
@@ -159,44 +167,4 @@ definition
         od)
     od"
 
-instance ..
-end
-
-
-instantiation unit :: state_ext_sched
-begin
-
-
-text \<open>
-  The scheduler is heavily underspecified.
-  It is allowed to pick any active thread or the idle thread.
-  If the thread the scheduler picked is the current thread, it
-  may omit the call to @{const switch_to_thread}. Likewise it
-  may omit the call to @{const switch_to_idle_thread} if the
-  idle thread is the current thread.
-\<close>
-definition schedule_unit :: "(unit,unit) s_monad" where
-"schedule_unit \<equiv> (do
-   cur \<leftarrow> gets cur_thread;
-   threads \<leftarrow> allActiveTCBs;
-   thread \<leftarrow> select threads;
-   (if thread = cur then
-     return () \<sqinter> switch_to_thread thread
-   else
-     switch_to_thread thread)
- od) \<sqinter>
- (do
-   cur \<leftarrow> gets cur_thread;
-   idl \<leftarrow> gets idle_thread;
-   if idl = cur then
-     return () \<sqinter> switch_to_idle_thread
-   else switch_to_idle_thread
-  od)"
-
-instance ..
-end
-
-
-lemmas schedule_def = schedule_det_ext_ext_def schedule_unit_def
-
 end
diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy
index b8c7a568ca..1c9c17d636 100644
--- a/spec/abstract/Structures_A.thy
+++ b/spec/abstract/Structures_A.thy
@@ -367,6 +367,8 @@ datatype thread_state
 
 type_synonym priority = word8
 
+type_synonym domain = word8
+
 record tcb =
  tcb_ctable        :: cap
  tcb_vtable        :: cap
@@ -377,8 +379,11 @@ record tcb =
  tcb_fault_handler :: cap_ref
  tcb_ipc_buffer    :: vspace_ref
  tcb_fault         :: "fault option"
- tcb_bound_notification     :: "obj_ref option"
+ tcb_bound_notification :: "obj_ref option"
  tcb_mcpriority    :: priority
+ tcb_priority      :: priority
+ tcb_time_slice    :: nat
+ tcb_domain        :: domain
  tcb_arch          :: arch_tcb (* arch_tcb must have a field for user context *)
 
 
@@ -396,9 +401,15 @@ where
 | "runnable (BlockedOnReply)        = False"
 
 
+definition default_domain :: "domain" where
+  "default_domain \<equiv> minBound"
+
+definition default_priority :: "priority" where
+  "default_priority \<equiv> minBound"
+
 definition
-  default_tcb :: tcb where
-  "default_tcb \<equiv> \<lparr>
+  default_tcb :: "domain \<Rightarrow> tcb" where
+  "default_tcb d \<equiv> \<lparr>
       tcb_ctable   = NullCap,
       tcb_vtable   = NullCap,
       tcb_reply    = NullCap,
@@ -410,6 +421,9 @@ definition
       tcb_fault      = None,
       tcb_bound_notification  = None,
       tcb_mcpriority = minBound,
+      tcb_priority   = default_priority,
+      tcb_time_slice = timeSlice,
+      tcb_domain     = d,
       tcb_arch       = default_arch_tcb\<rparr>"
 
 text \<open>
@@ -506,6 +520,15 @@ datatype irq_state =
  | IRQTimer
  | IRQReserved
 
+text \<open>The current scheduler action,
+  which is part of the scheduling state.\<close>
+datatype scheduler_action =
+    resume_cur_thread
+  | switch_thread (sch_act_target : obj_ref)
+  | choose_new_thread
+
+type_synonym ready_queue = "obj_ref list"
+
 text \<open>The kernel state includes a heap, a capability derivation tree
 (CDT), a bitmap used to determine if a capability is the original
 capability to that object, a pointer to the current thread, a pointer
@@ -527,6 +550,12 @@ record abstract_state =
   is_original_cap    :: "cslot_ptr \<Rightarrow> bool"
   cur_thread         :: obj_ref
   idle_thread        :: obj_ref
+  scheduler_action   :: scheduler_action
+  domain_list        :: "(domain \<times> machine_word) list"
+  domain_index       :: nat
+  cur_domain         :: domain
+  domain_time        :: "machine_word"
+  ready_queues       :: "domain \<Rightarrow> priority \<Rightarrow> ready_queue"
   machine_state      :: machine_state
   interrupt_irq_node :: "irq \<Rightarrow> obj_ref"
   interrupt_states   :: "irq \<Rightarrow> irq_state"
diff --git a/spec/abstract/Syscall_A.thy b/spec/abstract/Syscall_A.thy
index e3f5bafb76..605cbcb5c0 100644
--- a/spec/abstract/Syscall_A.thy
+++ b/spec/abstract/Syscall_A.thy
@@ -249,9 +249,9 @@ definition
   handle_yield :: "(unit,'z::state_ext) s_monad" where
   "handle_yield \<equiv> do
      thread \<leftarrow> gets cur_thread;
-     do_extended_op (tcb_sched_action (tcb_sched_dequeue) thread);
-     do_extended_op (tcb_sched_action (tcb_sched_append) thread);
-     do_extended_op (reschedule_required)
+     tcb_sched_action (tcb_sched_dequeue) thread;
+     tcb_sched_action (tcb_sched_append) thread;
+     reschedule_required
    od"
 
 definition
@@ -374,7 +374,7 @@ text \<open>
 \<close>
 
 definition
-  call_kernel :: "event \<Rightarrow> (unit,'z::state_ext_sched) s_monad" where
+  call_kernel :: "event \<Rightarrow> (unit, 'z::state_ext) s_monad" where
   "call_kernel ev \<equiv> do
        handle_event ev <handle>
            (\<lambda>_. without_preemption $ do
diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy
index 89fe35d96a..51aa1bddd6 100644
--- a/spec/abstract/Tcb_A.thy
+++ b/spec/abstract/Tcb_A.thy
@@ -44,8 +44,8 @@ definition
       cancel_ipc thread;
       setup_reply_master thread;
       set_thread_state thread Restart;
-      do_extended_op (tcb_sched_action (tcb_sched_enqueue) thread);
-      do_extended_op (possible_switch_to thread)
+      tcb_sched_action (tcb_sched_enqueue) thread;
+      possible_switch_to thread
     od
   od"
 
@@ -176,11 +176,11 @@ where
           $ check_cap_at (ThreadCap target) slot
           $ cap_insert new_cap src_slot (target, tcb_cnode_index 4);
       cur \<leftarrow> liftE $ gets cur_thread;
-      liftE $ when (target = cur) (do_extended_op reschedule_required)
+      liftE $ when (target = cur) reschedule_required
     odE);
     liftE $ case priority
               of None \<Rightarrow> return()
-               | Some (prio, _) \<Rightarrow> do_extended_op (set_priority target prio);
+               | Some (prio, _) \<Rightarrow> set_priority target prio;
     returnOk []
   odE"
 
@@ -203,7 +203,7 @@ where
         od) gpRegisters;
     cur \<leftarrow> gets cur_thread;
     arch_post_modify_registers cur dest;
-    when (dest = cur) (do_extended_op reschedule_required);
+    when (dest = cur) reschedule_required;
     return []
   od)"
 
@@ -227,7 +227,7 @@ where
     od;
     arch_post_modify_registers self dest;
     when resume_target $ restart dest;
-    when (dest = self) (do_extended_op reschedule_required);
+    when (dest = self) reschedule_required;
     return []
   od)"
 
@@ -247,25 +247,25 @@ where
   (liftE $ do
     as_user tcb $ setRegister tlsBaseRegister tls_base;
     cur \<leftarrow> gets cur_thread;
-    when (tcb = cur) (do_extended_op reschedule_required);
+    when (tcb = cur) reschedule_required;
     return []
   od)"
 
 definition
-  set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
+  set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> (unit, 'z::state_ext) s_monad" where
   "set_domain tptr new_dom \<equiv> do
      cur \<leftarrow> gets cur_thread;
      tcb_sched_action tcb_sched_dequeue tptr;
      thread_set_domain tptr new_dom;
      ts \<leftarrow> get_thread_state tptr;
-     when (runnable ts) (tcb_sched_action tcb_sched_enqueue tptr);
-     when (tptr = cur) reschedule_required
+     when (runnable ts) $ tcb_sched_action tcb_sched_enqueue tptr;
+     when (tptr = cur) $ reschedule_required
    od"
 
 definition invoke_domain:: "obj_ref \<Rightarrow> domain \<Rightarrow> (data list,'z::state_ext) p_monad"
 where
   "invoke_domain thread domain \<equiv>
-     liftE (do do_extended_op (set_domain thread domain); return [] od)"
+     liftE (do set_domain thread domain; return [] od)"
 
 text \<open>Get all of the message registers, both from the sending thread's current
 register file and its IPC buffer.\<close>