Loading...
Searching...
No Matches
VM API for VMX
Base API » Kernel Objects » Virtual Machines

Virtual machine API for VMX. More...

Collaboration diagram for VM API for VMX:

## Data Structures

struct | l4_vmx_offset_table_t
| Software VMCS field offset table. More...
struct | l4_vm_vmx_vcpu_vmcs_t
| VMX software VMCS. More...
struct | l4_vm_vmx_vcpu_infos_t
| VMX information members. More...
struct | l4_vm_vmx_vcpu_state_t
| VMX vCPU state. More...

## Typedefs

typedef struct l4_vmx_offset_table_t | l4_vmx_offset_table_t
| Software VMCS field offset table.
typedef struct l4_vm_vmx_vcpu_vmcs_t | l4_vm_vmx_vcpu_vmcs_t
| VMX software VMCS.
typedef struct l4_vm_vmx_vcpu_infos_t | l4_vm_vmx_vcpu_infos_t
| VMX information members.
typedef struct l4_vm_vmx_vcpu_state_t | l4_vm_vmx_vcpu_state_t
| VMX vCPU state.

## Enumerations

enum

L4_vm_vmx_caps_regs {
L4_VM_VMX_BASIC_REG = 0 , L4_VM_VMX_TRUE_PINBASED_CTLS_REG = 1 , L4_VM_VMX_TRUE_PROCBASED_CTLS_REG = 2 , L4_VM_VMX_TRUE_EXIT_CTLS_REG = 3 ,
L4_VM_VMX_TRUE_ENTRY_CTLS_REG = 4 , L4_VM_VMX_MISC_REG = 5 , L4_VM_VMX_CR0_FIXED0_REG = 6 , L4_VM_VMX_CR0_FIXED1_REG = 7 ,
L4_VM_VMX_CR4_FIXED0_REG = 8 , L4_VM_VMX_CR4_FIXED1_REG = 9 , L4_VM_VMX_VMCS_ENUM_REG = 10 , L4_VM_VMX_PROCBASED_CTLS2_REG = 11 ,
L4_VM_VMX_EPT_VPID_CAP_REG = 12 , L4_VM_VMX_NESTED_REVISION = 13 , L4_VM_VMX_NUM_CAPS_REGS
}

| Exported VMX capability registers. More...
enum | L4_vm_vmx_dfl1_regs { L4_VM_VMX_PINBASED_CTLS_DFL1_REG = 0 , L4_VM_VMX_PROCBASED_CTLS_DFL1_REG = 1 , L4_VM_VMX_EXIT_CTLS_DFL1_REG = 2 , L4_VM_VMX_ENTRY_CTLS_DFL1_REG = 3 , L4_VM_VMX_NUM_DFL1_REGS }
| Exported VMX capability registers (default to 1 bits). More...

enum

L4_vm_vmx_sw_fields {
L4_VM_VMX_VMCS_CR2 = 0x6880 , L4_VM_VMX_VMCS_NAT_ARG0 = 0x6882 , L4_VM_VMX_VMCS_NAT_ARG1 = 0x6884 , L4_VM_VMX_VMCS_NAT_ARG2 = 0x6886 ,
L4_VM_VMX_VMCS_NAT_ARG3 = 0x6888 , L4_VM_VMX_VMCS_XCR0 = 0x2880 , L4_VM_VMX_VMCS_MSR_SYSCALL_MASK = 0x2882 , L4_VM_VMX_VMCS_MSR_LSTAR = 0x2884 ,
L4_VM_VMX_VMCS_MSR_CSTAR = 0x2886 , L4_VM_VMX_VMCS_MSR_TSC_AUX = 0x2888 , L4_VM_VMX_VMCS_MSR_STAR = 0x288a , L4_VM_VMX_VMCS_MSR_KERNEL_GS_BASE = 0x288c
}

| Additional (software-defined) VMCS fields. More...
enum | L4_vm_vmx_vmcs_sizes { L4_VM_VMX_VMCS_SIZE_VALUES = 2560 , L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP = 320 }
| Sizes of software VMCS members. More...

## Functions

