Index: kernel/arch/ia32/src/drivers/i8259.c
===================================================================
--- kernel/arch/ia32/src/drivers/i8259.c	(revision 24abb85d299db39cc03f429adc41bb1ed4f23e23)
+++ kernel/arch/ia32/src/drivers/i8259.c	(revision df368491aa1c0ce3024a51c602b7d0cbe4bd84d3)
@@ -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);
 }