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 06ae793150dfa79fa455b8d805a4e29fd70413fe)
@@ -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);
 }