abstract: article Free Access Share on A System for Assisting Program Transformation Author: Martin S. Feather USC/Information Sciences Institute, 4676 Admiralty Way, Marina del Rey, CA USC/Information Sciences Institute, 4676 Admiralty Way, Marina del Rey, CAView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 4Issue 1Jan. 1982 pp 1–20https://doi.org/10.1145/357153.357154Published:01 January 1982Publication History 99citation430DownloadsMetricsTotal Citations99Total Downloads430Last 12 Months17Last 6 weeks1 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 Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


venue: toplas

title: The Evaluation of Expressions in Icon

abstract: of Expressions in IconExpressions in the Icon programming language may be conditional, possibly producing no result, or they may be generators, possibly producing a sequence of results.Generators, coupled with a goaldirected evaluation mechanism, provide a concise method for expressing many complex computations.This paper describes the evaluation of expressions in Icon and presents an Icon program that explicates the semantics of expression evaluation.This program also provides an executable "formalism" that can be used as a tool to design and test changes and additions to the language.


title: Symbolic Debugging of Optimized Code

abstract: of Optimized


title: A Value Transmission Method for Abstract Data Types

authors:
Maurice Herlihy
Barbara Liskov

abstract: data types have proved to be a useful technique for structuring systems.In large systems it is sometimes useful to have different regions of the system use different representations for the abstract data values.A technique is described for communicating abstract values between such regions.The method was developed for use in constructing distributed systems, where the regions exist at different computers and the values are communicated over a network.The method defines a call-by-value semantics; it is also useful in nondistributed systems wherever call by value is the desired semantics.An important example of such a use is a repository, such as a file system, for storing longlived data.


title: Programming with Equations

authors:
Christoph M. Hoffmann
Michael J. O'Donnell

abstract: Equations provide a convenient notation for defining many computations, for example, for programming language interpreters.This paper illustrates the usefulness of equational programs, describes the problems involved in implementing equational programs, and investigates practical solutions to those problems.The goal of the study is a system to automatically transform a set of equations into an efficient program which exactly implements the logical meaning of the equations.This logical meaning may be defined in terms of the traditional mathematical interpretation of equations, without using advanced computing concepts._


title: An Introduction to S/SL: Syntax/Semantic Language

authors:
Richard C. Holt
James R. Cordy
David B. Wortman

abstract: S/SL (Syntax/Semantic Language) is a language that was developed for implementing compilers.A subset called SL (Syntax Language) has the same recognition power as do LR(k) parsers.Complete S/SL includes invocation of semantic operations implemented in another language such as PASCAL.S/SL implies a top-down programming methodology.First, a data-free algorithm is developed in S/SL.The algorithm invokes operations on "semantic mechanisms."A semantic mechanism is an abstract object, specified, from the point of view of the S/SL, only by the effect of operations upon the object.Later, the mechanisms are implemented apart from the S/SL program.The separation of the algorithm from the data and the division of data into mechanisms reduce the effort needed to understand and maintain the resulting software.S/SL has been used to construct compilers for SPECKLE (a PL/I subset), PT (a PASCAL subset), Toronto EUCLID, and Concurrent EUCLID.It has been used to implement scanners, parsers, semantic analyzers, and code generators.S/SL programs are implemented by translating them into tables of integers.A "table walker" program executes the S/SL program by interpreting this table.The translation of S/SL programs into tables is performed by a program called the S/SL processor.This processor serves a function analogous to that served by an LR(k) parser generator.The implementation of S/SL is simple and portable.It is available in a small subset of PASCAL that can easily be transliterated into other high-level languages.


title: A Model for Implementing Euclid Modules and Prototypes

authors:
Richard C. Holt
David B. Wortman

abstract: article Free Access Share on A Model for Implementing EUCLID Modules and Prototypes Authors: Richard C. Holt Computer Systems Research Group, University of Toronto, Toronto, Ontario, Canada M5S 1A1 Computer Systems Research Group, University of Toronto, Toronto, Ontario, Canada M5S 1A1View Profile , David B. Wortman Computer Systems Research Group, University of Toronto, Toronto, Ontario, Canada M5S 1A1 Computer Systems Research Group, University of Toronto, Toronto, Ontario, Canada M5S 1A1View Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 4Issue 4Oct. 1982 pp 552–562https://doi.org/10.1145/69622.357183Published:01 October 1982Publication History 5citation236DownloadsMetricsTotal Citations5Total Downloads236Last 12 Months6Last 6 weeks1 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 Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: The Byzantine Generals Problem

authors:
Leslie Lamport
Robert E. Shostak
Marshall C. Pease

abstract: Reliable computer systems must handle malfunctioning components that give conflicting information to different parts of the system.This situation can be expressed abstractly in terms of a group of generals of the Byzantine army camped with their troops around an enemy city.Communicating only by messenger, the generals must agree upon a common battle plan.However, one or more of them may be traitors who will try to confuse the others.The problem is to find an algorithm to ensure that the loyal generals will reach agreement.It is shown that, using only oral messages, this problem is solvable if and only if more than two-thirds of the generals are loyal; so a single traitor can confound two loyal generals.With unforgeable written messages, the problem is solvable for any number of generals and possible traitors.Applications of the solutions to reliable computer systems are then discussed.


title: Formal Specification of Graphic Data Types

abstract: Formal specification techniques and data abstractions have seen little application to computer graphics.Many of the objects and operations unique to graphics programs can be handled conveniently by def'ming special graphic data types.Not only do graphic data types provide an attractive way to work with pictures, but they also allow specification techniques for data abstractions to be employed.Algebraic axioms, because of their definitional nature, are especially well suited to specifying the diversity of types useful in graphics applications.In this paper, definitions are given for some important concepts that appear in graphics programs.Based on these definitions, some illustrative graphic data types, called point, region, geometric function, graphic transformation, and tree-structured picture, are defined and specified algebraically.A simple graphics language for line drawings is created by embedding these new data types in the language PASCAL.Using the specifications, an outline of a correctness proof for a small programming example is presented.


title: An Efficient Unification Algorithm

authors:
Alberto Martelli
Ugo Montanari

abstract: The unification problem in f'mst-order predicate calculus is described in general terms as the solution of a system of equations, and a nondeterministic algorithm is given.A new unification algorithm, characterized by having the acyclicity test efficiently embedded into it, is derived from the nondeterministic one, and a PASCAL implementation is given.A comparison with other well-known unification algorithms shows that the algorithm described here performs well in all cases.


title: The VAL Language: Description and Analysis

abstract: VAL is a high-level, function-based language designed for use on data flow computers.A data flow computer has many small processors organized to cooperate in the execution of a single computation.A computation is represented by its data flow graph; each operator in a graph is scheduled for execution on one of the processors after all of its operands' values are known.VAL promotes the identification of concurrency in algorithms and simplifies the mapping into data flow graphs.This paper presents a detailed introduction to VAL and analyzes its usefulness for programming in a highly concurrent environment.VAL provides implicit concurrency (operations that can execute simultaneously are evident without the need for any explicit language notation).The language uses function-and expression-based features that prohibit all side effects, which simplifies translation to graphs.The salient language features are described and illustrated through examples taken from a complete VAL program for adaptive quadrature.Analysis of the language shows that VAL meets the critical needs for a data flow environment.The language encourages programmers to think in terms of general concurrency, enhances readability (due to the absence of side effects), and possesses a structure amenable to verification techniques.However, VAL is still evolving.The language definition needs refining, and more support tools for programmer use need to be developed.Also, some new kinds of optimization problems should be addressed.


title: Termination Detection of Diffusing Computations in Communicating Sequential Processes

authors:
Jayadev Misra
K. Mani Chandy

abstract: 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.


title: A Distributed Graph Algorithm: Knot Detection

abstract: 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.


title: Proving Liveness Properties of Concurrent Programs

authors:
Susan S. Owicki
Leslie Lamport

abstract: A liveness property asserts that program execution eventually reaches some desirable state.While termination has been studied extensively, many other liveness properties are important for concurrent programs.A formal proof method, based on temporal logic, for deriving liveness properties is presented.It allows a rigorous formulation of simple informal arguments.How to reason with temporal logic and how to use safety (invariance) properties in proving liveness is shown.The method is illustrated using, first, a simple programming language without synchronization primitives, then one with semaphores.However, it is applicable to any programming language.


title: Finite Differencing of Computable Expressions

authors:
Robert Paige
Shaye Koenig

abstract: Finite differencing is a program optimization method that generalizes strength reduction, and provides an efficient implementation for a host of program transformations including "iterator inversion."Finite differencing is formally specified in terms of more basic transformations shown to preserve program semantics.Estimates of the speedup that the technique yields are given.A full illustrative example of algorithm derivation is presented.


title: An O(n log n) Unidirectional Algorithm for the Circular Extrema Problem


title: Synchronization in Distributed Programs

