1/* 2 * Architecture-specific context switch 3 */ 4 5/* 6 * Copyright (c) 2015, ETH Zurich. 7 * All rights reserved. 8 * 9 * This file is distributed under the terms in the attached LICENSE file. 10 * If you do not find this file, copies can be found by writing to: 11 * ETH Zurich D-INFK, Universitaetstr. 6, CH-8092 Zurich. Attn: Systems Group. 12 */ 13 14#include <kernel.h> 15#include <dispatch.h> 16#include <paging_kernel_arch.h> 17 18/** 19 * \brief Switch context to 'dcb'. 20 * 21 * Switch to the dispatcher pointed to by 'dcb'. Sets 'dcb_current'. 22 * 23 * \param dcb Pointer to dispatcher to which to switch context. 24 */ 25void context_switch(struct dcb *dcb) 26{ 27 assert(dcb != NULL); 28 assert(dcb->vspace != 0); 29 30 // VM guests do not have a user space dispatcher 31 if (!dcb->is_vm_guest) { 32 assert(dcb->disp != 0); 33 } 34 35 paging_context_switch(dcb->vspace); 36 context_switch_counter++; 37 38 if (!dcb->is_vm_guest) { 39 assert(dcb->disp_cte.cap.type == ObjType_Frame); 40 41 maybe_reload_ldt(dcb, false); 42 } 43} 44