Index: kernel/arch/arm32/src/arm32.c
===================================================================
--- kernel/arch/arm32/src/arm32.c	(revision 60d931d2ab10130e11bbd48f2a9b389bc4e76ec1)
+++ kernel/arch/arm32/src/arm32.c	(revision 34511297c505e3db8e8d821daa74d5c4cb7abd4c)
@@ -49,4 +49,5 @@
 #include <str.h>
 #include <arch/ras.h>
+#include <sysinfo/sysinfo.h>
 
 /** Performs arm32-specific initialization before main_bsp() is called. */
@@ -116,4 +117,8 @@
 {
 	machine_input_init();
+	const char *platform = machine_get_platform_name();
+
+	sysinfo_set_item_data("platform", NULL, (void *) platform,
+	    str_size(platform));
 }
 
Index: kernel/arch/arm32/src/cpu/cpu.c
===================================================================
--- kernel/arch/arm32/src/cpu/cpu.c	(revision 60d931d2ab10130e11bbd48f2a9b389bc4e76ec1)
+++ kernel/arch/arm32/src/cpu/cpu.c	(revision 34511297c505e3db8e8d821daa74d5c4cb7abd4c)
@@ -44,14 +44,17 @@
 /** Implementators (vendor) names */
 static const char *imp_data[] = {
-	"?",					/* IMP_DATA_START_OFFSET */
-	"ARM Ltd",				/* 0x41 */
-	"",					/* 0x42 */
-	"",                             	/* 0x43 */
-	"Digital Equipment Corporation",	/* 0x44 */
-	"", "", "", "", "", "", "", "", "", "",	/* 0x45 - 0x4e */
-	"", "", "", "", "", "", "", "", "", "", /* 0x4f - 0x58 */
-	"", "", "", "", "", "", "", "", "", "", /* 0x59 - 0x62 */
-	"", "", "", "", "", "",			/* 0x63 - 0x68 */
-	"Intel Corporation"			/* 0x69 */
+	"?",                                     /* IMP_DATA_START_OFFSET */
+	"ARM Limited",                           /* 0x41 */
+	"", "",                                  /* 0x42 - 0x43 */
+	"Digital Equipment Corporation",         /* 0x44 */
+	"", "", "", "", "", "", "", "",          /* 0x45 - 0x4c */
+	"Motorola, Freescale Semicondutor Inc.", /* 0x4d */
+	"", "", "",                              /* 0x4e - 0x50 */
+	"Qualcomm Inc.",                         /* 0x51 */
+	"", "", "", "",                          /* 0x52 - 0x55 */
+	"Marvell Semiconductor",                 /* 0x56 */
+	"", "", "", "", "", "", "", "", "", "",  /* 0x57 - 0x60 */
+	"", "", "", "", "", "", "", "",          /* 0x61 - 0x68 */
+	"Intel Corporation"                      /* 0x69 */
 };
 
@@ -97,4 +100,23 @@
 void cpu_arch_init(void)
 {
+#if defined(PROCESSOR_armv7_a)
+	uint32_t control_reg = 0;
+	asm volatile (
+		"mrc p15, 0, %[control_reg], c1, c0"
+		: [control_reg] "=r" (control_reg)
+	);
+	
+	/* Turn off tex remap */
+	control_reg &= ~CP15_R1_TRE_BIT;
+	/* Turn off accessed flag */
+	control_reg &= ~(CP15_R1_AFE_BIT | CP15_R1_HA_ENABLE_BIT);
+	/* Enable caching */
+	control_reg |= CP15_R1_CACHE_ENABLE_BIT;
+	
+	asm volatile (
+		"mcr p15, 0, %[control_reg], c1, c0"
+		:: [control_reg] "r" (control_reg)
+	);
+#endif
 }
 
@@ -112,11 +134,12 @@
 	cpu_arch_t * cpu_arch = &m->arch;
 
