Formal verification of a lazy concurrent list-based set algorithm

被引:0
作者
Colvin, Robert [1 ]
Groves, Lindsay
Luchangco, Victor
Moir, Mark
机构
[1] Univ Queensland, Sch Informat Technol & Elect Engn, ARC Ctr Complex Syst, St Lucia, Qld 4067, Australia
[2] Univ Victoria, Sch Math Stat & Comp Sci, Wellington, New Zealand
[3] Sun Microsyst Labs, Burlington, MA 01803 USA
来源
COMPUTER AIDED VERIFICATION, PROCEEDINGS | 2006年 / 4144卷
关键词
D O I
暂无
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
We describe a formal verification of a recent concurrent list-based set algorithm due to Heller et al. The algorithm is optimistic: the add and remove operations traverse the list without locking, and lock only the nodes affected by the operation; the contains operation uses no locks and is wait-free. These properties make the algorithm challenging to prove correct, much more so than simple coarse-grained locking algorithms. We have proved that the algorithm is linearisable using simulation between input/output automata modelling the behaviour of an abstract set and the implementation. The automata and simulation proof obligations are specified and verified using PVS.
引用
收藏
页码:475 / 488
页数:14
相关论文
共 50 条
[31]   A List-Based Medium Access Control Algorithm in IEEE 802.11 Wireless Mesh Networks [J].
Jeong, Moo-Yeong ;
Choi, Bum-Gon ;
Lee, Ju Yong ;
Chung, Min Young .
12TH INTERNATIONAL CONFERENCE ON ADVANCED COMMUNICATION TECHNOLOGY: ICT FOR GREEN GROWTH AND SUSTAINABLE DEVELOPMENT, VOLS 1 AND 2, 2010, :750-753
[32]   List-Based Task Scheduling for Cloud Computing [J].
Akbar, Muhammad Fasih ;
Munir, Ehsan Ullah ;
Rafique, M. Mustafa ;
Malik, Zaki ;
Khan, Samee U. ;
Yang, Laurence T. .
2016 IEEE INTERNATIONAL CONFERENCE ON INTERNET OF THINGS (ITHINGS) AND IEEE GREEN COMPUTING AND COMMUNICATIONS (GREENCOM) AND IEEE CYBER, PHYSICAL AND SOCIAL COMPUTING (CPSCOM) AND IEEE SMART DATA (SMARTDATA), 2016, :652-659
[33]   A priority list-based evolutionary algorithm to solve large scale unit commitment problem [J].
Srinivasan, D ;
Chazelas, J .
2004 INTERNATIONAL CONFERENCE ON POWER SYSTEM TECHNOLOGY - POWERCON, VOLS 1 AND 2, 2004, :1746-1751
[34]   A List-based Heuristic Algorithm for Static Task Scheduling in Heterogeneous Distributed Computing Systems [J].
Gholami, Hadi ;
Zakerian, Reza .
2020 6TH INTERNATIONAL CONFERENCE ON WEB RESEARCH (ICWR), 2020, :21-26
[35]   Multi-agent list-based threshold-accepting algorithm for numerical optimisation [J].
Lin, Juan ;
Zhong, Yiwen .
INTERNATIONAL JOURNAL OF COMPUTING SCIENCE AND MATHEMATICS, 2015, 6 (05) :501-509
[36]   Automatic construction and verification algorithm for smart contracts based on formal verification [J].
Xie, Rui ;
Zhong, Xuejiao ;
Chen, Xin ;
Xu, Shaohui ;
Yu, Haiyang ;
Guo, Xinyuan .
AIP ADVANCES, 2024, 14 (11)
[37]   List-Based Optimisers: Experiments and Open Questions [J].
Clerc, Maurice .
INTERNATIONAL JOURNAL OF SWARM INTELLIGENCE RESEARCH, 2013, 4 (04) :23-38
[38]   Efficient List-Based Computation of the String Subsequence Kernel [J].
Bellaouar, Slimane ;
Cherroun, Hadda ;
Ziadi, Djelloul .
LANGUAGE AND AUTOMATA THEORY AND APPLICATIONS (LATA 2014), 2014, 8370 :138-148
[39]   A hybrid genetic algorithm, list-based simulated annealing algorithm, and different heuristic algorithms for travelling salesman problem [J].
Ilin, Vladimir ;
Simic, Dragan ;
Simic, Svetislav D. ;
Simic, Svetlana ;
Saulic, Nenad ;
Luis Calvo-Rolle, Jose .
LOGIC JOURNAL OF THE IGPL, 2023, 31 (04) :602-617
[40]   Program Transformation to Identify List-Based Parallel Skeletons [J].
Kannan, Venkatesh ;
Hamilton, G. W. .
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2016, (216) :118-136