From 2ae4366a82b8c47cad11018e21e6563c19340ecb Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Wed, 10 Jun 2026 12:40:43 +1000 Subject: [PATCH] manual: don't list out all MSRs and VMCS fields The previous approach is too unwieldy and required constant updates. We should just link the user to the kernel instead and have one source of truth. Signed-off-by: Bill Nguyen --- docs/manual.md | 190 +++++-------------------------------------------- 1 file changed, 16 insertions(+), 174 deletions(-) diff --git a/docs/manual.md b/docs/manual.md index e1369516c..a0a96cb2e 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -778,93 +778,9 @@ Read an 8, 16, or 32 bits value at port address `port_addr` from I/O Port with I Read a Virtual Machine Control Structure field specified by `field` for a given virtual CPU with ID `vcpu` using the `vmread` instruction. -All the VMCS fields are listed in the seL4 source at `include/arch/x86/arch/object/vcpu.h`. - -The following fields can be read from: - -* `VMX_GUEST_RIP` -* `VMX_GUEST_RSP` -* `VMX_GUEST_ES_SELECTOR` -* `VMX_GUEST_CS_SELECTOR` -* `VMX_GUEST_SS_SELECTOR` -* `VMX_GUEST_DS_SELECTOR` -* `VMX_GUEST_FS_SELECTOR` -* `VMX_GUEST_GS_SELECTOR` -* `VMX_GUEST_LDTR_SELECTOR` -* `VMX_GUEST_TR_SELECTOR` -* `VMX_GUEST_DEBUGCTRL` -* `VMX_GUEST_PAT` -* `VMX_GUEST_EFER` -* `VMX_GUEST_PERF_GLOBAL_CTRL` -* `VMX_GUEST_PDPTE0` -* `VMX_GUEST_PDPTE1` -* `VMX_GUEST_PDPTE2` -* `VMX_GUEST_PDPTE3` -* `VMX_GUEST_ES_LIMIT` -* `VMX_GUEST_CS_LIMIT` -* `VMX_GUEST_SS_LIMIT` -* `VMX_GUEST_DS_LIMIT` -* `VMX_GUEST_FS_LIMIT` -* `VMX_GUEST_GS_LIMIT` -* `VMX_GUEST_LDTR_LIMIT` -* `VMX_GUEST_TR_LIMIT` -* `VMX_GUEST_GDTR_LIMIT` -* `VMX_GUEST_IDTR_LIMIT` -* `VMX_GUEST_ES_ACCESS_RIGHTS` -* `VMX_GUEST_CS_ACCESS_RIGHTS` -* `VMX_GUEST_SS_ACCESS_RIGHTS` -* `VMX_GUEST_DS_ACCESS_RIGHTS` -* `VMX_GUEST_FS_ACCESS_RIGHTS` -* `VMX_GUEST_GS_ACCESS_RIGHTS` -* `VMX_GUEST_LDTR_ACCESS_RIGHTS` -* `VMX_GUEST_TR_ACCESS_RIGHTS` -* `VMX_GUEST_INTERRUPTABILITY` -* `VMX_GUEST_ACTIVITY` -* `VMX_GUEST_SMBASE` -* `VMX_GUEST_SYSENTER_CS` -* `VMX_GUEST_PREEMPTION_TIMER_VALUE` -* `VMX_GUEST_ES_BASE` -* `VMX_GUEST_CS_BASE` -* `VMX_GUEST_SS_BASE` -* `VMX_GUEST_DS_BASE` -* `VMX_GUEST_FS_BASE` -* `VMX_GUEST_GS_BASE` -* `VMX_GUEST_LDTR_BASE` -* `VMX_GUEST_TR_BASE` -* `VMX_GUEST_GDTR_BASE` -* `VMX_GUEST_IDTR_BASE` -* `VMX_GUEST_DR7` -* `VMX_GUEST_RFLAGS` -* `VMX_GUEST_PENDING_DEBUG_EXCEPTIONS` -* `VMX_GUEST_SYSENTER_ESP` -* `VMX_GUEST_SYSENTER_EIP` -* `VMX_CONTROL_CR0_MASK` -* `VMX_CONTROL_CR4_MASK` -* `VMX_CONTROL_CR0_READ_SHADOW` -* `VMX_CONTROL_CR4_READ_SHADOW` -* `VMX_DATA_INSTRUCTION_ERROR` -* `VMX_DATA_EXIT_INTERRUPT_INFO` -* `VMX_DATA_EXIT_INTERRUPT_ERROR` -* `VMX_DATA_IDT_VECTOR_INFO` -* `VMX_DATA_IDT_VECTOR_ERROR` -* `VMX_DATA_EXIT_INSTRUCTION_LENGTH` -* `VMX_DATA_EXIT_INSTRUCTION_INFO` -* `VMX_DATA_GUEST_PHYSICAL` -* `VMX_DATA_IO_RCX` -* `VMX_DATA_IO_RSI` -* `VMX_DATA_IO_RDI` -* `VMX_DATA_IO_RIP` -* `VMX_DATA_GUEST_LINEAR_ADDRESS` -* `VMX_CONTROL_ENTRY_INTERRUPTION_INFO` -* `VMX_CONTROL_PIN_EXECUTION_CONTROLS` -* `VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS` -* `VMX_CONTROL_SECONDARY_PROCESSOR_CONTROLS` -* `VMX_CONTROL_EXCEPTION_BITMAP` -* `VMX_CONTROL_ENTRY_CONTROLS` -* `VMX_CONTROL_EXIT_CONTROLS` -* `VMX_GUEST_CR0` -* `VMX_GUEST_CR3` -* `VMX_GUEST_CR4` +The seL4 kernel only allows certain VMCS fields to be read by userspace. For a full list of allowed +fields, see `decodeReadVMCS()` in seL4 source: +[src/arch/x86/object/vcpu.c](https://github.com/seL4/seL4/blob/master/src/arch/x86/object/vcpu.c) ## `void microkit_vcpu_x86_write_vmcs(microkit_child vcpu, seL4_Word field, seL4_Word value)` @@ -873,101 +789,27 @@ with ID `vcpu` using the `vmwrite` instruction. The value may be modified to ens that are fixed in the hardware are correct, and that any features required for kernel correctness are not disabled. -All the VMCS fields are listed in the seL4 source at `include/arch/x86/arch/object/vcpu.h`. - -The following fields can be written to: - -* `VMX_GUEST_RIP` -* `VMX_GUEST_RSP` -* `VMX_GUEST_ES_SELECTOR` -* `VMX_GUEST_CS_SELECTOR` -* `VMX_GUEST_SS_SELECTOR` -* `VMX_GUEST_DS_SELECTOR` -* `VMX_GUEST_FS_SELECTOR` -* `VMX_GUEST_GS_SELECTOR` -* `VMX_GUEST_LDTR_SELECTOR` -* `VMX_GUEST_TR_SELECTOR` -* `VMX_GUEST_DEBUGCTRL` -* `VMX_GUEST_PAT` -* `VMX_GUEST_EFER` -* `VMX_GUEST_PERF_GLOBAL_CTRL` -* `VMX_GUEST_PDPTE0` -* `VMX_GUEST_PDPTE1` -* `VMX_GUEST_PDPTE2` -* `VMX_GUEST_PDPTE3` -* `VMX_GUEST_ES_LIMIT` -* `VMX_GUEST_CS_LIMIT` -* `VMX_GUEST_SS_LIMIT` -* `VMX_GUEST_DS_LIMIT` -* `VMX_GUEST_FS_LIMIT` -* `VMX_GUEST_GS_LIMIT` -* `VMX_GUEST_LDTR_LIMIT` -* `VMX_GUEST_TR_LIMIT` -* `VMX_GUEST_GDTR_LIMIT` -* `VMX_GUEST_IDTR_LIMIT` -* `VMX_GUEST_ES_ACCESS_RIGHTS` -* `VMX_GUEST_CS_ACCESS_RIGHTS` -* `VMX_GUEST_SS_ACCESS_RIGHTS` -* `VMX_GUEST_DS_ACCESS_RIGHTS` -* `VMX_GUEST_FS_ACCESS_RIGHTS` -* `VMX_GUEST_GS_ACCESS_RIGHTS` -* `VMX_GUEST_LDTR_ACCESS_RIGHTS` -* `VMX_GUEST_TR_ACCESS_RIGHTS` -* `VMX_GUEST_INTERRUPTABILITY` -* `VMX_GUEST_ACTIVITY` -* `VMX_GUEST_SMBASE` -* `VMX_GUEST_SYSENTER_CS` -* `VMX_GUEST_PREEMPTION_TIMER_VALUE` -* `VMX_GUEST_ES_BASE` -* `VMX_GUEST_CS_BASE` -* `VMX_GUEST_SS_BASE` -* `VMX_GUEST_DS_BASE` -* `VMX_GUEST_FS_BASE` -* `VMX_GUEST_GS_BASE` -* `VMX_GUEST_LDTR_BASE` -* `VMX_GUEST_TR_BASE` -* `VMX_GUEST_GDTR_BASE` -* `VMX_GUEST_IDTR_BASE` -* `VMX_GUEST_DR7` -* `VMX_GUEST_RFLAGS` -* `VMX_GUEST_PENDING_DEBUG_EXCEPTIONS` -* `VMX_GUEST_SYSENTER_ESP` -* `VMX_GUEST_SYSENTER_EIP` -* `VMX_CONTROL_CR0_MASK` -* `VMX_CONTROL_CR4_MASK` -* `VMX_CONTROL_CR0_READ_SHADOW` -* `VMX_CONTROL_CR4_READ_SHADOW` -* `VMX_CONTROL_EXCEPTION_BITMAP` -* `VMX_CONTROL_ENTRY_INTERRUPTION_INFO` -* `VMX_CONTROL_ENTRY_EXCEPTION_ERROR_CODE` -* `VMX_CONTROL_PIN_EXECUTION_CONTROLS` -* `VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS` -* `VMX_CONTROL_SECONDARY_PROCESSOR_CONTROLS` -* `VMX_CONTROL_ENTRY_CONTROLS` -* `VMX_CONTROL_EXIT_CONTROLS` -* `VMX_GUEST_CR3` -* `VMX_GUEST_CR0` -* `VMX_GUEST_CR4` +The seL4 kernel only allows certain VMCS fields to be written by userspace. For a full list of allowed +fields, see `decodeWriteVMCS()` in seL4 source: +[src/arch/x86/object/vcpu.c](https://github.com/seL4/seL4/blob/master/src/arch/x86/object/vcpu.c) ## `seL4_Word microkit_vcpu_x86_read_msr(microkit_child vcpu, seL4_Word field)` -Read a 64-bit Model Specific Register of a given virtual CPU with ID `vcpu` specified by -`field` from hardware using the `rdmsr` instruction. The following registers can be written to: +Read a 64-bit Model Specific Register (MSR) of a given virtual CPU with ID `vcpu` specified by +`field` from hardware using the `rdmsr` instruction. -* `IA32_LSTAR_MSR` -* `IA32_STAR_MSR` -* `IA32_CSTAR_MSR` -* `IA32_FMASK_MSR` +The seL4 kernel only allows certain MSRs to be read by userspace. For a full list of allowed +MSRs, see `decodeVCPUReadMSR()` in seL4 source: +[src/arch/x86/object/vcpu.c](https://github.com/seL4/seL4/blob/master/src/arch/x86/object/vcpu.c) ## `void microkit_vcpu_x86_write_msr(microkit_child vcpu, seL4_Word field, seL4_Word value)` -Write a 64-bit Model Specific Register of a given virtual CPU with ID `vcpu` specified by -`field` to hardware using the `wrmsr` instruction. The following registers can be read from: +Write a 64-bit Model Specific Register (MSR) of a given virtual CPU with ID `vcpu` specified by +`field` to hardware using the `wrmsr` instruction. -* `IA32_LSTAR_MSR` -* `IA32_STAR_MSR` -* `IA32_CSTAR_MSR` -* `IA32_FMASK_MSR` +The seL4 kernel only allows certain MSRs to be written by userspace. For a full list of allowed +MSRs, see `decodeVCPUWriteMSR()` in seL4 source: +[src/arch/x86/object/vcpu.c](https://github.com/seL4/seL4/blob/master/src/arch/x86/object/vcpu.c) ## `void microkit_vcpu_x86_enable_ioport(microkit_child vcpu, microkit_ioport ioport_id, seL4_Word port_addr, seL4_Word length)`