Verify Linearizability of Concurrent Stacks
- URL: http://arxiv.org/abs/2110.05801v3
- Date: Mon, 15 Sep 2025 08:26:10 GMT
- Title: Verify Linearizability of Concurrent Stacks
- Authors: Tangliu Wen,
- Abstract summary: We propose a new proof technique for verifying linearizability of concurrent stacks.<n>We first prove the soundness of the elimination mechanism, a common optimization used in concurrent stacks.<n>We then present a stack theorem that reduces the problem of proving linearizability to establishing a set of conditions.
- Score: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Proving linearizability of concurrent data structures is crucial for ensuring their correctness, but is challenging especially for implementations that employ sophisticated synchronization techniques. In this paper, we propose a new proof technique for verifying linearizability of concurrent stacks. We first prove the soundness of the elimination mechanism, a common optimization used in concurrent stacks, which enables simplifying the linearizability proofs. We then present a stack theorem that reduces the problem of proving linearizability to establishing a set of conditions based on the happened-before order of operations. The key idea is to use an extended partial order to capture when a pop operation can observe the effect of a push operation. We apply our proof technique to verify two concurrent stack algorithms: the Treiber stack and the Time-Stamped stack, demonstrating its practicality. Our approach provides a systematic and compositional way to prove linearizability of concurrent stacks.
Related papers
- FlashEvaluator: Expanding Search Space with Parallel Evaluation [27.839033452409428]
We propose FlashEvaluator, which enables cross-sequence token information sharing and processes all sequences in a single forward pass.<n>This yields sublinear computational complexity that improves the system's efficiency and supports direct inter-sequence comparisons.<n>FlashEvaluator has been deployed in online recommender system of Kuaishou, delivering substantial and sustained revenue gains in practice.
arXiv Detail & Related papers (2026-03-03T03:35:34Z) - PRISM: Parallel Residual Iterative Sequence Model [52.26239951489612]
We propose PRISM (Parallel Residual Iterative Sequence Model) to resolve this tension.<n>PRISM introduces a solver-inspired inductive bias that captures key structural properties of multi-step refinement in a parallelizable form.<n>We prove that this formulation achieves Rank-$L$ accumulation, structurally expanding the update manifold beyond the single-step Rank-$1$ bottleneck.
arXiv Detail & Related papers (2026-02-11T12:39:41Z) - Fractional Reasoning via Latent Steering Vectors Improves Inference Time Compute [60.151643048803145]
We propose Fractional Reasoning, a framework that enables continuous control over reasoning intensity at inference time.<n>Our method operates by extracting the latent steering vector associated with deeper reasoning and reapplying it with a tunable scaling factor.<n> Experiments on GSM8K, MATH500, and GPQA demonstrate that Fractional Reasoning consistently improves performance across diverse reasoning tasks and models.
arXiv Detail & Related papers (2025-06-18T21:15:59Z) - Scaling Probabilistic Circuits via Monarch Matrices [109.65822339230853]
Probabilistic Circuits (PCs) are tractable representations of probability distributions.<n>We propose a novel sparse and structured parameterization for the sum blocks in PCs.
arXiv Detail & Related papers (2025-06-14T07:39:15Z) - Reasoning by Superposition: A Theoretical Perspective on Chain of Continuous Thought [56.71873693264532]
We prove that a two-layer transformer with $D$ steps of continuous CoTs can solve the directed graph reachability problem.<n>In our construction, each continuous thought vector is a superposition state that encodes multiple search frontiers simultaneously.
arXiv Detail & Related papers (2025-05-18T18:36:53Z) - Test-time Correlation Alignment [2.389598109913754]
Test-Time Adaptation (TTA) adapts using only unlabeled test data.<n>Test-time Correlation Alignment (TCA) can enhance test performances with a theoretical guarantee.<n> LinearTCA applies a simple linear transformation to achieve both instance and correlation alignment without additional model updates.<n> LinearTCA+ serves as a plug-and-play module that can easily boost existing TTA methods.
arXiv Detail & Related papers (2025-05-01T13:59:13Z) - Towards Transformer-Based Aligned Generation with Self-Coherence Guidance [51.42269790543461]
We introduce a training-free approach for enhancing alignment in Transformer-based Text-Guided Diffusion Models (TGDMs)<n>Existing TGDMs often struggle to generate semantically aligned images, particularly when dealing with complex text prompts or multi-concept attribute binding challenges.<n>Our method addresses these challenges by directly optimizing cross-attention maps during the generation process.
arXiv Detail & Related papers (2025-03-22T07:03:57Z) - MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
MathGAP generates problem statements and chain-of-thought reasoning traces according to specifications about their arithmetic proof structure.
Using MathGAP, we find that LLMs show a significant decrease in performance as proofs get deeper and wider.
arXiv Detail & Related papers (2024-10-17T12:48:14Z) - TSVD: Bridging Theory and Practice in Continual Learning with Pre-trained Models [103.45785408116146]
Continual learning (CL) aims to train a model that can solve multiple tasks presented sequentially.
Recent CL approaches have achieved strong performance by leveraging large pre-trained models that generalize well to downstream tasks.
However, such methods lack theoretical guarantees, making them prone to unexpected failures.
We aim to bridge this gap by designing a simple CL method that is theoretically sound and highly performant.
arXiv Detail & Related papers (2024-10-01T12:58:37Z) - Simple Ingredients for Offline Reinforcement Learning [86.1988266277766]
offline reinforcement learning algorithms have proven effective on datasets highly connected to the target downstream task.
We show that existing methods struggle with diverse data: their performance considerably deteriorates as data collected for related but different tasks is simply added to the offline buffer.
We show that scale, more than algorithmic considerations, is the key factor influencing performance.
arXiv Detail & Related papers (2024-03-19T18:57:53Z) - Stable Nonconvex-Nonconcave Training via Linear Interpolation [51.668052890249726]
This paper presents a theoretical analysis of linearahead as a principled method for stabilizing (large-scale) neural network training.
We argue that instabilities in the optimization process are often caused by the nonmonotonicity of the loss landscape and show how linear can help by leveraging the theory of nonexpansive operators.
arXiv Detail & Related papers (2023-10-20T12:45:12Z) - Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
We discuss the problem of bounding partially identifiable queries, such as counterfactuals, in Pearlian structural causal models.
A recently proposed iterated EM scheme yields an inner approximation of those bounds by sampling the initialisation parameters.
We show how a single symbolic knowledge compilation allows us to obtain the circuit structure with symbolic parameters to be replaced by their actual values.
arXiv Detail & Related papers (2023-10-05T07:10:40Z) - Range-Restricted Interpolation through Clausal Tableaux [0.0]
We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig in first-order logic.
The proof system is clausal tableaux, which stems from first-order ATP.
arXiv Detail & Related papers (2023-06-06T10:42:40Z) - Forward LTLf Synthesis: DPLL At Work [1.370633147306388]
We propose a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (LTLf)
Within such framework, we devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves.
We also propose a novel equivalence check for search nodes based on syntactic equivalence of state formulas.
arXiv Detail & Related papers (2023-02-27T14:33:50Z) - On the Robustness of Randomized Ensembles to Adversarial Perturbations [12.082239973914326]
Randomized ensemble classifiers (RECs) have emerged as an attractive alternative to traditional ensembling methods.
Recent works have shown that existing methods for constructing RECs are more vulnerable than initially claimed.
We propose a new boosting algorithm (BARRE) for training robust RECs, and empirically demonstrate its effectiveness at defending against strong $ell_infty$ norm-bounded adversaries.
arXiv Detail & Related papers (2023-02-02T19:17:34Z) - CD Tools -- Condensed Detachment and Structure Generating Theorem
Proving (System Description) [0.0]
CD Tools is a Prolog library for experimenting with condensed detachment in first-order ATP.
From the viewpoint of first-order ATP, condensed detachment offers a setting that is relatively simple but with essential features and serious applications.
For a historic problem often studied in ATP it produced a new proof that is much shorter than any known one.
arXiv Detail & Related papers (2022-07-18T09:15:08Z) - Don't Explain Noise: Robust Counterfactuals for Randomized Ensembles [50.81061839052459]
We formalize the generation of robust counterfactual explanations as a probabilistic problem.
We show the link between the robustness of ensemble models and the robustness of base learners.
Our method achieves high robustness with only a small increase in the distance from counterfactual explanations to their initial observations.
arXiv Detail & Related papers (2022-05-27T17:28:54Z) - Recursive Causal Structure Learning in the Presence of Latent Variables
and Selection Bias [27.06618125828978]
We consider the problem of learning the causal MAG of a system from observational data in the presence of latent variables and selection bias.
We propose a novel computationally efficient constraint-based method that is sound and complete.
We provide experimental results to compare the proposed approach with the state of the art on both synthetic and real-world structures.
arXiv Detail & Related papers (2021-10-22T19:49:59Z) - Online Matching in Sparse Random Graphs: Non-Asymptotic Performances of
Greedy Algorithm [20.582965700659788]
We estimate the competitive ratio of the simplest algorithm, GREEDY, by approximating some relevant discrete processes by their continuous counterparts.
We prove that, quite surprisingly, GREEDY can have better performance guarantees than RANKING, another celebrated algorithm for online matching.
arXiv Detail & Related papers (2021-07-02T12:18:19Z) - An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
We introduce a divide-and-conquer based diagnosis algorithm (FastDiag) which identifies minimal sets of faulty constraints in an over-constrained problem.
We compare FastDiag with the conflict-directed calculation of hitting sets and present an in-depth performance analysis.
arXiv Detail & Related papers (2021-02-17T19:55:42Z) - Efficient Generation of Structured Objects with Constrained Adversarial
Networks [25.74932947671932]
Generative Adversarial Networks (GANs) struggle to generate structured objects like molecules and game maps.
We propose Constrained Adversarial Networks (CANs), an extension of GANs in which the constraints are embedded into the model during training.
CANs support efficient inference of valid structures (with high probability) and allows to turn on and off the learned constraints at inference time.
arXiv Detail & Related papers (2020-07-26T19:04:37Z) - Refined bounds for algorithm configuration: The knife-edge of dual class
approximability [94.83809668933021]
We investigate how large should a training set be to ensure that a parameter's average metrics performance over the training set is close to its expected, future performance.
We show that if this approximation holds under the L-infinity norm, we can provide strong sample complexity bounds.
We empirically evaluate our bounds in the context of integer programming, one of the most powerful tools in computer science.
arXiv Detail & Related papers (2020-06-21T15:32:21Z) - POINTER: Constrained Progressive Text Generation via Insertion-based
Generative Pre-training [93.79766670391618]
We present POINTER, a novel insertion-based approach for hard-constrained text generation.
The proposed method operates by progressively inserting new tokens between existing tokens in a parallel manner.
The resulting coarse-to-fine hierarchy makes the generation process intuitive and interpretable.
arXiv Detail & Related papers (2020-05-01T18:11:54Z) - Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
A fundamental component of neural network verification is the computation of bounds on the values their outputs can take.
We propose a novel approach based on Lagrangian Decomposition.
We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
arXiv Detail & Related papers (2020-02-24T17:55:10Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.