abstract: A technique for solving synchronization problems in distributed programs is described.Use of this technique in environments in which processes may fail is discussed.The technique can be used to solve synchronization problems directly, to implement new synchronization mechanisms (which are presumably well suited for use in distributed programs), and to construct distributed versions of existing synchronization mechanisms.Use of the technique is illustrated with implementations of distributed semaphores and a conditional message-passing facility.


title: Some Observations Concerning Formal Differentiation of Set Theoretic Expressions

abstract: A variety of matters related to formal differentiation are considered.First, an algebraic approach to formal differentiation of a class of set theoretic expressions is suggested.Then the application of formal .differentiationto loop fusion is discussed.Finally, formal differentiation is applied to optimization of incremental construction of composite objects satisfying a given Predicate.The techniques developed are illustrated by transformational construction of a variety of algorithms.


title: Compact Storage of Binary Trees

abstract: Statistical measurements of the behavior of LISP programs have shown a marked asymmetry in the distribution of their data structures (binary trees).On the basis of a statistical model for such a distribution, we evaluate the expected storage cost of a representation of binary trees based on the use of k-pointer cells instead of conventional two-pointer ones.We conclude that LISP trees would be more efficiently encoded using three-pointer nodes.


title: Inessential Error Entries and Their Use in LR Parser Optimization

abstract: The use of "default reductions" in implementing LR parsers is considered in conjunction with the desire to decrease the number of states of the parser by making use of "don't-care" (also called "inessential" ) error entries.Default reductions are those which are performed independently of the lookahead string when other operations do not apply, and their use can lead to substantial savings in space and time.Don't-care error entries of an LR parser are those which are never consulted, and thus they can be arbitrarily replaced by nonerror entries in order to make a state compatible with another one.Determining don't-care error entries is most important in avoiding the growth of the size of the parser when eliminating reductions by single productions, that is, productions for which the right-hand side is a single symbol.The use of default reductions diminishes don't-care error entries.This effect is analyzed by giving a necessary and sufficient condition for an error entry to be don't-care when default reductions are used.As an application, elimination of reductions by single productions in conjunction with the use of default reductions is considered.


title: Using Peephole Optimization on Intermediate Code

authors:
Andrew S. Tanenbaum
Hans van Staveren
Johan W. Stevenson

abstract: Many portable compilers generate an intermediate code that is subsequently translated into the target machine's assembly language.In this paper a stack-machine-based intermediate code suitable for algebraic languages (e.g., PASCAL, C, FORTRAN) and most byte-addressed mini-and microcomputers is described.A table-driven peephole optimizer that improves this intermediate code is then discussed in detail and compared with other local optimization methods.Measurements show an improvement of about 15 percent, depending on the precise metric used.


title: Data Type Specification: Parameterization and the Power of Specification Techniques

authors:
James W. Thatcher
Eric G. Wagner
Jesse B. Wright

abstract: Our earlier work on abstract data types is extended by the answers to a number of questions on the power and limitations of algebraic specification techniques and by an algebraic treatment of parameterized data types like sets-of-( ) and stacks-of-().The "hidden function" problem (the need to include operations in specifications which are wanted hidden from the user) is investigated; the relative power of conditional specifications and equational specifications is investigated; and it is shown that parameterized specifications must contain "side conditions" (e.g., that finite-sets-of-d requires an equality predicate on d).


title: Deriving Target Code as a Representation of Continuation Semantics

abstract: Reynolds' technique for deriving interpreters is extended to derive compilers from continuation semantics.The technique starts by eliminating h-variables from the semantic equations through the introduction of special-purpose combinators.The semantics of a program phrase may be represented by a term built from these combinators.Then associative and distributive laws are used to simplify the terms.Last, a machine is built to interpret the simplified terms as the functions they represent.The combinators reappear as the instructions of this machine.The technique is illustrated with three examples.


title: Error Data Values in the Data-Flow Language VAL

abstract: The data-flow architecture is intended to support large scientific computations, and VAL is an algebraic, procedural language for use on a data-flow computer.VAL is apt for numerical computations but requires an error monitoring feature that can be used to diagnose and correct errors arising during program execution.Traditional monitoring methods (software traps and condition codes} are inappropriate for VAL; instead, VAL includes a set of error data values and an algebra for their manipulation.The error data values and their algebra are described and assessed; the conclusion is that error values provide a clean way for a high-level language to handle numeric (and some other) errors.


title: A Flexible Notation for Syntactic Definitions

abstract: Syntactic DefinitionsIn view of the proliferation of notations for defining the syntax of programming languages, it has been suggested that a simple notation should be adopted as a standard.However, any notation adopted as a standard should also be as versatile as possible.For this reason, a notation is presented here which is both simple and versatile and which has additional benefits when specifying the static semantic rules of a language.


title: On the Development of the Algebra of Functional Programs

abstract: The development of the algebraic approach to reasoning about functional programs that was introduced by Backus in his Turing Award Lecture is furthered.Precise definitions for the foundations on which the algebra is based are given, and some new expansion theorems that broaden the class of functions for which this approach is applicable are proved.In particular, the class of "overruntolerant" forms, nonlinear forms that include some of the familiar divide-and-conquer program schemes, are defined; an expansion theorem for such forms is proved; and that theorem is used to show how to derive expansions for some programs deemed by nonlinear forms.


title: An Effective Implementation for the Generalized Input-Output Construct of CSP

authors:
Gael N. Buckley
Abraham Silberschatz

abstract: Writing distributed algorithms in Hoare's CSP becomes more convenient if output statements are allowed in the guards of alternative and iterative commands.The major drawbacks of the previously published implementations of this construct are discussed.Criteria for an effective implementation are presented, and an algorithm that meets these criteria is constructed.


title: Eliminating Redundant Recursive Calls

abstract: CallsThe well-known recursive procedures to compute a given element of the Fibonacci series, to compute a binomial coefficient, and to solve the Towers of Hanoi puzzle define redundant computations.An invocation generally leads to many recursive calls with the same argument value.Such a redundant recursive procedure can be transformed into a nonredundant one when the operations appearing in the procedure have certain algebraic properties.The transformed programs avoid redundancy by saving exactly those intermediate results that will be needed again later in the computation.


title: Comparison of Compacting Algorithms for Garbage Collection

authors:
Jacques Cohen
Alexandru Nicolau

abstract: The relative efficiencies of four compactors of varisized cells are estimated by constructing their timeformulas.These are symbolic formulas expressing execution times as functions of the time to perform common, elementary operations such as assignment, addition, subscripting, and loop overhead.By binding the variables to numeric values corresponding to a specific machine one can estimate program execution times without resorting to empirical tests.The first of the compactors (Lisp 2) requires additional storage for pointer readjustment.The second (based on the work of Haddon and Waite) attempts to reduce these storage requirements at the expense of processing time.The last two (Morris' and Jonkers') are recently proposed compactors that require minimal additional storage and that update pointers by first threading them into linear lists.The paper provides unified descriptions of the algorithms and presents curves expressing the relative efficiencies of the compactors when run on a specific machine (PDP-10).It is straightforward to modify the given formulas to estimate compactors' efficiencies when run on other computers.


title: Parallel Generation of Postfix and Tree Forms

authors:
Eliezer Dekel
Sartaj Sahni

abstract: Efficient parallel algorithms to obtain the postfLx and tree forms of an infix arithmetic expression are developed.The shared memory model of parallel computing is used.


title: Experience with the SETL Optimizer

authors:
Stefan M. Freudenberger
Jacob T. Schwartz
Micha Sharir

abstract: The structure of an existing optimizer for the very high-level, set theoretically oriented programming language SETL is described, and its capabilities are illustrated.The use of novel techniques (supported by state-of-the-art interprocedural program analysis methods) enables the optimizer to accomplish various sophisticated optimizations, the most significant of which are the automatic selection of data representations and the systematic elimination of superfluous copying operations.These techniques allow quite sophisticated data-structure choices to be made automatically.


title: A Distributed Algorithm for Minimum-Weight Spanning Trees

authors:
Robert G. Gallager
Pierre A. Humblet
Philip M. Spira

abstract: A distributed algorithm is presented that constructs the minimum-weight spanning tree in a connected undirected graph with distinct edge weights.A processor exists at each node of the graph, knowing initially only the weights of the adjacent edges.The processors obey the same algorithm and exchange messages with neighbors until the tree is constructed.The total number of messages required for a graph of N nodes and E edges is at most 5N log2N + 2E, and a message contains at most one edge weight plus log28N bits.The algorithm can be initiated spontaneously at any node or at any subset of nodes.


title: Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability

