Searched refs:vcpu_switch (Results 1 - 6 of 6) sorted by relevance

/seL4-camkes-master/kernel/src/arch/arm/32/kernel/
H A Dthread.c18 vcpu_switch(tcb->tcbArch.tcbVCPU);
34 vcpu_switch(NULL);
/seL4-camkes-master/kernel/src/arch/arm/64/kernel/
H A Dthread.c17 vcpu_switch(tcb->tcbArch.tcbVCPU);
31 vcpu_switch(NULL);
/seL4-camkes-master/kernel/include/arch/arm/arch/32/mode/fastpath/
H A Dfastpath.h48 vcpu_switch(thread->tcbArch.tcbVCPU);
/seL4-camkes-master/kernel/include/arch/arm/arch/64/mode/fastpath/
H A Dfastpath.h36 vcpu_switch(thread->tcbArch.tcbVCPU);
/seL4-camkes-master/kernel/include/arch/arm/arch/object/
H A Dvcpu.h118 void vcpu_switch(vcpu_t *cpu);
202 #define vcpu_switch(x) do {} while(0) macro
/seL4-camkes-master/kernel/src/arch/arm/object/
H A Dvcpu.c224 void vcpu_switch(vcpu_t *new) function

Completed in 55 milliseconds