Module Name: src
Committed By: riastradh
Date: Thu Feb 23 03:03:45 UTC 2023
Modified Files:
src/sys/kern: subr_pcq.c
Log Message:
pcq(9): Sketch correctness proof for some critical properties.
No functional change intended.
To generate a diff of this commit:
cvs rdiff -u -r1.17 -r1.18 src/sys/kern/subr_pcq.c
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Modified files:
Index: src/sys/kern/subr_pcq.c
diff -u src/sys/kern/subr_pcq.c:1.17 src/sys/kern/subr_pcq.c:1.18
--- src/sys/kern/subr_pcq.c:1.17 Thu Feb 23 03:01:49 2023
+++ src/sys/kern/subr_pcq.c Thu Feb 23 03:03:45 2023
@@ -1,4 +1,4 @@
-/* $NetBSD: subr_pcq.c,v 1.17 2023/02/23 03:01:49 riastradh Exp $ */
+/* $NetBSD: subr_pcq.c,v 1.18 2023/02/23 03:03:45 riastradh Exp $ */
/*-
* Copyright (c) 2009, 2019 The NetBSD Foundation, Inc.
@@ -31,10 +31,94 @@
/*
* Lockless producer/consumer queue.
+ *
+ * Summary of the producer algorithm in pcq_put (may run many in
+ * parallel with each other and with a consumer):
+ *
+ * P1. initialize an item
+ *
+ * P2. atomic_cas(&pcq->pcq_pc) loop to advance the producer
+ * pointer, reserving a space at c (fails if not enough space)
+ *
+ * P3. atomic_store_release(&pcq->pcq_items[c], item) to publish
+ * the item in the space it reserved
+ *
+ * Summary of the consumer algorithm in pcq_get (must be serialized by
+ * caller with other consumers, may run in parallel with any number of
+ * producers):
+ *
+ * C1. atomic_load_relaxed(&pcq->pcq_pc) to get the consumer
+ * pointer and a snapshot of the producer pointer, which may
+ * point to null items or point to initialized items (fails if
+ * no space reserved for published items yet)
+ *
+ * C2. atomic_load_consume(&pcq->pcq_items[c]) to get the next
+ * unconsumed but potentially published item (fails if item
+ * not published yet)
+ *
+ * C3. pcq->pcq_items[c] = NULL to consume the next unconsumed but
+ * published item
+ *
+ * C4. membar_producer
+ *
+ * C5. atomic_cas(&pcq->pcq_pc) loop to advance the consumer
+ * pointer
+ *
+ * C6. use the item
+ *
+ * Note that there is a weird bare membar_producer which is not matched
+ * by membar_consumer. This is one of the rare cases of a memory
+ * barrier on one side that is not matched by a memory barrier on
+ * another side, but the ordering works out, with a somewhat more
+ * involved proof.
+ *
+ * Some properties that need to be proved:
+ *
+ * Theorem 1. For pcq_put call that leads into pcq_get:
+ * Initializing item at P1 is dependency-ordered before usage of
+ * item at C6, so items placed by pcq_put can be safely used by
+ * the caller of pcq_get.
+ *
+ * Proof sketch.
+ *
+ * Assume load/store P2 synchronizes with load/store C1
+ * (if not, pcq_get fails in `if (p == c) return NULL').
+ *
+ * Assume store-release P3 synchronizes with load-consume
+ * C2 (if not, pcq_get fails in `if (item == NULL) return
+ * NULL').
+ *
+ * Then:
+ *
+ * - P1 is sequenced before store-release P3
+ * - store-release P3 synchronizes with load-consume C2
+ * - load-consume C2 is dependency-ordered before C6
+ *
+ * Hence transitively, P1 is dependency-ordered before C6,
+ * QED.
+ *
+ * Theorem 2. For pcq_get call followed by pcq_put: Nulling out
+ * location at store C3 happens before placing a new item in the
+ * same location at store P3, so items are not lost.
+ *
+ * Proof sketch.
+ *
+ * Assume load/store C5 synchronizes with load/store P2
+ * (otherwise pcq_peek starts over the CAS loop or fails).
+ *
+ * Then:
+ *
+ * - store C3 is sequenced before membar_producer C4
+ * - membar_producer C4 is sequenced before load/store C5
+ * - load/store C5 synchronizes with load/store P2 at &pcq->pcq_pc
+ * - P2 is sequenced before store-release P3
+ *
+ * Hence transitively, store C3 happens before
+ * store-release P3, QED.
*/
#include <sys/cdefs.h>
-__KERNEL_RCSID(0, "$NetBSD: subr_pcq.c,v 1.17 2023/02/23 03:01:49 riastradh Exp $");
+__KERNEL_RCSID(0, "$NetBSD: subr_pcq.c,v 1.18 2023/02/23 03:03:45 riastradh Exp $");
#include <sys/param.h>
#include <sys/types.h>
@@ -186,7 +270,8 @@ pcq_get(pcq_t *pcq)
* because the only load we need to ensure happens first is the
* load of pcq->pcq_items[c], but that necessarily happens
* before the store to pcq->pcq_items[c] to null it out because
- * it is at the same memory location.
+ * it is at the same memory location. Yes, this is a bare
+ * membar_producer with no matching membar_consumer.
*/
#ifndef __HAVE_ATOMIC_AS_MEMBAR
membar_producer();
