/seL4-l4v-10.1.1/seL4/include/api/ |
H A D | types.h | 63 cap_transfer_t transfer; local 65 transfer.ctReceiveRoot = (cptr_t)wptr[0]; 66 transfer.ctReceiveIndex = (cptr_t)wptr[1]; 67 transfer.ctReceiveDepth = wptr[2]; 68 return transfer;
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | ipc.tex | 39 message registers and capabilities that the sending thread wishes to transfer, 46 \autoref{sec:cap-transfer}. 61 \ipcparam{seL4\_CPtr[]}{(in)}{caps}{Capabilities to transfer} 83 kernel uses as many physical registers as possible to transfer IPC 86 \texttt{msg} field to transfer arguments. However, it leaves room in 88 transfer or kernel object invocation required 136 \label{sec:cap-transfer} 142 result in transfer of the raw message, without any capability transfer. 187 no IPC or capability transfer take [all...] |
H A D | cspace.tex | 40 \autoref{sec:cap-transfer}). Furthermore, new capabilities can be
|
H A D | threads.tex | 25 cap transfer.
|
/seL4-l4v-10.1.1/HOL4/src/transfer/ |
H A D | transferScript.sml | 3 val _ = new_theory "transfer";
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | HSLScript.sml | 245 (transfer (s1,s0) ([],[]) = s1) /\ 246 (transfer (s1,s0) (dst::dstL, src::srcL) = 247 transfer (twrite s1 dst (tread s0 src), s0) (dstL, srcL))`; 280 transfer (hs,hs) (dstL,srcL)) 306 let s1 = transfer (empty_s, s) (callee_i, caller_i) in 308 transfer (s, s2) (caller_o, callee_o)) 471 (* Properites of the "transfer" operation *) 477 (tread (transfer (s1,s0) (dstL,srcL)) h = tread s1 h)`, 491 (MAP (tread (transfer (s1,s0) (dstL,srcL))) dstL = MAP (tread s0) srcL)`, 506 (tread (transfer (s [all...] |
H A D | HSL2CFLScript.sml | 492 same_content (transfer (empty_s,s) (callee_i,caller_i)) 506 `MAP (tread (transfer (empty_s,s) (callee_i,caller_i))) callee_i = MAP (tread s) caller_i`
|
H A D | funCallScript.sml | 96 let s1 = transfer (empty_s,s) (callee_i,caller_i) in 107 `(MAP (tread (transfer (s,s2) (caller_o,callee_o))) caller_o = MAP (tread s2) callee_o) /\ 110 `MAP (tread (run_hsl S_hsl (transfer (empty_s,s) (callee_i,caller_i)))) callee_o = 130 let s1 = transfer (empty_s,s) (callee_i,caller_i) in 2037 same_content (run_hsl S_hsl (transfer (empty_s,s) (callee_i,caller_i))) (run_cfl S_body st') m2
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/examples/ |
H A D | amba_ahb.sml | 149 (* all transfers complete eventually.. this is only for sanity checking, subsumed by transfer latency checks *) 164 (* transfer completes at most ten (two overhead + four waitstates + four beat burst) cycles from transfer start *) 165 (* FIXME: actually this does not properly detect burst termination, since slave says rdy+ok after every transfer *)
|
H A D | amba_ahbScript.sml | 22 (* transfer types {3-9} *) 297 (* keep requesting bus if you get ownership (so arbiter only takes it away for higher priorty req) until transfer is done *) 301 (* starting transfer (if not already in the middle of one) *) 304 (* do not start transfer if not master, or not ok+rdy *) 327 (* response to first cycle of error ;{3-23} gives the option of continuing or cancelling transfer - we choose cancel*) 330 (* response to second cycle of error ;{3-23} gives the option of continuing or cancelling transfer - we choose cancel*) 346 (* signal end of transfer (single or part of a burst) (don't need to check for rdy because value of rdy irrelevent to address phase) *)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | computer.ml | 13 % from a register-transfer point of view. It is used in the first %
|
H A D | computer_imp.ml | 7 % This theory is the specification of the register-transfer level %
|
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | ho_discrimTools.sml | 304 fun transfer (a, (n : int, b)) = (n, (a, b)); function 306 fun dest dl = (map snd o sort order o map transfer) dl;
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/tamarack2/ |
H A D | tamarack.ml | 16 % Specify register-transfer level implementation and functional %
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/port/tamarack2/ |
H A D | tamarackScript.sml | 10 (* Specify register-transfer level implementation and functional *)
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | buildutils.sml | 603 fun transfer binaryp (dir,file1,file2) = function 608 | _ => transfer binaryp (dir,file,file) 634 (transfer false (dir,file, file' ^".sig");
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | instructionSyntax.sml | 241 | mk_options _ = raise ERR "mk_ldm_stm" "not a block transfer instruction" 242 val err = ERR "mk_ldm_stm" "not a block transfer instruction" 703 val err = ERR "dest_ldm_stm" "not a variable-free block transfer instruction"
|
H A D | assemblerML.sml | 370 raise BadInstruction "Block transfer list too long" 845 val err = Parse "ldm_stm_to_string: not a block transfer instruction"
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_REMOVE_REDUNDANT.sml | 258 required. If, though, we have UseField we can transfer the corresponding
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/port-full/tamarack2/ |
H A D | tamarackScript.sml | 10 (* Specify register-transfer level implementation and functional *)
|
/seL4-l4v-10.1.1/HOL4/src/enumfset/ |
H A D | totoScript.sml | 505 to work with StrongLinearOrder, and transfer the results to TotOrd. *)
|
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
H A D | wpScript.sml | 904 (* And so we can transfer the following nice properties to wp transformers *)
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
H A D | forScript.sml | 1176 (* We can transfer the type soundness proof from FBS directly *)
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | ind_types.sml | 369 (* Instantiate the induction theorem on the representatives to transfer *)
|