After reviewing the basic definitions of harmony and stability, two of the central concepts in Proof-Theoretic Semantics, the paper considers the implicational fragment of the relevant logic R (Anderson&Belnap), under a labelled natural deduction (ND) system, where the labels keep track of ‘use’ of assumptions. Thereby, no assumption is discharged that has not been used. It is shown that the ND is not closed under composition of derivations using its standard definition, thereby prohibiting Prawitz's detour removal reductions, hence failing harmony. A revised definition of derivation composition is proposed, under which the ND system *is* closed, allowing reductions and reenabling harmony (and stability).

The paper surveys several views of proof-theoretic semantics and classifies them in accordance to the choice of which of the rules of a meaning-conferring natural-deduction system determines the meaning of the defined expression. Then, in contrast to the traditional approach that regards the rules as determining meaning implicitly, the paper proposes an explicit definition of meaning in terms of rules, appealing to collections of canonical derivations. A certain claim about a conclusion from the non-eliminability of the rules that are not meaning conferring is refuted, and an alternative explanation of non-eliminability is proposed.

A model of computation dealing with infinite alphabets is proposed. This model is based on replacing the equality test by substitution. It appears to be a natural generalization of the classical Rabin-Scott finite-state automata and possesses many of their closure and decision properties. Also, when restricted to finite alphabets the model is equivalent to finite-state automata.

Unbounded and bounded designs of asynchronous unison systems are discussed. It is shown that both systems are stabilizing in the sense that their steady state behaviors do not depend on their initial states. The systems can therefore tolerate memory and reconfiguration faults that may yield them in arbitrary states. It is also shown that unison systems are useful in designing multiphase systems.>

Abstract The paper considers the treatment of fairness assumptions which are not equivalence-robust , a central issue in relating interleaving semantics to partial order semantics . A notion of completion is introduced and studied, and two specific completions are considered: maximal completion , which is easier to implement (shown by a broadcast bus implementation) but guarantees only weak liveness properties of programs using it; and minimal completion , which may be harder to implement but induces stronger liveness properties on programs using it. Some properties of completions are formulated. Finally, the impact of non-equivalence-robustness on compositionality with respect to separate fairness assumptions is considered.

A model of computation dealing with infinite alphabets is proposed. The model is based on replacing the equality test by unification. It appears to be a natural generalization of the classical Rabin-Scott finite-state automata and possesses many of their properties.>

In this paper, a new fairness notion is proposed for languages with multi-party interactions as the sole interprocess synchronization and communication primitive. The main advantage of this fairness notion is the elimination of starvation occurring solely due to race conditions (i.e., ordering of independent actions). Also, this is the first fairness notion for such languages which is fully-adequate with respect to the criteria presented in [AFK88]. The paper defines the notion, proves its properties, and presents examples of its usefulness.

Circular attribute grammars appear in many data flow analysis problems. As one way of making the notion useful, an automatic translation of circular attribute grammars to equivalent non-circular attribute grammars is presented. It is shown that for circular attribute grammars that arise in many data flow analysis problems, the translation does not increase the asymptotic complexity of the semantic equations. Therefore, the translation may be used in conjunction with any evaluator generator to automate the development of efficient data flow analysis algorithms. As a result, the integration of such algorithms with other parts of a compiler becomes easier.

The authors consider the essential properties of a multiparty interaction construct which serves as a primitive for interprocess communication and synchronization in distributed programs. It is claimed that more general constructs, which violate the suggested properties, are appropriate for abstraction but should not be seen as a communication primitive, and that both facilities are needed. Several acceptability criteria are posed for multiparty interactions, and various possibilities for constructs satisfying these criteria are presented. These include introducing a novel kind of nondeterminism within the assignments of an interaction, weakening the synchronization among the participants in an interaction, and varying the number of participants in order to provide a high-level treatment of fault tolerance.>

A general definition of the notion of superimposition is presented. We show that previous constructions under the same name can be seen as special cases of our definition. We consider several properties of superimposition definable in our terms, notably the nonfreezing property. We also consider a syntactic representation of our construct in CSP

The relations among various languages and models for distributed computation and various possible definitions of fairness are considered. Natural semantic criteria are presented which an acceptable notion of fairness should satisfy. These are then used to demonstrate differences among the basic models, the added power of the fairness notion, and the sensitivity of the fairness notion to irrelevant semantic interleavings of independent operations. These results are used to show that from the considerable variety of commonly used possibilities, only strong process fairness is appropriate for CSP if these criteria are adopted. We also show that under these criteria, none of the commonly used notions of fairness are fully acceptable for a model with an n-way synchronization mechanism. Finally, the notion of fairness most often mentioned for Ada is shown to be fully acceptable.

We argue for the need of supporting a symmetric select construct, in which entry calls as well as accepts can be alternatives. We present several situations in which a symmetric select leads to a more natural programming style. We show that several semantic principles are violated by a nonsymmetric select, while being satisfied by a symmetric one. In particular, the suggested symmetric intertask communication mechanism is fully abstract and composable, and has a distributed termination rule which reduces the risk of deadlock. Our discussion is in terms of Ada™.

