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