l4_uint64_t | l4_vm_vmx_get_caps (l4_vm_vmx_vcpu_state_t const *vcpu_state, enum L4_vm_vmx_caps_regs caps_reg) L4_NOTHROW
| Get a capability register for VMX.
l4_uint32_t | l4_vm_vmx_get_caps_default1 (l4_vm_vmx_vcpu_state_t const *vcpu_state, enum L4_vm_vmx_dfl1_regs dfl1_reg) L4_NOTHROW
| Get a default to one capability register for VMX.
unsigned | l4_vm_vmx_field_len (unsigned field) L4_NOTHROW
| Return length in bytes of a VMCS field.
unsigned | l4_vm_vmx_field_order (unsigned field) L4_NOTHROW
| Return length in power of two (bytes) of a VMCS field.
void | l4_vm_vmx_clear (l4_vm_vmx_vcpu_vmcs_t *vmcs, l4_vm_vmx_vcpu_vmcs_t *dest_vmcs) L4_NOTHROW
| Save the content from the software VMCS to a different software VMCS.
void | l4_vm_vmx_ptr_load (l4_vm_vmx_vcpu_vmcs_t *vmcs, l4_vm_vmx_vcpu_vmcs_t *src_vmcs) L4_NOTHROW
| Load the content from a different software VMCS to the software VMCS.
l4_uint32_t | l4_vm_vmx_get_cr2_index (l4_vm_vmx_vcpu_vmcs_t const *vmcs) L4_NOTHROW
| Get the software VMCS field index of the virtual CR2 register.
l4_umword_t | l4_vm_vmx_read_nat (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
| Read a natural-width software VMCS field.
l4_uint16_t | l4_vm_vmx_read_16 (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
| Read a 16-bit software VMCS field.
l4_uint32_t | l4_vm_vmx_read_32 (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
| Read a 32-bit software VMCS field.
l4_uint64_t | l4_vm_vmx_read_64 (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
| Read a 64-bit software VMCS field.
l4_uint64_t | l4_vm_vmx_read (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field) L4_NOTHROW
| Read any software VMCS field.
void | l4_vm_vmx_write_nat (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_umword_t val) L4_NOTHROW
| Write to a natural-width software VMCS field.
void | l4_vm_vmx_write_16 (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_uint16_t val) L4_NOTHROW
| Write to a 16-bit software VMCS field.
void | l4_vm_vmx_write_32 (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_uint32_t val) L4_NOTHROW
| Write to a 32-bit software VMCS field.
void | l4_vm_vmx_write_64 (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
| Write to a 64-bit software VMCS field.
void | l4_vm_vmx_write (l4_vm_vmx_vcpu_vmcs_t *vmcs, unsigned field, l4_uint64_t val) L4_NOTHROW
| Write to an arbitrary software VMCS field.
void | l4_vm_vmx_set_hw_vmcs (l4_vm_vmx_vcpu_vmcs_t *vmcs, l4_cap_idx_t vmcs_cap) L4_NOTHROW
| Associate the software VMCS with a vCPU context, i.e.
l4_cap_idx_t | l4_vm_vmx_get_hw_vmcs (l4_vm_vmx_vcpu_vmcs_t *vmcs) L4_NOTHROW
| Get the vCPU context (i.e.

## Detailed Description

Virtual machine API for VMX.

## Typedef Documentation

## l4_vm_vmx_vcpu_state_t

typedef struct l4_vm_vmx_vcpu_state_t l4_vm_vmx_vcpu_state_t

VMX vCPU state.

This is a specialization of the generic vCPU state for VMX. This data structure represents the following memory layout:

- 0x000 - 0x1ff: Standard vCPU state (with padding). See l4_vcpu_state_t.
- 0x200 - 0x3ff: VMX information members (with padding). See l4_vm_vmx_vcpu_infos_t.
- 0x400 - 0xfff: VMX software VMCS. See l4_vm_vmx_vcpu_vmcs_t.

Note
  The memory layout is documented here for reference purposes. However, the users are strongly discouraged from accessing the data structure directly. The API functions defined in this file are the preferred way of achieving the functionality.

## l4_vm_vmx_vcpu_vmcs_t

typedef struct l4_vm_vmx_vcpu_vmcs_t l4_vm_vmx_vcpu_vmcs_t

VMX software VMCS.

This data structure represents the following memory layout:

- 0x000 - 0x007: Reserved (ignored by the kernel). In the hardware VMCS, the revision identifier and the abort indicator are stored in this area. Hereby we simply ignore these two entries.
- 0x008 - 0x00f: User space data (ignored by the kernel). This currently stores the pointer to a different software VMCS whose content has been loaded to this software VMCS.
- 0x010 - 0x013: VMCS field index of the software-defined CR2 field in the software VMCS.
- 0x014 - 0x017: Reserved.
- 0x018 - 0x01f: Capability of the vCPU context, i.e. the hardware VMCS object (with padding).
- 0x020 - 0x047: Software VMCS field offset table. See l4_vmx_offset_table_t.
- 0x048 - 0x0bf: Reserved.
- 0x0c0 - 0xabf: Software VMCS fields (with padding).
- 0xac0 - 0xbff: Software VMCS fields dirty bitmap (with padding).

Note
  The memory layout is documented here for reference purposes. However, the users are strongly discouraged from accessing the data structure directly. The API functions defined in this file are the preferred way of achieving the functionality.

## l4_vmx_offset_table_t

typedef struct l4_vmx_offset_table_t l4_vmx_offset_table_t

Software VMCS field offset table.

This data structure represents the following memory layout:

- 0x00 - 0x02: 3 offsets for 16-bit fields.
- 0x03: Reserved.
- 0x04 - 0x06: 3 offsets for 64-bit fields.
- 0x07: Reserved.
- 0x08 - 0x0a: 3 offsets for 32-bit fields.
- 0x0b: Reserved.
- 0x0c - 0x0e: 3 offsets for natural-width fields.
- 0x0f: Reserved.
- 0x10 - 0x12: 3 limits for 16-bit fields.
- 0x13: Reserved.
- 0x14 - 0x16: 3 limits for 64-bit fields.
- 0x17: Reserved.
- 0x18 - 0x1a: 3 limits for 32-bit fields.
- 0x1b: Reserved.
- 0x1c - 0x1e: 3 limits for natural-width fields.
- 0x1f: Reserved.
- 0x20 - 0x23: 4 index shifts.
- 0x24: Offset of the first software VMCS field.
- 0x25: Size of the software VMCS fields.
- 0x26 - 0x27: Reserved.

The offsets/limits in each size category are in the following order:

- Control fields.
- Read-only fields.
- Guest fields.

The index shifts are in the following order:

- 16-bit.
- 64-bit.
- 32-bit.
- Natural-width.

All offsets/limits/sizes are represented in a 64-byte granule.

The offsets (after being multiplied by 64) are indexes in the values array in l4_vm_vmx_vcpu_vmcs_t and bit indexes in the dirty_bitmap array in l4_vm_vmx_vcpu_vmcs_t.

The limits (after being multiplied by 64) represent the range of the available indexes.

Note
  The memory layout is documented here for reference purposes. However, the users are strongly discouraged from accessing the data structure directly. The API functions defined in this file are the preferred way of achieving the functionality.

## Enumeration Type Documentation

## L4_vm_vmx_caps_regs

enum L4_vm_vmx_caps_regs

Exported VMX capability registers.

Enumerator
L4_VM_VMX_BASIC_REG | Basic VMX capabilities.
L4_VM_VMX_TRUE_PINBASED_CTLS_REG | True pin-based control caps.
L4_VM_VMX_TRUE_PROCBASED_CTLS_REG | True processor based control caps.
L4_VM_VMX_TRUE_EXIT_CTLS_REG | True exit control caps.
L4_VM_VMX_TRUE_ENTRY_CTLS_REG | True entry control caps.
L4_VM_VMX_MISC_REG | Misc caps.
L4_VM_VMX_CR0_FIXED0_REG | Fixed to 0 bits of CR0.
L4_VM_VMX_CR0_FIXED1_REG | Fixed to 1 bits of CR0.
L4_VM_VMX_CR4_FIXED0_REG | Fixed to 0 bits of CR4.
L4_VM_VMX_CR4_FIXED1_REG | Fixed to 1 bits of CR4.
L4_VM_VMX_VMCS_ENUM_REG | VMCS enumeration info.
L4_VM_VMX_PROCBASED_CTLS2_REG | Processor based control 2 caps.
L4_VM_VMX_EPT_VPID_CAP_REG | EPT and VPID caps.
L4_VM_VMX_NESTED_REVISION | Nested VMCS revision.
L4_VM_VMX_NUM_CAPS_REGS | Total number of VMX capability registers.

Definition at line 28 of file __vm-vmx.h.

## L4_vm_vmx_dfl1_regs

enum L4_vm_vmx_dfl1_regs

Exported VMX capability registers (default to 1 bits).

Enumerator
L4_VM_VMX_PINBASED_CTLS_DFL1_REG | Default 1 bits in pin-based controls.
L4_VM_VMX_PROCBASED_CTLS_DFL1_REG | Default 1 bits in processor-based controls.
L4_VM_VMX_EXIT_CTLS_DFL1_REG | Default 1 bits in exit controls.
L4_VM_VMX_ENTRY_CTLS_DFL1_REG | Default 1 bits in entry controls.
L4_VM_VMX_NUM_DFL1_REGS | Total number of default on registers.

Definition at line 51 of file __vm-vmx.h.

## L4_vm_vmx_sw_fields

enum L4_vm_vmx_sw_fields

Additional (software-defined) VMCS fields.

The VMCS offsets defined here are actually not in the hardware VMCS. However our VMMs run in user mode and need to have access to certain registers available in kernel mode only. So we put them into our software VMCS.

Enumerator

L4_VM_VMX_VMCS_CR2

Software VMCS offset for CR2.

Note
  You usually need to check this value against the value you get from l4_vm_vmx_get_cr2_index() to make sure you are running on a compatible kernel.

L4_VM_VMX_VMCS_NAT_ARG0 | Custom argument passed from kernel to user space.
L4_VM_VMX_VMCS_NAT_ARG1 | Custom argument passed from kernel to user space.
L4_VM_VMX_VMCS_NAT_ARG2 | Custom argument passed from kernel to user space.
L4_VM_VMX_VMCS_NAT_ARG3 | Custom argument passed from kernel to user space.
L4_VM_VMX_VMCS_XCR0 | VMCS offset of extended control register XCR0.
L4_VM_VMX_VMCS_MSR_SYSCALL_MASK | VMCS offset of system call flag mask MSR.
L4_VM_VMX_VMCS_MSR_LSTAR | VMCS offset of IA32e mode system call target address MSR.
L4_VM_VMX_VMCS_MSR_CSTAR | VMCS offset of IA32 mode system call target address MSR.
L4_VM_VMX_VMCS_MSR_TSC_AUX | VMCS offset of auxiliary TSC signature MSR.
L4_VM_VMX_VMCS_MSR_STAR | VMCS offset of system call target address MSR.
L4_VM_VMX_VMCS_MSR_KERNEL_GS_BASE | VMCS offset of GS base address swap target MSR.

Definition at line 69 of file __vm-vmx.h.

## L4_vm_vmx_vmcs_sizes

enum L4_vm_vmx_vmcs_sizes

Sizes of software VMCS members.

Enumerator
L4_VM_VMX_VMCS_SIZE_VALUES | Size of the software VMCS values member.
L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP | Size of the software VMCS dirty bitmap member.

Definition at line 170 of file __vm-vmx.h.

## Function Documentation

## l4_vm_vmx_clear()

void l4_vm_vmx_clear | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | l4_vm_vmx_vcpu_vmcs_t * | dest_vmcs )

inline

Save the content from the software VMCS to a different software VMCS.

Parameters

  vmcs | Pointer to the source software VMCS.
  dest_vmcs | Pointer to the destination software VMCS.

This function is comparable to the VMX VMCLEAR instruction.

Definition at line 698 of file __vm-vmx.h.

References L4_NOTHROW, l4_vm_vmx_get_hw_vmcs(), l4_vm_vmx_set_hw_vmcs(), and L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP.

Referenced by l4_vm_vmx_ptr_load().

Here is the call graph for this function:
Here is the caller graph for this function:

## l4_vm_vmx_field_len()

unsigned l4_vm_vmx_field_len | ( | unsigned | field | ) |

inline

Return length in bytes of a VMCS field.

Parameters

  field | Field number.

Returns
  Width of field in bytes.

Definition at line 593 of file __vm-vmx.h.

References L4_NOTHROW, and l4_vm_vmx_field_order().

Here is the call graph for this function:

## l4_vm_vmx_field_order()

unsigned l4_vm_vmx_field_order | ( | unsigned | field | ) |

inline

Return length in power of two (bytes) of a VMCS field.

Parameters

  field | Field number.

Returns
  Width of field in power of two (bytes).

Definition at line 600 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_field_len().

Here is the caller graph for this function:

## l4_vm_vmx_get_caps()

l4_uint64_t l4_vm_vmx_get_caps | ( | l4_vm_vmx_vcpu_state_t const * | vcpu_state,
|  | enum L4_vm_vmx_caps_regs | caps_reg )

inline

Get a capability register for VMX.

Parameters

  vcpu_state | Pointer to the vCPU state.
  caps_reg | Capability register index (see L4_vm_vmx_caps_regs).

Returns
  The value of the capability register.

Definition at line 884 of file __vm-vmx.h.

References L4_NOTHROW.

## l4_vm_vmx_get_caps_default1()

l4_uint32_t l4_vm_vmx_get_caps_default1 | ( | l4_vm_vmx_vcpu_state_t const * | vcpu_state,
|  | enum L4_vm_vmx_dfl1_regs | dfl1_reg )

inline

Get a default to one capability register for VMX.

Parameters

  vcpu_state | Pointer to the vCPU state.
  dfl1_reg | Default to 1 capability register index (see L4_vm_vmx_dfl1_regs).

Returns
  The value of the capability register.

Definition at line 892 of file __vm-vmx.h.

References L4_NOTHROW.

## l4_vm_vmx_get_cr2_index()

l4_uint32_t l4_vm_vmx_get_cr2_index | ( | l4_vm_vmx_vcpu_vmcs_t const * | vmcs | ) |

inline

Get the software VMCS field index of the virtual CR2 register.

Parameters

  vmcs | Pointer to the software VMCS.

Returns
  The field index used for the virtual CR2 register as used by the current Fiasco.OC interface.

The CR2 register is actually not in the hardware VMCS, however our VMMs run in user mode and need to have access to this register so we put it into our software VMCS.

See also
  L4_VM_VMX_VMCS_CR2

Definition at line 900 of file __vm-vmx.h.

References L4_NOTHROW.

## l4_vm_vmx_get_hw_vmcs()

l4_cap_idx_t l4_vm_vmx_get_hw_vmcs | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs | ) |

inline

Get the vCPU context (i.e.

the hardware VMCS object) associated with the software VMCS.

Parameters

  vmcs | Pointer to the software VMCS.

Returns
  vCPU context (hardware VMCS object) capability.

Definition at line 915 of file __vm-vmx.h.

References L4_CAP_MASK, and L4_NOTHROW.

Referenced by l4_vm_vmx_clear(), and l4_vm_vmx_ptr_load().

Here is the caller graph for this function:

## l4_vm_vmx_ptr_load()

void l4_vm_vmx_ptr_load | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | l4_vm_vmx_vcpu_vmcs_t * | src_vmcs )

inline

Load the content from a different software VMCS to the software VMCS.

Parameters

  vmcs | Pointer to the destination software VMCS.
  src_vmcs | Pointer to the source software VMCS.

This function is comparable to the VMX VMPTRLD instruction.

Definition at line 719 of file __vm-vmx.h.

References L4_NOTHROW, l4_vm_vmx_clear(), l4_vm_vmx_get_hw_vmcs(), l4_vm_vmx_set_hw_vmcs(), and L4_VM_VMX_VMCS_SIZE_DIRTY_BITMAP.

Here is the call graph for this function:

## l4_vm_vmx_read()

l4_uint64_t l4_vm_vmx_read | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field )

inline

Read any software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.

Returns
  The value of the software VMCS field with the given index.

Definition at line 787 of file __vm-vmx.h.

References L4_NOTHROW, l4_vm_vmx_read_16(), l4_vm_vmx_read_32(), l4_vm_vmx_read_64(), and l4_vm_vmx_read_nat().

Here is the call graph for this function:

## l4_vm_vmx_read_16()

l4_uint16_t l4_vm_vmx_read_16 | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field )

inline

Read a 16-bit software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.

Returns
  The value of the software VMCS field with the given index.

Definition at line 754 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_read().

Here is the caller graph for this function:

## l4_vm_vmx_read_32()

l4_uint32_t l4_vm_vmx_read_32 | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field )

