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 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.