Using Uppaal and Actors for Property Checking of Mutual Exclusion Algorithms in Anonymous Memory

This paper proposes a method for formally modeling and analyzing mutual exclusion algorithms. The process starts with Uppaal timed automata and model checking. A Uppaal model is then reduced to a Java actor program to overcome the scalability issues associated with exhaustive verification. The method is applied to mutual exclusion in anonymous shared memory (ASM). ASM is challenging because concurrent/parallel processes do not agree on the names of the shared registers. Rather, each process uses a permutation of the register names. Processes have unknown identifiers and are symmetric, that is, they execute the same code. ASM is natural in bio-inspired, molecular applications. As a case study, the paper investigates a recent ASM mutual exclusion solution proposed by Taubenfeld. The algorithm proves correct for N=2 processes when m≥7 (m odd) registers are used. The algorithm does not extend to N≥3 processes. As a new contribution, this paper develops and formalizes a solution (TT - T2) that embeds Taubenfeld's algorithm for 2 processes (T2) in a tournament binary tree (TT) organization, where the basic algorithm acts as the arbitration unit in TT nodes. The paper demonstrates, through simulations of the reduced and scalable actor program, that the TT - T2 represents an effective solution for mutual exclusion in ASM for N≥2 processes.