diff --git a/tools/memory-model/litmus-tests/mpsc-rb+1p1c+bounded.litmus b/tools/memory-model/litmus-tests/mpsc-rb+1p1c+bounded.litmus
new file mode 100644
index 000000000000..cafd17afe11e
--- /dev/null
+++ b/tools/memory-model/litmus-tests/mpsc-rb+1p1c+bounded.litmus
@@ -0,0 +1,92 @@
+C mpsc-rb+1p1c+bounded
+
+(*
+ * Result: Always
+ *
+ * This litmus test validates BPF ring buffer implementation under the
+ * following assumptions:
+ * - 1 producer;
+ * - 1 consumer;
+ * - ring buffer has capacity for only 1 record.
+ *
+ * Expectations:
+ * - 1 record pushed into ring buffer;
+ * - 0 or 1 element is consumed.
+ * - no failures.
+ *)
+
+{
+	max_len = 1;
+	len1 = 0;
+	px = 0;
+	cx = 0;
+	dropped = 0;
+}
+
+P0(int *len1, int *cx, int *px)
+{
+	int *rLenPtr;
+	int rLen;
+	int rPx;
+	int rCx;
+	int rFail;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	rPx = smp_load_acquire(px);
+	if (rCx < rPx) {
+		if (rCx == 0)
+			rLenPtr = len1;
+		else
+			rFail = 1;
+
+		rLen = smp_load_acquire(rLenPtr);
+		if (rLen == 0) {
+			rFail = 1;
+		} else if (rLen == 1) {
+			rCx = rCx + 1;
+			smp_store_release(cx, rCx);
+		}
+	}
+}
+
+P1(int *len1, spinlock_t *rb_lock, int *px, int *cx, int *dropped, int *max_len)
+{
+	int rPx;
+	int rCx;
+	int rFail;
+	int *rLenPtr;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	spin_lock(rb_lock);
+
+	rPx = *px;
+	if (rPx - rCx >= *max_len) {
+		atomic_inc(dropped);
+		spin_unlock(rb_lock);
+	} else {
+		if (rPx == 0)
+			rLenPtr = len1;
+		else
+			rFail = 1;
+
+		*rLenPtr = -1;
+		smp_wmb();
+		smp_store_release(px, rPx + 1);
+
+		spin_unlock(rb_lock);
+
+		smp_store_release(rLenPtr, 1);
+	}
+}
+
+exists (
+	0:rFail=0 /\ 1:rFail=0
+	/\
+	(
+		(dropped=0 /\ px=1 /\ len1=1 /\ (cx=0 \/ cx=1))
+	)
+)
diff --git a/tools/memory-model/litmus-tests/mpsc-rb+1p1c+unbound.litmus b/tools/memory-model/litmus-tests/mpsc-rb+1p1c+unbound.litmus
new file mode 100644
index 000000000000..84f660598015
--- /dev/null
+++ b/tools/memory-model/litmus-tests/mpsc-rb+1p1c+unbound.litmus
@@ -0,0 +1,83 @@
+C mpsc-rb+1p1c+unbound
+
+(*
+ * Result: Always
+ *
+ * This litmus test validates BPF ring buffer implementation under the
+ * following assumptions:
+ * - 1 producer;
+ * - 1 consumer;
+ * - ring buffer capacity is unbounded.
+ *
+ * Expectations:
+ * - 1 record pushed into ring buffer;
+ * - 0 or 1 element is consumed.
+ * - no failures.
+ *)
+
+{
+	len1 = 0;
+	px = 0;
+	cx = 0;
+}
+
+P0(int *len1, int *cx, int *px)
+{
+	int *rLenPtr;
+	int rLen;
+	int rPx;
+	int rCx;
+	int rFail;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	rPx = smp_load_acquire(px);
+	if (rCx < rPx) {
+		if (rCx == 0)
+			rLenPtr = len1;
+		else
+			rFail = 1;
+
+		rLen = smp_load_acquire(rLenPtr);
+		if (rLen == 0) {
+			rFail = 1;
+		} else if (rLen == 1) {
+			rCx = rCx + 1;
+			smp_store_release(cx, rCx);
+		}
+	}
+}
+
+P1(int *len1, spinlock_t *rb_lock, int *px, int *cx)
+{
+	int rPx;
+	int rCx;
+	int rFail;
+	int *rLenPtr;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	spin_lock(rb_lock);
+
+	rPx = *px;
+	if (rPx == 0)
+		rLenPtr = len1;
+	else
+		rFail = 1;
+
+	*rLenPtr = -1;
+	smp_wmb();
+	smp_store_release(px, rPx + 1);
+
+	spin_unlock(rb_lock);
+
+	smp_store_release(rLenPtr, 1);
+}
+
+exists (
+	0:rFail=0 /\ 1:rFail=0
+	/\ px=1 /\ len1=1
+	/\ (cx=0 \/ cx=1)
+)
diff --git a/tools/memory-model/litmus-tests/mpsc-rb+2p1c+bounded.litmus b/tools/memory-model/litmus-tests/mpsc-rb+2p1c+bounded.litmus
new file mode 100644
index 000000000000..900104c4933b
--- /dev/null
+++ b/tools/memory-model/litmus-tests/mpsc-rb+2p1c+bounded.litmus
@@ -0,0 +1,152 @@
+C mpsc-rb+2p1c+bounded
+
+(*
+ * Result: Always
+ *
+ * This litmus test validates BPF ring buffer implementation under the
+ * following assumptions:
+ * - 2 identical producers;
+ * - 1 consumer;
+ * - ring buffer has capacity for only 1 record.
+ *
+ * Expectations:
+ * - either 1 or 2 records are pushed into ring buffer;
+ * - 0, 1, or 2 elements are consumed by consumer;
+ * - appropriate number of dropped records is recorded to satisfy ring buffer
+ *   size bounds;
+ * - no failures.
+ *)
+
+{
+	max_len = 1;
+	len1 = 0;
+	px = 0;
+	cx = 0;
+	dropped = 0;
+}
+
+P0(int *len1, int *cx, int *px)
+{
+	int *rLenPtr;
+	int rLen;
+	int rPx;
+	int rCx;
+	int rFail;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	rPx = smp_load_acquire(px);
+	if (rCx < rPx) {
+		if (rCx == 0)
+			rLenPtr = len1;
+		else if (rCx == 1)
+			rLenPtr = len1;
+		else
+			rFail = 1;
+
+		rLen = smp_load_acquire(rLenPtr);
+		if (rLen == 0) {
+			rFail = 1;
+		} else if (rLen == 1) {
+			rCx = rCx + 1;
+			smp_store_release(cx, rCx);
+		}
+	}
+
+	rPx = smp_load_acquire(px);
+	if (rCx < rPx) {
+		if (rCx == 0)
+			rLenPtr = len1;
+		else if (rCx == 1)
+			rLenPtr = len1;
+		else
+			rFail = 1;
+
+		rLen = smp_load_acquire(rLenPtr);
+		if (rLen == 0) {
+			rFail = 1;
+		} else if (rLen == 1) {
+			rCx = rCx + 1;
+			smp_store_release(cx, rCx);
+		}
+	}
+}
+
+P1(int *len1, spinlock_t *rb_lock, int *px, int *cx, int *dropped, int *max_len)
+{
+	int rPx;
+	int rCx;
+	int rFail;
+	int *rLenPtr;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	spin_lock(rb_lock);
+
+	rPx = *px;
+	if (rPx - rCx >= *max_len) {
+		atomic_inc(dropped);
+		spin_unlock(rb_lock);
+	} else {
+		if (rPx == 0)
+			rLenPtr = len1;
+		else if (rPx == 1)
+			rLenPtr = len1;
+		else
+			rFail = 1;
+
+		*rLenPtr = -1;
+		smp_wmb();
+		smp_store_release(px, rPx + 1);
+
+		spin_unlock(rb_lock);
+
+		smp_store_release(rLenPtr, 1);
+	}
+}
+
+P2(int *len1, spinlock_t *rb_lock, int *px, int *cx, int *dropped, int *max_len)
+{
+	int rPx;
+	int rCx;
+	int rFail;
+	int *rLenPtr;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	spin_lock(rb_lock);
+
+	rPx = *px;
+	if (rPx - rCx >= *max_len) {
+		atomic_inc(dropped);
+		spin_unlock(rb_lock);
+	} else {
+		if (rPx == 0)
+			rLenPtr = len1;
+		else if (rPx == 1)
+			rLenPtr = len1;
+		else
+			rFail = 1;
+
+		*rLenPtr = -1;
+		smp_wmb();
+		smp_store_release(px, rPx + 1);
+
+		spin_unlock(rb_lock);
+
+		smp_store_release(rLenPtr, 1);
+	}
+}
+
+exists (
+	0:rFail=0 /\ 1:rFail=0 /\ 2:rFail=0 /\ len1=1
+	/\
+	(
+		(dropped = 0 /\ px=2 /\ (cx=1 \/ cx=2))
+		\/
+		(dropped = 1 /\ px=1 /\ (cx=0 \/ cx=1))
+	)
+)
diff --git a/tools/memory-model/litmus-tests/mpsc-rb+2p1c+unbound.litmus b/tools/memory-model/litmus-tests/mpsc-rb+2p1c+unbound.litmus
new file mode 100644
index 000000000000..83372e9eb079
--- /dev/null
+++ b/tools/memory-model/litmus-tests/mpsc-rb+2p1c+unbound.litmus
@@ -0,0 +1,137 @@
+C mpsc-rb+2p1c+unbound
+
+(*
+ * Result: Always
+ *
+ * This litmus test validates BPF ring buffer implementation under the
+ * following assumptions:
+ * - 2 identical producers;
+ * - 1 consumer;
+ * - ring buffer capacity is unbounded.
+ *
+ * Expectations:
+ * - 2 records pushed into ring buffer;
+ * - 0, 1, or 2 elements are consumed.
+ * - no failures.
+ *)
+
+{
+	len1 = 0;
+	len2 = 0;
+	px = 0;
+	cx = 0;
+}
+
+P0(int *len1, int *len2, int *cx, int *px)
+{
+	int *rLenPtr;
+	int rLen;
+	int rPx;
+	int rCx;
+	int rFail;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	rPx = smp_load_acquire(px);
+	if (rCx < rPx) {
+		if (rCx == 0)
+			rLenPtr = len1;
+		else if (rCx == 1)
+			rLenPtr = len2;
+		else
+			rFail = 1;
+
+		rLen = smp_load_acquire(rLenPtr);
+		if (rLen == 0) {
+			rFail = 1;
+		} else if (rLen == 1) {
+			rCx = rCx + 1;
+			smp_store_release(cx, rCx);
+		}
+	}
+
+	rPx = smp_load_acquire(px);
+	if (rCx < rPx) {
+		if (rCx == 0)
+			rLenPtr = len1;
+		else if (rCx == 1)
+			rLenPtr = len2;
+		else
+			rFail = 1;
+
+		rLen = smp_load_acquire(rLenPtr);
+		if (rLen == 0) {
+			rFail = 1;
+		} else if (rLen == 1) {
+			rCx = rCx + 1;
+			smp_store_release(cx, rCx);
+		}
+	}
+}
+
+P1(int *len1, int *len2, spinlock_t *rb_lock, int *px, int *cx)
+{
+	int rPx;
+	int rCx;
+	int rFail;
+	int *rLenPtr;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	spin_lock(rb_lock);
+
+	rPx = *px;
+	if (rPx == 0)
+		rLenPtr = len1;
+	else if (rPx == 1)
+		rLenPtr = len2;
+	else
+		rFail = 1;
+
+	*rLenPtr = -1;
+	smp_wmb();
+	smp_store_release(px, rPx + 1);
+
+	spin_unlock(rb_lock);
+
+	smp_store_release(rLenPtr, 1);
+}
+
+P2(int *len1, int *len2, spinlock_t *rb_lock, int *px, int *cx)
+{
+	int rPx;
+	int rCx;
+	int rFail;
+	int *rLenPtr;
+
+	rFail = 0;
+	rCx = smp_load_acquire(cx);
+
+	spin_lock(rb_lock);
+
+	rPx = *px;
+	if (rPx == 0)
+		rLenPtr = len1;
+	else if (rPx == 1)
+		rLenPtr = len2;
+	else
+		rFail = 1;
+
+	*rLenPtr = -1;
+	smp_wmb();
+	smp_store_release(px, rPx + 1);
+
+	spin_unlock(rb_lock);
+
+	smp_store_release(rLenPtr, 1);
+}
+
+exists (
+	0:rFail=0 /\ 1:rFail=0 /\ 2:rFail=0
+	/\
+	px=2 /\ len1=1 /\ len2=1
+	/\
+	(cx=0 \/ cx=1 \/ cx=2)
+)
