diff --git a/configs/bpi-shmem-demo.c b/configs/bpi-shmem-demo.c
new file mode 100644
index 0000000..3ac9915
--- /dev/null
+++ b/configs/bpi-shmem-demo.c
@@ -0,0 +1,96 @@
+/*
+ * Jailhouse, a Linux-based partitioning hypervisor
+ *
+ * Configuration for ivshmem-demo on Banana Pi.
+ * Bananapi-gic-demo from Siemens
+ * 1 CPU, 64K RAM, serial ports 4-7, CCU+GPIO
+ *
+ * Copyright (c) Retotech AB, 2017
+ * Copyright (c) Siemens AG, 2014
+ *
+ * Authors:
+ *  Ola Redell <ola.redell@retotech.se>
+ *  Jan Kiszka <jan.kiszka@siemens.com>
+ *
+ * This work is licensed under the terms of the GNU GPL, version 2.  See
+ * the COPYING file in the top-level directory.
+ */
+
+#include <jailhouse/types.h>
+#include <jailhouse/cell-config.h>
+
+#define ARRAY_SIZE(a) sizeof(a) / sizeof(a[0])
+
+struct {
+	struct jailhouse_cell_desc cell;
+	__u64 cpus[1];
+	struct jailhouse_memory mem_regions[5];
+	struct jailhouse_pci_device pci_devices[1];
+//	struct jailhouse_pci_capability pci_caps[0];
+} __attribute__((packed)) config = {
+	.cell = {
+		.signature = JAILHOUSE_CELL_DESC_SIGNATURE,
+		.revision = JAILHOUSE_CONFIG_REVISION,
+		.name = "bpi-shmem-demo",
+		.flags = JAILHOUSE_CELL_PASSIVE_COMMREG,
+
+		.cpu_set_size = sizeof(config.cpus),
+		.num_memory_regions = ARRAY_SIZE(config.mem_regions),
+                .num_pci_devices = ARRAY_SIZE(config.pci_devices),
+/*                  .num_pci_caps = ARRAY_SIZE(config.pci_caps),*/
+	},
+
+	.cpus = {
+		0x2,
+	},
+
+	.mem_regions = {
+		/* CCU */ {
+			.phys_start = 0x01c20000,
+			.virt_start = 0x01c20000,
+			.size = 0x400,
+			.flags = JAILHOUSE_MEM_READ | JAILHOUSE_MEM_WRITE |
+				JAILHOUSE_MEM_IO | JAILHOUSE_MEM_IO_32,
+		},
+		/* GPIO: port H */ {
+			.phys_start = 0x01c208fc,
+			.virt_start = 0x01c208fc,
+			.size = 0x24,
+			.flags = JAILHOUSE_MEM_READ | JAILHOUSE_MEM_WRITE |
+				JAILHOUSE_MEM_IO | JAILHOUSE_MEM_IO_32,
+		},
+		/* UART 4-7 */ {
+			.phys_start = 0x01c29000,
+			.virt_start = 0x01c29000,
+			.size = 0x1000,
+			.flags = JAILHOUSE_MEM_READ | JAILHOUSE_MEM_WRITE |
+				JAILHOUSE_MEM_IO,
+		},
+		/* RAM */ {
+			.phys_start = 0x7d000000,
+			.virt_start = 0,
+			.size = 0x00010000,
+			.flags = JAILHOUSE_MEM_READ | JAILHOUSE_MEM_WRITE |
+				JAILHOUSE_MEM_EXECUTE | JAILHOUSE_MEM_LOADABLE,
+		},
+		/* IVSHMEM shared memory region */  {
+			.phys_start = 0x7bf00000,
+			.virt_start = 0x7bf00000,
+			.size = 0x100000,
+			.flags = JAILHOUSE_MEM_READ | JAILHOUSE_MEM_WRITE,
+                        },
+	},
+        
+              .pci_devices = {
+		{
+			.type = JAILHOUSE_PCI_TYPE_IVSHMEM,
+			.bdf = 0x00,
+			.bar_mask = {
+				0xffffff00, 0xffffffff, 0x00000000,
+				0x00000000, 0x00000000, 0x00000000,
+			},
+			.shmem_region = 4, /* must be no of IVSHMEM region above */
+			.shmem_protocol = JAILHOUSE_SHMEM_PROTO_VETH,
+		},
+                },
+};
diff --git a/hypervisor/ivshmem.c b/hypervisor/ivshmem.c
index cfe7d0a..317dd9d 100644
--- a/hypervisor/ivshmem.c
+++ b/hypervisor/ivshmem.c
@@ -348,7 +348,21 @@ int ivshmem_init(struct cell *cell, struct pci_device *device)
 		if (peer_mem->phys_start != mem->phys_start ||
 		    peer_mem->size != mem->size ||
 		    peer_dev->info->shmem_protocol != dev_info->shmem_protocol)