-	if ((cpu_arch->imp_num) > 0 &&
-	    (cpu_arch->imp_num < (imp_data_length + IMP_DATA_START_OFFSET))) {
+	const unsigned imp_offset = cpu_arch->imp_num - IMP_DATA_START_OFFSET;
+
+	if (imp_offset < imp_data_length) {
 		vendor = imp_data[cpu_arch->imp_num - IMP_DATA_START_OFFSET];
 	}
 
-	if ((cpu_arch->arch_num) > 0 &&
-	    (cpu_arch->arch_num < arch_data_length)) {
+	// TODO CPUs with arch_num == 0xf use CPUID scheme for identification
+	if (cpu_arch->arch_num < arch_data_length) {
 		architecture = arch_data[cpu_arch->arch_num];
 	}
Index: kernel/arch/arm32/src/exception.c
===================================================================
--- kernel/arch/arm32/src/exception.c	(revision 60d931d2ab10130e11bbd48f2a9b389bc4e76ec1)
+++ kernel/arch/arm32/src/exception.c	(revision 34511297c505e3db8e8d821daa74d5c4cb7abd4c)
@@ -117,9 +117,24 @@
 
 #ifdef HIGH_EXCEPTION_VECTORS
-/** Activates use of high exception vectors addresses. */
+/** Activates use of high exception vectors addresses.
+ *
+ * "High vectors were introduced into some implementations of ARMv4 and are
+ * required in ARMv6 implementations. High vectors allow the exception vector
+ * locations to be moved from their normal address range 0x00000000-0x0000001C
+ * at the bottom of the 32-bit address space, to an alternative address range
+ * 0xFFFF0000-0xFFFF001C near the top of the address space. These alternative
+ * locations are known as the high vectors.
+ *
+ * Prior to ARMv6, it is IMPLEMENTATION DEFINED whether the high vectors are
+ * supported. When they are, a hardware configuration input selects whether
+ * the normal vectors or the high vectors are to be used from
+ * reset." ARM Architecture Reference Manual A2.6.11 (p. 64 in the PDF).
+ *
+ * ARM920T (gta02) TRM A2.3.5 (PDF p. 36) and ARM926EJ-S (icp) 2.3.2 (PDF p. 42)
+ * say that armv4 an armv5 chips that we support implement this.
+ */
 static void high_vectors(void)
 {
-	uint32_t control_reg;
-	
+	uint32_t control_reg = 0;
 	asm volatile (
 		"mrc p15, 0, %[control_reg], c1, c0"
@@ -153,4 +168,5 @@
 void exception_init(void)
 {
+	// TODO check for availability of high vectors for <= armv5
 #ifdef HIGH_EXCEPTION_VECTORS
 	high_vectors();
Index: kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c
===================================================================
--- kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c	(revision 34511297c505e3db8e8d821daa74d5c4cb7abd4c)
+++ kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c	(revision 34511297c505e3db8e8d821daa74d5c4cb7abd4c)
@@ -0,0 +1,259 @@
+/*
+ * Copyright (c) 2012 Jan Vesely
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ *
+ * - Redistributions of source code must retain the above copyright
+ *   notice, this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright
+ *   notice, this list of conditions and the following disclaimer in the
+ *   documentation and/or other materials provided with the distribution.
+ * - The name of the author may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
+ * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
+ * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
+ * IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
+ * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
+ * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
+ * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+/** @addtogroup arm32beagleboardxm
+ * @{
+ */
+/** @file
+ *  @brief BeagleBoard-xM platform driver.
+ */
+
+#include <arch/exception.h>
+#include <arch/mach/beagleboardxm/beagleboardxm.h>
+#include <genarch/drivers/amdm37x_irc/amdm37x_irc.h>
+#include <genarch/drivers/amdm37x_uart/amdm37x_uart.h>
+#include <genarch/drivers/amdm37x_gpt/amdm37x_gpt.h>
+#include <genarch/drivers/amdm37x_dispc/amdm37x_dispc.h>
+#include <genarch/fb/fb.h>
+#include <genarch/srln/srln.h>
+#include <interrupt.h>
+#include <mm/km.h>
+#include <ddi/ddi.h>
+#include <ddi/device.h>
+
+static void bbxm_init(void);
+static void bbxm_timer_irq_start(void);
+static void bbxm_cpu_halt(void);
+static void bbxm_get_memory_extents(uintptr_t *start, size_t *size);
+static void bbxm_irq_exception(unsigned int exc_no, istate_t *istate);
+static void bbxm_frame_init(void);
+static void bbxm_output_init(void);
+static void bbxm_input_init(void);
+static size_t bbxm_get_irq_count(void);
+static const char *bbxm_get_platform_name(void);
+
+#define BBXM_MEMORY_START	0x80000000	/* physical */
+#define BBXM_MEMORY_SIZE	0x20000000	/* 512 MB */
+
+static struct beagleboard {
+	amdm37x_dispc_regs_t *dispc;
+	amdm37x_irc_regs_t *irc_addr;
+	amdm37x_uart_t uart;
+	amdm37x_gpt_t timer;
+} beagleboard;
+
+struct arm_machine_ops bbxm_machine_ops = {
+	.machine_init = bbxm_init,
+	.machine_timer_irq_start = bbxm_timer_irq_start,
+	.machine_cpu_halt = bbxm_cpu_halt,
+	.machine_get_memory_extents = bbxm_get_memory_extents,
+	.machine_irq_exception = bbxm_irq_exception,
+	.machine_frame_init = bbxm_frame_init,
+	.machine_output_init = bbxm_output_init,
+	.machine_input_init = bbxm_input_init,
+	.machine_get_irq_count = bbxm_get_irq_count,
+	.machine_get_platform_name = bbxm_get_platform_name
+};
+
+static irq_ownership_t bb_timer_irq_claim(irq_t *irq)
+{
+	return IRQ_ACCEPT;
+}
+
+static void bbxm_setup_fb(unsigned width, unsigned height, unsigned bpp)
+{
+	const unsigned pixel_bytes = (bpp / 8);
+	const size_t size = ALIGN_UP(width * height * pixel_bytes, FRAME_SIZE);
+	const unsigned frames = size / FRAME_SIZE;
+	unsigned order = 0;
+	unsigned frame = 1;
+	while (frame < frames) {
+		frame *= 2;
+		++order;
+	}
+	printf("Allocating %d (2^%d) frames.\n", size, order);
+	/* prefer highmem as we don't care about virtual mapping. */
+	void *buffer = frame_alloc(order, FRAME_LOWMEM);
+	ASSERT(buffer);
+
+	amdm37x_dispc_setup_fb(beagleboard.dispc, width, height, bpp,
+	    (uintptr_t) buffer);
+
+	fb_properties_t prop = {
+		.addr = (uintptr_t)buffer,
+		.offset = 0,
+		.x = width,
+		.y = height,
+		.scan = width * pixel_bytes,
+		.visual = VISUAL_RGB_5_6_5_LE
+	};
+	switch (bpp)
+	{
+	case 8:
+		prop.visual = VISUAL_INDIRECT_8; break;
+	case 16:
+		prop.visual = VISUAL_RGB_5_6_5_LE; break;
+	case 24:
+		prop.visual = VISUAL_BGR_8_8_8; break;
+	case 32:
+		prop.visual = VISUAL_RGB_8_8_8_0; break;
+	default:
+		printf("Invalid framebuffer bit depth: bailing out.\n");
+		return;
+	}
+	outdev_t *fb_dev = fb_init(&prop);
+	if (fb_dev)
+		stdout_wire(fb_dev);
+
+}
+
+static void bb_timer_irq_handler(irq_t *irq)
+{
+        /*
+         * We are holding a lock which prevents preemption.
+         * Release the lock, call clock() and reacquire the lock again.
+         */
+	amdm37x_gpt_irq_ack(&beagleboard.timer);
+	spinlock_unlock(&irq->lock);
+	clock();
+	spinlock_lock(&irq->lock);
+}
+
+static void bbxm_init(void)
+{
+	/* Initialize interrupt controller */
+	beagleboard.irc_addr =
+	    (void *) km_map(AMDM37x_IRC_BASE_ADDRESS, AMDM37x_IRC_SIZE,
+	    PAGE_NOT_CACHEABLE);
+	ASSERT(beagleboard.irc_addr);
+	amdm37x_irc_init(beagleboard.irc_addr);
+
+	/* Map display controller */
+	beagleboard.dispc = (void*) km_map(AMDM37x_DISPC_BASE_ADDRESS,
+	    AMDM37x_DISPC_SIZE, PAGE_NOT_CACHEABLE);
+	ASSERT(beagleboard.dispc);
+
+	/* Initialize timer, pick timer1, because it is in always-power domain
+	 * and has special capabilities for regular ticks */
+	amdm37x_gpt_timer_ticks_init(&beagleboard.timer,
+	    AMDM37x_GPT1_BASE_ADDRESS, AMDM37x_GPT1_SIZE, HZ);
+}
+
+static void bbxm_timer_irq_start(void)
+{
+	/* Initialize timer IRQ */
+	static irq_t timer_irq;
+	irq_initialize(&timer_irq);
+	timer_irq.devno = device_assign_devno();
+	timer_irq.inr = AMDM37x_GPT1_IRQ;
+	timer_irq.claim = bb_timer_irq_claim;
+	timer_irq.handler = bb_timer_irq_handler;
+	irq_register(&timer_irq);
+
+	/* Enable timer interrupt */
+	amdm37x_irc_enable(beagleboard.irc_addr, AMDM37x_GPT1_IRQ);
+
+	/* Start timer here */
+	amdm37x_gpt_timer_ticks_start(&beagleboard.timer);
+}
+
+static void bbxm_cpu_halt(void)
+{
+	while (1);
+}
+
+/** Get extents of available memory.
+ *
+ * @param start		Place to store memory start address (physical).
+ * @param size		Place to store memory size.
+ */
+static void bbxm_get_memory_extents(uintptr_t *start, size_t *size)
+{
+	*start = BBXM_MEMORY_START;
+	*size = BBXM_MEMORY_SIZE;
+}
+
+static void bbxm_irq_exception(unsigned int exc_no, istate_t *istate)
+{
+	const unsigned inum = amdm37x_irc_inum_get(beagleboard.irc_addr);
+	amdm37x_irc_irq_ack(beagleboard.irc_addr);
+
+	irq_t *irq = irq_dispatch_and_lock(inum);
+	if (irq) {
+		/* The IRQ handler was found. */
+		irq->handler(irq);
+		spinlock_unlock(&irq->lock);
+	} else {
+		/* Spurious interrupt.*/
+		printf("cpu%d: spurious interrupt (inum=%d)\n",
+		    CPU->id, inum);
+	}
+}
+
+static void bbxm_frame_init(void)
+{
+}
+
+static void bbxm_output_init(void)
+{
+#ifdef CONFIG_FB
+	bbxm_setup_fb(CONFIG_BFB_WIDTH, CONFIG_BFB_HEIGHT, CONFIG_BFB_BPP);
+#else
+	(void)bbxm_setup_fb;
+#endif
+	/* UART3 is wired to external RS232 connector */
+	const bool ok = amdm37x_uart_init(&beagleboard.uart,
+	    AMDM37x_UART3_IRQ, AMDM37x_UART3_BASE_ADDRESS, AMDM37x_UART3_SIZE);
+	if (ok) {
+		stdout_wire(&beagleboard.uart.outdev);
+	}
+}
+
+static void bbxm_input_init(void)
+{
+	srln_instance_t *srln_instance = srln_init();
+	if (srln_instance) {
+		indev_t *sink = stdin_wire();
+		indev_t *srln = srln_wire(srln_instance, sink);
+		amdm37x_uart_input_wire(&beagleboard.uart, srln);
+		amdm37x_irc_enable(beagleboard.irc_addr, AMDM37x_UART3_IRQ);
+	}
+}
+
+size_t bbxm_get_irq_count(void)
+{
+	return AMDM37x_IRC_IRQ_COUNT;
+}
+
+const char *bbxm_get_platform_name(void)
+{
+	return "beagleboardxm";
+}
+
+/**
+ * @}
+ */
Index: kernel/arch/arm32/src/machine_func.c
===================================================================
--- kernel/arch/arm32/src/machine_func.c	(revision 60d931d2ab10130e11bbd48f2a9b389bc4e76ec1)
+++ kernel/arch/arm32/src/machine_func.c	(revision 34511297c505e3db8e8d821daa74d5c4cb7abd4c)
@@ -42,4 +42,5 @@
 #include <arch/mach/integratorcp/integratorcp.h>
 #include <arch/mach/testarm/testarm.h>
+#include <arch/mach/beagleboardxm/beagleboardxm.h>
 
 /** Pointer to machine_ops structure being used. */
@@ -55,4 +56,6 @@
 #elif defined(MACHINE_integratorcp)
 	machine_ops = &icp_machine_ops;
+#elif defined(MACHINE_beagleboardxm)
+	machine_ops = &bbxm_machine_ops;
 #else
 #error Machine type not defined.
@@ -131,4 +134,10 @@
 }
 
+const char * machine_get_platform_name(void)
+{
+	if (machine_ops->machine_get_platform_name)
+		return machine_ops->machine_get_platform_name();
+	return NULL;
+}
 /** @}
  */
Index: kernel/arch/arm32/src/mm/page.c
===================================================================
--- kernel/arch/arm32/src/mm/page.c	(revision 60d931d2ab10130e11bbd48f2a9b389bc4e76ec1)
+++ kernel/arch/arm32/src/mm/page.c	(revision 34511297c505e3db8e8d821daa74d5c4cb7abd4c)
@@ -52,14 +52,16 @@
 void page_arch_init(void)
 {
-	int flags = PAGE_CACHEABLE;
+	int flags = PAGE_CACHEABLE | PAGE_EXEC;
 	page_mapping_operations = &pt_mapping_operations;
 
 	page_table_lock(AS_KERNEL, true);
 	
-	uintptr_t cur;
-
 	/* Kernel identity mapping */
-	for (cur = PHYSMEM_START_ADDR;
-	    cur < min(config.identity_size, config.physmem_end);
+	//FIXME: We need to consider the possibility that
+	//identity_base > identity_size and physmem_end.
+	//This might lead to overflow if identity_size is too big.
+	for (uintptr_t cur = PHYSMEM_START_ADDR;
+	    cur < min(KA2PA(config.identity_base) +
+	        config.identity_size, config.physmem_end);
 	    cur += FRAME_SIZE)
 		page_mapping_insert(AS_KERNEL, PA2KA(cur), cur, flags);
Index: kernel/arch/arm32/src/mm/page_fault.c
===================================================================
--- kernel/arch/arm32/src/mm/page_fault.c	(revision 60d931d2ab10130e11bbd48f2a9b389bc4e76ec1)
+++ kernel/arch/arm32/src/mm/page_fault.c	(revision 34511297c505e3db8e8d821daa74d5c4cb7abd4c)
@@ -42,27 +42,38 @@
 #include <print.h>
 
-/** Returns value stored in fault status register.
+/** Returns value stored in comnbined/data fault status register.
  *
  *  @return Value stored in CP15 fault status register (FSR).
+ *
+ *  "VMSAv6 added a fifth fault status bit (bit[10]) to both the IFSR and DFSR.
+ *  It is IMPLEMENTATION DEFINED how this bit is encoded in earlier versions of
+ *  the architecture. A write flag (bit[11] of the DFSR) has also been
+ *  introduced."
+ *  ARM Architecture Reference Manual version i ch. B4.6 (PDF p. 719)
+ *
+ *  See ch. B4.9.6 for location of data/instruction FSR.
+ *
  */
-static inline fault_status_t read_fault_status_register(void)
+static inline fault_status_t read_data_fault_status_register(void)
 {
-	fault_status_union_t fsu;
+	fault_status_t fsu;
 	
-	/* fault status is stored in CP15 register 5 */
+	/* Combined/Data fault status is stored in CP15 register 5, c0. */
 	asm volatile (
 		"mrc p15, 0, %[dummy], c5, c0, 0"
-		: [dummy] "=r" (fsu.dummy)
+		: [dummy] "=r" (fsu.raw)
 	);
 	
-	return fsu.fs;
+	return fsu;
 }
 
-/** Returns FAR (fault address register) content.
+/** Returns DFAR (fault address register) content.
  *
- * @return FAR (fault address register) content (address that caused a page
+ * This register is equivalent to FAR on pre armv6 machines.
+ *
+ * @return DFAR (fault address register) content (address that caused a page
  *         fault)
  */
-static inline uintptr_t read_fault_address_register(void)
+static inline uintptr_t read_data_fault_address_register(void)
 {
 	uintptr_t ret;
@@ -77,4 +88,5 @@
 }
 
+#if defined(PROCESSOR_armv4) | defined(PROCESSOR_armv5)
 /** Decides whether read or write into memory is requested.
  *
@@ -97,5 +109,5 @@
 		panic("page_fault - instruction does not access memory "
 		    "(instr_code: %#0" PRIx32 ", badvaddr:%p).",
-		    instr_union.pc, (void *) badvaddr);
+		    *(uint32_t*)instr_union.instr, (void *) badvaddr);
 		return PF_ACCESS_EXEC;
 	}
@@ -136,4 +148,5 @@
 	    inst, (void *) badvaddr);
 }
+#endif
 
 /** Handles "data abort" exception (load or store at invalid address).
@@ -145,10 +158,15 @@
 void data_abort(unsigned int exc_no, istate_t *istate)
 {
-	fault_status_t fsr __attribute__ ((unused)) =
-	    read_fault_status_register();
-	uintptr_t badvaddr = read_fault_address_register();
+	uintptr_t badvaddr = read_data_fault_address_register();
 
-	pf_access_t access = get_memory_access_type(istate->pc, badvaddr);
-
+#if defined(PROCESSOR_armv6) | defined(PROCESSOR_armv7_a)
+	fault_status_t fsr = read_data_fault_status_register();
+	const pf_access_t access =
+	    fsr.data.wr ? PF_ACCESS_WRITE : PF_ACCESS_READ;
+#elif defined(PROCESSOR_armv4) | defined(PROCESSOR_armv5)
+	const pf_access_t access = get_memory_access_type(istate->pc, badvaddr);
+#else
+#error "Unsupported architecture"
+#endif
 	int ret = as_page_fault(badvaddr, access, istate);
 
@@ -167,4 +185,5 @@
 void prefetch_abort(unsigned int exc_no, istate_t *istate)
 {
+	/* NOTE: We should use IFAR and IFSR here. */
 	int ret = as_page_fault(istate->pc, PF_ACCESS_EXEC, istate);
 