inline

Read a 32-bit software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.

Returns
  The value of the software VMCS field with the given index.

Definition at line 765 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_read().

Here is the caller graph for this function:

## l4_vm_vmx_read_64()

l4_uint64_t l4_vm_vmx_read_64 | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field )

inline

Read a 64-bit software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.

Returns
  The value of the software VMCS field with the given index.

Definition at line 776 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_read().

Here is the caller graph for this function:

## l4_vm_vmx_read_nat()

l4_umword_t l4_vm_vmx_read_nat | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field )

inline

Read a natural-width software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.

Returns
  The value of the software VMCS field with the given index.

Definition at line 743 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_read().

Here is the caller graph for this function:

## l4_vm_vmx_set_hw_vmcs()

void l4_vm_vmx_set_hw_vmcs | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | l4_cap_idx_t | vmcs_cap )

inline

Associate the software VMCS with a vCPU context, i.e.

a hardware VMCS object.

The VMX extended vCPU state is unable to be resumed unless it is associated with a vCPU context, i.e. a hardware VMCS object: An L4::Vcpu_context from the user space point of view with its kernel counterpart Vmx_vmcs.

Note
  When replacing the vCPU context, the dirty bitmap of the software VMCS is not touched, neither by the kernel nor by the API functions. This is on purpose, to enable efficient switching between separate VMs in the common case. If there is a logical discrepancy between the content of the software VMCS and the replaced vCPU context, the user is responsible for explicitly setting the relevant software VMCS fields and/or the relevant software VMCS dirty bitmap bits to ensure that the discrepancy is rectified on the next vCPU resume. This needs to be done regardless of using the API functions (the preferred way) or accessing the data structures directly (the discouraged way).
  Replacing the vCPU context while the vCPU is currently running has no immediate effect until the next vCPU resume. In addition to that, the kernel might cache the vCPU context internally (in other words, the capability is not looked up on every vCPU resume). To remove the association of the current vCPU context, simply replace it by an another vCPU context. The reference count of the previous vCPU context will be decremented accordingly on the next vCPU resume.
  To remove the association of the current vCPU context without replacing it by an another vCPU context, pass an invalid capability with the bit 3 set and trigger a vCPU resume. The vCPU resume will fail in this case (due to the missing vCPU context), but the reference count of the previous vCPU context will be decremented accordingly.
  There is no need to explicitly remove the association of the current vCPU context before deleting the software VMCS. Deleting the software VMCS automatically disassociates it from the vCPU context and a vCPU context with a reference count of 0 will be eventually deleted as well.
  If the hardware limitations on the usage of the vCPU context are not observed (i.e. no hardware VMCS being active on more than one physical CPU), the vCPU will fail to resume.

