Fair Mutual Exclusion for N Processes

Yousra Hafidi; Jeroen J.A. Keiren; Jan Friso Groote

doi:10.1007/978-3-031-50423-5_14

Fair Mutual Exclusion for N Processes

Yousra Hafidi, Jeroen J.A. Keiren (Corresponding author), Jan Friso Groote

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Downloads (Pure)

Abstract

Peterson’s mutual exclusion algorithm for two processes has been generalized to N processes in various ways. As far as we know, no such generalization is starvation free without making any fairness assumptions. In this paper, we study the generalization of Peterson’s algorithm to N processes using a tournament tree. Using the mCRL2 language and toolset we prove that it is not starvation free unless weak fairness assumptions are incorporated. Inspired by the counterexample for starvation freedom, we propose a fair N-process generalization of Peterson’s algorithm. We use model checking to show that our new algorithm is correct for small N. For arbitrary N, model checking is infeasible due to the state space explosion problem, and instead, we present a general proof that, for N≥ 4, when a process requests access to the critical section, other processes can enter first at most (N- 1 ) (N- 2 ) times.

Original language	English
Title of host publication	Tools and Methods of Program Analysis
Subtitle of host publication	6th International Conference, TMPA 2021, Tomsk, Russia, November 25–27, 2021, Revised Selected Papers
Editors	Rostislav Yavorskiy, Ana Rosa Cavalli, Anna Kalenkova
Place of Publication	Cham
Publisher	Springer
Pages	149-160
Number of pages	12
ISBN (Electronic)	978-3-031-50423-5
ISBN (Print)	978-3-031-50422-8
DOIs	https://doi.org/10.1007/978-3-031-50423-5_14
Publication status	Published - 3 Jan 2024
Event	6th International Conference on Tools and Methods of Program Analysis, TMPA 2021 - Tomsk, Russian Federation Duration: 25 Nov 2021 → 27 Nov 2021

Publication series

Name	Communications in Computer and Information Science (CCIS)
Volume	1559
ISSN (Print)	1865-0929
ISSN (Electronic)	1865-0937

Conference

Conference	6th International Conference on Tools and Methods of Program Analysis, TMPA 2021
Abbreviated title	TMPA 2021
Country/Territory	Russian Federation
City	Tomsk
Period	25/11/21 → 27/11/21

Funding

This work was supported partially by the MACHINAIDE project (ITEA3, No. 18030).

Keywords

Model-checking
Mutual exclusion
Peterson’s algorithm
Starvation freedom
mCRL2

Access to Document

10.1007/978-3-031-50423-5_14

pdfFinal published version, 292 KBLicence: TAVERNE

Cite this

Hafidi, Y., Keiren, J. J. A., & Groote, J. F. (2024). Fair Mutual Exclusion for N Processes. In R. Yavorskiy, A. R. Cavalli, & A. Kalenkova (Eds.), Tools and Methods of Program Analysis: 6th International Conference, TMPA 2021, Tomsk, Russia, November 25–27, 2021, Revised Selected Papers (pp. 149-160). (Communications in Computer and Information Science (CCIS); Vol. 1559). Springer. https://doi.org/10.1007/978-3-031-50423-5_14

Hafidi, Yousra ; Keiren, Jeroen J.A. ; Groote, Jan Friso. / Fair Mutual Exclusion for N Processes. Tools and Methods of Program Analysis: 6th International Conference, TMPA 2021, Tomsk, Russia, November 25–27, 2021, Revised Selected Papers. editor / Rostislav Yavorskiy ; Ana Rosa Cavalli ; Anna Kalenkova. Cham : Springer, 2024. pp. 149-160 (Communications in Computer and Information Science (CCIS)).

@inproceedings{ed9479335fc54fe9a84798111b92d259,

title = "Fair Mutual Exclusion for N Processes",

abstract = "Peterson{\textquoteright}s mutual exclusion algorithm for two processes has been generalized to N processes in various ways. As far as we know, no such generalization is starvation free without making any fairness assumptions. In this paper, we study the generalization of Peterson{\textquoteright}s algorithm to N processes using a tournament tree. Using the mCRL2 language and toolset we prove that it is not starvation free unless weak fairness assumptions are incorporated. Inspired by the counterexample for starvation freedom, we propose a fair N-process generalization of Peterson{\textquoteright}s algorithm. We use model checking to show that our new algorithm is correct for small N. For arbitrary N, model checking is infeasible due to the state space explosion problem, and instead, we present a general proof that, for N≥ 4, when a process requests access to the critical section, other processes can enter first at most (N- 1 ) (N- 2 ) times.",

keywords = "Model-checking, Mutual exclusion, Peterson{\textquoteright}s algorithm, Starvation freedom, mCRL2",

author = "Yousra Hafidi and Keiren, {Jeroen J.A.} and Groote, {Jan Friso}",

year = "2024",

month = jan,

day = "3",

doi = "10.1007/978-3-031-50423-5_14",

language = "English",

isbn = "978-3-031-50422-8",

series = "Communications in Computer and Information Science (CCIS)",

publisher = "Springer",

pages = "149--160",

editor = "Rostislav Yavorskiy and Cavalli, {Ana Rosa} and Anna Kalenkova",

booktitle = "Tools and Methods of Program Analysis",

address = "Germany",

note = "6th International Conference on Tools and Methods of Program Analysis, TMPA 2021, TMPA 2021 ; Conference date: 25-11-2021 Through 27-11-2021",

}

