Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos

被引：7

作者：

Hesselink, Wim H. ^{[1
]}

机构：

[1] Univ Groningen, Dept Comp Sci, NL-9700 AK Groningen, Netherlands

来源：

ACTA INFORMATICA | 2013年 / 50卷 / 03期

关键词：

LOCK-FREE; PARALLEL; COMMUNICATION; ALGORITHM; SYSTEMS;

D O I：

10.1007/s00236-013-0178-2

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

A simplification of the mutual exclusion algorithm of Lycklama and Hadzilacos (ACM Trans Program Lang Syst 13:558-576, 1991) is presented. It uses only four nonatomic shared bits per thread to guarantee mutual exclusion with the first-come-first-served property. The algorithm is verified by assertional methods, aided by the proof assistant PVS. A variation with five bits per thread is also given. This variation may give better performance when the number of threads is large. The use of the proof assistant made it easy to transfer the proof of the main algorithm to the variation.

引用

页码：199 / 228

页数：30

共 50 条

[41] Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Analyses [J].

Lopez-Garcia, Pedro ;

Bueno, Francisco ;

Hermenegildo, Manuel .

NEW GENERATION COMPUTING, 2010, 28 (02) :177-206

[42] The Average Message Complexity Analysis for Different Distributed Mutual Exclusion Site-tolerant Ways [J].

Li, MeiAn ;

Li, Wei ;

Ma, Dong .

ACHIEVEMENTS IN ENGINEERING MATERIALS, ENERGY, MANAGEMENT AND CONTROL BASED ON INFORMATION TECHNOLOGY, PTS 1 AND 2, 2011, 171-172 :675-678

[43] Optimal nodes selection in wireless sensor and actor networks based on prioritized mutual exclusion approach [J].

Ranga, Virender ;

Dave, Mayank ;

Verma, Anil K. .

KUWAIT JOURNAL OF SCIENCE, 2016, 43 (01) :150-173

[44] Proximity-Aware Distributed Mutual Exclusion for Effective Peer-to-Peer Replica Management [J].

Smith, Denvil ;

Tzeng, Nian-Feng .

2009 8TH IEEE INTERNATIONAL SYMPOSIUM ON NETWORK COMPUTING AND APPLICATIONS, 2009, :36-43

[45] On the performance of Dijkstra's third self-stabilizing algorithm for mutual exclusion and related algorithms [J].

Chernoy, Viacheslav ;

Shalom, Mordechai ;

Zaks, Shmuel .

DISTRIBUTED COMPUTING, 2010, 23 (01) :43-60

[46] Arbitration-based Reliable Distributed Mutual Exclusion for Mobile Ad-hoc Networks [J].

Parameswaran, Murali ;

Hota, Chittaranjan .

2013 11TH INTERNATIONAL SYMPOSIUM ON MODELING & OPTIMIZATION IN MOBILE, AD HOC & WIRELESS NETWORKS (WIOPT), 2013, :380-387

[47] Model checking and performance evaluation with CADP illustrated on shared-memory mutual exclusion protocols [J].

Mateescu, Radu ;

Serwe, Wendelin .

SCIENCE OF COMPUTER PROGRAMMING, 2013, 78 (07) :843-861

[48] Closed-loop Live Marked Graphs under Generalized Mutual Exclusion Constraint Enforcement [J].

Basile, Francesco ;

Recalde, Laura ;

Chiacchio, Pasquale ;

Silva, Manuel .

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2009, 19 (01) :1-30

[49] A Token-Based Solution to Group Local Mutual Exclusion Problem In Mobile Ad Hoc Networks [J].

Khanna, Ashish ;

Singh, Awadhesh Kumar ;

Swaroop, Abhishek .

ARABIAN JOURNAL FOR SCIENCE AND ENGINEERING, 2016, 41 (12) :5181-5194

[50] Formal Specification and Model Checking of the Walter-Welch-Vaidya Mutual Exclusion Protocol for Ad Hoc Mobile Networks [J].

Phyo, Yati ;

Ogata, Kazuhiro .

2018 25TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2018), 2018, :89-98

← 1 2 3 4 5 →