Fair Mutual Exclusion for N Processes (extended version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2021
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908480385843200 |
|---|---|
| author | Hafidi, Yousra Keiren, Jeroen J. A. Groote, Jan Friso |
| author_facet | Hafidi, Yousra Keiren, Jeroen J. A. Groote, Jan Friso |
| contents | 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 \geq 4$, when a process requests access to the critical section, other processes can enter first at most $(N-1)(N-2)$ times. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2111_02251 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Fair Mutual Exclusion for N Processes (extended version) Hafidi, Yousra Keiren, Jeroen J. A. Groote, Jan Friso Logic in Computer Science Distributed, Parallel, and Cluster Computing 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 \geq 4$, when a process requests access to the critical section, other processes can enter first at most $(N-1)(N-2)$ times. |
| title | Fair Mutual Exclusion for N Processes (extended version) |
| topic | Logic in Computer Science Distributed, Parallel, and Cluster Computing |
| url | https://arxiv.org/abs/2111.02251 |