1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Formalisation of interrupt handling. 9*) 10 11chapter "Arch-specific Interrupts" 12 13theory ArchInterrupt_A 14imports Ipc_A 15begin 16 17context Arch begin global_naming ARM_A 18 19definition handle_reserved_irq :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad" 20 where "handle_reserved_irq irq = return ()" 21 22fun arch_invoke_irq_handler :: "irq_handler_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" 23 where 24 "arch_invoke_irq_handler (ACKIrq irq) = (do_machine_op $ maskInterrupt False irq)" 25| "arch_invoke_irq_handler _ = return ()" 26 27definition arch_mask_irq_signal :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad" 28 where 29 "arch_mask_irq_signal irq \<equiv> do_machine_op $ maskInterrupt True irq" 30 31end 32 33end 34