Searched refs:ioredtbl_high (Results 1 - 1 of 1) sorted by relevance

/seL4-l4v-10.1.1/seL4/src/plat/pc99/machine/
H A Dioapic.c152 uint32_t ioredtbl_high = 0; local
157 ioredtbl_high = ioapic_read(ioapic, IOAPIC_WINDOW) & MASK(IOREDTBL_HIGH_RESERVED_BITS);
159 ioredtbl_high |= (ioapic_target_cpu << IOREDTBL_HIGH_RESERVED_BITS);
160 ioapic_write(ioapic, IOAPIC_WINDOW, ioredtbl_high);

Completed in 30 milliseconds