From 4b1aaf4c340ea5b2f5b2924b4b2c8634b5f697c1 Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Wed, 25 Mar 2026 13:24:33 +1100 Subject: [PATCH 1/3] tool: do not allow PPC for x86 VMM Because you cannot pass an endpoint object with the syscall. Signed-off-by: Bill Nguyen --- tool/microkit/src/sdf.rs | 19 +++++++++ .../tests/sdf/vm_x86_ppc_invalid_1.system | 39 +++++++++++++++++++ .../tests/sdf/vm_x86_ppc_invalid_2.system | 39 +++++++++++++++++++ .../tests/sdf/vm_x86_ppc_valid.system | 30 ++++++++++++++ tool/microkit/tests/test.rs | 23 +++++++++++ 5 files changed, 150 insertions(+) create mode 100644 tool/microkit/tests/sdf/vm_x86_ppc_invalid_1.system create mode 100644 tool/microkit/tests/sdf/vm_x86_ppc_invalid_2.system create mode 100644 tool/microkit/tests/sdf/vm_x86_ppc_valid.system diff --git a/tool/microkit/src/sdf.rs b/tool/microkit/src/sdf.rs index 365650100..1fbc03a8f 100644 --- a/tool/microkit/src/sdf.rs +++ b/tool/microkit/src/sdf.rs @@ -2151,6 +2151,25 @@ pub fn parse( )); } + // When seL4_VMEnter() is called, the kernel only checks the VMM's bound + // notification for pending signals. Because the endpoint object isn't passed + // or checked for pending messages, PPC won't work while the VCPU is on. + // Technically, PPC could still work when the VCPU is off, but we shouldn't + // expose this footgun to users. + if config.arch == Arch::X86_64 + && ((ch.end_a.pp && pd_b.virtual_machine.is_some()) + || (ch.end_b.pp && pd_a.virtual_machine.is_some())) + { + return Err(format!( + "Error: It is not possible to PPC to PD '{}' with a bound vCPU from PD '{}' on x86_64 @ {}:{}:{}", + if ch.end_a.pp {&pd_b.name} else {&pd_a.name}, + if ch.end_a.pp {&pd_a.name} else {&pd_b.name}, + filename.display(), + pd_a.text_pos.unwrap().row, + pd_a.text_pos.unwrap().col + )); + } + ch_ids[ch.end_a.pd].push(ch.end_a.id); ch_ids[ch.end_b.pd].push(ch.end_b.id); } diff --git a/tool/microkit/tests/sdf/vm_x86_ppc_invalid_1.system b/tool/microkit/tests/sdf/vm_x86_ppc_invalid_1.system new file mode 100644 index 000000000..f1fab020a --- /dev/null +++ b/tool/microkit/tests/sdf/vm_x86_ppc_invalid_1.system @@ -0,0 +1,39 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/tool/microkit/tests/sdf/vm_x86_ppc_invalid_2.system b/tool/microkit/tests/sdf/vm_x86_ppc_invalid_2.system new file mode 100644 index 000000000..db763e43e --- /dev/null +++ b/tool/microkit/tests/sdf/vm_x86_ppc_invalid_2.system @@ -0,0 +1,39 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/tool/microkit/tests/sdf/vm_x86_ppc_valid.system b/tool/microkit/tests/sdf/vm_x86_ppc_valid.system new file mode 100644 index 000000000..66d0faa1f --- /dev/null +++ b/tool/microkit/tests/sdf/vm_x86_ppc_valid.system @@ -0,0 +1,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/tool/microkit/tests/test.rs b/tool/microkit/tests/test.rs index 4a25465b3..8aa606eb3 100644 --- a/tool/microkit/tests/test.rs +++ b/tool/microkit/tests/test.rs @@ -761,6 +761,29 @@ mod virtual_machine { "Error: invalid memory region name 'mr1' on 'map' @", ) } + + #[test] + fn test_x86_ppc_invalid_1() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "vm_x86_ppc_invalid_1.system", + "Error: It is not possible to PPC to PD 'VMM' with a bound vCPU from PD 'some_service' on x86_64", + ) + } + + #[test] + fn test_x86_ppc_invalid_2() { + check_error( + &DEFAULT_X86_64_KERNEL_CONFIG, + "vm_x86_ppc_invalid_2.system", + "Error: It is not possible to PPC to PD 'VMM' with a bound vCPU from PD 'some_service' on x86_64", + ) + } + + #[test] + fn test_x86_ppc_valid() { + check_success(&DEFAULT_X86_64_KERNEL_CONFIG, "vm_x86_ppc_valid.system") + } } #[cfg(test)] From 90043b09c8da805492fc92d3778ae9b9d430fee2 Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Thu, 21 May 2026 15:33:07 +1000 Subject: [PATCH 2/3] libmicrokit: add x86 VCPU on/off APIs Add: microkit_vcpu_x86_on() microkit_vcpu_x86_off() Signed-off-by: Bill Nguyen --- libmicrokit/include/microkit.h | 131 ++++++++++++++++++++++++++------- libmicrokit/src/main.c | 113 ++++++++++++++++++++++------ 2 files changed, 194 insertions(+), 50 deletions(-) diff --git a/libmicrokit/include/microkit.h b/libmicrokit/include/microkit.h index 5c6b76e0b..a2dbe8e7e 100644 --- a/libmicrokit/include/microkit.h +++ b/libmicrokit/include/microkit.h @@ -10,6 +10,9 @@ #pragma once #include +#ifdef CONFIG_VTX +#include +#endif /* CONFIG_VTX */ typedef unsigned int microkit_channel; typedef unsigned int microkit_child; @@ -47,6 +50,15 @@ extern char microkit_name[MICROKIT_PD_NAME_LENGTH]; extern seL4_Bool microkit_have_signal; extern seL4_CPtr microkit_signal_cap; extern seL4_MessageInfo_t microkit_signal_msg; +#if defined(CONFIG_VTX) +struct microkit_x86_vcpu_state { + seL4_Bool do_resume; + seL4_Word rip; + seL4_Word prim_proc_ctl; + seL4_Word irq_info; +}; +extern struct microkit_x86_vcpu_state microkit_x86_vcpu_state; +#endif /* Symbols for error checking libmicrokit API calls. Patched by the Microkit tool * to set bits corresponding to valid channels for this PD. */ @@ -190,13 +202,8 @@ static inline void microkit_vcpu_restart(microkit_child vcpu, seL4_Word entry_po { seL4_Error err; seL4_UserContext ctxt = {0}; -#if defined(CONFIG_ARCH_AARCH64) ctxt.pc = entry_point; -#elif defined(CONFIG_ARCH_X86_64) - ctxt.rip = entry_point; -#else -#error "unknown architecture for 'microkit_vcpu_restart'" -#endif + err = seL4_TCB_WriteRegisters( BASE_VM_TCB_CAP + vcpu, seL4_True, @@ -220,9 +227,7 @@ static inline void microkit_vcpu_stop(microkit_child vcpu) microkit_internal_crash(err); } } -#endif -#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) static inline void microkit_vcpu_arm_inject_irq(microkit_child vcpu, seL4_Uint16 irq, seL4_Uint8 priority, seL4_Uint8 group, seL4_Uint8 index) { @@ -265,7 +270,7 @@ static inline void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word re microkit_internal_crash(err); } } -#endif +#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */ #if defined(CONFIG_ALLOW_SMC_CALLS) static inline void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMCContext *response) @@ -277,7 +282,7 @@ static inline void microkit_arm_smc_call(seL4_ARM_SMCContext *args, seL4_ARM_SMC microkit_internal_crash(err); } } -#endif +#endif /* CONFIG_ALLOW_SMC_CALLS */ #if defined(CONFIG_ARCH_X86_64) static inline void microkit_x86_ioport_write_8(microkit_ioport ioport_id, seL4_Word port_addr, seL4_Word data) @@ -393,28 +398,85 @@ static inline seL4_Uint32 microkit_x86_ioport_read_32(microkit_ioport ioport_id, return ret.result; } -#endif -#if defined(CONFIG_ARCH_X86_64) && defined(CONFIG_VTX) +#if defined(CONFIG_VTX) +/* Architecturally defined identifiers for a x86 VCPU's VMCS fields, + * see seL4 source: `include/arch/x86/arch/object/vcpu.h` + * or Intel® 64 and IA-32 Architectures Software Developer’s Manual + * Combined Volumes: 1, 2A, 2B, 2C, 2D, 3A, 3B, 3C, 3D, and 4 + * Order Number: 325462-084US June 2024 + * "Table B-8. Encodings for 32-Bit Control Fields (0100_00xx_xxxx_xxx0B)" and + * "Table B-14. Encodings for Natural-Width Guest-State Fields (0110_10xx_xxxx_xxx0B) (Contd.)". + * */ +#define VMX_GUEST_RIP 0x0000681E +#define VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS 0x00004002 +#define VMX_CONTROL_ENTRY_INTERRUPTION_INFO 0x00004016 + +/* Serve the guest's: + * - RIP, + * - Primary Processor Based VM Execution Controls, and + * - VM Entry Interruption-Information + * from local variables that were written to by `microkit_vcpu_x86_write_vmcs()`. + * The kernel will service reading from other fields. + */ static inline seL4_Word microkit_vcpu_x86_read_vmcs(microkit_child vcpu, seL4_Word field) { - seL4_X86_VCPU_ReadVMCS_t ret; - ret = seL4_X86_VCPU_ReadVMCS(BASE_VCPU_CAP + vcpu, field); - if (ret.error != seL4_NoError) { - microkit_dbg_puts("microkit_x86_read_vmcs: error reading data\n"); - microkit_internal_crash(ret.error); - } - - return ret.value; -} - + seL4_Word value; + + /* Assumes that a PD would only have access to 1 VCPU object. */ + switch (field) { + case VMX_GUEST_RIP: + value = microkit_x86_vcpu_state.rip; + break; + case VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS: + value = microkit_x86_vcpu_state.prim_proc_ctl; + break; + case VMX_CONTROL_ENTRY_INTERRUPTION_INFO: + value = microkit_x86_vcpu_state.irq_info; + break; + default: { + seL4_X86_VCPU_ReadVMCS_t ret = seL4_X86_VCPU_ReadVMCS(BASE_VCPU_CAP + vcpu, field); + if (ret.error != seL4_NoError) { + microkit_dbg_puts("microkit_x86_read_vmcs: error reading data\n"); + microkit_internal_crash(ret.error); + } + value = ret.value; + break; + } + } + + return value; +} + +/* These fields will be written to local variables rather than the actual VMCS: + * - RIP, + * - Primary Processor Based VM Execution Controls, and + * - VM Entry Interruption-Information. + * Because they will be passed to the kernel on `seL4_VMEnter()`, + * then the kernel will write them to the VMCS for us. + * Writing other VMCS fields will go to the real VMCS immeidately via a syscall. + */ static inline void microkit_vcpu_x86_write_vmcs(microkit_child vcpu, seL4_Word field, seL4_Word value) { - seL4_X86_VCPU_WriteVMCS_t ret; - ret = seL4_X86_VCPU_WriteVMCS(BASE_VCPU_CAP + vcpu, field, value); - if (ret.error != seL4_NoError) { - microkit_dbg_puts("microkit_x86_write_vmcs: error writing data\n"); - microkit_internal_crash(ret.error); + /* Assumes that a PD would only have access to 1 VCPU object. */ + switch (field) { + case VMX_GUEST_RIP: + microkit_x86_vcpu_state.rip = value; + break; + case VMX_CONTROL_PRIMARY_PROCESSOR_CONTROLS: + microkit_x86_vcpu_state.prim_proc_ctl = value; + break; + case VMX_CONTROL_ENTRY_INTERRUPTION_INFO: + microkit_x86_vcpu_state.irq_info = value; + break; + default: { + seL4_X86_VCPU_WriteVMCS_t ret = seL4_X86_VCPU_WriteVMCS(BASE_VCPU_CAP + vcpu, field, value); + if (ret.error != seL4_NoError) { + microkit_dbg_puts("microkit_x86_write_vmcs: error writing data\n"); + microkit_internal_crash(ret.error); + } + break; + } } } @@ -479,7 +541,20 @@ static inline void microkit_vcpu_x86_write_regs(microkit_child vcpu, seL4_VCPUCo } } -#endif +static inline void microkit_vcpu_x86_on(void) +{ + /* On x86, a TCB can only have one bound VCPU at any given time. + * So we don't take a `microkit_child vcpu` here. */ + microkit_x86_vcpu_state.do_resume = seL4_True; +} + +static inline void microkit_vcpu_x86_off(void) +{ + microkit_x86_vcpu_state.do_resume = seL4_False; +} + +#endif /* CONFIG_VTX */ +#endif /* CONFIG_ARCH_X86_64 */ static inline void microkit_deferred_notify(microkit_channel ch) { diff --git a/libmicrokit/src/main.c b/libmicrokit/src/main.c index 347ab0e23..bfc4ecd45 100644 --- a/libmicrokit/src/main.c +++ b/libmicrokit/src/main.c @@ -27,6 +27,12 @@ seL4_Bool microkit_have_signal = seL4_False; seL4_CPtr microkit_signal_cap; seL4_MessageInfo_t microkit_signal_msg; +#if defined(CONFIG_VTX) +struct microkit_x86_vcpu_state microkit_x86_vcpu_state; + +static seL4_Word microkit_x86_vmenter_result; +#endif /* CONFIG_VTX */ + seL4_Word microkit_irqs; seL4_Word microkit_notifications; seL4_Word microkit_pps; @@ -71,10 +77,89 @@ static void deferred_flush(void) } } +#if defined(CONFIG_VTX) +static seL4_MessageInfo_t x86_vcpu_resume(seL4_Word *badge) +{ + /* There isn't a seL4 syscall that atomically send signal then perform vmenter while waiting for + incoming notifications. So we have to dispatch any deferred signal first. Then switch execution + to the bound VCPU. A PD with a VCPU can't receive PPC on x86 so no need to check `have_reply`. */ + deferred_flush(); + + microkit_mr_set(SEL4_VMENTER_CALL_EIP_MR, microkit_x86_vcpu_state.rip); + microkit_mr_set(SEL4_VMENTER_CALL_CONTROL_PPC_MR, microkit_x86_vcpu_state.prim_proc_ctl); + microkit_mr_set(SEL4_VMENTER_CALL_INTERRUPT_INFO_MR, microkit_x86_vcpu_state.irq_info); + + microkit_x86_vmenter_result = seL4_VMEnter(badge); + + microkit_x86_vcpu_state.rip = microkit_mr_get(SEL4_VMENTER_CALL_EIP_MR); + microkit_x86_vcpu_state.prim_proc_ctl = microkit_mr_get(SEL4_VMENTER_CALL_CONTROL_PPC_MR); + microkit_x86_vcpu_state.irq_info = microkit_mr_get(SEL4_VMENTER_CALL_INTERRUPT_INFO_MR); + + /* Create a dummy tag so that we can call `fault()`, as VM Exits on x86 isn't modelled as an IPC like ARM. */ + if (microkit_x86_vmenter_result == SEL4_VMENTER_RESULT_FAULT) { + return seL4_MessageInfo_new(0, 0, 0, SEL4_VMENTER_NUM_FAULT_MSGS); + } else { + /* VCPU got interrupted due to a notification, no tag. */ + return seL4_MessageInfo_new(0, 0, 0, 0); + } +} +#endif + +static seL4_MessageInfo_t receive_event(bool have_reply, seL4_MessageInfo_t reply_tag, seL4_Word *badge) +{ +#if defined(CONFIG_VTX) + microkit_x86_vmenter_result = UINT64_MAX; + if (microkit_x86_vcpu_state.do_resume) { + return x86_vcpu_resume(badge); + } +#endif + + if (have_reply) { + deferred_flush(); + return seL4_ReplyRecv(INPUT_CAP, reply_tag, badge, REPLY_CAP); + } else if (microkit_have_signal) { + microkit_have_signal = seL4_False; + return seL4_NBSendRecv(microkit_signal_cap, microkit_signal_msg, INPUT_CAP, badge, REPLY_CAP); + } else { + return seL4_Recv(INPUT_CAP, badge, REPLY_CAP); + } +} + +static inline bool is_endpoint(seL4_Word badge) +{ + return badge >> 63; +} + +static bool is_fault(seL4_Word badge) +{ +#if defined(CONFIG_VTX) + if (microkit_x86_vmenter_result == SEL4_VMENTER_RESULT_FAULT) { + return true; + } +#endif + return (badge >> 62) & 1; +} + +static seL4_Bool handle_fault(seL4_Word badge, seL4_MessageInfo_t tag, seL4_MessageInfo_t *reply_tag) +{ + seL4_Bool reply_to_fault = fault(badge & PD_MASK, tag, reply_tag); +#if defined(CONFIG_VTX) + if (microkit_x86_vmenter_result == SEL4_VMENTER_RESULT_FAULT) { + /* There won't be anything to reply to for a VCPU fault. But + * if fault() returns false then we shouldn't resume the VCPU. */ + if (!reply_to_fault) { + microkit_x86_vcpu_state.do_resume = seL4_False; + } + reply_to_fault = seL4_False; + } +#endif + return reply_to_fault; +} + static void handler_loop(void) { bool have_reply = false; - seL4_MessageInfo_t reply_tag; + seL4_MessageInfo_t reply_tag = seL4_MessageInfo_new(0, 0, 0, 0); /** * Because of https://github.com/seL4/seL4/issues/1536 @@ -94,30 +179,14 @@ static void handler_loop(void) } for (;;) { - seL4_Word badge; - seL4_MessageInfo_t tag; - - if (have_reply) { - deferred_flush(); - tag = seL4_ReplyRecv(INPUT_CAP, reply_tag, &badge, REPLY_CAP); - } else if (microkit_have_signal) { - tag = seL4_NBSendRecv(microkit_signal_cap, microkit_signal_msg, INPUT_CAP, &badge, REPLY_CAP); - microkit_have_signal = seL4_False; - } else { - tag = seL4_Recv(INPUT_CAP, &badge, REPLY_CAP); - } - - uint64_t is_endpoint = badge >> 63; - uint64_t is_fault = (badge >> 62) & 1; + seL4_Word badge = 0; + seL4_MessageInfo_t tag = receive_event(have_reply, reply_tag, &badge); have_reply = false; - if (is_fault) { - seL4_Bool reply_to_fault = fault(badge & PD_MASK, tag, &reply_tag); - if (reply_to_fault) { - have_reply = true; - } - } else if (is_endpoint) { + if (is_fault(badge)) { + have_reply = handle_fault(badge, tag, &reply_tag); + } else if (is_endpoint(badge)) { have_reply = true; reply_tag = protected(badge & CHANNEL_MASK, tag); } else { From 93fde5bd4d581d7131855f97961a3ce3ba37d3f7 Mon Sep 17 00:00:00 2001 From: Bill Nguyen Date: Thu, 4 Jun 2026 13:43:18 +1000 Subject: [PATCH 3/3] manual: add x86 VCPU on/off APIs Add microkit_vcpu_x86_on() microkit_vcpu_x86_off() Signed-off-by: Bill Nguyen --- docs/manual.md | 53 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/docs/manual.md b/docs/manual.md index 5b9c3f1cd..2065151ed 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -649,6 +649,43 @@ To find the full list of possible faults that could occur and details regarding kind of fault, please see the 'Faults' section of the [seL4 reference manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf). +### x86 VCPU fault +Please see the 'VMX BASIC EXIT REASONS' section of the +[Intel® 64 and IA-32 Architectures Software Developer’s Manual Combined Volumes: 1, 2A, 2B, 2C, 2D, 3A, 3B, 3C, 3D, and 4] +(https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html) for a list of possible VM Exit reasons. + +These message registers contain data relating to the VM Exit: +- `SEL4_VMENTER_CALL_EIP_MR`: Instruction Pointer, +- `SEL4_VMENTER_CALL_CONTROL_PPC_MR`: Primary Processor Based VM Execution Controls, +- `SEL4_VMENTER_CALL_INTERRUPT_INFO_MR`: VM Entry Interruption-Information`, +- `SEL4_VMENTER_FAULT_REASON_MR`: VM Exit reason, +- `SEL4_VMENTER_FAULT_QUALIFICATION_MR`: VM Exit qualification, +- `SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR`: Length of instruction that caused the VM Exit, +- `SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR`: Guest Physical Address of the VM Exit, +- `SEL4_VMENTER_FAULT_RFLAGS_MR`: Guest FLAGS register, +- `SEL4_VMENTER_FAULT_GUEST_INT_MR`: Guest interruptability, +- `SEL4_VMENTER_FAULT_CR3_MR`: Guest CR3. + +Some of these message registers may not contain valid data depending on the VM Exit reason, +please consult the Intel SDM for more details. + +These message registers contain the guest general purpose registers at the time of VM Exit: +- `SEL4_VMENTER_FAULT_EAX` +- `SEL4_VMENTER_FAULT_EBX` +- `SEL4_VMENTER_FAULT_ECX` +- `SEL4_VMENTER_FAULT_EDX` +- `SEL4_VMENTER_FAULT_ESI` +- `SEL4_VMENTER_FAULT_EDI` +- `SEL4_VMENTER_FAULT_EBP` +- `SEL4_VMENTER_FAULT_R8` +- `SEL4_VMENTER_FAULT_R9` +- `SEL4_VMENTER_FAULT_R10` +- `SEL4_VMENTER_FAULT_R11` +- `SEL4_VMENTER_FAULT_R12` +- `SEL4_VMENTER_FAULT_R13` +- `SEL4_VMENTER_FAULT_R14` +- `SEL4_VMENTER_FAULT_R15` + ## `microkit_msginfo microkit_ppcall(microkit_channel ch, microkit_msginfo msginfo)` Performs a call to a protected procedure in a different PD. @@ -826,6 +863,20 @@ virtual CPU with ID `vcpu`. Write the registers of a given virtual CPU with ID `vcpu`. The `regs` argument is the pointer to the struct of registers `seL4_VCPUContext` that are written from. +## `void microkit_vcpu_x86_on(void)` + +Allow the PD to switch to guest execution mode with the bound vCPU every time `init()`, `notified()` or `fault()` return. + +The caller is responsible for initialising the VCPU's instruction pointer, Primary Processor-Based VM-Execution Controls, +VM-Entry Interruption-Information Field and other architectural states to the corresponding VMCS fields via +`microkit_vcpu_x86_write_vmcs()`. For more details, please see the 'Virtualisation' section of the +[seL4 reference manual](https://sel4.systems/Info/Docs/seL4-manual-latest.pdf). For architectural details, +please consult the [Intel SDM](https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html). + +## `void microkit_vcpu_x86_off(void)` + +Stop the PD from switching to guest execution mode when `init()`, `notified()` or `fault()` return. + ## `seL4_CPtr microkit_cspace_root_slot_to_cptr(seL4_Word slot)` {#libmicrokit_cspace_root_slot_to_cptr} Converts the slot identifier of the ``'s capability element into an @@ -948,6 +999,7 @@ The `virtual_machine` element has the following attributes: Additionally, it supports the following child elements: * `vcpu`: (one or more) Describes the virtual CPU that will be tied to the virtual machine. + * On x86-64, there is a limit of one VCPU per PD. * `map`: (zero or more) Describes mapping of memory regions into the virtual machine. The `vcpu` element has the following attributes: @@ -1027,6 +1079,7 @@ The `end` element has the following attributes: * `id`: Channel identifier in the context of the named protection domain. Must be at least 0 and less than 63. * `pp`: (optional) Indicates that the protection domain for this end can perform a protected procedure call to the other end; defaults to false. Protected procedure calls can only be to PDs of strictly higher priority. + On x86-64, PDs with virtual machines cannot receive protected procedure calls. * `notify`: (optional) Indicates that the protection domain for this end can send a notification to the other end; defaults to true. * `setvar_id`: (optional) Specifies a symbol in the program image. This symbol will be rewritten with the channel identifier.