abstract: In this paper the problems of parameter passing and implementation for parameterized algebraic specifications are studied on a proof theoretic level.A syntactic equivalent to the semantic notion of persistency deemed by the ADJ group is introduced for parameterized specifications.It is shown to lead to similar results concerning the correctness of parameter passing and the nesting of parameters.Then a formal notion of implementation is developed for persistent specifications.It allows for developing implementations in a stepwise fashion.Moreover, implementations for instantiations (i.e., specifications that result from applying a parameterized specification to an actual parameter) can be constructed mechanically from given implementations for the specification procedure and the actual parameter.Correctness of implementation is required only with respect to observable properties of a specification, so an increased amount of optimization is allowed.


title: A Formal Framework for the Derivation of Machine-Specific Optimizers

abstract: The derivation of machine-specific code optimizers starts from a description of the target machine.A formal instruction-set semantics precisely defmes the concepts characteristic to the machine-code level, such as addressing modes and instructions, side effects, and overlapping of registers or memory cells.The context information relevant for local optimizations is defined by abstract interpretation of instruction semantics.This leads to a notion of instruction equivalence relative to a given context.Based on this notion, optimization rules whose machine-specific applicability criteria can be derived automatically are introduced.The formal nature of this approach serves not only to guarantee the correctness of these criteria, but also to isolate program-dependent from only machine-dependent aspects.This leads to criteria which are most efficient in the sense that they only contain subconditions that must in fact be evaluated at optimization time, while those referring to properties of the instruction set only are folded away in the derivation process.


title: Basic Techniques for the Efficient Coordination of Very Large Numbers of Cooperating Sequential Processors

authors:
Allan Gottlieb
Boris D. Lubachevsky
Larry Rudolph

abstract: In this paper we implement several basic operating system primitives by using a "replace-add" operation, which can supersede the standard "test and set" and which appears to be a universal primitive for efficiently coordinating large numbers of independently acting sequential processors.We also present a hardware implementation of replace-add that permits multiple replace-adds to be processed nearly as efficiently as loads and stores.Moreover, the crucial special case of concurrent replace-adds updating the same variable is handled particularly well: If every processing element simultaneously addresses a replace-add at the same variable, all these requests are satisfied in the time required to process just one request.


title: Termination of Probabilistic Concurrent Program

authors:
Sergiu Hart
Micha Sharir
Amir Pnueli

abstract: The asynchronous execution behavior of several concurrent processes, which may use randomization, is studied.Viewing each process as a discrete Markov chain over the set of common execution states, necessary and sufficient conditions are given for the processes to converge almost surely to a given set of goal states under any fair, but otherwise arbitrary, schedule, provided that the state space is finite.(These conditions can be checked mechanically.)An interesting feature of the proof method is that it depends only on the topology of the transitions and not on the actual values of the probabilities.It is also shown that in this model synchronization protocols that use randomization are in certain cases no more powerful than deterministic protocols.This is demonstrated by (1) establishing lower bounds, similar to those known for deterministic protocols, on the size of a shared variable necessary to ensure mutual exclusion and lockout-free behavior of a "randomized" protocol and ( 2) showing that no fully symmetric "randomized" protocol can ensure mutual exclusion and freedom from lockout.


title: Postpass Code Optimization of Pipeline Constraints

authors:
John L. Hennessy
Thomas R. Gross

abstract: Pipeline interlocks are used in a pipelined architecture to prevent the execution of a machine instruction before its operands are available.An alternative to this complex piece of hardware is to rearrange the instructions at compile time to avoid pipeline interlocks.This problem is called code reorganization and is studied here.The basic problem of reorganization of machine-level instructions at compile time is shown to be NP-complete.A heuristic algorithm is proposed, and its properties and effectiveness are explored.Empirical data from MIPS, a VLSI processor design, are given.The impact of code reorganization techniques on the rest of a compiler system is discussed.


title: Tentative Steps Toward a Development Method for Interfering Programs

abstract: Development methods for (sequential) programs that run in isolation have been studied elsewhere.Programs that run in parallel can interfere with each other, either via shared storage or by sending messages.Extensions to earlier development methods are proposed for the rigorous development of interfering programs.In particular, extensions to the specification method based on postconditions that are predicates of two states and the development methods of operation decomposition and data refinement are proposed.


title: Final Data Types and Their Specification

abstract: A data type specification is a description of the properties of a data abstraction for the benefit of its users and implementers.The data abstraction has realizations, all of which behave in a certain way.It is those properties implied by this behavior which we consider essential; properties specific to some realization are extraneous.The specification problem is to present all of the essential properties and no extraneous ones.We propose a specification method based upon the notion of "final data type."A final data type is the smallest structure having a given behavior; every other structure having that behavior maps onto it homomorphically.This property makes the final data type specification a particularly good source of information about the abstraction it realizes, and eliminates "implementation bias" from the method.


title: Access-Right Expressions

authors:
Richard B. Kieburtz
Abraham Silberschatz

abstract: data types, and in particular those that are designed to provide resources for use by concurrently executable programs, are often designed to be used only in certain ways.The intended constraints on use of an instance of such a type can be expressed in two principal ways: as assertions on the domain of values input to each operator, and as constraints on the sequences in which the operators of the type can be called by a customer process.These constraints must be enforced in the environment in which an instance of the type is used.Nevertheless, they are very much a part of the type specification, for its definition is not complete, nor can the consistency of its representation be proved, without them.A notation is provided in which to express sequential constraints, which are here called accessright expressions.It is suggested that these expressions should be declared in a programming language that supports the definition of monitors or resource managers.Implications for the proof rules of monitors are discussed, and suggestions are made for a programming language implementation.


title: Specifying Concurrent Program Modules

abstract: Concurrent Program ModulesA method for specifying program modules in a concurrent program is described.It is based upon temporal logic, but uses new kinds of temporal assertions to make the specifications simpler and easier to understand.The semantics of the specifications is described informally, and a sequence of examples are given culminating in a specification of three modules comprising the alternating-bit communication protocol.A formal semantics is given in the appendix.


title: VLSI Layout as Programming

authors:
Richard J. Lipton
Jacobo Valdes
Gopalakrishnan Vijayan
Stephen C. North
Robert Sedgewick

abstract: The first component of a VLSI (very large-scale integration) design environment being built at Princeton University is described.The general theme of this effort is to make the design of VLSI circuits as similar to programming as possible.The attempt is to build tools that do for the VLSI circuit designer what the best software tools do for the implementer of large software systems.


title: Guardians and Actions: Linguistic Support for Robust, Distributed Programs

authors:
Barbara Liskov
Robert Scheifler

abstract: An overview is presented of an integrated programming language and system designed to support the construction and maintenance of distributed programs: programs in which modules reside and execute at communicating, but geographically distinct, nodes.The language is intended to support a class of applications concerned with the manipulation and preservation of long-lived, on-line, distributed data.The language addresses the writing of robust programs that survive hardware failures without loss of distributed information and that provide highly concurrent access to that information while preserving its consistency.Several new linguistic constructs are provided; among them are atomic actions, and modules called guardians that survive node failures.


title: Automatic Program Improvement: Variable Usage Transformations

authors:
B. Maher
Derek H. Sleeman

abstract: The design objective of the Leeds Transformation System is to transform existing programs, written in a variety of languages, into "tidier" programs.The total system was conceived of as having three phases: syntactic transformations, variable usage transformations, and synthesizing features.Because programmers vary greatly in what they consider to be a more acceptable form, we have aimed to make the system as data driven as possible.(That also enables us to deal with a variety of programming languages.)The paper reviews the first two phases, reports the second in some detail, and illustrates the use of the system on an ALGOL 60 program.Redundant assignments, redundant variables, and loop-invariant statements are discovered by means of a novel approach which represents variable usage within a program as a correspondence matrix.Potential enhancements of the system are also discussed.


title: On the Construction of Submodule Specifications and Communication Protocols

authors:
Philip M. Merlin
Gregor von Bochmann

abstract: The problem of elaborating the specification for the submodules of a system is considered.A new method for the construction of submodule specifications is described.If the system is to consist of n submodules and the system as well as (n -1) submodules are specified, then the method described determines the specification of the additional nth submodule.A formula is given which defines the specification of the additional submodule in the general case where module specifications are given in terms of sets of possible execution sequences, and interaction occurs when several modules participate in the execution of an atomic interaction.For the restricted context of finite-state machines, a constructive algorithm for the evaluation of the formula is given.The use of this design method is demonstrated by examples, including a simple communication protocol involving error detection and retransmission.Possible applications in other areas, as well as remaining problems, are indicated.


title: Correctness Proofs of Communicating Processes: Three Illustrative Examples from the Literature

abstract: The proof method for networks of processes proposed by Misra and Chandy is demonstrated on three examples from the literature.It is shown that this method is easy to use, preserves process autonomy in the network proof, and conforms naturally to the hierarchical structure of the network.Two very large-scale integration algorithms and a sorting network are presented in Hoare's communicating sequential processes model, specified completely, and formally proved.


title: Concurrent Reading While Writing