+		{
+			if (peer_mem->phys_start != mem->phys_start)
+				printk("phys_start differ (%#llx!=%#llx)",
+				       peer_mem->phys_start, mem->phys_start);
+			if (peer_mem->size != mem->size)
+				printk("size differ (%#llx!=%#llx)",
+				       peer_mem->size, mem->size);
+			if (peer_dev->info->shmem_protocol !=
+			    dev_info->shmem_protocol)
+				printk("shmem_protocol differ (%d!=%d)",
+				       peer_dev->info->shmem_protocol,
+				       dev_info->shmem_protocol);
+
 			return trace_error(-EINVAL);
+		}
 
 		printk("Shared memory connection established: "
 		       "\"%s\" <--> \"%s\"\n",
diff --git a/inmates/demos/arm/Makefile b/inmates/demos/arm/Makefile
index b0fda4e..afef36c 100644
--- a/inmates/demos/arm/Makefile
+++ b/inmates/demos/arm/Makefile
@@ -12,9 +12,10 @@
 
 include $(INMATES_LIB)/Makefile.lib
 
-INMATES := gic-demo.bin uart-demo.bin
+INMATES := gic-demo.bin uart-demo.bin ivshmem-demo.bin
 
 gic-demo-y	:= gic-demo.o
 uart-demo-y	:= uart-demo.o
+ivshmem-demo-y	:= ivshmem-demo.o
 
 $(eval $(call DECLARE_TARGETS,$(INMATES)))
diff --git a/inmates/demos/arm/ivshmem-demo.c b/inmates/demos/arm/ivshmem-demo.c
new file mode 100644
index 0000000..fd04acd
--- /dev/null
+++ b/inmates/demos/arm/ivshmem-demo.c
@@ -0,0 +1,204 @@
+/*
+ * Jailhouse, a Linux-based partitioning hypervisor
+ *
+ * Copyright (c) Siemens AG, 2014-2016
+ *
+ * Authors:
+ *  Henning Schild <henning.schild@siemens.com>
+ *
+ * This work is licensed under the terms of the GNU GPL, version 2.  See
+ * the COPYING file in the top-level directory.
+ */
+#include <inmate.h>
+
+#define VENDORID	0x1af4
+#define DEVICEID	0x1110
+
+#define IVSHMEM_CFG_SHMEM_PTR	0x40
+#define IVSHMEM_CFG_SHMEM_SZ	0x48
+
+#define JAILHOUSE_SHMEM_PROTO_UNDEFINED	0x0000
+
+#define IVSHMEM_IRQ	155
+
+#define MAX_NDEV	4
+#define UART_BASE	0x3F8
+
+static char str[64] = "Hello from bare-metal ivshmem-demo inmate!!!  ";
+static int irq_counter;
+
+struct ivshmem_dev_data {
+	u16 bdf;
+	u32 *registers;
+	void *shmem;
+	//u32 *msix_table;
+	u64 shmemsz;
+	u64 bar2sz;
+};
+
+static struct ivshmem_dev_data devs[MAX_NDEV];
+
+
+static u64 pci_cfg_read64(u16 bdf, unsigned int addr)
+{
+	u64 bar;
+
+	bar = ((u64)pci_read_config(bdf, addr + 4, 4) << 32) |
+	      pci_read_config(bdf, addr, 4);
+	return bar;
+}
+
+static void pci_cfg_write64(u16 bdf, unsigned int addr, u64 val)
+{
+	pci_write_config(bdf, addr + 4, (u32)(val >> 32), 4);
+	pci_write_config(bdf, addr, (u32)val, 4);
+}
+
+static u64 get_bar_sz(u16 bdf, u8 barn)
+{
+	u64 bar, tmp;
+	u64 barsz;
+
+	bar = pci_cfg_read64(bdf, PCI_CFG_BAR + (8 * barn));
+	pci_cfg_write64(bdf, PCI_CFG_BAR + (8 * barn), 0xffffffffffffffffULL);
+	tmp = pci_cfg_read64(bdf, PCI_CFG_BAR + (8 * barn));
+	barsz = ~(tmp & ~(0xf)) + 1;
+	pci_cfg_write64(bdf, PCI_CFG_BAR + (8 * barn), bar);
+
+	return barsz;
+}
+
+static int map_shmem_and_bars(struct ivshmem_dev_data *d)
+{
+	if (0 > pci_find_cap(d->bdf, PCI_CAP_MSIX)) {
+		printk("IVSHMEM ERROR: device is not MSI-X capable\n");
+		//return 1;
+	}
+
+	d->shmemsz = pci_cfg_read64(d->bdf, IVSHMEM_CFG_SHMEM_SZ);
+	d->shmem = (void *)((u32)(0xffffffff & pci_cfg_read64(d->bdf, IVSHMEM_CFG_SHMEM_PTR)));
+
+	printk("IVSHMEM: shmem is at %p\n", d->shmem);
+	d->registers =
+	  (u32 *)(((u32)(d->shmem + d->shmemsz + PAGE_SIZE - 1)) & PAGE_MASK);
+	pci_cfg_write64(d->bdf, PCI_CFG_BAR, (u32)d->registers);
+	printk("IVSHMEM: bar0 is at %p\n", d->registers);
+	d->bar2sz = get_bar_sz(d->bdf, 2);
+
+	/*
+	d->msix_table =
+	  (u32 *)(d->registers + PAGE_SIZE);
+	pci_cfg_write64(d->bdf, PCI_CFG_BAR + 16, (u32)d->msix_table);
+	printk("IVSHMEM: bar2 is at %p\n", d->msix_table);
+	*/
+
+	pci_write_config(d->bdf, PCI_CFG_COMMAND,
+			 (PCI_CMD_MEM | PCI_CMD_MASTER), 2);
+	return 0;
+}
+
+static u32 get_ivpos(struct ivshmem_dev_data *d)
+{
+	return mmio_read32(d->registers + 2);
+}
+
+static void send_irq(struct ivshmem_dev_data *d)
+{
+	printk("IVSHMEM: %02x:%02x.%x sending IRQ (by writing 1 to 0x%x)\n",
+	       d->bdf >> 8, (d->bdf >> 3) & 0x1f, d->bdf & 0x3,
+	       d->registers + 3);
+	mmio_write32(d->registers + 3, 1);
+}
+
+static void enable_irq(struct ivshmem_dev_data *d)
+{
+	printk("IVSHMEM: Enabling IVSHMEM_IRQs\n");
+	mmio_write32(d->registers, 0xffffffff);
+}
+
+static void handle_irq(unsigned int irqn)
+{
+	printk("IVSHMEM: handle_irq(irqn:%d) - interrupt #%d\n",
+	       irqn, irq_counter++);
+}
+
+void inmate_main(void)
+{
+	unsigned int i = 0;
+	/* FIXME: Get the PCI configuration space base address from
+	// command line arguments
+	// (originally, get it from the root cell config
+	// file:config.header.platform_info.pci_mmconfig_base) */
+	int bdf = 0;
+	unsigned int class_rev;
+	struct ivshmem_dev_data *d;
+	volatile char *shmem;
+	int ndevices = 0;
+
+	gic_setup(handle_irq);
+
+	while ((ndevices < MAX_NDEV) &&
+	       (-1 != (bdf = pci_find_device(VENDORID, DEVICEID, bdf)))) {
+		printk("IVSHMEM: Found %04x:%04x at %02x:%02x.%x\n",
+		       pci_read_config(bdf, PCI_CFG_VENDOR_ID, 2),
+		       pci_read_config(bdf, PCI_CFG_DEVICE_ID, 2),
+		       bdf >> 8, (bdf >> 3) & 0x1f, bdf & 0x3);
+		class_rev = pci_read_config(bdf, 0x8, 4);
+		if (class_rev != (PCI_DEV_CLASS_OTHER << 24 |
+				  JAILHOUSE_SHMEM_PROTO_UNDEFINED << 8)) {
+			printk("IVSHMEM: class/revision %08x, not supported "
+			       "skipping device\n", class_rev);
+			bdf++;
+			continue;
+		}
+		ndevices++;
+		d = devs + ndevices - 1;
+		d->bdf = bdf;
+		if (map_shmem_and_bars(d)) {
+			printk("IVSHMEM: Failure mapping shmem and bars.\n");
+			return;
+		}
+
+		printk("IVSHMEM: mapped shmem and bars, got position %p\n",
+		       get_ivpos(d));
+
+		//printk("IVSHMEM: memcpy(%p, %s, %d)\n", d->shmem, str, 32);
+		//memcpy(d->shmem, str, 32);
+		//printk("IVSHMEM: %p:%s\n", d->shmem, d->shmem);
+
+		gic_enable_irq(IVSHMEM_IRQ + ndevices - 1);
+		printk("IVSHMEM: Enabled IRQ:0x%x\n", IVSHMEM_IRQ +  ndevices -1);
+
+		enable_irq(d);
+
+		//pci_msix_set_vector(bdf, IVSHMEM_IRQ + ndevices - 1, 0);
+		//printk("IVSHMEM: Vector set for PCI MSI-X.\n");
+		bdf++;
+	}
+
+	if (!ndevices) {
+		printk("IVSHMEM: No PCI devices found .. nothing to do.\n");
+		return;
+	}
+
+	printk("IVSHMEM: Done setting up...\n");
+
+	{
+		u8 buf[32];
+		memcpy(buf, d->shmem, sizeof(buf)/sizeof(buf[0]));
+		printk("IVSHMEM: %s\n", buf);
+		memcpy(d->shmem, str, sizeof(str)/sizeof(str[0]));
+	}
+
+	while (1) {
+		for (i = 0; i < ndevices; i++) {
+			d = devs + i;
+			//delay_us(1000*1000);
+			shmem = d->shmem;
+			shmem[19]++;
+			send_irq(d);
+		}
+		printk("IVSHMEM: waiting for interrupt.\n");
+		asm volatile("wfi" : : : "memory");
+	}
+}
diff --git a/inmates/lib/arm/Makefile b/inmates/lib/arm/Makefile
index f126bce..3626118 100644
--- a/inmates/lib/arm/Makefile
+++ b/inmates/lib/arm/Makefile
@@ -20,3 +20,5 @@ ccflags-y := -ffunction-sections
 lib-y				:= $(COMMON_OBJECTS)
 lib-y				+= header.o
 lib-$(CONFIG_ARM_GIC_V3)	+= gic-v3.o
+lib-y				+= pci.o
+lib-y				+= ../pci.o
diff --git a/inmates/lib/arm/include/inmate.h b/inmates/lib/arm/include/inmate.h
index bbf9313..c0453d5 100644
--- a/inmates/lib/arm/include/inmate.h
+++ b/inmates/lib/arm/include/inmate.h
@@ -13,6 +13,38 @@
 #ifndef _JAILHOUSE_INMATE_H
 #define _JAILHOUSE_INMATE_H
 
+#define HEAP_BASE 0x0
+
+// FIXME: Consider moving the PCI related definitions and declarations below to
+// jailhouse/inmates/lib/pci.h instead?!?!?
+
+#define PAGE_SIZE		(4 * 1024UL)
+#define PAGE_MASK		(~(PAGE_SIZE - 1))
+
+#define PCI_CFG_VENDOR_ID	0x000
+#define PCI_CFG_DEVICE_ID	0x002
+#define PCI_CFG_COMMAND		0x004
+# define PCI_CMD_IO		(1 << 0)
+# define PCI_CMD_MEM		(1 << 1)
+# define PCI_CMD_MASTER		(1 << 2)
+# define PCI_CMD_INTX_OFF	(1 << 10)
+#define PCI_CFG_STATUS		0x006
+# define PCI_STS_INT		(1 << 3)
+# define PCI_STS_CAPS		(1 << 4)
+#define PCI_CFG_BAR		0x010
+# define PCI_BAR_64BIT		0x4
+#define PCI_CFG_CAP_PTR		0x034
+
+#define PCI_ID_ANY		0xffff
+
+#define PCI_DEV_CLASS_OTHER	0xff
+
+#define PCI_CAP_MSI		0x05
+#define PCI_CAP_MSIX		0x11
+
+#define MSIX_CTRL_ENABLE	0x8000
+#define MSIX_CTRL_FMASK		0x4000
+
 #ifndef __ASSEMBLY__
 typedef signed char s8;
 typedef unsigned char u8;
@@ -36,6 +68,11 @@ static inline void mmio_write8(void *address, u8 value)
 	*(volatile u8 *)address = value;
 }
 
