Reseña: Mutual exclusion by four shared bits with not more than quadratic complexity

Se ha publicado un artículo de razonamiento formalizado en PVS sobre concurrencia titulado Mutual exclusion by four shared bits with not more than quadratic complexity.

Su autor es Wim H. Hesselink (de la Universidad de Groninga, Países Bajos).

Su resumen es

For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) was the optimal mutual exclusion algorithm with the first-come-first-served property, with a minimal number of (non-atomic) communication variables (5 bits per thread). Recently, Aravind published an improvement of it, which uses 4 bits per threads and has simplified waiting conditions. This algorithm is extended here with fault tolerance, and it is verified by assertional methods, using the proof assistant PVS. Progress is proved by means of UNITY logic. The paper proposes a new measure of concurrent time complexity, and proves that the concurrent complexity for throughput of the present algorithm is not more than quadratic in the number of threads.

El código de las correspondientes teorías en PVS se encuentra aquí.