Nicolas Markey

Résumé

We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm of [J. Aspnes; Fast deterministic consensus in a noisy environment; J. Algorithms, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.

@inproceedings{icalp2022-BMSW,
  author =              {Bertrand, Nathalie and Markey, Nicolas and Sankur,
                         Ocan and Waldburger, Nicolas},
  title =               {Parameterized safety verification of round-based
                         shared-memory systems},
  editor =              {Woodruff, David and Boja{\'n}czyk, Miko{\l}aj},
  booktitle =           {{P}roceedings of the 49th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'22)},
  acronym =             {{ICALP}'22},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  pages =               {113:1-113:20},
  year =                {2022},
  month =               jul,
  doi =                 {10.4230/LIPIcs.ICALP.2022.113},
  abstract =            {We consider the parameterized verification problem
                         for distributed algorithms where the goal is to
                         develop techniques to prove the correctness of a
                         given algorithm regardless of the number of
                         participating processes. Motivated by an
                         asynchronous binary consensus algorithm~of
                         [J.~Aspnes; Fast deterministic consensus in a noisy
                         environment; J.~Algorithms,~2002], we~consider
                         round-based distributed algorithms communicating
                         with shared memory. A~particular challenge in these
                         systems is that 1)~the~number of processes is
                         unbounded, and, more importantly, 2)~there is a
                         fresh set of registers at each round. A~verification
                         algorithm thus needs to manage both sources of
                         infinity. In~this setting, we~prove that the safety
                         verification problem, which consists in deciding
                         whether all possible executions avoid a given error
                         state, is PSPACE-complete. For~negative instances of
                         the safety verification problem, we~also provide
                         exponential lower and upper bounds on the minimal
                         number of processes needed for an error execution
                         and on the minimal round on which the error state
                         can be covered.},
}