Searched refs:transfer (Results 1 - 24 of 24) sorted by relevance

/seL4-l4v-10.1.1/seL4/include/api/
H A Dtypes.h63 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 Dipc.tex39 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 Dcspace.tex40 \autoref{sec:cap-transfer}). Furthermore, new capabilities can be
H A Dthreads.tex25 cap transfer.
/seL4-l4v-10.1.1/HOL4/src/transfer/
H A DtransferScript.sml3 val _ = new_theory "transfer";
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DHSLScript.sml245 (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 DHSL2CFLScript.sml492 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 DfunCallScript.sml96 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 Damba_ahb.sml149 (* 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 Damba_ahbScript.sml22 (* 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 Dcomputer.ml13 % from a register-transfer point of view. It is used in the first %
H A Dcomputer_imp.ml7 % This theory is the specification of the register-transfer level %
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/
H A Dho_discrimTools.sml304 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 Dtamarack.ml16 % Specify register-transfer level implementation and functional %
/seL4-l4v-10.1.1/HOL4/examples/hardware/port/tamarack2/
H A DtamarackScript.sml10 (* Specify register-transfer level implementation and functional *)
/seL4-l4v-10.1.1/HOL4/tools/
H A Dbuildutils.sml603 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 DinstructionSyntax.sml241 | 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 DassemblerML.sml370 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 DCODETREE_REMOVE_REDUNDANT.sml258 required. If, though, we have UseField we can transfer the corresponding
/seL4-l4v-10.1.1/HOL4/examples/hardware/port-full/tamarack2/
H A DtamarackScript.sml10 (* Specify register-transfer level implementation and functional *)
/seL4-l4v-10.1.1/HOL4/src/enumfset/
H A DtotoScript.sml505 to work with StrongLinearOrder, and transfer the results to TotOrd. *)
/seL4-l4v-10.1.1/HOL4/examples/pgcl/src/
H A DwpScript.sml904 (* 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 DforScript.sml1176 (* We can transfer the type soundness proof from FBS directly *)
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A Dind_types.sml369 (* Instantiate the induction theorem on the representatives to transfer *)

Completed in 280 milliseconds