abstract: While WritingThe problem of asynchronous processes reading shared data while the data are being modified by another process is considered.This problem differs from the standard readers/writers problem in that concurrent reading while writing is allowed.The model used here strongly limits the use and size of the shared variables.If multiple copies of the shared data are allowed, then simple, efficient solutions are found.In general, solutions which are more time efficient because they avoid waiting are seen to require more copies of the shared data.The number of copies used by all algorithms is shown to be the best possible.The main solution demonstrates that any system of processes which uses large distributed variables can be strongly simulated by a system which uses only binary distributed variables.


title: A New Solution to Lamport's Concurrent Programming Problem Using Small Shared Variables

abstract: Concurrent Small SharedA new solution to the concurrent programming control (mutual exclusion) problem that is immune to process failures and restarts is presented.The algorithm uses just four values of shared memory per process, which is within one value of the known lower bound.The algorithm is implemented using two binary variables that make it immune to read errors occurring during writes, that is, "flickering bits."


title: Generation of Compiler Symbol Processing Mechanisms

abstract: Compiler symbol processing has become complex as programming languages have evolved.In this paper we describe a comprehensive model of symbol processing, and a system that uses this model to generate the symbol processing portions of a compiler from simple specifications.The model supports a variety of entities with different types of names.It includes a detailed view of scoping.It provides a simple picture of the complex mapping from a source token to a specific entity.The model is illustrated with examples from Ada.The system is divided into two parts.The first takes a nonprocedural description of the semantics of symbols in the language and produces a symbol table module for a compiler for that language.The second supports a simple symbol processing language that allows the easy connection of syntax and semantic processing to the symbol module.


title: Incremental Context-Dependent Analysis for Language-Based Editors

authors:
Thomas W. Reps
Tim Teitelbaum
Alan J. Demers

abstract: Knowledge of a programming language's grammar allows language-based editors to enforce syntactic correctness at all times during development by restricting editing operations to legitimate modifications ot ~ the program's context-free derivation tree; however, not all language constraints can be enforced in this way because not all features can be described by the context-free formalism.Attribute grammars permit context-dependent language features to be expressed in a modular, declarative fashion and thus are a good basis for specifying language-based editors.Such editors represent programs as attributed trees, Which are modified by operations such as subtree pruning and grafting.Incremental analysis is performed by updating attribute values after every modification.This paper discusses how updating can be carried out and presents several algorithms for the task, including one that is asymptotically optimal in time.


title: Control Flow Aspects of Semantics-Directed Compiling

abstract: This paper is a demonstration of a semantics-directed compiler generator.We focus on the part of a compiler between syntax analysis and code generation.A language is specified by adding semantic rules in a functional notation to the syntax of the language.Starting with a small sublanguage of while statements, statement constructs of the C programming language are added in stages.Using a small ad hoc code generator, a compiler is automatically constructed from the semantics.The semantic description is analogous to a syntax-directed construction of a flow diagram for a program.By analogy with grammars and parser generators, minimal knowledge of the underlying theory is required.For the control flow aspects of languages, efficient compilers can quickly be generated.


title: A Syntax-Error-Handling Technique and Its Experimental Analysis

authors:
Seppo Sippu
Eljas Soisalon-Soininen

abstract: A syntax-error-handling technique is defined as an extension of LR parsing.The technique is automatic, and the generation of the error-handling algorithm is based only on the context-free grammar and the lexical description of the language.The heart of the algorithm is a "phrase-lever' error-recovery strategy, which is an improvement upon the basic strategy of Leinius.The notion of phrase-level recovery is further generalized such that "local correction" is included within the basic framework.Special attention is paid to diagnostic aspects, such as the generation of descriptive recovery-independent error messages.The technique has been implemented in the compiler-writing system HLP (Helsinki Language Processor).Promising experimental results have been obtained by testing the technique with erroneous student-written ALGOL and Pascal programs.


title: User Format Control in a Lisp Prettyprinter

abstract: A LISP prettyprinter is presented that makes it easy for a user to control the format of the output produced.The printer can be used as a general mechanism for printing data structures as well as programs.It is divided into two parts: a set of formatting functions and an output routine.The user specifies how a particular type of object should be formatted by creating a formatting function for the type.When an object of that type is passed to it, the formatting function creates a sequence of directions that specify how the object should be printed if it can fit on one line and how it should be printed if it must be broken up across multiple lines.A simple template language makes it easy to specify these directions.Based on the line length available, the output routine decides what structures have to be broken up across multiple lines and produces the actual output following the directions created by the formatting functions.The paper concludes with a discussion of how the prettyprinting method presented could be applied to languages other than LISP.


title: Assessing Test Data Adequacy through Program Inference

abstract: Despite the almost universal reliance on testing as the means of locating software errors and its long history of use, few criteria have been proposed for deciding when software has been thoroughly tested.As a basis for the development of usable notions of test data adequacy, an abstract definition is proposed and examined, and approximations to this definition are considered.


title: Encapsulation Constructs in Systems Programming Languages

authors:
William F. Appelbe
Anders P. Ravn

abstract: This paper investigates the desirable properties of programming language constructs that support encapsulation of environments and abstract data types.These properties are illustrated by using a simple multiuser file system as a model.The requirements for such a file system are outlined; then the model file system design is described by a hierarchy of encapsulated abstract data types and environments.The high-level language constructs necessary to directly implement the model file system design are identified.It is concluded that environment encapsulation and abstract data types must be supported by different constructs, and the desirable properties of such constructs are outlined.A superset of Ada e that effectively supports both environments and abstract data types is introduced and used to implement the model file system.The encapsulation constructs of several modern systems programming languages are evaluated.Each of these languages is shown to be insufficient for a direct implementation of the model file system design.


title: Modeling the Distributed Termination Convention of CSP

authors:
Krzysztof R. Apt
Nissim Francez

abstract: 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.


title: User Recovery and Reversal in Interactive Systems

authors:
James E. Archer Jr.
Richard Conway
Fred B. Schneider

abstract: Interactive systems, such as editors and program development environments, should explicitly support facilities that permit a user to reverse the effects of past actions and to restore an object to a prior state.A model for interactive systems that allows such recovery facilities to be defined precisely and user and system responsibilities to be delineated is presented.Various techniques for implementing recovery are described.Application of a general recovery facility to support reverse execution is discussed.A program development system (called COPE} with extensive recovery facilities, including reverse execution, is described.


title: Global Data Flow Analysis Problems Arising in Locally Least-Cost Error Recovery

abstract: Locally least-cost error recovery is a technique for recovering from syntax errors by editing the input string at the point of error detection.A scheme for its implementation in recursive descent parsers, which in principle embodies a process of passing a parameter to each procedure in the parser for each terminal symbol in the grammar, has been suggested.For this scheme to be practical it is vital that as much parameterization as possible is eliminated from the recursive descent parser.This oPtimization problem and how it may be split into three separate global data flow analysis problems-classifying terminal symbols and the so-called min and max follow cost problems--are discussed.The max follow cost problem is a particularly difficult one to solve.The application of Gaussian elimination to its solution is shown by expressing it as a continuous data flow problem, and it is also related to an "idiosyncratic" data flow problem arising in the optimization of very high level languages.Classifying terminal symbols is also difficult since the problem is unsolvable in general.However, for the class of LL(1) grammars, the problem is shown to be expressible as a distributive data flow problem and so may be solved using, say, Gauss-Seidel iteration.


title: Algorithms for On-the-fly Garbage Collection

abstract: A new algorithm is described for on-the-fly garbage collection.The new algorithm uses only two colors and has a simple correctness proof.Two variations on the algorithm are then derived: One attempts to minimize the amount of marking that must be done, and the other is an incremental garbage collector.


title: The Promotion and Accumulation Strategies in Transformational Programming

abstract: The promotion strategy in transformational programming is a general method for achieving efficiency by exploiting the recursive structure in the dominant term of an algorithmic expression.For it to be carried out successfully, the original problem often has to be generalized by the inclusion of an extra parameter, a technique known as accumulation.These strategies are illustrated by deriving algorithms for two nontrivial problems: (1) determining whether a given digraph is acyclic, and (2) constructing the longest subsequence of a given sequence of vertices that forms a connected path in a given digraph.The derivations also serve to emphasize the usefulness of certain notational devices in applicative expressions, especially infix operators.Not only do such operators enhance the succinctness and readability of expressions, they also allow many transformations to be formulated as algebraic laws about their distributive and other properties.


title: An APL Compiler for a Vector Processor

abstract: Although vector processors have been available for over a decade, the software necessary to make effective use of these facilities has generally not been available.In this paper the design of a compiler for the programming language APL, which produces code that allows most operations to be performed in parallel, is described.This design is based on a similar sequential compiler currently in use.Both compilers use a technique called dragthrough to reduce the size of intermediate values generated during the course of execution.


