{"id":"59a71e7f-3eb6-4a38-a66f-167cc6a49359","arxiv_id":"2411.14420","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"Aggregating Funnels use one hardware fetch-and-add per thread to form batches that a delegate applies to the main variable, yielding a strongly linearizable fetch-and-add that is faster and more scalable than hardware fetch-and-add.","lead":"The paper introduces Aggregating Funnels, a software method that lets concurrent fetch-and-add operations share a single hardware instruction by grouping themselves into batches across several memory locations. It reports throughput gains of up to 4x over hardware fetch-and-add and prior combining techniques, and up to 2.5x faster concurrent queue throughput.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 3.5 depends on an unstated bound on Fetch&Add arguments; a legal 64-bit argument exceeding 2^63/p can wrap an Aggregator's value and invalidate the linearizability proof.","rationale":"The reader's weakest-assumption field identifies exactly the load-bearing issue: the proof of Invariant 3.1 assumes A.value never overflows, and that is guaranteed only under the Section 3.1.1 argument bound. I agree with that identification. The concern is real because the paper's headline claims, including the abstract's 'can be used in place of F&A in any application' and Theorem 3.5 as stated, are broader than the proven domain; the same issue also affects the experimental section, which disables the overflow-handling path. However, this is an explicitly disclosed limitation within the paper, not a hidden inconsistency: for arguments bounded by the stated threshold, the linearizability argument appears coherent, the machine-checked proof is absent but the informal proof is detailed, and the artifact is substantial. The reader's CONDITIONAL verdict is appropriate. I would not change the verdict to REJECT because the bounded-argument version of the algorithm appears correct and the performance claims use workloads where the bound is never approached. I would not change to ACCEPT because the unconditional wording of the main theorem and the drop-in claim should be revised to state the precondition, and the overflow-handling overhead should be measured before claiming it is insignificant. Thus the verdict stays CONDITIONAL.","tokens_in":21879,"tokens_out":15569,"duration_ms":165979,"concrete_test":"Instrument the artifact's implementation with the cyan overflow-handling code enabled, and run four threads on one positive Aggregator. Have each thread perform exactly one Fetch&Add(2^62+1), and insert a barrier (or equivalent synchronization) after line 22 so that all four F&A operations on A.value complete before any thread executes line 27. Check whether A.value wraps and whether the returned values respect linearizability. If the implementation instead refuses or excludes such arguments, rerun the test with arguments just below 2^63/4 to confirm the bounded-domain guarantee, and check that increasing one argument to 2^62+1 produces an observable correctness failure.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The correctness proof rests on Invariant 3.1, whose proof says: 'Since all Fetch&Add operations applied to A have positive arguments and A.value never overflows by the argument in Section 3.1.1, A.value can only increase.' Section 3.1.1 guarantees no overflow only if every argument has absolute value strictly less than 2^63/p, with p the number of threads and Threshold fixed at 2^63. This bound is stated in the algorithm description but not in Theorem 3.5, the abstract, or the contributions, which present Algorithm 1 as a strongly linearizable Fetch&Add object without input restrictions. For an ordinary 64-bit Fetch&Add interface, the restriction can be violated. For example, with p=4 and argument value 2^62+1 on the same sign aggregator, four threads can each execute line 22 before any delegate reads A.value on line 27. A.value then goes 0 -> 2^62+1 -> 2^63+2 -> 3*2^62+3 -> 2^64+4, wrapping to 4. The batch sum recorded by the delegate becomes 4 instead of 4*(2^62+1), the monotonicity used by Invariant 3.1 fails, and the linearization order plus the non-delegate result computation in lines 35-37 no longer match. The cyan retirement code cannot prevent this wrap because the wrap occurs before a delegate reads A.value. Additionally, Section 4.1 states the experiments run without the cyan overflow-handling code, so the measured speedups are for a variant whose correctness is proven only under an input restriction, and the overhead of the real code is unmeasured. This makes the abstract's claim that the implementation can replace F&A 'in any application' overbroad. The algorithm and proof appear sound for arguments satisfying the stated bound, so this is an applicability and specification concern rather than a proof error within the bounded domain.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Aggregating Funnels, a software Fetch&Add algorithm that reduces contention by spreading operations over multiple aggregator objects. Each aggregator batches concurrent operations using a single hardware F&A per operation; a delegate applies the batch sum to a main variable, and non-delegates compute their results from immutable batch metadata. The authors prove strong linearizability of the algorithm, describe a recursive variant to further reduce contention, and present experiments on a 176-thread machine showing up to 4x throughput over hardware F&A and Combining Funnels in microbenchmarks, and up to 2.5x improvement in the LCRQ concurrent queue.","tokens_in":22285,"tokens_out":14284,"duration_ms":136893,"significance":"If the correctness claims hold, this is a significant practical contribution: a simple Fetch&Add combining scheme using only Load, Store, and F&A instructions that scales better than hardware F&A, with a detailed proof of strong linearizability and a publicly available artifact. The experiments are thorough, covering multiple workloads, machines, and an application-level queue benchmark. The proof structure (Invariant 3.1, Lemmas 3.2 and 3.4, Theorem 3.5) is clear and matches the pseudocode. However, the central theorem is stated without an input restriction that the proof actually requires, and the algorithm as presented has an unbounded-memory behavior that contradicts the paper's space claim; these issues need to be addressed before the results can be accepted as stated.","major_comments":[{"comment":"Theorem 3.5 states that Algorithm 1 is a strongly linearizable implementation of a Fetch&Add object, without any restriction on arguments. However, the proof of Invariant 3.1 explicitly relies on 'A.value never overflows by the argument in Section 3.1.1', and Section 3.1.1 guarantees this only when every argument to Fetch&Add has absolute value strictly less than 2^63/p (or more generally 2^64 - p·B). This bound is not stated in the theorem, the abstract, or the contributions. The cyan overflow-handling code cannot prevent an overflow if several large arguments arrive before a delegate reads A.value on line 27; a wrap can occur before any retirement, breaking the monotonicity needed by Invariant 3.1 and the batch-identification logic of lines 35-37. The theorem and the paper's claims of a general Fetch&Add object must either state the required input bound explicitly or the overflow-handling mechanism must be redesigned.","section":"Theorem 3.5 and Section 3.1.1"},{"comment":"The space complexity claim is incorrect. The text says 'a Batch is retired as soon as it is not pointed to by an Aggregator' and concludes that at most Θ(m) Aggregator and Batch objects have not yet been retired. In Algorithm 1, each new Batch's previous pointer points to the prior a.last, and no batch is ever unlinked while its Aggregator is active. Thus every historical batch remains reachable from a.last, and no batch is retired. Because a delayed operation can traverse arbitrarily far back along the previous chain, no old batch can be safely reclaimed. The batch list grows without bound with the total number of operations, so memory usage is not Θ(m) but Θ(total operations) in the worst case. The paper's own admission that it cannot prove a worst-case memory bound conflicts with the subsequent Θ(m) claim.","section":"Section 3.1.2"},{"comment":"The experiments are run with the simpler version of Algorithm 1 without the cyan overflow-handling code. Therefore the reported speedups (e.g., up to 4x for Fetch&Add, 2.5x for LCRQ) are measured for a restricted variant whose correctness is proven only under an input assumption, and the overhead of the full algorithm is unmeasured. The statement 'We believe the overhead added by the overflow handling code should be insignificant' is not a substitute for measurement. At minimum, the paper should report whether the full algorithm was benchmarked and, if not, explicitly quantify the common-case overhead of the additional checks in lines 23-24 and the retirement path in lines 29-32.","section":"Section 4.1"}],"minor_comments":[{"comment":"There is a typo: 'throguhput' should be 'throughput'.","section":"Section 4.5"},{"comment":"The artifact checklist says 'Graphs from Section 3 as png files' but the experimental graphs are in Section 4; this should be corrected.","section":"Artifact appendix A.2"},{"comment":"The recursive construction's linearizability is asserted by replacing an atomic object with a linearizable implementation. This is plausible, but the proof of Lemmas 3.2 and 3.4 assumes that the F&A on Main on line 28 is an atomic step; when Main is itself an Aggregating Funnels instance, the linearization point of the outer batch must be shifted to the inner object's linearization point. A short argument for this composition would make the section self-contained.","section":"Section 3.2"},{"comment":"The first sentence says 'Our implementation in Section 4 uses epoch-based reclamation' but Section 4 is the experimental evaluation; this should refer to the experimental implementation presented there, not the algorithm section.","section":"Section 3.1.2"}],"recommendation":"major_revision","confidential_remarks":"The paper has a strong and elegant core idea, and the proof is largely sound under the stated input bound. The main issues are that the central theorem overstates its applicability by omitting the bound, the space claim is demonstrably false for the presented algorithm, and the full algorithm's overhead is not measured. These are fixable in revision, but they are load-bearing for the paper's claims, so I recommend major revision rather than acceptance at this stage."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a real algorithmic contribution. The aggregator trick—one F&A on a value field to register, close batches dynamically, elect a delegate by equality with the previous batch's after value, and let non-delegates compute responses from immutable batch records—is distinct from Combining Funnels' pairwise funnel layers and from Tang–Yew's k-way combining that needs Fetch&Add&Store. The recursive contention reduction is a nice bonus, though not the main result.\n\nWhat's solid: the linearizability proof (Invariant 3.1, Lemma 3.2, Invariant 3.3, Lemma 3.4, Theorem 3.5) is structurally sound and matches the pseudocode. The experimental work is thorough: multiple machines, varying workloads, and they replace F&A in LCRQ and get up to 2.5x. The artifact is substantial and publicly available. They also report batch size and fairness, not just throughput. That's good practice.\n\nSoft spots, in order of severity:\n\n1. The overflow bound is not optional. Section 3.1.1 guarantees no overflow only if every argument has absolute value < 2^63/p, with p threads. That bound is not in Theorem 3.5, the abstract, or the contributions. The stress-test example is correct: with p=4 and argument 2^62+1, four threads can F&A on the same aggregator before any delegate reads A.value, the value wraps to 4, and the monotonicity used by Invariant 3.1 breaks. So the proof is sound only for the bounded domain. The abstract's claim that the implementation can replace F&A in any application is overbroad. This is fixable: state the bound in the theorem and abstract, and note that for a general 64-bit interface the implementation must either handle overflow (the cyan code) or assume bounded inputs.\n\n2. The measured numbers are for the version without the cyan overflow-handling code. Their defense—that the overhead should be insignificant—is plausible but not measured. Since the cyan code is part of the correct algorithm for the general interface, its cost should be benchmarked or at least argued more carefully.\n\n3. Weak memory model correctness is hand-waved: \"we used the appropriate memory fences.\" Given the proof is in the standard shared-memory model, this is a gap between the proof and the implementation, but it's common in this literature and not load-bearing for the main contribution.\n\n4. m=6 is chosen as default based on the same benchmarks where it's then reported. They do show results for several m values, which mitigates this. Minor.\n\nVerdict: the central mechanism is new and appears correct under a stated bound. The paper deserves a serious referee and likely acceptance after the bound is made explicit and the overflow path is at least discussed honestly. I'd bring it to reading group and would cite it in work on combining techniques.","headline":"A genuinely new combining mechanism for fetch-and-add with a mostly sound proof, but the abstract overclaims: correctness holds only under an unstated bound on argument size, and the experiments omit the overflow-handling path.","tokens_in":22836,"tokens_out":2080,"would_cite":true,"duration_ms":19190,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Aggregating Funnels batch fetch-and-add operations across many memory locations, cutting contention and speeding up state-of-the-art queues, while remaining strongly linearizable.","keywords":["fetch-and-add","software combining","contention reduction","strong linearizability","concurrent queues","LCRQ","aggregating funnels","shared-memory algorithms"],"falsifier":"Run Algorithm 1 on hardware whose F&A wraps around modulo $2^{64}$, with $p$ threads issuing positive arguments whose sum on one Aggregator exceeds $2^{64}$ (for example, two arguments of $2^{63}$ each), and compare each operation's returned value against the sequential order of the batch's linearization at Main; any mismatch falsifies the linearizability claim.","tokens_in":21737,"feed_emoji":"⚡","tokens_out":9555,"duration_ms":86218,"temperature":0.7,"pith_summary":"The paper presents Aggregating Funnels, a software implementation of fetch-and-add that spreads contention across many memory locations instead of concentrating every operation on one hot spot. Each Fetch&Add does one hardware fetch-and-add on an Aggregator's value field; threads that land together form a batch, and only the batch's delegate performs a fetch-and-add on the main variable. The implementation is proved strongly linearizable, so it can replace hardware fetch-and-add in any concurrent algorithm that uses the primitive. Experiments show up to 4x throughput over hardware fetch-and-add and Combining Funnels at high thread counts, and replacing fetch-and-add in the LCRQ queue improves throughput up to 2.5x.","feed_headline":"Aggregating Funnels cut fetch-and-add contention by up to 4x","feed_subtitle":"Batching operations across many locations also speeds a state-of-the-art queue by up to 2.5x","key_machinery":"The load-bearing object is the Aggregator, an ancillary shared memory cell whose 64-bit value field only increases, paired with an immutable singly-linked list of Batch records. A Fetch&Add with argument $df$ does F&A($|df|$) on the Aggregator's value; the returning $aBefore$ locates the operation in a batch. The first operation in a batch, the one whose $aBefore$ equals the previous Batch's $after$, becomes delegate, reads $aAfter$, applies F&A(Main, $(aAfter-aBefore)\\cdot \\mathrm{sgn}(df)$), and appends a new Batch storing $aBefore$, $aAfter$, and $mainBefore$. Non-delegates walk the Batch list and return $mainBefore + (aBefore-batch.before)\\cdot \\mathrm{sgn}(df)$. This one-instruction registration closes the batch, selects the delegate, sums the operations, and gives every operation the data it needs to compute its result.","core_discovery":"The central discovery is that a single hardware F&A per operation, aimed at one of several Aggregator value fields, is enough to batch operations and still return every caller the value hardware F&A would have returned. An operation's F&A on the Aggregator both registers it in a batch and tells it whether it is the first (delegate) operation of that batch; the delegate reads the Aggregator's accumulated value, applies the batch's total to Main with one F&A, and appends an immutable Batch record containing the before and after values and Main's prior value. Every other operation in the batch finds its Batch record and computes its return value from the difference between its F&A result and the batch's before field. Linearizing the whole batch at the delegate's F&A on Main preserves the order in which operations hit the Aggregator, and the proof shows this order is consistent with each operation's invocation and response, hence strongly linearizable.","pith_inferences":["A testable extension is to make Aggregator choice NUMA-aware: since Algorithm 2 partitions threads into $\\sqrt{p}$ groups, a socket-local grouping could reduce cross-socket traffic on machines with multiple processors, at the possible cost of uneven batch sizes.","The overflow-bounded proof suggests that an implementation with 128-bit or wrap-safe Aggregator values, or a retry scheme for oversized arguments, would extend the linearizability guarantee to unbounded workloads; the paper only sketches the threshold parameter and the practical implementation omits the overflow path.","Because every Read in the base algorithm touches Main, a read-aggregating counterpart could reduce Main contention in read-heavy workloads; the paper's experiments show Reads dominate contention at 50% and 10% Fetch&Add mixes but no such variant is evaluated.","The Fetch&AddDirect path could be scheduled dynamically rather than reserved for fixed high-priority threads; for example, a low-priority thread that finds its Aggregator's batch list long might switch to Main and affect the latency-throughput tradeoff, an option the paper does not explore."],"forward_implications":["Because Algorithm 1 is strongly linearizable, applications that require the stronger property for randomized algorithms can replace a hardware F&A with this Fetch&Add object and preserve correctness; ordinary linearizable applications can do so as well.","At thread counts above about 30, the aggregate throughput of Fetch&Add operations is up to 4 times higher than hardware F&A and Combining Funnels, and the improvement grows with thread count on all machines tested.","Replacing the fetch-and-add objects in LCRQ raises queue throughput by up to 2.5x, showing the contention reduction remains effective inside a real data structure rather than only in microbenchmarks.","A Fetch&AddDirect operation gives selected threads a low-latency path straight to Main; in experiments one or two high-priority threads can get up to 40x the throughput of low-priority threads without reducing total throughput.","Applying the construction recursively by replacing Main with another instance reduces the worst-case contention on any memory location to $O(p^{1/(k+1)})$ after $k$ replacements, at the cost of $\\Theta(\\log p)$ accesses per operation when $k=\\log_2 p$."],"supporting_citations":[{"why":"Supplies the Combining Funnels baseline, the previous best software combining technique that Aggregating Funnels must beat.","marker":"[48]"},{"why":"Defines the fetch-and-add primitive whose semantics the implementation reproduces and whose hardware version is the main comparison point.","marker":"[22]"},{"why":"Provides the earlier k-way combining approach that used Fetch&Add&Store, which the aggregator improves on using only Load, Store, and F&A.","marker":"[52]"},{"why":"Defines strong linearizability, the correctness property Theorem 3.5 establishes for Algorithm 1.","marker":"[20]"},{"why":"Provides the standard linearizability condition that the implementation is designed to satisfy and uses as its baseline correctness notion.","marker":"[27]"},{"why":"Supplies the LCRQ concurrent queue whose fetch-and-add objects are replaced in the queue experiments.","marker":"[39]"},{"why":"Provides the recent claim and benchmark artifact showing LCRQ is the fastest concurrent queue, which the queue comparison builds on.","marker":"[45]"}],"fun_headline_variants":["Aggregating Funnels: 4x faster fetch-and-add, 2.5x faster queues","Funnels batch fetch-and-add to beat contention by 4x","Aggregating Funnels: one batch, many results, 4x throughput","Queue bottleneck gone: Aggregating Funnels 2.5x","Aggregating Funnels: fewer hot spots, faster queues"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The proof assumes every Fetch&Add argument has absolute value less than $2^{63}/p$, where $p$ is the thread count, so no Aggregator's 64-bit value can overflow; if a thread supplies a larger argument, the batch-ordering invariant and the linearizability guarantee no longer hold.","fun_headline_variants_meta":{"raw":{"variants":["Aggregating Funnels: 4x faster fetch-and-add, 2.5x faster queues","Funnels batch fetch-and-add to beat contention by 4x","Aggregating Funnels: one batch, many results, 4x throughput","Queue bottleneck gone: Aggregating Funnels 2.5x","Aggregating Funnels: fewer hot spots, faster queues"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000501,"raw_usage":{"total_tokens":2422,"prompt_tokens":892,"completion_tokens":1530,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":508,"completion_tokens_details":{"reasoning_tokens":1423}},"tokens_in":508,"tokens_out":1530,"duration_ms":10736,"temperature":1.0,"reasoning_tokens":1423,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T15:12:54.542587+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Algorithm 1 on hardware whose F&A wraps around modulo $2^{64}$, with $p$ threads issuing positive arguments whose sum on one Aggregator exceeds $2^{64}$ (for example, two arguments of $2^{63}$ each), and compare each operation's returned value against the sequential order of the batch's linearization at Main; any mismatch falsifies the linearizability claim.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the Combining Funnels baseline, the previous best software combining technique that Aggregating Funnels must beat."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the fetch-and-add primitive whose semantics the implementation reproduces and whose hardware version is the main comparison point."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the earlier k-way combining approach that used Fetch&Add&Store, which the aggregator improves on using only Load, Store, and F&A."},{"cited_title":"Herlihy and Jeannette M","cited_arxiv_id":null,"evidence_quote":"Provides the standard linearizability condition that the implementation is designed to satisfy and uses as its baseline correctness notion."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the LCRQ concurrent queue whose fetch-and-add objects are replaced in the queue experiments."}],"review_version":1}