Rupak Majumdar ; Ramanathan S. Thinniyam ; Georg Zetzsche - General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond

lmcs:7606 - Logical Methods in Computer Science, October 21, 2022, Volume 18, Issue 4 - https://doi.org/10.46298/lmcs-18(4:2)2022
General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond

Authors: Rupak Majumdar ; Ramanathan S. Thinniyam ; Georg Zetzsche

    The model of asynchronous programming arises in many contexts, from low-level systems software to high-level web programming. We take a language-theoretic perspective and show general decidability and undecidability results for asynchronous programs that capture all known results as well as show decidability of new and important classes. As a main consequence, we show decidability of safety, termination and boundedness verification for higher-order asynchronous programs -- such as OCaml programs using Lwt -- and undecidability of liveness verification already for order-2 asynchronous programs. We show that under mild assumptions, surprisingly, safety and termination verification of asynchronous programs with handlers from a language class are decidable iff emptiness is decidable for the underlying language class. Moreover, we show that configuration reachability and liveness (fair termination) verification are equivalent, and decidability of these problems implies decidability of the well-known "equal-letters" problem on languages. Our results close the decidability frontier for asynchronous programs.


    Volume: Volume 18, Issue 4
    Published on: October 21, 2022
    Accepted on: January 15, 2022
    Submitted on: June 20, 2021
    Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Programming Languages,F.3.1
    Fundings :
      Source : OpenAIRE Research Graph
    • imPACT – Privacy, Accountability, Compliance, and Trust in Tomorrow’s Internet; Funder: European Commission; Code: 610150

    Share

    Consultation statistics

    This page has been seen 461 times.
    This article's PDF has been downloaded 253 times.