title: Annotations to Control Parallelism, Reduction Order in the Distributed Evaluation of Functional Programs

abstract: When evaluating a functional program on a network of processors, it is necessary to decide when parallelism is desirable, which work may be transferred to another processor, and in what form the work is to be transferred.If the wrong decisions are made, a parallel evaluation may require asymptotically more time than a sequential evaluation, owing to communication costs.The introduction of annotations to give the programmer control over the above decisions is proposed.The annotations and their effects are defined in terms of the lambda calculus.Each application must have one of three annotations.No other annotations are required.Examples and possible extensions to this work, including annotated combinators, are briefly considered.


title: Grammar-Based Definition of Metaprogramming Systems

authors:
Robert D. Cameron
Mabo Robert Ito

abstract: A metaprogramming system is a programming facility (subprogramming system or language) whose basic data objects include the programs and program fragments of some particular programming language, known as the target language of the system.Such systems are designed to facilitate the writing of metaprograms, that is, programs about programs.Metaprograms take as input programs and fragments in the target language, perform various operations on them, and possibly generate modified target-language programs as output.A grammar-based approach to the specification of the syntactic-manipulation component of a metaprogramming system is described.The method derives the specifications for a set of programmanipulating subprograms from an augmented BNF grammar for the target language.The method is applicable to any programming language and is illustrated in its particular application to Pascal.


title: The Drinking Philosopher's Problem

authors:
K. Mani Chandy
Jayadev Misra

abstract: 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.


title: Recursion As an Effective Step in Program Development

abstract: A general translation rule from recursive procedures to iterative ones is augmented by also translating the correctness proof.The augmented translation rule is defined within the framework of Pascal programs, with the correctness proof expressed in the Hoare style.The translation is consistent with the stepwise development of Pascal programs.Moreover the translation can be done automatically provided that the assertions are expressed in a formal specification language.Given are a few simplification rules, whose applicability, after the translation, is easily detectable and strongly suggested by the translated assertions.It is shown that the particular cases of linear, tail, and simple recursion (which are known to be easily handled and simplified when expressed in a schematic functional notation) can be simplified automatically after the translation step without leaving the Pascal language.Two examples are provided to show that the given simplification rules can also effectively apply to more general recursive procedures.


title: The Type Theory of PL/CV3

authors:
Robert L. Constable
Daniel R. Zlatin

abstract: article Free Access Share on The Type Theory of PL/CV3 Authors: Robert L. Constable Department of Computer Science, 405 Upson Hall, Cornell University, Ithaca, N.Y. Department of Computer Science, 405 Upson Hall, Cornell University, Ithaca, N.Y.View Profile , Daniel R. Zlatin Department of Computer Science, 405 Upson Hall, Cornell University, Ithaca, N.Y. Department of Computer Science, 405 Upson Hall, Cornell University, Ithaca, N.Y.View Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 6Issue 1Jan. 1984 pp 94–117https://doi.org/10.1145/357233.357238Online:01 January 1984Publication History 25citation305DownloadsMetricsTotal Citations25Total Downloads305Last 12 Months12Last 6 weeks2 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 Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Code Selection through Object Code Optimization

authors:
Jack W. Davidson
Christopher W. Fraser

abstract: This paper shows how thorough object code optimization has simplified a compiler and made it easy to retarget.The code generator forgoes case analysis and emits naive code that is improved by a retargetable object code optimizer.With this technique, cross-compilers have been built for seven machines, some in as few as three person days.These cross-compilers emit code comparable to hostspecific compilers.


title: Optimization of Parser Tables for Portable Compilers

authors:
Peter Dencker
Karl Dürre
Johannes Heuft

abstract: Six methods for parser table compression are compared.The investigations are focused on four methods that allow the access of table entries with a constant number of index operations.The advantage of these methods is that the access to the compressed tables can be programmed efficiently in portable high-level languages like Pascal or FORTRAN.The results are related to two simple methods based on list searching.Experimental results on eleven different grammars show that, on the average, a method based on graph coloring turns out best.


title: Transformations and Reduction Strategies for Typed Lambda Expressions

abstract: A scheme is described that allows languages supporting higher order functions to be efficiently implemented using a standard run-time stack.A machine for evaluating typed lambda expressions is first constructed.In essence, the machine simply extends the standard SECD machine to allow partial application of abstractions representing multiadic functions.Some transformations of these typed lambda expressions into a so-called simple form are then described.Evaluation of simple-form expressions on the extended SECD machine produces stacklike environment structures rather than the treelike structures produced by expressions of arbitrary form.This allows implementation of the machine using a standard runtime stack.The SECD machine is then further modified so that closures are applied "in situ" rather than returned as values.The order of reduction is also changed so that the evaluation of function-valued expressions is deferred until they can be applied to sufficient arguments to allow reduction to nonfunctional values.It is shown that this function-deferring machine can be implemented using a standard run-time stack and thus can evaluate arbitrary lambda expressions without prior transformation to simple form.Finally, application of the above schemes to standard programming languages, such as ALGOL, Pascal, Ada, and LISP, is considered.


title: A Directly Executable Encoding for APL

abstract: A canonical internal form for APL is derived.A directly executable language (ADEL) follows DEL principles first developed by Flynn and Hoevel.APL usage statistics are reported and used to help determine an efficient encoding strategy.Two execution models are discussed.The models show that for a vector-oriented host machine, the use of expression temporaries may be ~nore efficient, not less efficient as expected for a scalar-oriented host.


title: Communicating Sequential Processes for Centralized and Distributed Operating System Design

authors:
M. Elizabeth C. Hull
R. M. McKeag

abstract: This paper demonstrates how the notation of Communicating Sequential Processes may be used in the design of an operating system.It goes further to show how such an approach assists in the design and development of a system distributed over a network of computers.The technique uses a welldefined design methodology.


title: Proving Failure-Free Properties of Concurrent Systems Using Temporal Logic

abstract: In a failure-free concurrent system, no process is delayed forever by any of the system synchronization primitives.Previously, it was difficult to prove even the simplest concurrent system failure free, let alone attempt such a proof for a "real" operating system.First for semaphores and then for monitors, necessary and sufficient conditions for failure-free systems are derived.In both cases, the important properties of the system are stated using temporal logic, a concise formalism that allows reasoning about the future progress of program computations.Temporal logic permits a precise and explicit statement of exactly those properties necessary to establish that a concurrent system is truly failure free.In conclusion, a short example is given and then the applicability of these results to several existing systems and languages (UNIX o, MODULA and MESA) is examined.


title: Translation of Attribute Grammars into Procedures

abstract: An efficient method for evaluating attribute grammars by translating them into sets of procedures is presented.The basic idea behind the method is to consider nonterminal symbols of the grammar as functions that map their inherited attributes to their synthesized attributes.Associated with the nonterminal symbols are procedures that realize the functions.The attribute grammar is translated into a program consisting of these procedures.The essential point about this method is that attribute grammars are completely compiled into procedures, in contrast with evaluation algorithms that work interpretively in a table-driven manner.No information is stored in the nodes of derivation trees.Although this evaluation method is applicable principally to absolutely noncircular attribute grammars in which the dependency relation among attribute occurrences of every production rule does not contain cycles, it is shown how the method is extended to the general noncircular attribute grammars.Problems of evaluating a set of attributes simultaneously and of recursive descent evaluation are also discussed.


title: Tailored-List and Recombination-Delaying Buddy Systems

abstract: Two improved variations of the binary buddy system for dynamic memory management, the tailoredlist buddy system (TLBS) and the recombination-delaying buddy system (RDBS), are introduced.In an attempt to save on execution time, these variations do not recombine free buddies every time recombination is possible.In the TLBS recombination is delayed in such a way as to tailor the available free-space lists to the request-size distribution.In the RDBS time is saved by recombining buddies only when larger blocks are unavailable during allocation.Comparative simulation experiments indicate that for not very heavy loads the TLBS is slightly faster than the RDBS, which, in turn, is significantly faster than the traditional system.Since no significant variation has been found among the memory utilizations of the three systems, the TLBS is preferable to the other systems provided that the load is not very heavy and the expected requestsize distribution is at hand.Otherwise, the RDBS is recommended.


title: Distributed Algorithms for Finding Centers and Medians in Networks

authors:
Ephraim Korach
Doron Rotem
Nicola Santoro

abstract: The problem of determining in a distributed fashion the centers and the medians of a network is considered.Lower bounds on the time needed to solve these problems are proved.Algorithms that achieve those bounds for tree networks are presented; the number of exchanged messages is linear in the number of nodes.These techniques are extended to work on general networks in O(n) time units exchanging O(n.e) messages, where n is the number of nodes and e the number of edges in the network.In addition, a comparison with a simple heuristic approach is included.


title: Comments on Soisalon-Soininen's "Inessential Error Entries"