+static inline u16 mmio_read16(void *address)
+{
+	return *((volatile u16 *)address);
+}
+
 static inline void mmio_write16(void *address, u16 value)
 {
 	*(volatile u16 *)address = value;
@@ -56,6 +93,12 @@ static inline void cpu_relax(void)
 	asm volatile("" : : : "memory");
 }
 
+static inline unsigned int cpu_id(void) {
+	// FIXME: We should get the real CPI ID (from cp15?)!!!
+	// x86 does this: return read_msr(X2APIC_ID);
+	return 1;
+}
+
 /*
  * To ease the debugging, we can send a spurious hypercall, which should return
  * -ENOSYS, but appear in the hypervisor stats for this cell.
@@ -80,6 +123,14 @@ u64 timer_get_ticks(void);
 u64 timer_ticks_to_ns(u64 ticks);
 void timer_start(u64 timeout);
 
+u32 pci_read_config(u16 bdf, unsigned int addr, unsigned int size);
+void pci_write_config(u16 bdf, unsigned int addr, u32 value,
+		      unsigned int size);
+int pci_find_device(u16 vendor, u16 device, u16 start_bdf);
+int pci_find_cap(u16 bdf, u16 cap);
+void pci_msi_set_vector(u16 bdf, unsigned int vector);
+void pci_msix_set_vector(u16 bdf, unsigned int vector, u32 index);
+
 #endif /* !__ASSEMBLY__ */
 
 #include "../inmate_common.h"
