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

← 1 2 3 4 5 →