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