This talk will describe a view of concurrency, the author's own, as it has evolved since the late 1970s. Early notions of concurrency were intimately tied with physical hardware and speeding up of computations, which proved to be an impediment to the development of a logical theory of concurrency. In collaboration with K. Mani Chandy, the author developed a theory called UNITY that combined a programming notation with a verification logic to describe a large class of fundamental concurrent algorithms arising in operating systems, communication protocols and distributed systems. Several model checkers, including Murphi, developed by David Dill, are based on UNITY.

Abstract We propose a scheme for secure voting that involves the candidates themselves in implementing the voting system. It exploits the competing interests (rivalry) and mutual distrust among the candidates to force an honest election.

No abstract available.

The objective of this project is to design a domain-independent framework that allows rapid development of applications customized for specific user needs. We see three major components in the design: (1) persistent storage management, (2) computational logic and execution environment, and (3) methods for orchestrating computations. Recent developments in industry and academia have made available solutions for persistent storage management and distributed execution of computational tasks (e.g., the .NET and the Websphere infrastructures). This project builds upon these efforts; it permits the specification and instantiation of scripts for orchestrating the execution of several computational tasks. The orchestration script specifies what computations to perform and when; but no information on how to perform the computations.

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.

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 program P that not only implements S , but for which ${\overline P}$ = ${\overline 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.

Many data-parallel algorithms—Fast Fourier Transform, Batcher's sorting schemes, and the prefix-sum—exhibit recursive structure. We propose a data structure called powerlist that permits succinct descriptions of such algorithms, highlighting the roles of both parallelism and recursion. Simple algebraic properties of this data structure can be explotied to derive properties of these algorithms and to establish equivalence of different algorithms that solve the same problem.

Abstract A deterministic message-communicating process can be characterised by a “continuous” function f which describes the relationship between the inputs and the outputs of the process. The operational behaviour of a network of deterministic processes can be deduced from the least fixpoint of a function g , where g is obtained from the functions that characterise the component processes of the network. We show in this paper that a nondeter-ministic process can be characterised by a “description” consisting of a pair of functions. The behaviour of a network consisting of such processes can be obtained from the “smooth” solutions of the descriptions characterising its component processes. The notion of smooth solution is a generalisation of least fixpoint. Descriptions enjoy the crucial property that a variable may be replaced by its definition.

No abstract available.

This paper develops a message-based approach to discrete-event simulation. Although message-based simulators have the same expressive power as traditional discrete-event simulation lanuages, they provide a more natural environment for simulating distributed systems. In message-based simulations, a physical system is modeled by a set of message-communicating processes. The events in the system are modeled by message-communications. The paper proposes the entity construct to represent a message-communicating process operating in simulated time. A general wait until construct is used for process scheduling and message-communication. Based on these two notions, the paper proposes a language fragment comprising a small set of primitives. The language fragment can be implemented in any general-purpose, sequential programming language to construct a message-based simulator. We give an example of a message-based simulation language, called MAY, developed by implementing the language fragment in Fortran. MAY is in the public domain and is available on request.

We propose a methodology for the development of concurrent programs and apply it to an important class of problems: quiescence detection. The methodology is based on a novel view of programs. A key feature of the methodology is the separation of concerns between the core problem to be solved and details of the forms of concurrency employed in the target architecture and programming language. We begin development of concurrent programs by ignoring issues dealing with concurrency and introduce such concerns in manageable doses. The class of problems solved includes termination and deadlock detection.

The problem of concurrent accesses to registers by asynchronous components is considered. A set of axioms about the values in a register during concurrent accesses is proposed. It is shown that if these axioms are met by a register, then concurrent accesses to it may be viewed as nonconcurrent, thus making it possible to analyze asynchronous algorithms without elaborate timing analysis of operations. These axioms are shown, in a certain sense, to be the weakest. Motivation for this work came from analyzing low-level hardware components in a VLSI chip which concurrently accesses a flip-flop.

The problem of resolving conflicts between processes in distributed systems is of practical importance.A conflict between a set of processes must be resolved in favor of some (usually one) process and against the others: a favored process must have some property that distinguishes it from others.To guarantee fairness, the distinguishing property must be such that the process selected for favorable treatment is not always the same.A distributed implementation of an acyclic precedence graph, in which the depth of a process (the longest chain of predecessors) is a distinguishing property, is presented.A simple conflict resolution rule coupled with the acyclic graph ensures fair resolution of all conflicts.To make the problem concrete, two paradigms are presented: the well-known distributed dining philosophers problem and a generalization of it, the distributed drinking philosophers problem.

A problem of considerable importance in designing computations by process networks, is detection of termination. We propose a very simple algorithm for termination detection in an arbitrary network using a single marker We show an application of this scheme in solving the problem of token loss detection and token regeneration in a token ring.

Distributed deadlock models are presented for resource and communication deadlocks.Simple distributed algorithms for detection of these deadlocks are given.We show that all true deadlocks are detected and that no false deadlocks are reported.In our algorithms, no process maintains global information; all messages have an identical short length.The algorithms can be applied in distributed database and other message communication systems.

This paper presents a distributed algorithm to detect deadlocks in distributed data bases. Features of this paper are (1) a formal model of the problem is presented, (2) the correctness of the algorithm is proved, i.e. we show that all true deadlocks will be detected and deadlocks will not be reported falsely, (3) no assumptions are made other than that messages are received correctly and in order and (4) the algorithm is simple.

A method is proposed for reasoning about safety and liveness properties of message passing networks. The method is hierarchical and is based upon combining the specifications of component processes to obtain the specification of a network. The inference rules for safety properties use induction on the number of messages transmitted; liveness proofs use techniques similar to termination proofs in sequential programs. We illustrate the method with two examples: concatenations of buffers to construct larger buffers and a special case of Stenning protocol for message communication over noisy channels.

In this paper it is shown how the Dijkstra-Scholten scheme for termination detection in a diffusing computation can be adapted to detect termination or deadlock in a network of communicating sequential processes as defined by Hoare.

A knot in a directed graph is a useful concept in deadlock detection.A distributed algorithm for identifying a knot in a graph by using a network of processes is presented.The algorithm is based on the work of Dijkstra and Scholten.

article An Exercise in Program Explanation Share on Author: Jayadev Misra Department of Computer Sciences, College of Natural Sciences, The University of Texas at Austin, Austin, TX Department of Computer Sciences, College of Natural Sciences, The University of Texas at Austin, Austin, TXView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 3Issue 1Jan. 1981 pp 104–109https://doi.org/10.1145/357121.357128Published:01 January 1981 4citation294DownloadsMetricsTotal Citations4Total Downloads294Last 12 Months6Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

We present a proof method for networks of processes in which component processes communicate exclusively through messages. We show how to construct proofs of invariant properties which hold at all times during network computation, and terminal properties which hold upon termination of network computation, if network computation terminates. The proof method is based upon specifying a process by a pair of assertions, analogous to pre-and post-conditions in sequential program proving. The correctness of network specification is proven by applying inference rules to the specifications of component processes. Several examples are proved using this technique.

The problem of system simulation is typically solved in a sequential manner due to the wide and intensive sharing of variables by all parts of the system. We propose a distributed solution where processes communicate only through messages with their neighbors; there are no shared variables and there is no central process for message routing or process scheduling. Deadlock is avoided in this system despite the absence of global control. Each process in the solution requires only a limited amount of memory. The correctness of a distributed system is proven by proving the correctness of each of its component processes and then using inductive arguments. The proposed solution has been empirically found to be efficient in preliminary studies. The paper presents formal, detailed proofs of correctness.

This paper is concerned with the pros and cons of writing distributed applications software. Most applications software is highly sequential due to the sharing of variables. Here we focus attention on one such application: discrete-event simulatiom. We show how to develop distributed software for this application by taking a radically different view of the application. We outline proofs that our distributed software is correct. Our goal is to develop guidelines for writing distributed applications software.

A technique is presented which is shown to be useful in designing algorithms which operate on sequences (strings). A generalization of the principle is presented for more general data structure.

A method for formal description of programming prinicples is presented in this paper. Programming principles, such as sequential search can be defined and proven even in the absence of an application. We represent a principle as a program scheme which has partially interpreted functions in it. The functions must obey certain input constraints. Use of these ideas in program proving is illustrated with examples.

The problem of proving whether or not a loop computes a given function is investigated. We consider loops which have a certain "closure" property and derive necessary and sufficient conditions for such a loop to compute a given function. It is argued that closure is a fundamental concept in program proving. Extensions of the basic result to proofs involving relations other than functional relations, which typically arise in nondeterministic loops, are explored. Several applications of these results are given, particularly in showing that certain classes of programs may be directly proven (their loop invariants generated) given only their input-output relationships. Implications of these results are discussed.

Given a rooted tree with a positive weight associated with every node, a linear algorithm is presented that will partition the tree into a minimum number of subtrees such that the sum of node weights in no subtree exceed a prespecified value k.

The problem of generation of loop invariants from the input, output assertions of a loop program $({\textbf{while }}B{\textbf{ do }}S)$ is considered. The problem is theoretically unsolvable in general. As a special case we consider assertions of the form $xRy$, where R denotes a binary relation, x denotes the variables manipulated by the program and y denotes variables that are not modified by the(program. We derive conditions for R such that if any loop program has $xRy$ as the input and output assertions, then $xRy$ is a loop invariant. These conditions for R are shown to be necessary and sufficient in that if some $R'$ does not meet these conditions, then there are loop programs for which $xR'y$ holds at entrance and exit, though not following every iteration. In particular it is shown that if R is an equivalence relation, then under certain reasonable restrictions on the loop, $xRy$ holds at entrance and exit of the loop if and only if it holds after every iteration.

This paper studies the problem of algorithm design on well defined data structures. A general principle is presented which is shown to be useful in designing algorithms which operate on sequences (strings). A generalization of the principle is presented for more general data structures. Implications of these results are discussed.

No abstract available.

Given a `DO WHILE' programPand a functionFon a domainD, the authors investigate the problem of proving (or disproving) ifPcomputesFoverD. It is shown that ifPsatisfies certain natural constraints (well behaved), then there is a loop assertion independent of the structure of the loop body, that is both necessary and sufficient for proving the hypothesis. These results are extended to classes of loop programs which are not well behaved and to FOR loops. The sufficiency of Hoare's DO WHILE axiom for well-behaved loop programs is shown. Applications of these ideas to the problem of mechanical generation of assertions is discussed.