abstract: article Free Access Share on Technical Correspondence: Comments on Soisalon-Soininen's ``Inessential Error Entries and Their Use in LR Parser Optimization'' Author: Wilf R. LaLonde School of Computer Science, Carleton University, Colonel By Drive, Ottawa, Canada K1S 5B6 School of Computer Science, Carleton University, Colonel By Drive, Ottawa, Canada K1S 5B6View Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 6Issue 3pp 432–439https://doi.org/10.1145/579.357255Published:01 July 1984Publication History 0citation244DownloadsMetricsTotal Citations0Total Downloads244Last 12 Months8Last 6 weeks2 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 SiteeReaderPDF


title: Using Time Instead of Timeout for Fault-Tolerant Distributed Systems

abstract: A general method is described for implementing a distributed system with any desired degree of faulttolerance.Instead of relying upon explicit timeouts, processes execute a simple clock-driven algorithm.Reliable clock synchronization and a solution to the Byzantine Generals Problem are assumed.


title: The "Hoare Logic" of CSP, and All That

authors:
Leslie Lamport
Fred B. Schneider

abstract: Generalized Hoare Logic is a formal logical system for deriving invariance properties of programs.It provides a uniform way to describe a variety of methods for reasoning about concurrent programs, including noninterference, satisfaction, and cooperation proofs.We describe a simple recta-rule of the Generalized Hoare Logic--the Decomposition Principle--and show how all these methods can be derived using it.


title: Synthesis of Communicating Processes from Temporal Logic Specifications

authors:
Zohar Manna
Pierre Wolper

abstract: In this paper, Propositional Temporal Logic (PTL) is applied to the specification and synthesis of the synchronization part of communicating processes.To specify a process, a PTL formula that describes its sequence of communications is given.The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL.This model can then be interpreted as a program.


title: Selective and Locally Controlled Transport of Privileges

abstract: In a system based on authorization, the ability of a subject to operate on the system is a function of the privileges that he possesses.In this paper a mechanism, called Send-Receive, for the transport of such privileges, is introduced and studied.The control provided by this mechanism over the movement of privileges has two notable properties.--The control is selective, in the sense that it permits the creation of transport channels, which allow for the movement of only certain types of privileges and only between certain kinds of subjects.--The control is local, in the sense that every movement of privileges into and out of the domain of a given subject must be authorized by privileges already in his domain.The proposed transport mechanism is shown to allow the imposition of a local upper bound on the power of any given subject.This bound is independent of the rest of the system and can, therefore, be viewed as an intrinsic property of the subject.The ability to impose such bounds is considered essential for effective modularization of computer systems.In addition, the locality of our control has beneficial global effects on the flow of privileges.In particular, it helps remove the undesirable symmetry of transport, exhibited by the conventional Take-Grant mechanism.


title: Jump Minimization in Linear Time

authors:
M. V. S. Ramanath
Marvin H. Solomon

abstract: Unlike other instructions, which compute or test values, unconditional branch instructions do no useful work.Rather, they are artifacts of the translation from a flow graph to the linear form of conventional machine language.Careful ordering of the basic blocks of a program can decrease the number of branches required by allowing a basic block to "fall through" to a successor.It is shown that although the general problem of minimizing the number of branches is NP-complete, an efficient algorithm is possible for "structured" programs--those written without goto statements.More specifically, an algorithm is presented that produces an optimal ordering of the basic blocks of any program that uses only the control structures if-then-else, loop, and exit.The running time of the algorithm is proportional to the length of the program, provided the number of loops exited by any exit statement can be bounded by a constant.


title: Real-Time Synchronization of Interprocess Communications

authors:
John H. Reif
Paul G. Spirakis

abstract: This paper considers a fixed (possibly infinite) set of distributed asynchronous processes, which at various times are willing to communicate with each other.Each process has various ports, each of which is used for communication with a distinct neighbor process.Each process can have at most one port open at any time, and its other ports must be closed.Two processes handshake over a time interval A if their respective ports are open for mutual communication during this interval.Note that the handshake relation is a matching.Successful communication requires a handshake of at least one step of each process; during the one-step overlap a message can be transmitted between processes.The problem is to synchronize processes (via a distributed scheduler) so that they can successfully handshake at their will, given that the means of synchronization is some low-level construct that does not guarantee the handshake property if used in an unsophisticated way.Probabilistic distributed algorithms for synchronizing processes so that they can handshake at will are described.A process is considered to be tame over a time interval A if its speed varies within certain arbitrarily fixed nonzero bounds.Our synchronization algorithms are shown to have real-time response: If a pair of processers are mutually willing to communicate within a time interval A of length at least a given constant and the pair are tame on A, then they establish communication within A with high likelihood (for the worst case behavior of the system), and the expected time for establishment of communication is also constant.Our model and algorithms are applied to solve a large class of real-time resource allocation problems, as well as real-time implementation of the synchronization primitives of Hoare's multiprocessing language CSP.


title: Using Message Passing for Distributed Programming: Proof Rules, Disciplines

authors:
Richard D. Schlichting
Fred B. Schneider

abstract: Inference rules are derived for proving partial correctness of concurrent programs that use message passing.These rules extend the notion of a satisfaction proof, first proposed for proving correctness of programs that use synchronous message-passing, to asynchronous message-passing, rendezvous, and remote procedures.Two types of asynchronous message-passing are considered: unreliable datagrams and reliable virtual circuits.The proof rules show how interference can arise and be controlled.


title: Axiomatic Semantics of Communicating Sequential Processes

abstract: A simple definition of the axiomatic semantics of Communicating Sequential Processes is presented.The most important aspect of the approach is that it allows dealing with the individual processes of a program in isolation from the other processes.The axiomatic semantics is used to prove the correctness of a program for partitioning sets.


title: Magma2: A Language Oriented toward Experiments in Control

abstract: article Free Access Share on Magma2: a language oriented toward experiments in control Author: Franco Turini Univ. di Pisa, Pisa, Italy Univ. di Pisa, Pisa, ItalyView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 6Issue 4Oct. 1984 pp 468–486https://doi.org/10.1145/1780.1784Published:01 October 1984Publication History 8citation277DownloadsMetricsTotal Citations8Total Downloads277Last 12 Months18Last 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 SiteeReaderPDF


title: Unassigned Objects

abstract: There are various ways in which programming languages may deal with the use of objects that have no value.They may or may not treat such uses as errors and may or may not trap such errors.The evolution from the preliminary version of Ada TM to the 1980 version and then to the 1982 version is a case in point.A basis for investigation resting on the desire for more reliable software is presented.Ways of declaring types with and without the value unassigned, derivations from such types, and the meaning of unassigned for composite types are all investigated.Static and dynamic assignment of the value unassigned are introduced, and the interaction of these with other design factors, especially unassigned composite objects, is detailed.It is shown that the typical dual view of composite objects, both as objects and composites of other objects, leads to inconsistencies in the dynamic treatment of unassigned composites and to significant implementation inefficiencies.


title: Procedures as Persistent Data Objects

authors:
Malcolm P. Atkinson
Ronald Morrison

abstract: A persistent programming environment, together with a language that supports first class procedures, may be used to provide the semantic features of other object modeling languages. In particular, the two concepts may be combined to implement abstract data types, modules, separate compilation, views, and data protection. Furthermore, the ideas may be used in system construction and version control, as demonstrated here.


title: Describing and Analyzing Distributed Software System Designs

authors:
George S. Avrunin
Jack C. Wileden

abstract: In this paper we outline an approach to describing and analyzing designs for distributed software systems. A descriptive notation is introduced, and analysis techniques applicable to designs expressed in that notation are presented. The usefulness of the approach is illustrated by applying it to a realistic distributed software-system design problem involving mutual exclusion in a computer network.


title: Optimal Parallel Generation of a Computation Tree Form

authors:
Ilan Bar-On
Uzi Vishkin

abstract: Given a general arithmetic expression, we find a computation binary tree representation in O (log n ) time using n /log n processors on a concurrent-read, exclusive-write, parallel random-access machine. A new algorithm is introduced for this purpose. Unlike previous serial and parallel solutions, it is not based on using a stack.


title: On Convergence Toward a Database of Program Transformations

abstract: Several fairly large sets of programming rules have been developed recently. It is natural to ask whether the process of developing such rule bases may converge. Having developed sets of rules for specific programming tasks and domains, will they be helpful when other tasks and domains are considered? While it is too early to give definitive answers, experience with the rules of the PECOS system has been positive. Both during the process of developing the rule set and while developing rules for another domain, the existence of already codified rules proved very helpful.


title: Proofs as Programs

authors:
Joseph L. Bates
Robert L. Constable

abstract: The significant intellectual cost of programming is for problem solving and explaining, not for coding. Yet programming systems offer mechanical assistance for the coding process exclusively. We illustrate the use of an implemented program development system, called PRL ("pearl"), that provides automated assistance with the difficult part. The problem and its explained solution are seen as formal objects in a constructive logic of the data domains. These formal explanations can be executed at various stages of completion. The most incomplete explanations resemble applicative programs, the most complete are formal proofs.


