1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11chapter "The Fault Monad" 12 13theory FaultMonad_H 14imports KernelStateData_H Fault_H 15begin 16 17context begin interpretation Arch . 18requalify_consts 19 getActiveIRQ 20end 21 22type_synonym ('f, 'a) kernel_f = "('f + 'a) kernel" 23 24translations 25 (type) "('f,'a) kernel_f" <= (type) "('f + 'a) kernel" 26 27subsubsection "Error Handling" 28 29definition 30 withoutFailure :: "'a kernel \<Rightarrow> ('f, 'a) kernel_f" 31where 32 withoutFailure_def[simp]: 33 "withoutFailure \<equiv> liftE" 34 35definition 36 throw :: "'f \<Rightarrow> ('f, 'a) kernel_f" 37where 38 throw_def[simp]: 39 "throw \<equiv> throwError" 40 41definition 42 catchFailure :: "('f, 'a) kernel_f \<Rightarrow> ('f \<Rightarrow> 'a kernel) \<Rightarrow> 'a kernel" 43where 44 catchFailure_def[simp]: 45 "catchFailure \<equiv> catch" 46 47definition 48 rethrowFailure :: "('f1 \<Rightarrow> 'f2) \<Rightarrow> ('f1, 'a) kernel_f \<Rightarrow> ('f2, 'a) kernel_f" 49where 50 "rethrowFailure f m \<equiv> m <handle2> (throwError \<circ> f)" 51 52definition 53 ignoreFailure :: "( 'f , unit ) kernel_f \<Rightarrow> unit kernel" 54where 55 "ignoreFailure x \<equiv> (catchFailure x (const (return ())))" 56 57 58#INCLUDE_HASKELL_PREPARSE SEL4/API/Failures.lhs 59#INCLUDE_HASKELL SEL4/Model/Failures.lhs NOT KernelF withoutFailure catchFailure throw rethrowFailure nullCapOnFailure nothingOnFailure ignoreFailure emptyOnFailure 60 61definition 62 nullCapOnFailure :: "('f, capability) kernel_f \<Rightarrow> capability kernel" 63where 64 "nullCapOnFailure m \<equiv> m <catch> (\<lambda>x. return NullCap)" 65 66definition 67 emptyOnFailure :: "('f, 'a list) kernel_f \<Rightarrow> 'a list kernel" 68where 69 "emptyOnFailure m \<equiv> m <catch> (\<lambda>x. return [])" 70 71definition 72 nothingOnFailure :: "('f, 'a option) kernel_f \<Rightarrow> 'a option kernel" 73where 74 "nothingOnFailure m \<equiv> m <catch> (\<lambda>x. return Nothing)" 75 76subsection "Preemption" 77 78type_synonym 'a kernel_p = "(irq + 'a) kernel" 79 80translations 81 (type) "'a kernel_p" <= (type) "(irq + 'a) kernel" 82 83definition 84 withoutPreemption :: "'a kernel \<Rightarrow> 'a kernel_p" 85where 86 withoutPreemption_def[simp]: 87 "withoutPreemption \<equiv> liftE" 88 89definition 90 workUnitsLimit :: machine_word 91where 92 "workUnitsLimit \<equiv> 0x64" 93 94definition 95 preemptionPoint :: "unit kernel_p" 96where 97 "preemptionPoint \<equiv> doE 98 liftE $ modifyWorkUnits (\<lambda>u. u + 1); 99 workUnits <- liftE $ getWorkUnits; 100 whenE (workUnitsLimit <= workUnits) $ doE 101 liftE $ setWorkUnits 0; 102 preempt <- liftE $ doMachineOp (getActiveIRQ True); 103 case preempt of 104 Some irq => throwError irq 105 | None => returnOk () 106 odE 107 odE" 108 109 110end 111