Fairness has become one of the main issues in the theory of non-determinism and concurrency. Recently, the problem of proof rules for fair termination of programs (and some of its variants) has attracted considerable attention ([AO83], [APS82], [GFK83], [GFMR81], [LPS81], [P83]). However, though the main interest and motivation for the consideration of fair termination stems from concurrency, almost all of the recent results are formulated in terms of nondeterministic programs. The main reason for this is the elegance of formalisms for structured nondeterminism, such as Guarded Commands [DIJ76], and their convenience for syntax directed proofs. Other attempts use transition-systems as the program model, and temporal logic as the underlying reasoning formalism ([QS82], [P83]), thereby giving up the structured, syntax-directed, approach.

We present a generalization of the known fairness and equifairness notions, called @@@@-fairness, in three versions: unconditional, weak and strong. For each such version, we introduce a proof rule for the @@@@-fair termination induced by it, using well-foundedness and countable ordinals. Each such rule is proved to be sound and semantically complete. We suggest directions for further research.

How the distributed termination convention of CSP repetitive commands can be modeled using other CSP constructs is shown.The presented transformation suggests a simple implementation of this convention.We argue that this convention should be used as a compiler option.

In this paper, we introduce a new abstraction mechanism, called a script, which hides the low-level details that implement patterns of communication. A script localizes the communication between a set of roles (formal processes), to which actual processes enroll in order to participate in the action of the script. The paper discusses the addition of scripts to the languages CSP and Ada, as well as to a shared-variable language with monitors.

A methodology for transforming sequential recursive algorithms to distributive ones is suggested. The assumption is that the program segments between recursive calls have a distributive implementation. The methodology is applied to two k-selection algorithms and yields new distributed k-selection algorithms. Some complexity issues of the resulting algorithms are discussed.

In this paper, we view computer networks as distributed systems that provide their users with a set of services, in a way which hides the distinction between those services which are local and those which are remote. We conceive of a given target network configuration as a network of communicating virtual machines and its behavior is modelled by a system of communicating sequential processes. Network protocols are described by a high level concurrent language (CSP) and a methodology is developed which permits the verification of partial and total correctness assertions about the system in a simple and natural way. Global invariants are used to establish invariant properties of the whole system and histories to record the sequence of communication exchanges between every matching pair of processes. Eventuality properties are expressed using linear temporal logic.

Exchange of information between executing processes is one of the primary reasons for process interaction. Many distributed systems implement explicit message passing primitives to facilitate intercommunication. Typically, a process executes a write command to pass a message to another process, and the target process accepts the message by executing a read command. The semantics of write and read may differ considerably depending on the methods used for storing or buffering messages that have been sent but not yet accepted by the receiving process.

We present two extensions of Communicating Sequential Processes [HO78]: computed communication targets and unspecified communication targets, as well as corresponding extensions to the system of cooperating proofs [AFR80] for verifying distributed programs. These extensions are important for the natural expressibility of many distributed programs. Examples of the use of these extensions are discussed and verified.

An efficient algorithm for achieving distributed termination without introducing new communicaton channels and without delaying the basic computations ("freezing") is presented. The algorithm is related to the methodology of designing distributed programs where the programmer is relieved from the problem of distributed termination. An informal correctness proof and complexity analysis are included.

A denotational semantics is given for a distributed language based on communication (CSP). The semantics uses linear sequences of communications to record computations; for any well formed program segment the semantics is a relation between attainable states and the communication sequences needed to attain these states. In binding two or more processes we match and merge the communication sequences assumed by each process to obtain a sequence and State of the combined process. The approach taken here is distinguished by relatively simple semantic domains and ordering.

From the users' point of view, resource management schemes may be considered as an abstract data type. An abstract specification of such schemes using axioms holding in partial algebras and relatively distributed implementations (expressed as CSP programs) are given and analyzed. Then the idea of probabilistic implementation of guard scheduling is suggested, which allows completely distributed symmetric programs. It frees the designer of an algorithm from looking for specific probabilistic algorithms, by allowing the compiler to generate probabilistic target code from nonprobabilistic source code.

An axiomatic proof system is presented for proving partial correctness and absence of deadlock (and failure) of communicating sequential processes. The key (meta) rule introduces cooperation between proofs, a new concept needed to deal with proofs about synchronization by message passing. CSP's new convention for distributed termination of loops is dealt with. Applications of the method involve correctness proofs for two algorithms, one for distributed partitioning of sets, the other for distributed computation of the greatest common divisor of n numbers.

Discussed is a distributed system based on communication among disjoint processes, where each process is capable of achieving a post-condition of its local space in such a way that the conjunction of local post-conditions implies a global post-condition of the whole system. The system is then augmented with extra control communication in order to achieve distributed termination, without adding new channels of communication. The algorithm is applied to a problem of constructing a sorted partition.

A parallel program, Dijkstra's "on-the-fly" garbage collector, is proved correct using analysis along the lines suggested by Francez and Pnueli for cyclic programs. The method is briefly reviewed, and the proof is compared to another proof by D. Gries, based on a method by S. Owickd. The differences between the two approaches are discussed.