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 条

[21] A Permission based Multilevel Parallel Solution for Distributed Mutual Exclusion [J].

Rahman, Mohammad Ashiqur ;

Akbar, M. Mostofa .

JOURNAL OF COMPUTERS, 2012, 7 (08) :1831-1846

[22] Info-based approach in distributed mutual exclusion algorithms [J].

Neamatollahi, Peyman ;

Taheri, Hoda ;

Naghibzadeh, Mahmoud .

JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2012, 72 (05) :650-665

[23] A scalable mutual exclusion algorithm for mobile ad hoc networks [J].

Wu, WG ;

Cao, JN ;

Yang, J .

ICCCN 2005: 14th International Conference on Computer Communications and Networks, Proceedings, 2005, :165-170

[24] Distributed mutual exclusion token-permission based by prioritized groups [J].

Housni, A ;

Trehel, M .

ACS/IEEE INTERNATIONAL CONFERENCE ON COMPUTER SYSTEMS AND APPLICATIONS, PROCEEDINGS, 2001, :253-259

[25] Mutual exclusion by four shared bits with not more than quadratic complexity [J].

Hesselink, Wim H. .

SCIENCE OF COMPUTER PROGRAMMING, 2015, 102 :57-75

[26] Petri net controllers for Generalized Mutual Exclusion Constraints with floor operators [J].

Ma, Ziyue ;

Li, Zhiwu ;

Giua, Alessandro .

AUTOMATICA, 2016, 74 :238-246

[27] A log (N) distributed mutual exclusion algorithm based on path reversal [J].

Naimi, M ;

Trehel, M ;

Arnold, A .

JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 1996, 34 (01) :1-13

[28] A distributed token based h-out of-k Mutual Exclusion protocol for mobile ad hoc networks [J].

Benchaiba, Mahfoud ;

Nacer, Mohamed Ahmed .

INTERNATIONAL JOURNAL OF AD HOC AND UBIQUITOUS COMPUTING, 2010, 5 (02) :117-135

[29] A fair starvation-free prioritized mutual exclusion algorithm for distributed systems [J].

Lejeune, Jonathan ;

Arantes, Luciana ;

Sopena, Julien ;

Sens, Pierre .

JOURNAL OF PARALLEL AND DISTRIBUTED COMPUTING, 2015, 83 :13-29

[30] High-performance N-thread software solutions for mutual exclusion [J].

Buhr, Peter A. ;

Dice, David ;

Hesselink, Wim H. .

CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2015, 27 (03) :651-701

← 1 2 3 4 5 →