Proving Properties of Dekker’s Algorithm for Mutual Exclusion of N Processes
Dekker’s algorithm for mutual exclusion of two processes is the well-known first developed correct solution based only on software mechanisms. The algorithm served as the starting point for researchers to create subsequent safe solutions both for two and N > 2 processes. In recent years, Dekker p...
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2025-04-01
|
| Series: | Algorithms |
| Subjects: | |
| Online Access: | https://www.mdpi.com/1999-4893/18/4/226 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | Dekker’s algorithm for mutual exclusion of two processes is the well-known first developed correct solution based only on software mechanisms. The algorithm served as the starting point for researchers to create subsequent safe solutions both for two and N > 2 processes. In recent years, Dekker proposed a generalization of his mutual exclusion algorithm for N > 2 processes (here referred to as Dekker-N). To the best of our knowledge, Dekker-N correctness was only proven by the author using informal arguments. This paper’s original contribution consists of formal modeling and verification of Dekker-N using an approach based on timed automata (TA) and the Uppaal model checker. The Dekker-N model is checked under atomic registers and also in cases where non-atomic registers are used. This paper first demonstrates that Dekker-N is correct and fair with atomic registers and effectively ensures bounded waiting for competing processes through a linear overtaking. Unfortunately, the algorithm becomes incorrect when non-atomic registers are used. The adopted formal approach, though, allowed us to prove that by making just one single common variable safe, Dekker-N turns out to be fully correct and fair with non-atomic registers as well. The paper presents the TA-based formal approach and goes on by presenting models of Dekker-N and by verifying all its mutual-exclusion properties. |
|---|---|
| ISSN: | 1999-4893 |