{"id":"f87a10d0-162e-4e0c-9672-d69743cdada0","arxiv_id":"1908.04511","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"SCQ is a lock-free, linearizable, memory-efficient MPMC FIFO queue that uses fetch-and-add on hot paths and avoids livelock via a threshold counter.","lead":"SCQ is a new lock-free FIFO queue for multiple producers and consumers that scales well on many cores while using a small fixed memory buffer. The bounded version needs no allocator or reclamation scheme, which suits data pools, kernels, and CPUs without double-width compare-and-set.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The linearizability claim is delegated to CRQ, but SCQ's cycle, IsSafe, and threshold mechanisms are not covered by that proof; this is a genuine proof gap.","rationale":"I read the paper in good faith. The design is plausible: cycle bits plus IsSafe plausibly prevent ABA and the threshold plausibly breaks livelocks, and the benchmarks give independent evidence that the implementation performs. However, the strongest claim is a correctness claim, 'lock-free and linearizable', and Section 6's one-sentence delegation to CRQ is not enough. The mechanisms that make SCQ different from CRQ are exactly those that a linearizability proof would have to handle: bounded ring reuse, IsSafe, Threshold, and the failed-enqueuer retry path. The k <= n assumption that the Reader highlighted is one symptom of the same incompleteness: the lock-freedom proof relies on it, but the paper never proves that the threshold bound (or the algorithm) survives outside that regime. I did not find an obvious counterexample, so the right response is to keep the CONDITIONAL verdict and ask for either a formal proof or an exhaustive small-configuration check, not to reject or accept outright.","tokens_in":14450,"tokens_out":27068,"duration_ms":309713,"concrete_test":"Exhaustively model-check the Figure 8 algorithm for n=2 (2n=4 slots, Threshold=5) with two producers and two consumers, abstracting Cache_Remap as identity, enumerating all interleavings of the atomic operations (FAA, CAS, Load/Store, Atomic_OR). Check that every history is linearizable to a sequential FIFO queue and that no infinite execution has zero completed operations. If a violation is found, the central claim fails; if not, the issue is a proof gap rather than a demonstrated bug. Optionally rerun with three consumers to test the k <= n assumption.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 6 states that SCQ's linearizability follows from CRQ [19] because of similarity. That is the load-bearing step for the strongest claim. CRQ is proved for an unbounded array of slots with double-width CAS; SCQ is a bounded 2n-slot ring with per-slot cycles and cycle arithmetic, a separate IsSafe bit that dequeue clears and enqueue checks, an Atomic_OR consumption step, a catchup procedure, and a global Threshold used by dequeue to return empty. None of these appear in the CRQ derivation. The paper gives no linearization points for SCQ enqueue/dequeue and no invariant relating Head order to the order of completed enqueues, in particular for the case where an enqueuer FAA-reserves a slot, fails, and retries with a later Tail value, or where Threshold causes a dequeue to report empty while an enqueuer's CAS has already made an entry visible. The lock-freedom argument is likewise a sketch: it refers to line numbers from Figure 6 (Lines 14/15) while discussing Figure 8, assumes k <= n, and asserts without derivation that the threshold value 3n-1 bounds all failure paths. These may be fixable, but as written the central correctness claim is not established.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents SCQ, a bounded lock-free MPMC FIFO queue design that uses fetch-and-add (FAA) on the Head and Tail pointers, a threshold mechanism to prevent livelocks, and a bounded ring buffer with cycle arithmetic to avoid the ABA problem without double-width CAS. The design is extended to an unbounded queue (LSCQ) by chaining SCQ buffers. The paper claims that SCQ is scalable, memory-efficient, ABA-safe, does not require external memory allocators or safe memory reclamation, and is portable across architectures without double-width CAS, including PowerPC. The authors provide a correctness section with an informal proof of lock-freedom, and they benchmark SCQ against M&S, CCQUEUE, LCRQ, and WFQUEUE on x86-64 and POWER8, reporting competitive performance and much lower memory usage than LCRQ.","tokens_in":14728,"tokens_out":5334,"duration_ms":51071,"significance":"If the correctness claims hold, SCQ is a practically valuable contribution: it offers a bounded lock-free queue with FAA-based scaling and no dependency on safe memory reclamation, which is important for fixed-size data pools and for architectures lacking double-width CAS. The memory-efficiency evidence (e.g., Figure 12b) is compelling, and the portability across x86-64 and POWER8 is demonstrated by benchmarks. The paper also provides a public implementation, which supports reproducibility. However, the central correctness proof, especially the linearizability argument, is not rigorous enough to support the strongest claims, and the lock-freedom proof contains gaps that need to be addressed.","major_comments":[{"comment":"The claim that \"SCQ's linearizability follows from ... the corresponding CRQ linearizability derivations [19]\" is not supported. CRQ's proof is for an algorithm over an unbounded array of slots with double-width CAS; SCQ's bounded 2n-slot ring with cycle arithmetic, the per-slot IsSafe bit, the Atomic_OR consumption step, the catchup procedure, and the Threshold-based empty return are all absent from that earlier proof. The paper needs to give explicit linearization points for dequeue (including the Threshold-triggered empty return and the catchup path) and for enqueue (including the case where the FAA in Line 13 reserves a slot whose CAS on Line 18 fails, and the thread retries with a later Tail value), and to prove the FIFO invariant that the order of linearized enqueues matches the order of values returned by dequeues. As written, the central correctness claim is not established.","section":"Section 6 (Correctness), first paragraph"},{"comment":"The lock-freedom proof of Theorem 2 is a sketch rather than a proof. It does not account for all reasons the condition on Line 16 of Figure 8 can be false; for example, if Cycle(Ent) > Cycle(T), the enqueuer's Tail is stale, which is not covered by the two cases listed. The threshold argument in Section 5.1 is developed for the infinite-array queue of Figure 6 and then extended to SCQ with the sentence \"the threshold value should now become (n−1+2n)=3n−1\" without a derivation of the counting bound for SCQ's additional failure modes (e.g., CAS failures due to competing enqueuers, the interaction of IsSafe with Head, and the catchup path). The proof also does not handle the possibility that pending enqueuers reset Threshold at Line 21 after the threshold is depleted. A rigorous progress argument with explicit bounds on the number of failures is needed to support the lock-free claim.","section":"Section 6, Theorem 2"},{"comment":"The entire progress proof relies on the assumption k ≤ n, stated in Section 3. The paper does not discuss what happens when this assumption is violated, and the threshold value 3n−1 is derived using the bound of at most n−1 concurrent dequeuers. Since the abstract and contributions present SCQ as a general lock-free queue, the dependence on k ≤ n must be stated as a formal condition in the main theorems and highlighted as a limitation; alternatively, the authors should extend the proof beyond this bound.","section":"Section 3 (Assumptions) and Section 6 (Theorem 2)"}],"minor_comments":[{"comment":"The manuscript contains numerous typographical artifacts (e.g., \"/f_inite\", \"/f_irst\", \"/f_lexible\") that should be cleaned in the final version.","section":"Throughout"},{"comment":"The full-queue check allows Tail to run up to 3n slots ahead of Head, but no invariant is provided to justify the threshold increase from 3n−1 to 4n−1 beyond the informal statement in the text.","section":"Section 5.4, Figure 10"},{"comment":"The unbounded LSCQ extension is presented without a correctness argument; the paper should at least state which parts of the CRQ list-construction proof apply and which do not, given that SCQ cannot be finalized in the same way as CRQ.","section":"Section 5.3"}],"recommendation":"major_revision","confidential_remarks":"The main issue is the correctness proof. I would like to see a rigorous linearizability proof or a clear reduction to CRQ with explicit invariants, and a more complete lock-freedom argument. The practical contribution, especially memory efficiency and portability, is interesting and the benchmarks are useful, so I am not recommending rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"What you should know about this paper: it's a genuinely new lock-free bounded queue design with real implementations and competitive benchmarks, but the correctness proof is a handwave. The algorithm is worth your time; the proof is not.\n\nWhat's actually new: the two-queue indirection (fq/aq) with indices, the threshold mechanism that prevents livelocks, and the fact that it only needs single-width CAS. The code is on GitHub, and it runs on both x86-64 and PowerPC. The benchmarks show SCQ roughly competitive with LCRQ and WFQUEUE on balanced loads, and far more memory-efficient than LCRQ. That's a real contribution: a fixed-size queue that doesn't need an external allocator or safe memory reclamation.\n\nThe soft spot is the correctness case. Section 6 says SCQ's linearizability follows from CRQ because of similarity. That's not a proof. SCQ changes the entry format, adds a two-queue indirection, a threshold, an atomic-OR consumption step, and a catchup procedure; none of those appear in CRQ's proof. There are no linearization points for SCQ. The lock-freedom proof is a sketch with apparent line-number errors (it cites Figure 6 lines while discussing Figure 8). The threshold value 3n−1 is derived from a hand-drawn argument that is plausible but not rigorous, and the k≤n assumption is stated but its consequences are not worked out. These gaps feel fixable, but as written the central claim 'lock-free and linearizable' is not established.\n\nBenchmarks lack error bars and use different compilers for SCQP versus the others; that's a minor methodological issue, not a fatal one.\n\nBottom line: this is a systems/algorithm paper that deserves a serious referee, but the referee should require a rigorous correctness proof before publication. I'd bring it to a reading group as a case study in why 'similar to CRQ' isn't a proof.","headline":"This is a genuinely new lock-free bounded queue design with solid benchmarks, but the correctness proof is a handwave that needs to be redone.","tokens_in":15227,"tokens_out":5630,"would_cite":true,"duration_ms":49873,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper presents SCQ, a bounded lock-free MPMC FIFO queue that uses fetch-and-add on its most contended hot spots, avoids ABA problems, needs no safe memory reclamation, and is portable to any architecture with single-width CAS.","keywords":["lock-free queue","MPMC FIFO","fetch-and-add","ring buffer","ABA safety","memory efficiency","linearizability","SCQ"],"falsifier":"Set the queue capacity to n=2 and run k=3 threads in a tight loop of enqueue and dequeue with delays chosen to force one thread to be preempted mid-operation; if there is an execution in which after some finite point no thread ever completes another operation, the lock-freedom guarantee fails when k>n. Alternatively, instrument the algorithm to count consecutive failed dequeue attempts, threshold decrements, between successful enqueues: under the paper's assumptions a value above 3n−1 would contradict the livelock-prevention argument.","tokens_in":14268,"feed_emoji":"🧵","tokens_out":8391,"duration_ms":80251,"temperature":0.7,"pith_summary":"The paper tries to establish that a concurrent FIFO queue, one that many producers and many consumers can use at once, can be both lock-free and scalable without paying the usual memory costs. Its design, SCQ, is a bounded ring buffer that uses fetch-and-add (FAA) rather than compare-and-set (CAS) on the contended head and tail pointers, which makes it fast under high contention. Because it stores indices instead of pointers and recycles them through two internal queues, SCQ needs no external memory allocator and no safe memory reclamation, and it is immune to the ABA problem. If the claims hold, SCQ would be a drop-in queue for fixed-size data pools and for architectures without double-width CAS, such as PowerPC, MIPS, and RISC-V. The paper also gives an unbounded variant, LSCQ, that chains SCQ buffers together and is more memory-efficient than the prior LCRQ design.","feed_headline":"Lock-free FIFO queue cuts memory waste and needs no reclamation","feed_subtitle":"It runs on chips without double-width CAS and can serve as its own allocator for fixed-size data pools.","key_machinery":"The algorithm's central object is a circular buffer of 2n entries, each carrying a cycle number, an index into a separate data array, and a one-bit safety flag. Head and Tail are monotonically increasing counters updated by FAA, so both positions grow as position plus cycle times n; ABA is avoided because entries are matched to cycles rather than recycled pointers. A dequeuer that arrives early clears the safety bit with a CAS, or consumes the entry with an atomic OR when cycles match, and an enqueuer is allowed to write only when the slot is free, the cycle is old enough, and either the safety bit is set or Head has caught up. A Cache_Remap function spreads adjacent entries over different cache lines to reduce false sharing. The livelock barrier is a shared Threshold counter set to 3n−1 by each successful enqueue and decremented by each failed dequeue, bounding how far dequeuers can run ahead of the last inserted entry.","core_discovery":"The paper's central claim is that SCQ is a standalone, linearizable, lock-free MPMC FIFO queue that is scalable, memory-efficient, and ABA-safe while relying only on single-width atomic operations. Enqueue and dequeue advance the head and tail counters with fetch-and-add, and dequeue marks a consumed slot with an atomic OR instead of a CAS; a shared threshold counter, reset by every successful enqueue and decremented by failed dequeues, stops the livelock that made earlier FAA-based ring buffers unusable alone. Entries hold an index into a separate data array rather than a pointer, and a pair of internal queues (fq and aq) recycle those indices, which is why no memory allocator or safe memory reclamation is needed. The paper argues linearizability by analogy with CRQ and proves lock-freedom under the assumption that the number of threads k never exceeds the queue size n, then reports benchmarks on x86-64 and PowerPC showing throughput competitive with LCRQ and WFQUEUE while consuming a small fixed buffer where LCRQ can consume hundreds of megabytes.","pith_inferences":["The threshold-counter idea is a generic pattern that could be transplanted to other FAA-based ring buffers to give them operation-wise lock-freedom without a fallback queue.","The same fq/aq indirection suggests an immediate application as a lock-free object pool or slab allocator, where the queue itself performs allocation and reclamation.","A stress test at k > n would show whether the queue degrades to merely practical or loses its guarantee; nothing in the paper's proof covers that regime.","If SCQ's memory advantage holds at large scale, it may be preferable to higher-peak-throughput queues in memory-constrained and latency-critical systems."],"forward_implications":["SCQ can be used as a lock-free queue in fixed-size data pools without an external memory allocator, since it recycles its own entries through the fq/aq pair.","Architectures without double-width CAS, such as PowerPC, MIPS, SPARC, and RISC-V, can implement SCQ directly, which prior high-performance designs like LCRQ could not.","Bounded SCQ eliminates the need for hazard pointers or other safe-memory-reclamation schemes in the common case, simplifying integration into kernels and embedded systems.","The unbounded LSCQ variant chains SCQ buffers and, according to the paper, uses less memory than LCRQ because SCQ does not prematurely finalize buffers due to livelocks.","On the reported benchmarks, SCQ and SCQP match or exceed the throughput of LCRQ and WFQUEUE on x86-64 and generally outperform them on PowerPC, while keeping memory usage at roughly 512KB to 1MB."],"supporting_citations":[{"why":"Supplies the prior CRQ/LCRQ ring-buffer design that SCQ builds on, including its livelock problem and its need for double-width CAS plus an external allocator.","marker":"[19]"},{"why":"Provides the helping technique used in NCQ and serves as a key performance baseline.","marker":"[16]"},{"why":"Provides the wait-free queue baseline and the benchmark harness used in the evaluation.","marker":"[24]"},{"why":"Documents a prior FAA-based ring buffer that is not lock-free, motivating the threshold approach.","marker":"[4]"},{"why":"Hazard pointers are the safe-memory-reclamation technique that SCQ avoids.","marker":"[15]"},{"why":"The combining queue serves as a non-lock-free baseline for performance comparison.","marker":"[3]"}],"fun_headline_variants":["Lock-free FIFO queue with no reclamation uses less memory","Scalable queue avoids reclamation and shrinks memory footprint","FAA-based lock-free queue is portable and memory-efficient","Self-allocating lock-free queue cuts memory and keeps scalability","Memory-lean FIFO queue skips safe memory reclamation entirely"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the number of concurrent threads k never exceeds the queue size n (k ≤ n), because the threshold value 3n−1 that prevents livelock is derived from that bound; with more active threads than slots, dequeuers could keep invalidating slots and the lock-freedom proof no longer applies.","fun_headline_variants_meta":{"raw":{"variants":["Lock-free FIFO queue with no reclamation uses less memory","Scalable queue avoids reclamation and shrinks memory footprint","FAA-based lock-free queue is portable and memory-efficient","Self-allocating lock-free queue cuts memory and keeps scalability","Memory-lean FIFO queue skips safe memory reclamation entirely"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000587,"raw_usage":{"total_tokens":2775,"prompt_tokens":984,"completion_tokens":1791,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":600,"completion_tokens_details":{"reasoning_tokens":1706}},"tokens_in":600,"tokens_out":1791,"duration_ms":11940,"temperature":1.0,"reasoning_tokens":1706,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:40:34.640437+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Set the queue capacity to n=2 and run k=3 threads in a tight loop of enqueue and dequeue with delays chosen to force one thread to be preempted mid-operation; if there is an execution in which after some finite point no thread ever completes another operation, the lock-freedom guarantee fails when k>n. Alternatively, instrument the algorithm to count consecutive failed dequeue attempts, threshold decrements, between successful enqueues: under the paper's assumptions a value above 3n−1 would contradict the livelock-prevention argument.","supporting_citations":[{"cited_title":"Morrison and Y","cited_arxiv_id":null,"evidence_quote":"Supplies the prior CRQ/LCRQ ring-buffer design that SCQ builds on, including its livelock problem and its need for double-width CAS plus an external allocator."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the helping technique used in NCQ and serves as a key performance baseline."},{"cited_title":"Yang and J","cited_arxiv_id":null,"evidence_quote":"Provides the wait-free queue baseline and the benchmark harness used in the evaluation."},{"cited_title":"Feldman and D","cited_arxiv_id":null,"evidence_quote":"Documents a prior FAA-based ring buffer that is not lock-free, motivating the threshold approach."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Hazard pointers are the safe-memory-reclamation technique that SCQ avoids."},{"cited_title":"Fatourou and N","cited_arxiv_id":null,"evidence_quote":"The combining queue serves as a non-lock-free baseline for performance comparison."}],"review_version":1}