aarch64: updates for GICv3 split EOI mode

Brings changes for split EOI (End Of Interrupt) mode from seL4/seL4#1183
into the verification.

Most of what changes in the seL4 pull request is underneath the machine
interface and implements a different mechanism for masking/unmasking
interrupts (using priority drop instead of actual masking/unmasking).
For the purposes of the proof, what we want from the hardware remains
the same: when deactivated, the interrupt will no longer fire.

Signed-off-by: Gerwin Klein <[email protected]>

proof/crefine/AARCH64/Interrupt_C.thy

@@ -15,9 +15,17 @@ lemma invokeIRQHandler_AckIRQ_ccorres:
   "ccorres dc xfdc
        invs' (UNIV \<inter> {s. irq_' s = ucast irq}) []
      (InterruptDecls_H.invokeIRQHandler (AckIRQ irq)) (Call invokeIRQHandler_AckIRQ_'proc)"
-  apply (cinit lift: irq_' simp: Interrupt_H.invokeIRQHandler_def invokeIRQHandler_def)
+  (* C has "if (config_set(CONFIG_ARM_GIC_V3_SUPPORT))", which will render as IF 0 = 1 or IF 1 = 1.
+     Pretend we don't know what the result of that is and make a case distinction that matches
+     the condition up with config_ARM_GIC_V3. *)
+  apply (cinit (no_ccorres_rewrite)
+               lift: irq_'
+               simp: Interrupt_H.invokeIRQHandler_def invokeIRQHandler_def dmo_if)
+   apply (rule ccorres_cond_both'[where Q=\<top> and Q'=\<top>])
+     apply (simp add: Kernel_Config.config_ARM_GIC_V3_def) (* match C condition *)
+    apply (ctac add: deactivateInterrupt_ccorres)
    apply (ctac add: maskInterrupt_ccorres)
-  apply simp
+  apply (simp add: theIRQ_def)
   done
 
 lemma getIRQSlot_ccorres:

proof/crefine/AARCH64/Machine_C.thy

@@ -62,6 +62,12 @@ assumes maskInterrupt_ccorres:
            (doMachineOp (maskInterrupt m irq))
            (Call maskInterrupt_'proc)"
 
+(* This function is only implemented on GICv3 configs, hence the precondition *)
+assumes deactivateInterrupt_ccorres:
+  "ccorres dc xfdc (\<lambda>_. config_ARM_GIC_V3) (\<lbrace>\<acute>irq = ucast irq\<rbrace>) []
+           (doMachineOp (deactivateInterrupt irq))
+           (Call deactivateInterrupt_'proc)"
+
 (* This is a simplification until complete FPU handling is added at a future date *)
 assumes fpuThreadDelete_ccorres:
   "ccorres dc xfdc (tcb_at' thread) (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs

proof/crefine/AARCH64/Syscall_C.thy

@@ -2229,26 +2229,45 @@ lemma ccorres_handleReservedIRQ:
                   simp flip: word_unat.Rep_inject split: if_splits)
   done
 
+(* Because of a case distinction, this proof occurs multiple times in handleInterrupt_ccorres below.
+   The proof is carefully manual to match up the C expression
+   "if (!config_set(CONFIG_ARM_GIC_V3_SUPPORT))", which renders as IF False or IF True in Simpl,
+   with config_ARM_GIC_V3 from the spec side. *)
+method maybe_maskInterrupt_before_ack =
+    simp only: maskIrqSignal_def when_def,
+    rule ccorres_cond_seq,
+    rule ccorres_cond_both[where P="\<lambda>_. \<not>config_ARM_GIC_V3" and R=\<top>],
+       simp add: Kernel_Config.config_ARM_GIC_V3_def, (* match up !config_set(..) condition *)
+      rule ccorres_gen_asm[where P="\<not>config_ARM_GIC_V3"],
+      simp,
+      ctac (no_vcg) add: maskInterrupt_ccorres,
+       ctac add: ackInterrupt_ccorres,
+      wp,
+     rule ccorres_gen_asm[where P="config_ARM_GIC_V3"],
+     simp,
+     ctac add: ackInterrupt_ccorres
+
 lemma handleInterrupt_ccorres:
   "ccorres dc xfdc
      (invs' and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> sch_act_not (ksCurThread s) s))
      \<lbrace>\<acute>irq = ucast irq\<rbrace>
      hs
      (handleInterrupt irq)
      (Call handleInterrupt_'proc)"
-  apply (cinit lift: irq_' cong: call_ignore_cong)
+  (* Use (no_ccorres_rewrite) to avoid rewriting the static condition coming out of
+     "if (!config_set(CONFIG_ARM_GIC_V3_SUPPORT))" in C *)
+  apply (cinit (no_ccorres_rewrite) lift: irq_' cong: call_ignore_cong)
    apply (rule ccorres_Cond_rhs_Seq)
     apply (simp add:  Kernel_C_maxIRQ del: Collect_const)
     apply (rule ccorres_rhs_assoc)+
     apply (subst doMachineOp_bind)
       apply (rule maskInterrupt_empty_fail)
      apply (rule ackInterrupt_empty_fail)
+    apply ccorres_rewrite
     apply (ctac add: maskInterrupt_ccorres)
       apply (subst bind_return_unit[where f="doMachineOp (ackInterrupt irq)"])
       apply (ctac add: ackInterrupt_ccorres)
-        apply (rule ccorres_split_throws)
-         apply (rule ccorres_return_void_C)
-        apply vcg
+        apply (rule ccorres_return_void_C)
        apply wp
       apply (vcg exspec=ackInterrupt_modifies)
      apply wp
@@ -2285,31 +2304,26 @@ lemma handleInterrupt_ccorres:
          apply csymbr
          apply csymbr
          apply (ctac (no_vcg) add: sendSignal_ccorres)
-          apply (simp add: maskIrqSignal_def)
-          apply (ctac (no_vcg) add: maskInterrupt_ccorres)
-           apply (ctac add: ackInterrupt_ccorres)
-          apply wp+
+          apply maybe_maskInterrupt_before_ack
+         apply clarsimp
+         apply wp
         apply (simp del: Collect_const)
         apply (rule ccorres_cond_true_seq)
         apply (rule ccorres_rhs_assoc)+
         apply csymbr+
         apply (rule ccorres_cond_false_seq)
-        apply (simp add: maskIrqSignal_def)
-        apply (ctac (no_vcg) add: maskInterrupt_ccorres)
-         apply (ctac add: ackInterrupt_ccorres)
-        apply wp
+        apply (rule ccorres_seq_skip[THEN iffD2])
+        apply maybe_maskInterrupt_before_ack
        apply (rule_tac P=\<top> and P'="{s. ret__int_' s = 0 \<and> cap_get_tag cap \<noteq> scast cap_notification_cap}" in ccorres_inst)
        apply (clarsimp simp: isCap_simps simp del: Collect_const)
        apply (case_tac rva, simp_all del: Collect_const)[1]
                   prefer 3
                   apply metis
-                 apply ((simp add: maskIrqSignal_def,
-                        rule ccorres_guard_imp2,
-                        rule ccorres_cond_false_seq, simp,
+                 apply ((rule ccorres_guard_imp2,
                         rule ccorres_cond_false_seq, simp,
-                        ctac (no_vcg) add: maskInterrupt_ccorres,
-                        ctac (no_vcg) add: ackInterrupt_ccorres,
-                        wp, simp)+)
+                        rule ccorres_cond_false_seq, rule ccorres_seq_skip[THEN iffD2],
+                        maybe_maskInterrupt_before_ack,
+                        simp)+)[11]
       apply (wpsimp wp: getSlotCap_wp)
      apply simp
      apply vcg

proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy

@@ -65,7 +65,7 @@ lemma invoke_irq_control_bcorres[wp]: "bcorres (invoke_irq_control a) (invoke_ir
   done
 
 lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_irq_handler a)"
-  by (cases a; wpsimp)
+  by (cases a; (wpsimp | rule conjI)+)
 
 lemma make_arch_fault_msg_bcorres[wp,BCorres2_AI_assms]:
   "bcorres (make_arch_fault_msg a b) (make_arch_fault_msg a b)"

proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy

@@ -194,6 +194,11 @@ lemma vgic_maintenance_empty_fail[wp]: "empty_fail vgic_maintenance"
                    get_gic_vcpu_ctrl_misr_def
                    vgic_maintenance_def)
 
+lemma deactivateInterrupt_empty_fail[wp]:
+  "config_ARM_GIC_V3 \<Longrightarrow> empty_fail (deactivateInterrupt irq)"
+  unfolding deactivateInterrupt_def
+  by wpsimp
+
 crunch possible_switch_to, handle_event, activate_thread
   for (empty_fail) empty_fail[wp, EmptyFail_AI_assms]
   (simp: cap.splits arch_cap.splits split_def invocation_label.splits Let_def

proof/invariant-abstract/AARCH64/ArchInterrupt_AI.thy

@@ -82,10 +82,10 @@ lemma maskInterrupt_invs_ARCH[Interrupt_AI_assms]:
                          cur_tcb_def valid_irq_states_def valid_irq_masks_def)
   done
 
-crunch plic_complete_claim
+crunch plic_complete_claim (* FIXME AARCH64: remove plic_complete_claim *)
   for device_state_inv[wp]: "\<lambda>ms. P (device_state ms)"
 
-lemma dmo_plic_complete_claim[wp]:
+lemma dmo_plic_complete_claim[wp]: (* FIXME AARCH64: remove plic_complete_claim *)
   "do_machine_op (plic_complete_claim irq) \<lbrace>invs\<rbrace>"
   apply (wp dmo_invs)
   apply (auto simp: plic_complete_claim_def machine_op_lift_def machine_rest_lift_def in_monad select_f_def)
@@ -109,6 +109,14 @@ lemma (* set_irq_state_valid_cap *)[Interrupt_AI_assms]:
 crunch set_irq_state
   for valid_global_refs[Interrupt_AI_assms]: "valid_global_refs"
 
+lemma deactivateInterrupt_invs:
+  "\<lbrace>invs and (\<lambda>s. interrupt_states s irq \<noteq> IRQInactive) and K config_ARM_GIC_V3\<rbrace>
+   do_machine_op (deactivateInterrupt irq)
+   \<lbrace>\<lambda>rv. invs\<rbrace>"
+  unfolding deactivateInterrupt_def
+  by (cases config_ARM_GIC_V3; simp)
+     (wpsimp wp: maskInterrupt_invs)
+
 lemma invoke_irq_handler_invs'[Interrupt_AI_assms]:
   assumes dmo_ex_inv[wp]: "\<And>f. \<lbrace>invs and ex_inv\<rbrace> do_machine_op f \<lbrace>\<lambda>rv::unit. ex_inv\<rbrace>"
   assumes cap_insert_ex_inv[wp]: "\<And>cap src dest.
@@ -139,8 +147,7 @@ lemma invoke_irq_handler_invs'[Interrupt_AI_assms]:
    done
   show ?thesis
   apply (cases i, simp_all)
-    apply (wp dmo_plic_complete_claim maskInterrupt_invs)
-    apply simp+
+    apply (rule conjI; wpsimp wp: deactivateInterrupt_invs maskInterrupt_invs)
    apply (rename_tac irq cap prod)
    apply (rule hoare_pre)
     apply (wp valid_cap_typ [OF cap_delete_one_typ_at])

proof/refine/AARCH64/Interrupt_R.thy

@@ -334,16 +334,16 @@ lemma valid_globals_ex_cte_cap_irq:
   apply (simp add: global_refs'_def cte_level_bits_def cteSizeBits_def shiftl_t2n mult.commute mult.left_commute)
   done
 
-lemma no_fail_plic_complete_claim [simp, wp]:
-  "no_fail \<top> (AARCH64.plic_complete_claim irw)"
-  unfolding AARCH64.plic_complete_claim_def
-  by (rule no_fail_machine_op_lift)
+lemma no_fail_deactivateInterrupt[wp, simp]:
+  "config_ARM_GIC_V3 \<Longrightarrow> no_fail \<top> (deactivateInterrupt irq)"
+  unfolding deactivateInterrupt_def
+  by wpsimp
 
 lemma arch_invokeIRQHandler_corres:
   "irq_handler_inv_relation i i' \<Longrightarrow>
    corres dc \<top> \<top> (arch_invoke_irq_handler i) (AARCH64_H.invokeIRQHandler i')"
-  apply (cases i; clarsimp simp: AARCH64_H.invokeIRQHandler_def)
-  apply (rule corres_machine_op, rule corres_Id; simp?)
+  apply (cases i; clarsimp simp: AARCH64_H.invokeIRQHandler_def theIRQ_def)
+  apply (intro conjI impI; rule corres_machine_op, rule corres_Id; simp?)
   done
 
 
@@ -429,9 +429,16 @@ lemma doMachineOp_maskInterrupt_False[wp]:
                    ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def)
   done
 
+lemma doMachineOp_deactivateInterrupt[wp]:
+  "\<lbrace> \<lambda>s. invs' s \<and> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive \<and> config_ARM_GIC_V3 \<rbrace>
+   doMachineOp (deactivateInterrupt irq)
+   \<lbrace>\<lambda>_. invs'\<rbrace>"
+  unfolding deactivateInterrupt_def
+  by (cases config_ARM_GIC_V3; wpsimp)
+
 lemma invoke_arch_irq_handler_invs'[wp]:
   "\<lbrace>invs' and irq_handler_inv_valid' i\<rbrace> AARCH64_H.invokeIRQHandler i \<lbrace>\<lambda>rv. invs'\<rbrace>"
-  by (cases i; wpsimp simp: AARCH64_H.invokeIRQHandler_def)
+  by (cases i; (wpsimp simp: AARCH64_H.invokeIRQHandler_def theIRQ_def | rule conjI)+)
 
 lemma invoke_irq_handler_invs'[wp]:
   "\<lbrace>invs' and irq_handler_inv_valid' i\<rbrace>

spec/abstract/AARCH64/ArchInterrupt_A.thy

@@ -77,11 +77,15 @@ definition handle_reserved_irq :: "irq \<Rightarrow> (unit,'z::state_ext) s_mona
    od"
 
 fun arch_invoke_irq_handler :: "irq_handler_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
-  "arch_invoke_irq_handler (ACKIrq irq) = (do_machine_op $ maskInterrupt False irq)"
+  "arch_invoke_irq_handler (ACKIrq irq) =
+     do_machine_op (if Kernel_Config.config_ARM_GIC_V3
+                    then deactivateInterrupt irq
+                    else maskInterrupt False irq)"
 | "arch_invoke_irq_handler _ = return ()"
 
 definition arch_mask_irq_signal :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad" where
-  "arch_mask_irq_signal irq \<equiv> do_machine_op $ maskInterrupt True irq"
+  "arch_mask_irq_signal irq \<equiv>
+     when (\<not>Kernel_Config.config_ARM_GIC_V3) (do_machine_op $ maskInterrupt True irq)"
 
 end
 

spec/design/skel/AARCH64/Hardware_H.thy

@@ -15,7 +15,7 @@ context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs Platform=Platform.AARCH64 CONTEXT AARCH64_H \
   NOT PT_Type plic_complete_claim getMemoryRegions getDeviceRegions getKernelDevices \
-  loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt \
+  loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt deactivateInterrupt \
   configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory \
   clearMemoryVM initMemory freeMemory setHardwareASID wordFromPDE wordFromPTE \
   VMFaultType HypFaultType VMPageSize pageBits pageBitsForSize toPAddr \

spec/haskell/src/SEL4/Machine/Hardware.lhs

@@ -66,7 +66,7 @@ Depending on the architecture, real physical addresses may be the same as the ad
 
 An interrupt request from an external device, or from the CPU's timer, is represented by the type "IRQ".
 
-> newtype IRQ = IRQ Arch.IRQ
+> newtype IRQ = IRQ { theIRQ :: Arch.IRQ }
 >     deriving (Enum, Bounded, Ord, Ix, Eq, Show)
 
 The maximum and minimum IRQ are given explicit constant names here. In Haskell, these are extracted from instantiation of IRQ into the Bounded class. In the formalisation, these constants are generated and defined in Kernel_Config.thy.

spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs

@@ -382,6 +382,9 @@ maskInterrupt maskI irq = do
     cbptr <- ask
     liftIO $ Platform.maskInterrupt cbptr maskI irq
 
+deactivateInterrupt :: IRQ -> MachineMonad ()
+deactivateInterrupt irq = error "Unimplemented - GICv3 machine op"
+
 debugPrint :: String -> MachineMonad ()
 debugPrint str = liftIO $ putStrLn str
 

spec/haskell/src/SEL4/Object/Interrupt/AARCH64.hs

@@ -24,6 +24,7 @@ import SEL4.API.InvocationLabels.AARCH64 as ArchLabels
 import {-# SOURCE #-} SEL4.Object.CNode
 import {-# SOURCE #-} SEL4.Kernel.CSpace
 import {-# SOURCE #-} SEL4.Object.Interrupt
+import SEL4.Machine.Hardware.AARCH64 (config_ARM_GIC_V3, deactivateInterrupt)
 import qualified SEL4.Machine.Hardware.AARCH64 as Arch
 import SEL4.Machine.Hardware.AARCH64.PLATFORM (irqInvalid)
 import SEL4.Object.VCPU.TARGET (vgicMaintenance, vppiEvent, irqVPPIEventIndex)
@@ -58,7 +59,10 @@ performIRQControl (ArchInv.IssueIRQHandler (IRQ irq) destSlot srcSlot trigger)
     return ()
 
 invokeIRQHandler :: IRQHandlerInvocation -> Kernel ()
-invokeIRQHandler (AckIRQ irq) = doMachineOp $ maskInterrupt False irq
+invokeIRQHandler (AckIRQ irq) =
+    doMachineOp (if config_ARM_GIC_V3
+                 then deactivateInterrupt (theIRQ irq)
+                 else maskInterrupt False irq)
 invokeIRQHandler _ = return ()
 
 handleReservedIRQ :: IRQ -> Kernel ()
@@ -68,7 +72,8 @@ handleReservedIRQ irq = do
     return ()
 
 maskIrqSignal :: IRQ -> Kernel ()
-maskIrqSignal irq = doMachineOp $ maskInterrupt True irq
+maskIrqSignal irq =
+    when (not config_ARM_GIC_V3) (doMachineOp $ maskInterrupt True irq)
 
 initInterruptController :: Kernel ()
 initInterruptController = error "Unimplemented. Init code."

spec/machine/AARCH64/MachineOps.thy

@@ -92,9 +92,14 @@ definition debugPrint :: "unit list \<Rightarrow> unit machine_monad" where
 
 subsection \<open>Interrupt Controller\<close>
 
+(* Interface function for the Haskell IRQ wrapper type *)
 definition IRQ :: "irq \<Rightarrow> irq" where
   "IRQ \<equiv> id"
 
+(* Interface function for the Haskell IRQ wrapper type *)
+definition theIRQ :: "irq \<Rightarrow> irq" where
+  "theIRQ \<equiv> id"
+
 consts' setIRQTrigger_impl :: "irq \<Rightarrow> bool \<Rightarrow> unit machine_rest_monad"
 definition setIRQTrigger :: "irq \<Rightarrow> bool \<Rightarrow> unit machine_monad" where
   "setIRQTrigger irq trigger \<equiv> machine_op_lift (setIRQTrigger_impl irq trigger)"
@@ -131,6 +136,14 @@ definition ackInterrupt :: "irq \<Rightarrow> unit machine_monad" where
 definition setInterruptMode :: "irq \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> unit machine_monad" where
   "setInterruptMode \<equiv> \<lambda>irq levelTrigger polarityLow. return ()"
 
+text \<open>Only exists on GICv3 platforms. We model interrupt deactivation as unmasking
+  for the purposes of the interrupt oracle.\<close>
+definition deactivateInterrupt :: "irq \<Rightarrow> unit machine_monad" where
+  "deactivateInterrupt irq \<equiv> do
+     assert config_ARM_GIC_V3;
+     maskInterrupt False irq
+   od"
+
 
 subsection "User Monad and Registers"