title: Information-Flow and Data-Flow Analysis of while-Programs

authors:
Jean-Francois Bergeretti
Bernard Carré

abstract: Until recently, information-flow analysis has been used primarily to verify that information transmission between program variables cannot violate security requirements. Here, the notion of information flow is explored as an aid to program development and validation. Information-flow relations are presented for while-programs, which identify those program statements whose execution may cause information to be transmitted from or to particular input, internal, or output values. It is shown with examples how these flow relations can be helpful in writing, testing, and updating programs; they also usefully extend the class of errors which can be detected automatically in the “static analysis” of a program.


title: Addendum to "The Promotion and Accumulation Strategies in Transformational Programming"


title: Side Effects and Aliasing Can Have Simple Axiomatic Descriptions

abstract: We present a different style of axiomatic definition for programming languages. It is oriented toward imperative languages, such as Algol 68, that do not distinguish between statements and expressions. Rather than basing the logic on a notion of pre- or postcondition, we use the value of a programming language expression as the underlying primitive. A number of language constructs are examined in this framework. We argue that this style of definition gives us a significantly different view of the notion of “easy axiomatixability.” Side effects in expressions as well as aliasing between variables are shown to be “easily axiomatizable” in our system.


title: The Denotational Semantics of Dynamic Networks of Processes

authors:
Arie de Bruin
A. P. Wim Böhm

abstract: DNP (dynamic networks of processes) is a variant of the language introduced by Kahn and MacQueen [11, 12]. In the language it is possible to create new processes dynamically. We present a complete, formal denotational semantics for the language, along the lines sketched by Kahn and MacQueen. An informal explanation of the formal semantics is also given.


title: Program Abstraction and Instantiation

abstract: Our goal is to develop formal methods for abstracting a given set of programs into a program schema and for instantiating a given schema to satisfy concrete specifications. Abstraction and instantiation are two important phases in software development which allow programmers to apply knowledge learned in the solutions of past problems when faced with new situations. For example, from two programs using a linear (or binary) search technique, an abstract schema can be derived that embodies the shared idea and that can be instantiated to solve similar new problems. Along similar lines, the development and application of program transformations are considered. We suggest the formulation of analogies as a basic tool in program abstraction. An analogy is first sought between the specifications of the given programs; this yields an abstract specification that may be instantiated to any of the given concrete specifications. The analogy is then used as a basis for transforming the existing programs into an abstract schema that represents the embedded technique, with the invariant assertions and correctness proofs of the given programs helping to verify and complete the analogy. A given concrete specification of a new problem may then be compared with the abstract specification of the schema to suggest an instantiation of the schema that yields a correct program.


title: Data Types Are Values

authors:
James E. Donahue
Alan J. Demers

abstract: An important goal of programming language research is to isolate the fundamenal concepts of languages, those basic ideas that allow us to understand the relationships among various language features. This paper examines one of these underlying notions, that of data type , with particular attention to the treatment of generic or polymorphic procedures and static type-checking.


title: Generalizing Specifications for Uniformly Implemented Loops

authors:
Douglas D. Dunlop
Victor R. Basili

abstract: The problem of generalizing functional specifications for while loops is considered. This problem occurs frequently when trying to verify that an initialized loop satisfies some functional specification, i.e., produces outputs which are some function of the program inputs. The notion of a valid generalization of a loop specification is defined. A particularly simple valid generalization, a base generalization, is discussed. A property of many commonly occurring while loops, that of being uniformly implemented, is defined. A technique is presented which exploits this property in order to systematically achieve a valid generalization of the loop specification. Two classes of uniformly implemented loops that are particularly susceptible to this form of analysis are defined and discussed. The use of the proposed technique is illustrated with a number of applications. Finally, an implication of the concept of uniform loop implementation for the validation of the obtained generalization is explained.


title: Symmetric Intertask Communication

authors:
Nissim Francez
Shaula Yemini

abstract: 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™.


title: Optimal Prepaging and Font Caching

authors:
David R. Fuchs
Donald E. Knuth

abstract: An efficient algorithm for communicating letter-shape information from a high-speed computer with a large memory to a typesetting device that has a limited memory is presented. The encoding is optimum, in the sense that the total time for typesetting is minimized, using a model that generalizes well-known “demand paging” strategies to the case where changes to the cache are allowed before the associated information is actually needed. Extensive empirical data show that good results are obtained even when difficult technical material is being typeset on a machine that can store information concerning only 100 characters. The methods of this paper are also applicable to other hardware and software caching applications with restricted lookahead.


title: Affix Grammar Driven Code Generation

authors:
Mahadevan Ganapathi
Charles N. Fischer

abstract: Affix grammars are used to describe the instruction set of a target architecture for purposes of compiler code generation. A code generator is obtained automatically for a compiler using attributed parsing techniques. A compiler built on this model can automatically perform most popular machine-dependent optimizations, including peephole optimizations. Code generators based on this model demonstrate retargetability for the VAX 1 -11, iAPX 2 -86, Z-8000 3 , PDP 4 -11, MC-68000, NS32032, FOM, and IBM-370 architectures.


title: Generative Communication in Linda

abstract: Generative communication is the basis of a new distributed programming langauge that is intended for systems programming in distributed settings generally and on integrated network computers in particular. It differs from previous interprocess communication models in specifying that messages be added in tuple-structured form to the computation environment, where they exist as named, independent entities until some process chooses to receive them. Generative communication results in a number of distinguishing properties in the new language, Linda, that is built around it. Linda is fully distributed in space and distributed in time; it allows distributed sharing, continuation passing, and structured naming. We discuss these properties and their implications, then give a series of examples. Linda presents novel implementation problems that we discuss in Part II. We are particularly concerned with implementation of the dynamic global name space that the generative communication model requires.


title: Dealing with World-Model-Based Programs

authors:
Giuseppina C. Gini
Maria L. Gini

abstract: We introduce POINTY, an interactive system for constructing world-model-based programs for robots. POINTY combines an interactive programming environment with the teaching-by-guiding methodology that has been successful in industrial robotics. Owing to its ability to control robots in real time, and to interact with the user, POINTY provides a friendly and powerful programming environment for robot applications. In the past few years, POINTY has been in use at Stanford to write, test, and debug various robot programs.


title: Multilisp: A Language for Concurrent Symbolic Computation

abstract: Multilisp is a version of the Lisp dialect Scheme extended with constructs for parallel execution. Like Scheme, Multilisp is oriented toward symbolic computation. Unlike some parallel programming languages, Multilisp incorporates constructs for causing side effects and for explicitly introducing parallelism. The potential complexity of dealing with side effects in a parallel context is mitigated by the nature of the parallelism constructs and by support for abstract data types: a recommended Multilisp programming style is presented which, if followed, should lead to highly parallel, easily understandable programs. Multilisp is being implemented on the 32-processor Concert multiprocessor; however, it is ultimately intended for use on larger multiprocessors. The current implementation, called Concert Multilisp , is complete enough to run the Multilisp compiler itself and has been run on Concert prototypes including up to eight processors. Concert Multilisp uses novel techniques for task scheduling and garbage collection. The task scheduler helps control excessive resource utilization by means of an unfair scheduling policy; the garbage collector uses a multiprocessor algorithm based on the incremental garbage collector of Baker.


title: Towards Monolingual Programming Environments

authors:
Jan Heering
Paul Klint

abstract: Most programming environments are much too complex. One way of simplifying them is to reduce the number of mode-dependent languages the user has to be familiar with. As a first step towards this end, the feasibility of unified command/programming/debugging languages, and the concepts on which such languages have to be based, are investigated. The unification process is accomplished in two phases. First, a unified command/programming framework is defined and, second, this framework is extended by adding an integrated debugging capability to it. Strict rules are laid down by which to judge language concepts presenting themselves as candidates for inclusion in the framework during each phase. On the basis of these rules many of the language design questions that have hitherto been resolved this way or that, depending on the taste of the designer, lose their vagueness and can be decided in an unambiguous manner.


title: Virtual Time

abstract: Virtual time is a new paradigm for organizing and synchronizing distributed systems which can be applied to such problems as distributed discrete event simulation and distributed database concurrency control. Virtual time provides a flexible abstraction of real time in much the same way that virtual memory provides an abstraction of real memory. It is implemented using the Time Warp mechanism, a synchronization protocol distinguished by its reliance on lookahead-rollback, and by its implementation of rollback via antimessages.


title: Circal and the Representation of Communication, Concurrency, and Time

