Original scientific paper

https://doi.org/10.20532/cit.2025.1006091

Specifying Relaxed Concurrent Data Structures Using NADTs

Jie Peng ; School of Information Engineering, Gannan University of Science and Technology, Ganzhou, China *
Tangliu Wen ; School of Information Engineering, Gannan University of Science and Technology, Ganzhou, China

* Corresponding author.

Abstract

To improve performance scalability of concurrent data structures, one solution is to relax their sequential semantics. While a variety of specification approaches focus on characterizing the relaxed semantics, client-side reasoning using the current methodologies is difficult. We employ nondeterministic abstract data types (NADTs) for the first time to specify the relaxed concurrent data structures, and as instantiations of our specification approach, we propose new correctness criteria of out-of-order queues and stacks. We further prove the relaxation equivalence of the out-of-order dequeue and enqueue operations. Our specification approach is intuitive and generic, and can provide clients with explicit interfaces. As a demonstration of our approach, we specify and verify the k-segment queue.

Keywords

relaxed concurrent data structures; specification; nondeterministic abstract data type

Hrčak ID:

346524

URI

https://hrcak.srce.hr/346524

Publication date:

30.1.2026.

Visits: 29 *