Hafidi, Y, Keiren, JJA & Groote, JF 2024, Fair Mutual Exclusion for N Processes. in R Yavorskiy, AR Cavalli & A Kalenkova (eds), Tools and Methods of Program Analysis: 6th International Conference, TMPA 2021, Tomsk, Russia, November 25–27, 2021, Revised Selected Papers. Communications in Computer and Information Science (CCIS), vol. 1559, Springer, Cham, pp. 149-160, 6th International Conference on Tools and Methods of Program Analysis, TMPA 2021, Tomsk, Russian Federation, 25/11/21. https://doi.org/10.1007/978-3-031-50423-5_14

Fair Mutual Exclusion for N Processes. / Hafidi, Yousra; Keiren, Jeroen J.A. (Corresponding author); Groote, Jan Friso.
Tools and Methods of Program Analysis: 6th International Conference, TMPA 2021, Tomsk, Russia, November 25–27, 2021, Revised Selected Papers. ed. / Rostislav Yavorskiy; Ana Rosa Cavalli; Anna Kalenkova. Cham: Springer, 2024. p. 149-160 (Communications in Computer and Information Science (CCIS); Vol. 1559).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Fair Mutual Exclusion for N Processes

AU - Hafidi, Yousra

AU - Keiren, Jeroen J.A.

AU - Groote, Jan Friso

PY - 2024/1/3

Y1 - 2024/1/3

N2 - Peterson’s mutual exclusion algorithm for two processes has been generalized to N processes in various ways. As far as we know, no such generalization is starvation free without making any fairness assumptions. In this paper, we study the generalization of Peterson’s algorithm to N processes using a tournament tree. Using the mCRL2 language and toolset we prove that it is not starvation free unless weak fairness assumptions are incorporated. Inspired by the counterexample for starvation freedom, we propose a fair N-process generalization of Peterson’s algorithm. We use model checking to show that our new algorithm is correct for small N. For arbitrary N, model checking is infeasible due to the state space explosion problem, and instead, we present a general proof that, for N≥ 4, when a process requests access to the critical section, other processes can enter first at most (N- 1 ) (N- 2 ) times.

AB - Peterson’s mutual exclusion algorithm for two processes has been generalized to N processes in various ways. As far as we know, no such generalization is starvation free without making any fairness assumptions. In this paper, we study the generalization of Peterson’s algorithm to N processes using a tournament tree. Using the mCRL2 language and toolset we prove that it is not starvation free unless weak fairness assumptions are incorporated. Inspired by the counterexample for starvation freedom, we propose a fair N-process generalization of Peterson’s algorithm. We use model checking to show that our new algorithm is correct for small N. For arbitrary N, model checking is infeasible due to the state space explosion problem, and instead, we present a general proof that, for N≥ 4, when a process requests access to the critical section, other processes can enter first at most (N- 1 ) (N- 2 ) times.

KW - Model-checking

KW - Mutual exclusion

KW - Peterson’s algorithm

KW - Starvation freedom

KW - mCRL2

UR - http://www.scopus.com/inward/record.url?scp=85181982358&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-50423-5_14

DO - 10.1007/978-3-031-50423-5_14

M3 - Conference contribution

SN - 978-3-031-50422-8

T3 - Communications in Computer and Information Science (CCIS)

SP - 149

EP - 160

BT - Tools and Methods of Program Analysis

A2 - Yavorskiy, Rostislav

A2 - Cavalli, Ana Rosa

A2 - Kalenkova, Anna

PB - Springer

CY - Cham

T2 - 6th International Conference on Tools and Methods of Program Analysis, TMPA 2021

Y2 - 25 November 2021 through 27 November 2021

ER -

Hafidi Y, Keiren JJA , Groote JF. Fair Mutual Exclusion for N Processes. In Yavorskiy R, Cavalli AR, Kalenkova A, editors, Tools and Methods of Program Analysis: 6th International Conference, TMPA 2021, Tomsk, Russia, November 25–27, 2021, Revised Selected Papers. Cham: Springer. 2024. p. 149-160. (Communications in Computer and Information Science (CCIS)). doi: 10.1007/978-3-031-50423-5_14