/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | KeyMap.sml | 43 type priority = Word.word; type 60 priority : priority, 68 val Node {priority = p1, ...} = node1 69 and Node {priority = p2, ...} = node2 126 else raise Bug "left child has greater priority" 133 else raise Bug "right child has greater priority" 165 fun mkNode priority left key value right = 171 priority = priority, 234 val priority = randomPriority () value [all...] |
H A D | Map.sml | 35 type priority = Word.word; type 52 priority : priority, 60 val Node {priority = p1, ...} = node1 61 and Node {priority = p2, ...} = node2 118 else raise Bug "left child has greater priority" 125 else raise Bug "right child has greater priority" 157 fun mkNode priority left key value right = 163 priority = priority, 226 val priority = randomPriority () value [all...] |
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | KeyMap.sml | 43 type priority = Word.word; type 60 priority : priority, 68 val Node {priority = p1, ...} = node1 69 and Node {priority = p2, ...} = node2 126 else raise Bug "left child has greater priority" 133 else raise Bug "right child has greater priority" 165 fun mkNode priority left key value right = 171 priority = priority, 234 val priority = randomPriority () value [all...] |
H A D | Map.sml | 35 type priority = Word.word; type 52 priority : priority, 60 val Node {priority = p1, ...} = node1 61 and Node {priority = p2, ...} = node2 118 else raise Bug "left child has greater priority" 125 else raise Bug "right child has greater priority" 157 fun mkNode priority left key value right = 163 priority = priority, 226 val priority = randomPriority () value [all...] |
/seL4-l4v-master/seL4/src/arch/arm/machine/ |
H A D | gic_v2.c | 75 /* reset interrupts priority */ 78 gic_dist->priority[i >> 2] = 0x80808080; 80 gic_dist->priority[i >> 2] = 0; 121 gic_dist->priority[0] = 0x80808080; 124 gic_dist->priority[0] = 0x0; 133 /* the write to priority mask is ignored if the kernel is 134 * in non-secure mode and the priority mask is already configured
|
H A D | gic_v3.c | 142 uint32_t priority; local 157 /* Default priority for global interrupts */ 158 priority = (GIC_PRI_IRQ << 24 | GIC_PRI_IRQ << 16 | GIC_PRI_IRQ << 8 | 161 gic_dist->ipriorityrn[(i / 4)] = priority; 237 uint32_t priority; local 245 /* Set priority on PPI and SGI interrupts */ 246 priority = (GIC_PRI_IRQ << 24 | GIC_PRI_IRQ << 16 | GIC_PRI_IRQ << 8 | 249 gic_rdist_sgi_ppi_map[CURRENT_CPU_INDEX()]->ipriorityrn[i / 4] = priority; 272 /* No priority grouping: ICC_BPR1_EL1 */ 275 /* Set priority mas [all...] |
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | Map.sml | 29 priority : real, 56 T {size = 1, priority = randomPriority (), 61 val {priority = p1, key = k1, ...} = x1 value 62 and {priority = p2, key = k2, ...} = x2 value 112 | GREATER => raise Error "left child has greater priority" 120 | GREATER => raise Error "right child has greater priority" 149 T {size = treeSize l + 1 + treeSize r, priority = p, 174 val {priority = p2, value 182 val {priority = p1, value 194 | mkLeft (({priority,lef 221 val {priority = p1, value 246 val {priority = p1, value 281 val {priority = p1, value [all...] |
/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | syntax.tex | 18 Each grammar rule is given by a mixfix declaration, which has a priority, 19 and each argument place has a priority. This general approach handles 24 an operator of lower priority unless brackets are used. Consider 25 first-order logic, where $\exists$ has lower priority than $\disj$, 26 which has lower priority than $\conj$. There, $P\conj Q \disj R$ 48 priorities; instead, the rules appear in order of decreasing priority.
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
H A D | syntax.tex | 18 Each grammar rule is given by a mixfix declaration, which has a priority, 19 and each argument place has a priority. This general approach handles 24 an operator of lower priority unless brackets are used. Consider 25 first-order logic, where $\exists$ has lower priority than $\disj$, 26 which has lower priority than $\conj$. There, $P\conj Q \disj R$ 48 priorities; instead, the rules appear in order of decreasing priority.
|
/seL4-l4v-master/l4v/spec/haskell/include/ |
H A D | gic.h | 24 uint32_t priority[255]; /* [0x400, 0x7FC) */ member in struct:gic_dist_map_t
|
/seL4-l4v-master/seL4/src/arch/arm/object/ |
H A D | vcpu.c | 381 word_t vid, priority, group, index; local 395 priority = (mr0 >> 16) & 0xff; 411 priority = (mr0 >> 16) & 0xff; 425 if (priority > 31) { 456 virq_t virq = virq_virq_pending_new(group, priority, 1, vid);
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Travrules.sml | 58 * priority - hence the "foldl" below.
|
H A D | Traverse.sml | 14 * - apply reducers where possible, "rewriters" at high priority and
|
/seL4-l4v-master/seL4/include/object/ |
H A D | tcb.h | 81 /* Add TCB into the priority ordered endpoint queue */ 199 prio_t mcp, prio_t priority, 204 prio_t mcp, prio_t priority, cap_t cRoot_newCap,
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | threads.tex | 78 seL4 uses a preemptive, tickless scheduler with 256 priority levels (0 --- 255). All threads have 79 a maximum controlled priority (MCP) and a priority, the latter being the effective priority of the 81 When a thread modifies a another threads priority (including itself) it must provide a 84 The initial task starts with an MCP and priority as the highest priority in the system (\texttt{seL4\_MaxPrio}). 85 Thread priority and MCP can be 91 Of threads eligible for scheduling, the highest priority thread in a runnable state is chosen. 93 Thread priority (structur [all...] |
H A D | bootup.tex | 12 is started at priority \texttt{seL4\_MaxPrio} and maximum control priority \texttt{seL4\_MaxPrio}.
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibSupport.sml | 167 fun priority n = 1e~12 * Real.fromInt n; function 176 val w = siz * lit * sat * (1.0 + dist) + priority id
|
/seL4-l4v-master/seL4/include/arch/arm/arch/machine/ |
H A D | gic_v2.h | 63 uint32_t priority[255]; /* [0x400, 0x7FC) */ member in struct:gic_dist_map 229 /* Active priority: bitfield of active priorities */
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | basics.tex | 184 the usual logical connectives (in decreasing order of priority): 235 equality has a high priority, as befitting a relation, while if-and-only-if 236 typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P = 262 A particular problem for novices can be the priority of operators. If
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | basics.tex | 184 the usual logical connectives (in decreasing order of priority): 235 equality has a high priority, as befitting a relation, while if-and-only-if 236 typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P = 262 A particular problem for novices can be the priority of operators. If
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | functionEncodeLib.sml | 200 fun add_conditional_rewrite priority name thm = 217 a <= priority handle e => wrapException "add_conditional_rewrite" e 224 fun p (a,b,c) = "Rewrite: " ^ b ^ " with priority: " ^ int_to_string a ^ ":\n" ^ thm_to_string c ^ "\n" 250 (map (fn thm' => rewrites := Net.insert (lhs final,(priority:int,name:string,thm')) (!rewrites)) all_thms ; ()) 289 fun add_standard_rewrite priority name thm = 293 add_conditional_rewrite priority name toadd 310 Net.filter (fn (priority,name,thm) => Theory.uptodate_thm thm) 846 fun instantiate_encoders (priority,name,thm) = 857 (priority,name, 1408 fun exists_polytypic_theorem previous (priority,nam [all...] |
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 554 with their priorities, or precedences; they are $\nand$ of priority~35 and 555 $\xor$ of priority~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor Q) 594 defines, for each argument position, the minimal priority an expression 595 at that position must have. The final integer is the priority of the 598 appear everywhere because 1000 is the highest priority. On the other 604 the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority 609 because expressions in parentheses have maximal priority.
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | advanced.tex | 554 with their priorities, or precedences; they are $\nand$ of priority~35 and 555 $\xor$ of priority~30. Hence $P \xor Q \xor R$ is parsed as $(P\xor Q) 594 defines, for each argument position, the minimal priority an expression 595 at that position must have. The final integer is the priority of the 598 appear everywhere because 1000 is the highest priority. On the other 604 the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority 609 because expressions in parentheses have maximal priority.
|
/seL4-l4v-master/seL4/src/object/ |
H A D | tcb.c | 41 /* can't assign a priority greater than our own mcp */ 448 /* reschedule if the target core is idle or we are waking a higher priority thread (or 1162 userError("Set priority: authority cap not a TCB."); 1171 userError("TCB SetPriority: Requested priority %lu too high (max %lu).", 1215 userError("TCB SetMCPriority: Requested maximum controlled priority %lu too high (max %lu).", 1303 userError("TCB SetSchedParams: Requested maximum controlled priority %lu too high (max %lu).", 1310 userError("TCB SetSchedParams: Requested priority %lu too high (max %lu).", 1753 cptr_t faultep, prio_t mcp, prio_t priority, 1820 setPriority(target, priority); 1830 prio_t mcp, prio_t priority, 1752 invokeTCB_ThreadControl(tcb_t *target, cte_t *slot, cptr_t faultep, prio_t mcp, prio_t priority, cap_t cRoot_newCap, cte_t *cRoot_srcSlot, cap_t vRoot_newCap, cte_t *vRoot_srcSlot, word_t bufferAddr, cap_t bufferCap, cte_t *bufferSrcSlot, thread_control_flag_t updateFlags) argument 1828 invokeTCB_ThreadControlSched(tcb_t *target, cte_t *slot, cap_t fh_newCap, cte_t *fh_srcSlot, prio_t mcp, prio_t priority, sched_context_t *sc, thread_control_flag_t updateFlags) argument [all...] |
/seL4-l4v-master/HOL4/examples/HolCheck/examples/ |
H A D | amba_ahb.sml | 138 (* for low priority guy we can't guarantee the bus but the possibility should exist *)
|