Index: kernel/arch/ia32/src/drivers/i8259.c
===================================================================
--- kernel/arch/ia32/src/drivers/i8259.c	(revision 38b0ae2913b97fd6187fb83fbd73a39c7517ae23)
+++ kernel/arch/ia32/src/drivers/i8259.c	(revision a211838659e5f36770cab316785a73bb49c1fca5)
@@ -50,5 +50,5 @@
 {
 	/* ICW1: this is ICW1, ICW4 to follow */
-	pio_write_8(PIC_PIC0PORT1, PIC_ICW1 | PIC_NEEDICW4);
+	pio_write_8(PIC_PIC0PORT1, PIC_ICW1 | PIC_ICW1_NEEDICW4);
 
 	/* ICW2: IRQ 0 maps to INT IRQBASE */
@@ -62,5 +62,5 @@
 
 	/* ICW1: ICW1, ICW4 to follow */
-	pio_write_8(PIC_PIC1PORT1, PIC_ICW1 | PIC_NEEDICW4);
+	pio_write_8(PIC_PIC1PORT1, PIC_ICW1 | PIC_ICW1_NEEDICW4);
 
 	/* ICW2: IRQ 8 maps to INT (IVT_IRQBASE + 8) */
@@ -122,6 +122,6 @@
 void pic_eoi(void)
 {
-	pio_write_8((ioport8_t *) 0x20, 0x20);
-	pio_write_8((ioport8_t *) 0xa0, 0x20);
+	pio_write_8(PIC_PIC0PORT1, PIC_OCW4 | PIC_OCW4_NSEOI);
+	pio_write_8(PIC_PIC1PORT1, PIC_OCW4 | PIC_OCW4_NSEOI);
 }
 
