Rajeev Joshi
ABSTRACT
Typically, program design involves constructing a program P that implements a given specification S; that is, the set P of executions of P is a subset of the set S of executions satisfying S. In many cases, we seek a program P that not only implements S, but for which P = S. Then, every execution satisfying the specification is a possible execution of the program; we then call P maximal for the specification S. We argue that maximality is an important criterion in the context of designing concurrent programs because it disallows implementations that do not exhibit enough concurrency. In addition, a maximal solution can serve as a basis for deriving a variety of implementations, each appropriate for execution on a specific computing platform.
This paper also describes a method for proving the maximality of a program with respect to a given specification. Even though we prove facts about possible executions of programs, there is no need to appeal to branching time logics; we employ a fragment of linear temporal logic for our proofs. The method results in concise proofs of maximality for several non-trivial examples. The method may also serve as a guide in constructing maximal programs.
- 1.K. M. Chandy and J. Misra. The drinking philosophers problem. A CM Transactions on Programming Languages and Systems, 6(4):632-646, 1984. Google Scholar
Digital Library
- 2.K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison Wesley, 1988. Google ScholarDigital Library
- 3.E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, New Jersey, 1976. Google ScholarDigital Library
- 4.R. Joshi and J. Misra. Maximally concurrent programs. Formal Aspects of Computing, (to appear).Google Scholar
- 5.L. Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 657-668, Paris, Sep 1983. IFIP, North-Holland.Google Scholar
- 6.R. Milner. Communication and Concurrency. International Series in Computer Science, C. A. R. Hoare, Series Editor. Prentice-Hall International, London, 1989. Google ScholarDigital Library
- 7.J. Misra. A logic for concurrent programming: Progress. Journal of Computer and Software Engineering, 3(2):273-300, 1995.Google Scholar
- 8.J. Misra. A logic for concurrent programming: Safety. Journal of Computer and Software Engineering, 3(2):239-272, 1995.Google Scholar
- 9.J. Misra. A discipline of multiprogramming, work in progress, ftp access at ftp://ftp, cs. utexas, edu/pub/psp/seuss/discipline, ps. Z, 1996. Google ScholarDigital Library
Index Terms
- Toward a theory of maximally concurrent programs (shortened version)
Recommendations
Maximally Concurrent Programs
Abstract.Typically, program design involves constructing a program P that implements a given specification S; that is, the set ${\overline P}$ of executions of P is a subset of the set ${\overline S}$ of executions satisfying S. In many cases, we seek a ...
Execution privatization for scheduler-oblivious concurrent programs
OOPSLA '12Making multithreaded execution less non-deterministic is a promising solution to address the difficulty of concurrent programming plagued by the non-deterministic thread scheduling. In fact, a vast category of concurrent programs are scheduler-oblivious:...
Comments