diff --git a/repos/os/src/drivers/gpu/intel/main.cc b/repos/os/src/drivers/gpu/intel/main.cc
index bc46e0eb72..9b2e318ae8 100644
--- a/repos/os/src/drivers/gpu/intel/main.cc
+++ b/repos/os/src/drivers/gpu/intel/main.cc
@@ -662,6 +662,12 @@ struct Igd::Device
 			/* save old tail */
 			Ring_buffer::Index const tail = el.ring_tail();
 
+			/*
+			 * IHD-OS-BDW-Vol 7-11.15 p. 18 ff.
+			 *
+			 * Pipeline synchronization
+			 */
+
 			/* prolog */
 			if (1)
 			{
@@ -768,7 +774,8 @@ struct Igd::Device
 			/* w/a */
 			if (1)
 			{
-				for (size_t i = 0; i < 2; i++) {
+				enum { CMD_NUM = 2, };
+				for (size_t i = 0; i < CMD_NUM; i++) {
 					advance += el.ring_append(0);
 				}
 			}
@@ -918,17 +925,14 @@ struct Igd::Device
 		(void)ctx_switch;
 		bool const user_complete = Mmio::GT_0_INTERRUPT_IIR::Cs_mi_user_interrupt::get(v);
 
+		if (v) { _clear_rcs_iir(v); }
+
 		Vgpu *notify_gpu = nullptr;
 		if (user_complete) { notify_gpu = _current_vgpu(); }
 
-		if (v) { _clear_rcs_iir(v); }
-
 		bool const fault_valid = _mmio->fault_regs_valid();
 		if (fault_valid) { Genode::error("FAULT_REG valid"); }
 
-		bool const csb = _mmio->csb_unread();
-		(void)csb;
-
 		_mmio->update_context_status_pointer();
 
 		if (user_complete) {
@@ -1089,6 +1093,7 @@ struct Igd::Device
 		_irq->ack_irq();
 
 		_mmio->dump();
+		_mmio->context_status_pointer_dump();
 
 		_timer.sigh(_watchdog_timeout_sigh);
 	}
@@ -1535,7 +1540,8 @@ class Gpu::Session_component : public Genode::Session_object<Gpu::Session>
 		{
 			if (!cap.valid()) { return false; }
 
-			bool result = false;
+			enum { ALLOC_FAILED, MAP_FAILED, OK } result = ALLOC_FAILED;
+
 			auto lookup_and_map = [&] (Buffer &buffer) {
 				if (!(buffer.cap == cap)) { return; }
 
@@ -1552,10 +1558,11 @@ class Gpu::Session_component : public Genode::Session_object<Gpu::Session>
 					_vgpu.rcs_map_ppgtt(va, phys_addr, actual_size);
 					buffer.ppgtt_va = va;
 					buffer.ppgtt_va_valid = true;
-					result = true;
+					result = OK;
 				} catch (Igd::Device::Could_not_map_buffer) {
 					/* FIXME do not result in Out_of_ram */
 					Genode::error("could not map buffer object into PPGTT");
+					result = MAP_FAILED;
 					return;
 				}
 				/* will throw below */
@@ -1563,9 +1570,14 @@ class Gpu::Session_component : public Genode::Session_object<Gpu::Session>
 			};
 			_buffer_registry.for_each(lookup_and_map);
 
-			if (!result) { throw Gpu::Session::Out_of_ram(); }
-
-			return result;
+			switch (result) {
+			case ALLOC_FAILED:
+				throw Gpu::Session::Out_of_ram();
+			case OK:
+				return true;
+			default:
+				return false;
+			}
 		}
 
 		void unmap_buffer_ppgtt(Genode::Dataspace_capability cap,
diff --git a/repos/os/src/drivers/gpu/intel/mmio.h b/repos/os/src/drivers/gpu/intel/mmio.h
index 7d48da97b7..7635d8a041 100644
--- a/repos/os/src/drivers/gpu/intel/mmio.h
+++ b/repos/os/src/drivers/gpu/intel/mmio.h
@@ -795,21 +795,11 @@ class Igd::Mmio : public Genode::Mmio
 		 * IHD-OS-BDW-Vol 6-11.15 p. 19 ff.
 		 */
 		enum {
-			CTXT_ST_BUF_QW_NUM = 8,
 			CTXT_ST_BUF_NUM    = 6,
+			CTXT_ST_BUF_DWORDS = 12,
 		};
 		template <long int BASE>
-		struct CTXT_ST_BUF_BASE : Register_array<BASE + 0x370, 64, CTXT_ST_BUF_NUM, 64>
-		{
-			using B = Register_array<BASE + 0x370, 64, CTXT_ST_BUF_NUM, 64>;
-
-			/*
-			 * Judging by the documentation it seems that one context status
-			 * buffer in fact contains the same DWORD twice.
-			 */
-			struct Context_status_udw : B::template Bitfield<32, 32> { };
-			struct Context_status_ldw : B::template Bitfield< 0, 32> { };
-		};
+		struct CTXT_ST_BUF_BASE : Register_array<BASE + 0x370, 32, CTXT_ST_BUF_DWORDS, 32> { };
 
 		struct CTXT_ST_BUF_RCSUNIT : CTXT_ST_BUF_BASE<0x2000> { };
 
@@ -1233,15 +1223,6 @@ class Igd::Mmio : public Genode::Mmio
 			write<RCS_RING_CONTEXT_STATUS_PTR>(v);
 		}
 
-		bool csb_unread()
-		{
-			RCS_RING_CONTEXT_STATUS_PTR::access_t const r = read<RCS_RING_CONTEXT_STATUS_PTR::Read_pointer>();
-			RCS_RING_CONTEXT_STATUS_PTR::access_t const w = read<RCS_RING_CONTEXT_STATUS_PTR::Write_pointer>();
-
-			return (r != w) && (r + 1) % CTXT_ST_BUF_NUM <= w; /* XXX */
-		}
-
-
 		uint32_t find_free_fence()
 		{
 			uint32_t id = 0xff;
diff --git a/repos/os/src/drivers/gpu/intel/mmio_dump.cc b/repos/os/src/drivers/gpu/intel/mmio_dump.cc
index c13dc6d740..f470a0fbcf 100644
--- a/repos/os/src/drivers/gpu/intel/mmio_dump.cc
+++ b/repos/os/src/drivers/gpu/intel/mmio_dump.cc
@@ -305,16 +305,20 @@ void Igd::Mmio::context_status_pointer_dump()
 
 	uint32_t r = rp;
 	uint32_t w = wp;
-	if (r > w) { w += CTXT_ST_BUF_NUM; }
-	while (r < w) {
-		uint32_t const i = ++r % CTXT_ST_BUF_NUM;
 
-		uint64_t const cs  = read<CTXT_ST_BUF_RCSUNIT>(i);
-		uint32_t const csu = read<CTXT_ST_BUF_RCSUNIT::Context_status_udw>(i);
-		uint32_t const csl = read<CTXT_ST_BUF_RCSUNIT::Context_status_ldw>(i);
+	while (r != w) {
+
+		if (++r == CTXT_ST_BUF_NUM) { r = 0; }
+
+		uint32_t const i = r;
+
+		uint32_t const csu = read<CTXT_ST_BUF_RCSUNIT>(i*2+1);
+		uint32_t const csl = read<CTXT_ST_BUF_RCSUNIT>(i*2);
+		uint64_t const cs  = ((uint64_t)csu << 32) | csl;
+
 		log(i, "  Context_status:     ", Hex(cs));
 
-		Igd::Context_status_qword::access_t const v = csl;
+		Igd::Context_status_qword::access_t const v = cs;
 		log(i, "    Context_complete:  ", Igd::Context_status_qword::Context_complete::get(v));
 		log(i, "    Active_to_idle:    ", Igd::Context_status_qword::Active_to_idle::get(v));
 		log(i, "    Element_switch:    ", Igd::Context_status_qword::Element_switch::get(v));
diff --git a/repos/os/src/drivers/gpu/intel/utils.h b/repos/os/src/drivers/gpu/intel/utils.h
index eeb87b5ad5..4547be33b4 100644
--- a/repos/os/src/drivers/gpu/intel/utils.h
+++ b/repos/os/src/drivers/gpu/intel/utils.h
@@ -35,7 +35,7 @@ namespace Utils {
 
 	template <unsigned int ELEMENTS> class Address_map;
 
-	void clflush(volatile void *addr)
+	inline void clflush(volatile void *addr)
 	{
 		asm volatile("clflush %0" : "+m" (*(volatile char *)addr));
 	}