Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Decidability of Livelock Detection for Parameterized Self-Disabling Unidirectional Rings

Aly Farahat

Abstract

We prove that livelock detection is \emph{decidable in polynomial time} for parameterized symmetric unidirectional rings of self-disabling processes with bounded domain $\mathbb{Z}_m$. Given a protocol specified by its set of local transitions $T$, the algorithm decides whether a livelock exists for \emph{some} ring size $K\!\geq\!2$, running in $O(|T|^3)$ time independent of $K$. The algorithm computes the greatest fixed point of a deflationary monotone operator on the finite set $T$ and returns \emph{livelock} iff the fixed point is non-empty. The livelock freedom argument rests on maximality: the fix-point is the largest set of transitions that can together sustain a pseudolivelock at every process; its emptiness certifies freedom for all $K$ without any search over ring sizes. The work is grounded in the algebraic characterization of livelocks from Farahat~\citep{farahat2012}, which establishes necessary and sufficient conditions for livelock existence but does not address decidability. We also handle the $(1,1)$-asymmetric case in which one distinguished process $P_0$ differs from the remaining $K\!-\!1$ identical processes. Code and algebraic foundation are at the URL: https://github.com/cosmoparadox/mathematical-tools.

Decidability of Livelock Detection for Parameterized Self-Disabling Unidirectional Rings

Abstract

We prove that livelock detection is \emph{decidable in polynomial time} for parameterized symmetric unidirectional rings of self-disabling processes with bounded domain . Given a protocol specified by its set of local transitions , the algorithm decides whether a livelock exists for \emph{some} ring size , running in time independent of . The algorithm computes the greatest fixed point of a deflationary monotone operator on the finite set and returns \emph{livelock} iff the fixed point is non-empty. The livelock freedom argument rests on maximality: the fix-point is the largest set of transitions that can together sustain a pseudolivelock at every process; its emptiness certifies freedom for all without any search over ring sizes. The work is grounded in the algebraic characterization of livelocks from Farahat~\citep{farahat2012}, which establishes necessary and sufficient conditions for livelock existence but does not address decidability. We also handle the -asymmetric case in which one distinguished process differs from the remaining identical processes. Code and algebraic foundation are at the URL: https://github.com/cosmoparadox/mathematical-tools.
Paper Structure (17 sections, 6 theorems, 8 equations, 1 table, 2 algorithms)

This paper contains 17 sections, 6 theorems, 8 equations, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Contribution.
  3. Foundation.
  4. Setting and Definitions
  5. Ring topology.
  6. Algorithm
  7. Notation for the proof.
  8. Correctness
  9. Livelock freedom---the maximality argument.
  10. Circulation Law
  11. The $(1,1)$-Asymmetric Case
  12. Termination.
  13. Complexity.
  14. Correctness.
  15. Experimental Results
  16. ...and 2 more sections

Key Result

Lemma 1

A livelock exists for some $K\!\geq\!2$ if and only if there exist a pseudolivelock $H$ and propagation $E$ on a non-empty support $\mathcal{L}\subseteq T$, satisfying: We call such $(H,E,\mathcal{L})$ a Farahat witness.

Theorems & Definitions (21)

  • Definition 1: Transition and protocol
  • Definition 2: Enabling and execution
  • Definition 3: $(l,q)$-ring topology
  • Definition 4: Pseudolivelock graph $H(S)$ and operator $\mathrm{PL}$
  • Definition 5: Shadow of a pseudolivelock --- $\mathrm{Shad}$
  • Definition 6: Filter operator $\mathrm{Filter}$
  • Remark 1: Shadow witnesses are exactly the equivariance condition
  • Definition 7: Fixed-point operator $\boldsymbol{\Phi}$ and livelock kernel $\mathcal{L}^{*}$
  • Definition 8: Propagation $E^{*}$
  • Lemma 1: Farahat's characterisation farahat2012
  • ...and 11 more