abstract: The CIRCAL calculus is presented as a mathematical framework in which to describe and analyze concurrent systems, whether hardware or software. The dot operator is used to compose CIRCAL descriptions, and it is this operator which permits the natural modeling of asynchronous and simultaneous behavior, thus allowing the representation and analysis of system timing properties such as those found in circuits. The CIRCAL framework uses an abstraction operator to permit the modeling of a system at different levels of detail. Behavioral complexity of real systems makes abstraction crucial when producing a tractable model, and we illustrate how abstraction introduces nondeterminisim into system representations. An operational semantics, acceptance semantics, is introduced, and it is in terms of this active experimentation that meaning is given to the CIRCAL syntax, thus allowing proof of system properties to be constructed.


title: Program Transformations in a Denotational Setting

abstract: Program transformations are frequently performed by optimizing compilers, and the correctness of applying them usually depends on data flow information. For language-to-same-language transformations, it is shown how a denotational setting can be useful for validating such program transformations. Strong equivalence is obtained for transformations that exploit information from a class of forward data flow analyses, whereas only weak equivalence is obtained for transformations that exploit information from a class of backward data flow analyses. To obtain strong equivalence, both the original and the transformed program must be data flow analysed, but consideration of a transformation-exploiting liveness of variables indicates that a more satisfactory approach may be possible.


title: Editing by Example

abstract: An editing by example system is an automatic program synthesis facility embedded in a text editor that can be used to solve repetitive text editing problems. The user provides the editor with a few examples of a text transformation. The system analyzes the examples and generalizes them into a program that can perform the transformation to the rest of the user's text. This paper presents an overview of the design, analysis, and implementation of a practical editing by example system. It studies the problem of synthesizing a text processing program that generalizes the transformation implicitly described by a small number of input/output examples. A class of text processing programs called gap programs is defined and the problems associated with synthesizing them from examples are examined, leading to an efficient heuristic that provably synthesizes a gap program from examples of its input/output behavior. The editing by example system derived from this analysis has been embedded in a production text editor. By developing an editing by example system that solves a useful class of text processing problems, this work demonstrates that program synthesis is feasible in the domain of text editing.


title: A New Analysis of LALR Formalisms

authors:
Joseph C. H. Park
Kwang-Moo Choe
C. H. Chang

abstract: The traditional LALR analysis is reexamined using a new operator and an associated graph. An improved method that allows factoring out a crucial part of the computation for defining states of LR(0) canonical collection and for computing LALR(1) lookahead sets is presented. This factorization leads to significantly improved algorithms with respect to execution time as well as storage requirements. Experimental results including comparison with other known methods are presented.


title: A Note on Cohen's "Eliminating Redundant Recursive Calls"

abstract: article Free Access Share on A note on Cohen's “eliminating redundant recursive calls” Author: Norman H. Cohen Softech Inc. 705 Masons Mill Business Park, Huntingdon Valley, PA 19006 Softech Inc. 705 Masons Mill Business Park, Huntingdon Valley, PA 19006View Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 7Issue 4Oct. 1985 pp 680–685https://doi.org/10.1145/4472.215006Online:01 October 1985Publication History 0citation193DownloadsMetricsTotal Citations0Total Downloads193Last 12 Months4Last 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 SiteeReaderPDF


title: Efficient Demand-Driven Evaluation - Part 1

authors:
Keshav Pingali
Arvind

abstract: We describe a program transformation technique for programs in a general stream language L whereby a data-driven evaluation of the transformed program performs exactly the same computation as a demand-driven evaluation of the original program. The transformational technique suggests a simple denotational characterization of demand-driven evaluation.


title: Noncorrecting Syntax Error Recovery

abstract: A parser must be able to continue parsing after encountering a syntactic error to check the remainder of the input. To achieve this, it is not necessary to perform corrections on either the input text or the stack contents. A formal framework is provided in which noncorrecting syntax error recovery concepts are defined and investigated. The simplicity of these concepts allows the statement of provable properties, such as the absence of spurious error messages or the avoidance of skipping input text. These properties are due to the fact that no assumptions about the nature of the errors need be made to continue parsing.


title: Detecting Global Variables in Denotational Specifications

abstract: Sufficient criteria are given for replacing all occurrences of the store argument in a Scott-Strachey denotational definition of a programming language by a single global variable. The criteria and transformation are useful for transforming denotational definitions into compilers and interpreters for imperative machines, for optimizing applicative programs, and for judging the suitability of semantic notations for describing imperative languages. An example transformation of a semantics of a repeat-loop language to one which uses a global store variable is given to illustrate the technique.


title: A Note on Hennessy's "Symbolic Debugging of Optimized Code"

authors:
David W. Wall
Amitabh Srivastava
Fred Templin

abstract: article Free Access Share on A note on Hennessy's “symbolic debugging of optimized code” Authors: David Wall Computer Science Department, Whitmore Laboratory, The Pennsylvania State University, University Park, PA Computer Science Department, Whitmore Laboratory, The Pennsylvania State University, University Park, PAView Profile , Amitabh Srivastava Computer Science Department, Whitmore Laboratory, The Pennsylvania State University, University Park, PA Computer Science Department, Whitmore Laboratory, The Pennsylvania State University, University Park, PAView Profile , Fred Templin Computer Science Department, Whitmore Laboratory, The Pennsylvania State University, University Park, PA Computer Science Department, Whitmore Laboratory, The Pennsylvania State University, University Park, PAView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 7Issue 1pp 176–181https://doi.org/10.1145/2363.215005Published:02 January 1985Publication History 14citation167DownloadsMetricsTotal Citations14Total Downloads167Last 12 Months14Last 6 weeks2 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 SiteeReaderPDF


title: Implementation of Resilient, Atomic Data Types

authors:
William E. Weihl
Barbara Liskov

abstract: A major issue in many applications is how to preserve the consistency of data in the presence of concurrency and hardware failures. We suggest addressing this problem by implementing applications in terms of abstract data types with two properties: Their objects are atomic (they provide serializability and recoverability for activities using them) and resilient (they survive hardware failures with acceptably high probability). We define what it means for abstract data types to be atomic and resilient. We also discuss issues that arise in implementing such types, and describe a particular linguistic mechanism provided in the Argus programming language.


title: A Modular Verifiable Exception-Handling Mechanism

authors:
Shaula Yemini
Daniel M. Berry

abstract: This paper presents a new model for exception handling, called the replacement model. The replacement model, in contrast to other exception-handling proposals, supports all the handler responses of resumption, termination, retry, and exception propagation, within both statements and expressions, in a modular, simple, and uniform fashion. The model can be embedded in any expression-oriented language and can also be adapted to languages which are not expression oriented with almost all the above advantages. This paper presents the syntactic extensions for embedding the replacement model into Algol 68 and its operational semantics. An axiomatic semantic definition for the model can be found in [27].


title: A Distributed Alternative to Finite-State-Machine Specifications

abstract: A specification technique, formally equivalent to finite-state machines, is offered as an alternative because it is inherently distributed and more comprehensible. When applied to modules whose complexity is dominated by control, the technique guides the analyst to an effective decomposition of complexity, encourages well-structured error handling, and offers an opportunity for parallel computation. When applied to distributed protocols, the technique provides a unique perspective and facilitates automatic detection of some classes of error. These applications are illustrated by a controller for a distributed telephone system and the full-duplex alternating-bit protocol for data communication. Several schemes are presented for executing the resulting specifications.


title: Correctness Proofs of Distributed Termination Algorithms

abstract: The problem of correctness of the solutions to the distributed termination problem of Francez [7] is addressed. Correctness criteria are formalized in the customary framework for program correctness. A very simple proof method is proposed and applied to show correctness of a solution to the problem. It allows us to reason about liveness properties of temporal logic (see, e.g., Manna and Pnueli [12]) using a new notion of weak total correctness .


title: The PSG System: From Formal Language Definitions to Interactive Programming Environments

authors:
Rolf Bahlke
Gregor Snelting

abstract: The PSG programming system generator developed at the Technical University of Darmstadt produces interactive, language-specific programming environments from formal language definitions. All language-dependent parts of the environment are generated from an entirely nonprocedural specification of the language's syntax, context conditions, and dynamic semantics. The generated environment consists of a language-based editor, supporting systematic program development by named program fragments, an interpreter, and a fragment library system. The major component of the environment is a full-screen editor, which allows both structure and text editing. In structure mode the editor guarantees prevention of both syntactic and semantic errors, whereas in textual mode it guarantees their immediate recognition. PSG editors employ a novel algorithm for incremental semantic analysis which is based on unification. The algorithm will immediately detect semantic errors even in incomplete program fragments. The dynamic semantics of the language are defined in denotational style using a functional language based on the lambda calculus. Program fragments are compiled to terms of the functional language which are executed by an interpreter. The PSG generator has been used to produce environments for Pascal, ALGOL 60, MODULA-2, and the formal language definition language itself.


title: An Example of Stepwise Refinement of Distributed Programs: Quiescence Detection

authors:
K. Mani Chandy
Jayadev Misra

abstract: 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.