Searched refs:priority (Results 1 - 25 of 49) sorted by relevance

12

/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DKeyMap.sml43 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 DMap.sml35 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 DKeyMap.sml43 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 DMap.sml35 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 Dgic_v2.c75 /* 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 Dgic_v3.c142 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 DMap.sml29 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 Dsyntax.tex18 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 Dsyntax.tex18 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 Dgic.h24 uint32_t priority[255]; /* [0x400, 0x7FC) */ member in struct:gic_dist_map_t
/seL4-l4v-master/seL4/src/arch/arm/object/
H A Dvcpu.c381 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 DTravrules.sml58 * priority - hence the "foldl" below.
H A DTraverse.sml14 * - apply reducers where possible, "rewriters" at high priority and
/seL4-l4v-master/seL4/include/object/
H A Dtcb.h81 /* 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 Dthreads.tex78 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 Dbootup.tex12 is started at priority \texttt{seL4\_MaxPrio} and maximum control priority \texttt{seL4\_MaxPrio}.
/seL4-l4v-master/HOL4/src/metis/
H A DmlibSupport.sml167 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 Dgic_v2.h63 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 Dbasics.tex184 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 Dbasics.tex184 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 DfunctionEncodeLib.sml200 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 Dadvanced.tex554 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 Dadvanced.tex554 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 Dtcb.c41 /* 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 Damba_ahb.sml138 (* for low priority guy we can't guarantee the bus but the possibility should exist *)

Completed in 163 milliseconds

12