L4Re Operating System Framework
Interface and Usage Documentation
Loading...
Searching...
No Matches
vcpu.h
Go to the documentation of this file.
1/*
2 * (c) 2009 Adam Lackorzynski <adam@os.inf.tu-dresden.de>,
3 * Alexander Warg <warg@os.inf.tu-dresden.de>
4 * economic rights: Technische Universität Dresden (Germany)
5 *
6 * This file is part of TUD:OS and distributed under the terms of the
7 * GNU General Public License 2.
8 * Please see the COPYING-GPL-2 file for details.
9 *
10 * As a special exception, you may use this file as part of a free software
11 * library without restriction. Specifically, if other files instantiate
12 * templates or use macros or inline functions from this file, or you compile
13 * this file and link it with other files to produce an executable, this
14 * file does not by itself cause the resulting executable to be covered by
15 * the GNU General Public License. This exception does not however
16 * invalidate any other reasons why the executable file might be covered by
17 * the GNU General Public License.
18 */
23#pragma once
24
25#include <l4/sys/types.h>
26#include <l4/sys/__vcpu-arch.h>
27
107
173
184
196L4_INLINE int
198
199/* IMPLEMENTATION: ------------------------------------------------*/
200
201L4_INLINE int
@ L4_VCPU_STATE_VERSION
Architecture-specific version ID.
Definition __vcpu-arch.h:36
unsigned long l4_umword_t
Unsigned machine word.
Definition l4int.h:51
unsigned short int l4_uint16_t
Unsigned 16bit value.
Definition l4int.h:38
unsigned long l4_cap_idx_t
Capability selector type.
Definition types.h:359
L4_vcpu_sticky_flags
Sticky flags of a vCPU.
Definition vcpu.h:179
L4_vcpu_state_flags
State flags of a vCPU.
Definition vcpu.h:113
@ L4_VCPU_SF_IRQ_PENDING
An event is pending: Either an IRQ or another thread attempts to send an IPC to this vCPU thread.
Definition vcpu.h:182
@ L4_VCPU_F_USER_MODE
User task will be used.
Definition vcpu.h:163
@ L4_VCPU_F_EXCEPTIONS
Exceptions enabled.
Definition vcpu.h:153
@ L4_VCPU_F_IRQ
Receiving of IRQs and IPC enabled.
Definition vcpu.h:125
@ L4_VCPU_F_FPU_ENABLED
FPU enabled.
Definition vcpu.h:171
@ L4_VCPU_F_PAGE_FAULTS
Page faults enabled.
Definition vcpu.h:140
#define L4_NOTHROW
Mark a function declaration and definition as never throwing an exception.
Definition compiler.h:188
#define L4_INLINE
L4 Inline function attribute.
Definition compiler.h:62
Common L4 ABI Data Types.
Architecture-specific vCPU state.
Definition __vcpu-arch.h:86
vCPU message registers.
Definition __vcpu-arch.h:95
vCPU registers.
Definition __vcpu-arch.h:67
State of a vCPU.
Definition vcpu.h:87
l4_umword_t entry_sp
Stack pointer for entry (when coming from user task)
Definition vcpu.h:102
l4_vcpu_arch_state_t arch_state
Architecture-specific state.
Definition vcpu.h:105
l4_uint16_t sticky_flags
Pending flags. See L4_vcpu_sticky_flags.
Definition vcpu.h:97
l4_uint16_t state
Current vCPU state. See L4_vcpu_state_flags.
Definition vcpu.h:95
l4_vcpu_regs_t r
Register state.
Definition vcpu.h:92
l4_umword_t version
vCPU ABI version.
Definition vcpu.h:88
l4_umword_t entry_ip
IP for entry.
Definition vcpu.h:103
l4_cap_idx_t user_task
User task to use.
Definition vcpu.h:100
l4_umword_t user_data[7]
User-specific data.
Definition vcpu.h:91
l4_vcpu_ipc_regs_t i
IPC state.
Definition vcpu.h:93
l4_uint16_t saved_state
Saved vCPU state. See L4_vcpu_state_flags.
Definition vcpu.h:96
int l4_vcpu_check_version(l4_vcpu_state_t const *vcpu) L4_NOTHROW
Check if a vCPU state has the right version.
Definition vcpu.h:202