diff --git a/src/kernel/boot/platform/bios_ia32/bios.h b/src/kernel/boot/platform/bios_ia32/bios.h
index 531ee628f5..c5f122b1c7 100644
--- a/src/kernel/boot/platform/bios_ia32/bios.h
+++ b/src/kernel/boot/platform/bios_ia32/bios.h
@@ -25,6 +25,10 @@ struct bios_regs {
 
 #define CARRY_FLAG	0x01
 
+static const addr_t kDataSegmentScratch = 0x10020;	// about 768 bytes
+static const addr_t kDataSegmentBase = 0x10000;
+static const addr_t kExtraSegmentScratch = 0x2000;	// about 24 kB
+
 extern
 #ifdef __cplusplus
 "C"