diff --git a/inmates/lib/arm/pci.c b/inmates/lib/arm/pci.c
new file mode 100644
index 0000000..00c79eb
--- /dev/null
+++ b/inmates/lib/arm/pci.c
@@ -0,0 +1,112 @@
+/*
+ * Jailhouse, a Linux-based partitioning hypervisor
+ *
+ * Copyright (c) Siemens AG, 2014
+ *
+ * Authors:
+ *  Jan Kiszka <jan.kiszka@siemens.com>
+ *
+ * This work is licensed under the terms of the GNU GPL, version 2.  See
+ * the COPYING file in the top-level directory.
+ */
+
+#include <inmate.h>
+
+// PCI configuration space base address taken from the
+// root cell config file:config.header.platform_info.pci_mmconfig_base
+#define PCI_CFG_BASE	(0x02000000)
+
+u32 pci_read_config(u16 bdf, unsigned int addr, unsigned int size)
+{
+	u32 reg_addr = PCI_CFG_BASE | ((u32)bdf << 8) | (addr & 0xfc);
+	//printk("%s(bdf:0x%x, addr:%p, size:0x%x), reg_addr0x%x\n", __func__, bdf, addr, size, reg_addr);
+	switch (size) {
+	case 1:
+		return mmio_read8((u8 *)(reg_addr + (addr & 0x3)));
+	case 2:
+		return mmio_read16((u16 *)(reg_addr + (addr & 0x3)));
+	case 4:
+		return mmio_read32((u32 *)(reg_addr));
+	default:
+		return -1;
+	}
+}
+
+void pci_write_config(u16 bdf, unsigned int addr, u32 value, unsigned int size)
+{
+	u32 reg_addr = PCI_CFG_BASE | ((u32)bdf << 8) | (addr & 0xfc);
+	//printk("%s(bdf:0x%x, addr:%p, value:0x%x, size:0x%x), reg_addr0x%x\n", __func__, bdf, addr, value, size, reg_addr);
+	switch (size) {
+	case 1:
+		mmio_write8((u8 *)(reg_addr + (addr & 0x3)), value);
+		break;
+	case 2:
+		mmio_write16((u16 *)(reg_addr + (addr & 0x3)), value);
+		break;
+	case 4:
+		mmio_write32((u32 *)(reg_addr), value);
+		break;
+	}
+}
+
+void pci_msix_set_vector(u16 bdf, unsigned int vector, u32 index)
+{
+	int cap = pci_find_cap(bdf, PCI_CAP_MSIX);
+	unsigned int bar;
+	u64 msix_table = 0;
+	u32 addr;
+	u16 ctrl;
+	u32 table;
+
+	if (cap < 0)
+		return;
+	ctrl = pci_read_config(bdf, cap + 2, 2);
+	/* bounds check */
+	if (index > (ctrl & 0x3ff))
+		return;
+	table = pci_read_config(bdf, cap + 4, 4);
+	bar = (table & 7) * 4 + PCI_CFG_BAR;
+	addr = pci_read_config(bdf, bar, 4);
+
+	if ((addr & 6) == PCI_BAR_64BIT) {
+		msix_table = pci_read_config(bdf, bar + 4, 4);
+		msix_table <<= 32;
+	}
+	msix_table |= addr & ~0xf;
+	msix_table += table & ~7;
+
+	/* enable and mask */
+	ctrl |= (MSIX_CTRL_ENABLE | MSIX_CTRL_FMASK);
+	pci_write_config(bdf, cap + 2, ctrl, 2);
+
+	msix_table += 16 * index;
+	mmio_write32((u32 *)((u32)msix_table), 0xfee00000 | cpu_id() << 12);
+	mmio_write32((u32 *)((u32)(msix_table + 4)), 0);
+	mmio_write32((u32 *)((u32)(msix_table + 8)), vector);
+	mmio_write32((u32 *)((u32)(msix_table + 12)), 0);
+
+	/* enable and unmask */
+	ctrl &= ~MSIX_CTRL_FMASK;
+	pci_write_config(bdf, cap + 2, ctrl, 2);
+}
+
+void pci_msi_set_vector(u16 bdf, unsigned int vector)
+{
+	int cap = pci_find_cap(bdf, PCI_CAP_MSI);
+	u16 ctl, data;
+
+	if (cap < 0)
+		return;
+
+	pci_write_config(bdf, cap + 0x04, 0xfee00000 | (cpu_id() << 12), 4);
+
+	ctl = pci_read_config(bdf, cap + 0x02, 2);
+	if (ctl & (1 << 7)) {
+		pci_write_config(bdf, cap + 0x08, 0, 4);
+		data = cap + 0x0c;
+	} else
+		data = cap + 0x08;
+	pci_write_config(bdf, data, vector, 2);
+
+	pci_write_config(bdf, cap + 0x02, 0x0001, 2);
+}
diff --git a/inmates/lib/pci.c b/inmates/lib/pci.c
index 99b57e1..e1d2d0a 100644
--- a/inmates/lib/pci.c
+++ b/inmates/lib/pci.c
@@ -12,12 +12,18 @@
 
 #include <inmate.h>
 
+// Each PCI device has 256B (1<<8) of configuration space.
+// The PCI device configuration area provided by Jailhouse is 1MiB (1<<20).
+// The maximum number of PCI device configurations is 1MiB/256B,
+// i.e. ((1 << 20) / (1 << 8)), which is (1 << (20 - 8))
+#define PCI_CFG_DEVS_MAX (1 << 12)
+
 int pci_find_device(u16 vendor, u16 device, u16 start_bdf)
 {
 	unsigned int bdf;
 	u16 id;
 
-	for (bdf = start_bdf; bdf < 0x10000; bdf++) {
+	for (bdf = start_bdf; bdf < PCI_CFG_DEVS_MAX; bdf++) {
 		id = pci_read_config(bdf, PCI_CFG_VENDOR_ID, 2);
 		if (id == PCI_ID_ANY || (vendor != PCI_ID_ANY && vendor != id))
 			continue;
