23
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony

      Preprint
      , , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          We address the problem of verifying message passing programs, defined as a set of parallel processes communicating through unbounded FIFO buffers. We introduce a bounded analysis that explores a special type of computations, called k-synchronous. These computations can be viewed as (unbounded) sequences of interaction phases, each phase allowing at most k send actions (by different processes), followed by a sequence of receives corresponding to sends in the same phase. We give a procedure for deciding k-synchronizability of a program, i.e., whether every computation is equivalent (has the same happens-before relation) to one of its k-synchronous computations. We also show that reachability over k-synchronous computations and checking k-synchronizability are both PSPACE-complete. Furthermore, we introduce a class of programs called {\em flow-bounded} for which the problem of deciding whether there exists a k>0 for which the program is k-synchronizable, is decidable.

          Related collections

          Most cited references21

          • Record: found
          • Abstract: not found
          • Book Chapter: not found

          Language primitives and type discipline for structured communication-based programming

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            Measurement of the pressure dependence of air fluorescence emission induced by electrons

              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              Verifying Programs with Unreliable Channels

                Bookmark

                Author and article information

                Journal
                18 April 2018
                Article
                1804.06612
                572d9233-20d5-4ee1-86d5-0eb7373fc56d

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                cs.PL

                Programming languages
                Programming languages

                Comments

                Comment on this article