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

@@ -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,

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

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,15 +82,15 @@ 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);
             ep' \<leftarrow> return (case queue' of
                            [] \<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

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

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>

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