Parameters

  vmcs | Pointer to the software VMCS.
  vmcs_cap | vCPU context (hardware VMCS object) capability.

Definition at line 907 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_clear(), and l4_vm_vmx_ptr_load().

Here is the caller graph for this function:

## l4_vm_vmx_write()

void l4_vm_vmx_write | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field,
|  | l4_uint64_t | val )

inline

Write to an arbitrary software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.
  val | The value that shall be written to the given field.

Definition at line 868 of file __vm-vmx.h.

References L4_NOTHROW, l4_vm_vmx_write_16(), l4_vm_vmx_write_32(), l4_vm_vmx_write_64(), and l4_vm_vmx_write_nat().

Here is the call graph for this function:

## l4_vm_vmx_write_16()

void l4_vm_vmx_write_16 | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field,
|  | l4_uint16_t | val )

inline

Write to a 16-bit software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.
  val | The value that shall be written to the given field.

Definition at line 820 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_write().

Here is the caller graph for this function:

## l4_vm_vmx_write_32()

void l4_vm_vmx_write_32 | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field,
|  | l4_uint32_t | val )

inline

Write to a 32-bit software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.
  val | The value that shall be written to the given field.

Definition at line 836 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_write().

Here is the caller graph for this function:

## l4_vm_vmx_write_64()

void l4_vm_vmx_write_64 | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field,
|  | l4_uint64_t | val )

inline

Write to a 64-bit software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.
  val | The value that shall be written to the given field.

Definition at line 852 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_write().

Here is the caller graph for this function:

## l4_vm_vmx_write_nat()

void l4_vm_vmx_write_nat | ( | l4_vm_vmx_vcpu_vmcs_t * | vmcs,
|  | unsigned | field,
|  | l4_umword_t | val )

inline

Write to a natural-width software VMCS field.

Parameters

  vmcs | Pointer to the software VMCS.
  field | The VMCS field index as used on VMX hardware.
  val | The value that shall be written to the given field.

Definition at line 804 of file __vm-vmx.h.

References L4_NOTHROW.

Referenced by l4_vm_vmx_write().

Here is the caller graph for this function: