title: Adding Liveness Properties to Coupled Finite-State Machines

authors:
Sudhir Aggarwal
Costas Courcoubetis
Pierre Wolper

abstract: Informal specifications of protocols are often imprecise and incomplete and are usually not sufficient to ensure the correctness of even very simple protocols. Consequently, formal specification methods, such as finite-state models, are increasingly being used. The selection/resolution (S/R) model is a finite-state model with a powerful communication mechanism that makes it easy to describe complex protocols as a collection of simple finite-state machines. A software environment, called SPANNER, has been developed to specify and analyze protocols specified with the S/R model. SPANNER provides the facility to compute the joint behavior of a number of finite-state machines and to check if the “product” machine has inaccessible states, states corresponding to deadlocks, and loops corresponding to livelocks. So far, however, SPANNER has had no facility to systematically deal with liveness conditions. For example, one might wish to specify that, although a communication channel is unreliable, a message will get through if it is sent infinitely often, and to check that the infinite behavior of the protocol viewed as an infinite sequence will always be in some ω-regular set (possibly specified in terms of a formula in temporal logic or as an ω-automata). In this paper we show that with very minor modifications to the implemented system it is possible to substantially extend the type of properties that can be specified and checked by SPANNER. This is done by extending the S/R model to include acceptance conditions found in automatons on infinite words, which permits the incorporation of arbitrary liveness conditions into the model. We show how these extensions can be easily incorporated into SPANNER (and into essentially any finite-state verification system) and how the resulting system is used to automatically verify the correctness of protocols.


venue: toplas

title: A Method for Specializing Logic Programs

authors:
Annalisa Bossi
Nicoletta Cocco
Susi Dulli

abstract: A specialization method for logic programs that allows one to restrict a general program to special cases by means of constraint predicates is presented. A set of basic transformation operations, which are shown to produce equivalent programs, is defined. The method uses these operations for propagating the constraint information through the program and for consequently simplifying it whenever possible. Some examples of specializations are given, and some improvements and developments of the method are discussed.


title: An Interval-Based Approach to Exhaustive and Incremental Interprocedural Data-Flow Analysis

abstract: We reformulate interval analysis so that it can he applied to any monotone data-flow problem, including the nonfast problems of flow-insensitive interprocedural analysis. We then develop an incremental interval analysis technique that can be applied to the same class of problems. When applied to flow-insensitive interprocedural data-flow problems, the resulting algorithms are simple, practical, and efficient. With a single update, the incremental algorithm can accommodate any sequence of program changes that does not alter the structure of the program call graph. It can also accommodate a large class of structural changes. For alias analysis, we develop an incremental algorithm that obtains the exact solution as computed by an exhaustive algorithm. Finally, we develop a transitive closure algorithm that is particularly well suited to the very sparse matrices associated with the problems we address.


title: Type Extension Through Polymorphism

abstract: A record data type can be extended by addition of more fields. The extended type is a subtype of the original, in that any value of the extended type can be regarded as a value of the original type by ignoring the additional fields. This results in a type hierarchy. Milner [3] has proposed a polymorphic type system. With the Milner approach, the type of a function may contain type variables. This also results in a type hierarchy. In a language with a polymorphic type system, if it is anticipated that a record type will need to be extended, then the record type can be defined to have a dummy extension field . In the parent type, the extension field will have null contents of type void . The type of the extension field can differ with different subtypes. The approach can be extended to allow a type to be subtype of two or more parent types. To a limited extent, this approach can be used in Ada and other languages with generic program units.


title: The Priority-Based Coloring Approach to Register Allocation

authors:
Fred C. Chow
John L. Hennessy

abstract: Global register allocation plays a major role in determining the efficacy of an optimizing compiler. Graph coloring has been used as the central paradigm for register allocation in modern compilers. A straightforward coloring approach can suffer from several shortcomings. These shortcomings are addressed in this paper by coloring the graph using a priority ordering. A natural method for dealing with the spilling emerges from this approach. The detailed algorithms for a priority-based coloring approach are presented and are contrasted with the basic graph-coloring algorithm. Various extensions to the basic algorithms are also presented. Measurements of large programs are used to determine the effectiveness of the algorithm and its extensions, as well as the causes of an imperfect allocation. Running time of the allocator and the impact of heuristics aimed at reducing that time are also measured.


title: A Mechanism for Environment Integration

authors:
Geoffrey Clemm
Leon J. Osterweil

abstract: This paper describes research associated with the development and evaluation of Odin-an environment integration system based on the idea that tools should be integrated around a centralized store of persistent software objects. The paper describes this idea in detail and then presents the Odin architecture, which features such notions as the typing of software objects, composing tools out of modular tool fragments, optimizing the storage and rederivation of software objects, and isolating tool interconnectivity information in a single centralized object. The paper then describes some projects that have used Odin to integrate tools on a large scale. Finally, it discusses the significance of this work and the conclusions that can be drawn about superior software environment architectures.


title: Search Direction by Goal Failure in Goal-Directed Programming

abstract: A new approach to goal-oriented programming is described, whereby the search for values of variables to satisfy a goal is invariably directed by that goal or by information provided by its failure. This goal-directed approach is in contrast to that employed by logic programming systems, which attempt to satisfy a goal that has failed by resatisfying an already tested goal, and which furthermore do this in a way determined solely by the order of facts and rules in the database and without reference to the goal that has failed. Proposed changes in the control structure of logic programs designed to improve their execution serve more to reduce the search space than to add goal direction. A goal-directed language that embodies the new approach is presented. It is at the same time a functional programming language and a specification interpreter for the direct execution and testing of functional specifications, and permits the user to write executable program descriptions in which some of the constituent functions are fully defined while others are “merely” specified. The language has been successfully tested on examples drawn from such fields as deductive question answering and problem solving, where it compares favorably with the logic programming languages.


title: An Approach to Support Automatic Generation of User Interfaces

authors:
Prasun Dewan
Marvin H. Solomon

abstract: In traditional interactive programming environments, each application individually manages its interaction with the human user. The result is duplication of effort in implementing user interface code and nonuniform—hence confusing—input conventions. This paper presents an approach to support automatic generation of user interfaces in environments based on algebraic languages. The approach supports the editing model of interaction, which allows a user to view all applications as data that can be edited. An application interacts with a user by submitting variables (of arbitrary types) to a dialogue manager , which displays their presentations to the user and offers type-directed editing of these presentations. Applications and dialogue managers communicate through a protocol that allows a presentation to be kept consistent with the variable it displays. A particular implementation of the approach, called Dost, has been constructed for the Xerox development environment and the Mesa programming language. Dost is used as a concrete example to describe the editing model, the primitives to support it, and our preliminary experience with these primitives. The approach is compared with related work, its shortcomings are discussed, and suggestions for future work are made.


title: Using Symbolic Execution for Verification of Ada Tasking Programs

abstract: A method is presented for using symbolic execution to generate the verification conditions required for proving correctness of programs written in a tasking subset of Ada. The symbolic execution rules are derived from proof systems that allow tasks to be verified independently in local proofs, which are then checked for cooperation. The isolation nature of this approach to symbolic execution of concurrent programs makes it better suited to formal verification than the more traditional interleaving approach, which suffers from combinatorial problems. The criteria for correct operation of a concurrent program include partial correctness, as well as more general safety properties, such as mutual exclusion and freedom from deadlock.


title: A Correctness Proof for Combinator Reduction with Cycles

authors:
William M. Farmer
John D. Ramsdell
Ronald J. Watro

abstract: Turner popularized a technique of Wadsworth in which a cyclic graph rewriting rule is used to implement reduction of the fixed point combinator Y . We examine the theoretical foundation of this approach. Previous work has concentrated on proving that graph methods are, in a certain sense, sound and complete implementations of term methods. This work is inapplicable to the cyclic Y rule, which is unsound in this sense since graph normal forms can exist without corresponding term normal forms. We define and prove the correctness of combinator head reduction using the cyclic Y rule; the correctness of normal reduction is an immediate consequence. Our proof avoids the use of infinite trees to explain cyclic graphs. Instead, we show how to consider reduction with cycles as an optimization of reduction without cycles.


title: Linearizability: A Correctness Condition for Concurrent Objects

authors:
Maurice Herlihy
Jeannette M. Wing

abstract: A concurrent object is a data object shared by concurrent processes. Linearizability is a correctness condition for concurrent objects that exploits the semantics of abstract data types. It permits a high degree of concurrency, yet it permits programmers to specify and reason about concurrent objects using known techniques from the sequential domain. Linearizability provides the illusion that each operation applied by concurrent processes takes effect instantaneously at some point between its invocation and its response, implying that the meaning of a concurrent object's operations can be given by pre- and post-conditions. This paper defines linearizability, compares it to other correctness conditions, presents and demonstrates a method for proving the correctness of implementations, and shows how to reason about concurrent objects, given they are linearizable.


title: Interprocedural Slicing Using Dependence Graphs

authors:
Susan Horwitz
Thomas W. Reps
David W. Binkley

abstract: The notion of a program slice , originally introduced by Mark Weiser, is useful in program debugging, automatic parallelization, and program integration. A slice of a program is taken with respect to a program point p and a variable x ; the slice consists of all statements of the program that might affect the value of x at point p . This paper concerns the problem of interprocedural slicing—generating a slice of an entire program, where the slice crosses the boundaries of procedure calls. To solve this problem, we introduce a new kind of graph to represent programs, called a system dependence graph , which extends previous dependence representations to incorporate collections of procedures (with procedure calls) rather than just monolithic programs. Our main result is an algorithm for interprocedural slicing that uses the new representation. (It should be noted that our work concerns a somewhat restricted kind of slice: rather than permitting a program to b e sliced with respect to program point p and an arbitrary variable, a slice must be taken with respect to a variable that is defined or used at p .) The chief difficulty in interprocedural slicing is correctly accounting for the calling context of a called procedure. To handle this problem, system dependence graphs include some data dependence edges that represent transitive dependences due to the effects of procedure calls, in addition to the conventional direct-dependence edges. These edges are constructed with the aid of an auxiliary structure that represents calling and parameter-linkage relationships. This structure takes the form of an attribute grammar. The step of computing the required transitive-dependence edges is reduced to the construction of the subordinate characteristic graphs for the grammar's nonterminals.


title: A Distributed Deadlock Detection Algorithm for CSP-Like Communication

abstract: An algorithm for detecting deadlocks in distributed systems with CSP-like communication is proposed. Unlike previous work, the proposed algorithm avoids periodically sending deadlock-detecting messages by the processes and requires no local storage for the processes with size predetermined by the number of processes in the system. The algorithm is proven to have the following properties: (0) it never detects false deadlocks; (1) it has only one process in a knot report the deadlock; and (2) it detects every true deadlock in finite time.


title: Efficient Evaluation of Circular Attribute Grammars

abstract: We present efficient algorithms for exhaustive and incremental evaluation of circular attributes under any conditions that guarantee finite convergence. The algorithms are derived from those for noncircular attribute grammars by partitioning the underlying attribute dependency graph into its strongly connected components and by ordering the evaluations to follow a topological sort of the resulting directed acyclic graph. The algorithms are efficient in the sense that their worst-case running time is proportional to the cost of computing the fixed points of only those strongly connected components containing affected attributes or attributes directly dependent on affected attributes. When the attribute grammar is noncircular or the specific dependency graph under consideration is acyclic, both algorithms reduce to the standard optimal algorithms for noncircular attribute evaluation.


title: An Exercise in the Formal Derivation of Parallel Programs: Maximum Flows in Graphs

abstract: We apply a new method for the development of parallel programs to the problem of finding maximum flows in graphs. The method facilitates concurrent program design by separating the concerns of correctness from those of hardware and implementation. It uses predicate transformer semantics to define a set of basic operators for the specification and verification of programs. From an initial specification program development proceeds by a series of refinement steps, each of which constitutes a strengthening of the specification of the previous refinement. The method is completely formal in the sense that all reasoning steps are performed within predicate calculus. A program is viewed as a mathematical object enjoying certain properties, rather than in terms of its possible executions. We demonstrate the usefulness of the approach by deriving an efficient algorithm for the Maximum Flow Problem in a top-down manner.


title: A Modular Technique for the Design of Efficient Distributed Leader Finding Algorithms

authors:
Ephraim Korach
Shay Kutten
Shlomo Moran

abstract: A general, modular technique for designing efficient leader finding algorithms in distributed, asynchronous networks is developed. This technique reduces the problem of efficient leader finding to a simpler problem of efficient serial traversing of the corresponding network. The message complexity of the resulting leader finding algorithms is bounded by [ f ( n ) + n )(log 2 k + 1) (or ( f ( m ) + n )(log 2 k + 1)], where n is the number of nodes in the network [ m is the number of edges in the network], k is the number of nodes that start the algorithm, and f ( n ) [ f ( m )] is the message complexity of traversing the nodes [edges] of the network. The time complexity of these algorithms may be as large as their message complexity. This technique does not require that the FIFO discipline is obeyed by the links. The local memory needed for each node, besides the memory needed for the traversal algorithm, is logarithmic in the maximal identity of a node in the network. This result achieves in a unified way the best known upper bounds on the message complexity of leader finding algorithms for circular, complete, and general networks. It is also shown to be applicable to other classes of networks, and in some cases the message complexity of the resulting algorithms is better by a constant factor than that of previously known algorithms.


title: win and sin: Predicate Transformers for Concurrency


title: On Kilbury's Modification of Earley's Algorithm

abstract: We improve on J. Kilbury's proposal to interchange “predictor” and “scanner” in Earley's parser. This modification of Earley's parser can trivially be combined with those suggested by S. Graham, M. Harrison, and W. Ruzzo, leading to smaller parse tables and almost the power of lookahead 1. Along these lines we can also obtain Earley-parsers having partial lookahead r ≥ 1, without storing right contexts. Parse trees with shared structure can be stored in the parse tables directly, rather than constructing the trees from “dotted rules."


title: Creating User Interfaces Using Programming by Example, Visual Programming, and Constraints

abstract: Peridot is an experimental tool that allows designers to create user interface components without conventional programming. The designer draws pictures of what the interface should look like and then uses the mouse and other input devices to demonstrate how the interface should operate. Peridot generalizes from these example pictures and actions to create parameterized procedures, such as those found in conventional user interface libraries such as the Macintosh Toolbox. Peridot uses visual programming, programming by example, constraints, and plausible inferencing to allow nonprogrammers to create menus, buttons, scroll bars, and many other interaction techniques easily and quickly. Peridot created its own interface and can create almost all of the interaction techniques in the Macintosh Toolbox. Therefore, Peridot demonstrates that it is possible to provide sophisticated programming capabilities to nonprogrammers in an easy-to-use manner and still have sufficient power to generate interesting and useful programs.


title: On Iterative Constructs

abstract: The wheel is repeatedly reinvented because it is a good idea. Perhaps Anson's "A Generalized Iterative Construct and Its Semantics" [1] confirms that “A Generalized Control Structure and Its Formal Definition” [2], and the earlier “An Alternative Control Structure and its Formal Definition” [3] presented good ideas. However, there are several misstatements in [1] that should be corrected. The discussion of these issues is made a bit academic by the four-year delay between Anson's submission of his paper (which apparently coincided with the publication of [2]) and the publication of [1]. In that time a generalization of both schemes has been published as a Technical Report [6] and has been submitted for publication. In this generalization the decision about whether a command is iterating or terminating can be made during execution, and the semantics must be that of DO TERM. Further generalizations make the seman tics of the constructs more practical, since side-effects are accurately treated in all cases. A method for reducing the length of guards and avoiding duplicated subexpressions is also provided.


title: Remote Evaluation

authors:
James W. Stamos
David K. Gifford

abstract: A new technique for computer-to-computer communication is presented that can increase the performance of distributed systems. This technique, called remote evaluation, lets one computer send another computer a request in the form of a program. A computer that receives such a request executes the program in the request and returns the results to the sending computer. Remote evaluation provides a new degree of flexibility in the design of distributed systems. In present distributed systems that use remote procedure calls, server computers are designed to offer a fixed set of services. In a system that uses remote evaluation, server computers are more properly viewed as programmable processors. One consequence of this flexibility is that remote evaluation can reduce the amount of communication that is required to accomplish a given task. In this paper we discuss the semantics of remote evaluation and its effect on distributed system design. We also summarize our experience with a prototype implementation.


title: Production Trees: A Compact Representation of Parsed Programs

abstract: Abstract syntax trees were devised as a compact alternative to parse trees, because parse trees are known to require excessive amounts of storage to represent parsed programs. However, the savings that abstract syntax trees actually achieve have never been precisely described because the necessary analysis has been missing. Without it, one can only measure particular cases that may not adequately represent all the possible behaviors. We introduce a data structure, production trees, that are more compact than either abstract syntax trees or parse trees. Further, we develop the necessary analysis to characterize the storage requirements of parse trees, abstract syntax trees, and production trees and relate the size of all three to the size of the program's text. The analysis yields the parameters needed to characterize these storage behaviors over their entire range. We flesh out the analysis by measuring these parameters for a sample of “C” programs. For these programs, production trees were from 1/15 to 1/23 the size of the corresponding parse tree, l/2.7 the size of a (minimal) abstract syntax tree, and averaged only 2.83 times the size of the program text.


title: Linguistic Support for Atomic Data Types

abstract: The problems of concurrency and failures in distributed systems can be addressed by implementing applications in terms of atomic data types: data types whose objects provide serializability and recoverability for transactions using them. The specifications of the types can be used to permit high levels of concurrency among transactions while still ensuring atomicity. However, highly concurrent implementations can be quite complicated. In this paper we analyze the expressive power of existing proposals for language features intended to support the implementation of atomic types. We illustrate several limitations of existing proposals and propose a new approach that avoids these problems.


title: A Comparative Evaluation of Object Definition Techniques

authors:
Jack C. Wileden
Lori A. Clarke
Alexander L. Wolf

abstract: Although prototyping has long been touted as a potentially valuable software engineering activity, it has never achieved widespread use by developers of large-scale, production software. This is probably due in part to an incompatibility between the languages and tools traditionally available for prototyping (e.g., LISP or Smalltalk) and the needs of large-scale-software developers, who must construct and experiment with large prototypes. The recent surge of interest in applying prototyping to the development of large-scale, production software will necessitate improved prototyping languages and tools appropriate for constructing and experimenting with large, complex prototype systems. We explore techniques aimed at one central aspect of prototyping that we feel is especially significant for large prototypes, namely that aspect concerned with the definition of data objects. We characterize and compare various techniques that might be useful in defining data objects in large prototype systems, after first discussing some distinguishing characteristics of large prototype systems and identifying some requirements that they imply. To make the discussion more concrete, we describe our implementations of three techniques that represent different possibilities within the range of object definition techniques for large prototype systems.


title: Dynamic Typing in a Statically Typed Language

authors:
Martín Abadi
Luca Cardelli
Benjamin C. Pierce
Gordon D. Plotkin

abstract: Statically typed programming languages allow earlier error checking, better enforcement of diciplined programming styles, and the generation of more efficient object code than languages where all type consistency checks are performed at run time. However, even in statically typed languages, there is often the need to deal with datawhose type cannot be determined at compile time. To handle such situations safely, we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T . Instances of Dynamic are built with an explicit tagging construct and inspected with a type safe typecase construct. This paper explores the syntax, operational semantics, and denotational semantics of a simple language that includes the type Dynamic . We give examples of how dynamically typed values can be used in programming. Then we discuss an operational semantics for our language and obtain a soundness theorem. We present two formulations of the denotational semantics of this language and relate them to the operational semantics. Finally, we consider the implications of polymorphism and some implementation issues.


title: Efficient Construction of LR(k) States and Tables

authors:
Massimo Ancona
Gabriella Dodero
Vittoria Gianuzzi
M. Morgavi


title: Table Compression for Tree Automata

authors:
Jürgen Börstler
Ulrich Möncke
Reinhard Wilhelm

abstract: The compression of bottom-up tree automata and their representation as implemented in the OPTRAN tree transformation system are described here as a four-step process.First, the vertically working tree automata traversing one generation in one step are replaced by horizontally working automata, splitting this step into rank (operator) steps, This replaces each matrix of dimension rank (operator) by a tree of depth rank (operator), A second step replaces this tree by a shortened directed acyclic graph (DAG), that is, a DAG where equivalent states of the tree are identified and paths in the tree with no gain in information are condensed, The acceptance property of the automaton is not changed.This and the following size reduction steps critically depend on the "no-error" assumption, that is, the assumption that input trees are correctly built and that no error detection is required of the tree automata.The third step embeds the DAG, which is naturally represented by two-dimensional tables, into a linear array using row displacement and row column schemes.In addition, this step compresses strings of consecl~.,veidentical entries, which occur often in this type of automaton.The last step exploits the memory structure and addressability of the target machine.Using information on automata and table sizes, the most efilcient storage representation is selected.The data structures and access functions are generated as C objects and functions, respectively.Results showing the effectiveness of the different steps are given.


title: The Concurrent Language, Shared Prolog

authors:
Antonio Brogi
Paolo Ciancarini

abstract: Shared Prolog is a new concurrent logic language. A Shared Prolog system is composed of a set of parallel agents that are Prolog programs extended by a guard mechanism. The programmer controls the granularity of parallelism, coordinating communication and synchronization of the agents via a centralized data structure. The communication mechanism is inherited from the blackboard model of problem solving. Intuitively, the granularity of the logic processes to be elaborated in parallel is large, while the resources shared on the blackboard can be very fined grained. An operational semantics for Shared Prolog is given in terms of a distributed model. Through an abstract notion of computation, the kinds of parallelism supported by the language, as well as properties of infinite computations, such as local deadlocks, are studied. The expressiveness of the language is shown with respect to the specification of two classes of applications: metaprogramming and blackboard systems.


title: Reply to "Subtypes and Quantification"


title: Techniques for Debugging Parallel Programs with Flowback Analysis

authors:
Jong-Deok Choi
Barton P. Miller
Robert H. B. Netzer

abstract: Flowback analysis is a powerful technique for debugging programs.It allows the programmer to examine dynamic dependence in a program's execution history without having to reexecute the program.The goal is to present to the programmer a graphical view of the dynamic program dependence.We are building a system, called PPD, that performs flowback analysis while keeping the execution time overhead low.We also extend the semantics of flowback analysis to parallel programs.This paper describes details of the graphs and algorithms needed to implement efficient flowback analysis for parallel programs.Execution-time overhead is kept low by recording only a small amount of trace during a program's execution.We use semantic analysis and a technique called incremental tracing to keep the time and space overhead low.As part of the semantic analysis, PPD uses a static program dependence graph structure that reduces the amount of work done at compile time and takes advantage of the dynamic information produced during execution time.Parallel programs have been accommodated in two ways.First, the flowback dependence can span process boundaries; that is, the most recent modification to a variable might be traced to a different process than that one that contains the current reference.The static dynamic program dependence graphs of the individual processes are tied together with synchronization and data dependence information to form complete graphs that represent the entire program.Second, our algorithms will detect potential data-race conditions in the access to shared variables.The programmer can be directed to the cause of the race condition.PPD is currently being implemented for the C programming language on a Sequent Symmetry shared-memory .


title: Type-Extension Type Tests Can Be Performed In Constant Time

abstract: article Free AccessType-extension type test can be performed in constant time Author: Norman H. Cohen T. J. Watson Research Center, Yorktown Heights, NY T. J. Watson Research Center, Yorktown Heights, NYView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 13Issue 4Oct. 1991 pp 626–629https://doi.org/10.1145/115372.115297Published:01 October 1991Publication History 63citation439DownloadsMetricsTotal Citations63Total Downloads439Last 12 Months29Last 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 AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


title: Efficiently Computing Static Single Assignment Form and the Control Dependence Graph

authors:
Ron Cytron
Jeanne Ferrante
Barry K. Rosen
Mark N. Wegman
F. Kenneth Zadeck

abstract: In optimizing compilers, data structure choices directly influence the power and efficiency of practical program optimization.A poor choice of data structure can inhibit optimization or slow compilation to the point that advanced optimization features become undesirable.Recently, static single assignment form and the control dependence graph have been proposed to represent data flow and control flow propertiee of programs.Each of these previously unrelated techniques lends efficiency and power to a useful class of program optimization.Although both of these structures are attractive, the difficulty of their construction and their potential size have discouraged their use.We present new algorithms that efficiently compute these data structures for arbitrary control flow graphs.The algorithms use dominance frontiers, a new concept that may have other applications.We also give analytical and experimental evidence that all of these data structures are usually linear in the size of the original program.This paper thus presents strong evidence that these structures can be of practical use in optimization.


title: Practical Adaptation of the Global Optimization Algorithm of Morel and Renvoise

abstract: We present some modifications to Morel and Renvoise's algorithm for global optimization by suppression of partial redundancies.The modifications are motivated by the desire to ( 1) eliminate redundant code motion, and (2) extend the scope of optimization to the movement of assignments.The complexity of the modified algorithm is compared with that of the original algorithm.


title: Compilation of Functional Languages by Program Transformation

authors:
Pascal Fradet
Daniel Le Métayer

abstract: One of the most important issues concerning functional languages is the efficiency and the correctness of their implementation. We focus on sequential implementations for conventional von Neumann computers. The compilation process is described in terms of program transformations in the functional framework. The original functional expression is transformed into a functional term that can be seen as a traditional machine code. The two main steps are the compilation of the computation rule by the introduction of continuation functions and the compilation of the environment management using combinators. The advantage of this approach is that we do not have to introduce an abstract machine, which makes correctness proofs much simpler. As far as efficiency is concerned, this approach is promising since many optimizations can be described and formally justified in the functional framework.


title: Wait-Free Synchronization

abstract: A wait-free implementation of a concurrent data object is one that guarantees that any process can complete any operation in a finite number of steps, regardless of the execution speeds of the other processes. The problem of constructing a wait-free implementation of one data object from another lies at the heart of much recent work in concurrent algorithms, concurrent data structures, and multiprocessor architectures. First, we introduce a simple and general technique, based on reduction to a concensus protocol, for proving statements of the form, “there is no wait-free implementation of X by Y.” We derive a hierarchy of objects such that no object at one level has a wait-free implementation in terms of objects at lower levels. In particular, we show that atomic read/write registers, which have been the focus of much recent attention, are at the bottom of the hierarchy: thay cannot be used to construct wait-free implementations of many simple and familiar data types. Moreover, classical synchronization primitives such as test&set and fetch&add , while more powerful than read and write , are also computationally weak, as are the standard message-passing primitives. Second, nevertheless, we show that there do exist simple universal objects from which one can construct a wait-free implementation of any sequential object.


title: Collecting Interpretations of Expressions

authors:
Paul Hudak
Jonathan Young

abstract: A collecting interpretation of expressions is an interpretation of a program that allows one to answer questions of the sort: “What are all possible values to which an expression might evaluate during program execution?” Answering such questions in a denotational framework is akin to traditional data flow analysis and, when used in the context of abstract interpretation, allows one to infer properties that approximate the run-time behavior of expression evaluation. Exact collecting interpretations of expressions are developed for three abstract functional languages: a strict first-order language, a nonstrict first-order language, and a nonstrict higher order language (the full untyped lambda calculus with constants). It is argued that the method is simple (in particular, no powerdomains are needed), Natural (it captures the intuitive operational behavior of a cache), yet more expressive than existing methods (it is the first exact collecting interpretation for either nonstrict higher order languages). Correctness of the interpretations with respect to the standard semantics is shown via a generalization of the notion of strictness. It is further shown how to form abstractions of these exact interpretations, using as an example a collecting strictness analysis which yields compile-time information not previously captured by conventional strictness analyses.


title: Incremental Attribute Evaluation: A Flexible Algorithm for Lazy Update

abstract: This paper introduces a new algorithm for incremental attribute evaluation.The algorithm is lazy: Itevaluates only theattributes that are both affected byachange andthat are directly or indirectly observable by the user.In this way, the wasted work of computing values that are never actually used is avoided.Although the algorithm is not optimal, it performs better than the standard "optimal" algorithm in cases where expensive but optional computations need to be supported.Furthermore, the algorithm does not have some of the limitations of other algorithms.It works for general attributed graphs as well as for standard attributed trees.In addition, it does not presume any special editing model, and it supports multiple change points without loss of efficiency.


title: A Fully Abstract Semantics for a First-Order Functional Language with Logic Variables

authors:
Radha Jagadeesan
Keshav Pingali
Prakash Panangaden

abstract: There is much interest in combining the functional and logic programming paradigms � in particular, there have been several proposals for adding logic variables to functional languages, since that permits incremental construction of data structures through constraint intersection. While it is straight-forward to give an abstract semantics for functional languages and for logic languages, it has proven surprisingly di cult to give a proper semantic account of functional languages with logic variables. In this paper, we present a rst-order functional language with logic variables and give its meaning using a structural operational semantics. We also give it a denotational semantics, using a novel technique involving closure operators on a Scott domain. Finally, we show that these two semantics correspond in the strongest possible way|weshow that the denotational semantics is fully abstract with respect to the operational semantics. The techniques developed in this paper are quite general, and can be used to give semantics to any constraint-based logic programming languages. Our results can also be interpreted as a generalization of Kahn semantics for data ow networks in which processes not only exchange messages, but have access to a shared global address space in which variables are bound through constraint intersection. Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Functional Programming � D.3.1 [Programming Languages]: Formal De nitions and Theory- semantics � D.3.2 [Programming Languages]: Data ow Languages � F.3.2 [Theory of Computation]: Semantics of Programming Languages- denotational semantics � F.4.1 [Theory of Computation]: Mathematical Logic- logic programming


title: A First-Come-First-Served Mutual-Exclusion Algorithm with Small Communication Variables

authors:
Edward A. Lycklama
Vassos Hadzilacos

abstract: We present an algorithm for the mutual-exclusion problem that satisfies the "first-come-firstserved" property and requires only five shared bits per participant.The algorithm works in a model of concurrency that does not assume atomic operations.


title: An Ad Hoc Approach to the Implementation of Polymorphism

authors:
Ronald Morrison
Alan Dearle
Richard C. H. Connor
Alfred L. Brown

abstract: Polymorphicabstraction provides the ability to write programs that are independent of the form of the data over which they operate.There are a number of different categories of polymorphic expression-ad hoc and umversal, which includes parametric and inclusion-all of which have many advantages in terms of code reuse and software economics.It has proved difficult to provide efficient implementations of polymorphism.Here, we address this problem and describe a new technique that can implement all forms of polymorphism, use a conventional machine architecture, and support nonuniform data representations.Furthermore, the method ensures that any extra cost of implementation applies to polymorphic forms only, and allows such polymorphic forms to persist over program invocations.


title: An Improved Storage Management Scheme for Block Structured Languages

abstract: The conventional storage allocation scheme for block structured languages requires the allocation of stack space and the building of a dmplay with each procedure call.Several techniques have been proposed for analyzing the call graph of a program that make it possible to eliminate these operations from many call sequences.In this paper.we compare these techniques and propose an improved allocation scheme which can substantially reduce allocation overhead, even in the presence of recursion and support for separate compilation.


title: Data Flow Analysis of Communicating Finite State Machines

authors:
Wuxu Peng
S. Purushothaman

abstract: Let ( F'l, Pz, . . . .Pm) be a network of n finite state machines, communicating with each other asynchronously using typed messages over unbounded FIFO channels, In this paper we present a data flow approach to analyzing these communicating machines for nonprogress properties (deadlock and unspecified reception).We set up flow equations to compute the set of pending messages in the queues at any given state of such a network, The central technical contribution of this paper is an algorithm to compute approximations to solutions for the ensuing equations We then show how these approximate solutions can be used to check that interactions between the processes are free of nonprogress errors.We conclude with a number of example protocols that our algorithm certifies to be free of nonprog-ess errors.Included in the examples is a specification of X25 call establishment/clear protocol,


title: Linking Programs Incrementally

authors:
Russell W. Quong
Mark A. Linton

abstract: Linking is traditionally a batch process that resolves cross-references between object modules and run-time libraries to produce a stand-alone executable image. Because most program changes only involve a small part of the program, we have implemented an incremental linker, named Inclink, that processes only the changed modules. Inclink generates a new executable in time proportional to the size of change; in contrast, a batch linker generates an executable in time proporitonal to the size of the program. To minimize updates to the executable, Inclink allocates extra space for every module. By allocating 24 percent more space in the executable for overflows, Inclink can update a module in place over 97 percent of the time. Measurements show that Inclink is more than an order of magnitude faster than the UNIX [2] batch linker and that 88 percent of all links will take less than 2 s of CPU time on a MicroVAX-2, independent of program size.


title: Automatic Generation and Use of Abstract Structure Operators

abstract: structures are those structures definable by parametric and recursive type equations.Manipulation of the instances of such structures is often expressed as recursive functions.These functions can be quite complex and tedious to write, especially for types needed to model complex objects found in many modern applications.We define a set of operators for computing over abstract structures that provide a clean interface with large functionality.These operations


title: Subtypes and Quantification

abstract: No abstract available.


title: Automatic Transformation of Series Expressions into Loops

abstract: The benefits of programming in a functional style are well known. In particular, algorithms that are expressed as compositions of functions operating on sequences/vectors/streams of data elements are easier to understand and modify than equivalent algorithms expressed as loops. Unfortunately, this kind of expression is not used anywhere near as often as it could be, for at least three reasons: (1) most programmers are less familiar with this kind of expression than with loops; (2) most programming languages provide poor support for this kind of expression; and (3) when support is provided, it is seldom effcient. In any programming language, the second and third problems can be largely solved by introducing a data type called series , a comprehensive set of procedures operating on series, and a preprocessor (or compiler extension) that automatically converts most series expressions into efficient loops. A set of restrictions specifies which series expressions can be optimized. If programmers stay within the limits imposed, they are guaranteed of high efficiency at all times. A common Lisp macro package supporting series has been in use for some time. A prototype demonnstrates that series can be straightforwardly supported in Pascal.


title: Constant Propagation with Conditional Branches

authors:
Mark N. Wegman
F. Kenneth Zadeck

abstract: Constant propagation is a well-known global flow analysis problem. The goal of constant propagation is to discover values that are constant on all possible executions of a program and to propagate these constant values as far foward through the program as possible. Expressions whose operands are all constants can be evaluated at compile time and the results propagated further. Using the algorithms presented in this paper can produce smaller and faster compiled programs. The same algorithms can be used for other kinds of analyses (e.g., type of determination). We present four algorithms in this paper, all conservitive in the sense that all constants may not be found, but each constant found is constant over all possible executions of the program. These algorithms are among the simplest, fastest, and most powerful global constant propagation algorithms known. We also present a new algorithm that performs a form of interprocedural data flow analysis in which aliasing information is gathered in conjunction with constant progagation. Several variants of this algorithm are considered.


title: Reply to "Type-Extension Tests Can Be Performed In Constant Time"

abstract: No abstract available.


title: INC: A Language for Incremental Computations

authors:
Daniel M. Yellin
Robert E. Strom

abstract: An incremental computation is one that is performed repeatedly on nearly identical inputs. Incremental computations occur naturally in many environments, such as compilers, language-based editors, spreadsheets, and formatters. This article describes a proposed tool for making it easy to write incremental programs. The tool consists of a programming language, INC, and a set of compile-time transformations for the primitive elements of INC. A programmer defines an algorithm in INC without regard to efficient incremental execution. The transformations automatically convert this algorithm into an efficient incremental algorithm. INC is a functional language. The implementation of an INC program is a network of processes. Each INC function is transformed into a process that receives and transmits messages describing changes to its inputs and outputs. We give an overview to the language and illustrate the incremental techniques employed by INC. We present the static and incremental complexity bounds for the primitive INC functions. We also present some example programs illustrating INC's flexibility.


title: The Euclidian Definition of the Functions div and mod

abstract: The definitions of the functions div and mod in the computer science literature and in programming languages are either similar to the Algol of Pascal definition (which is shown to be an unfortunate choice) or based on division by truncation (T-definition) or division by flooring as defined by Knuth (F-definition). The differences between various definitions that are in common usage are discussed, and an additional one is proposed, which is based on Euclid's theorem and therefore is called the Euclidean definition (E-definition). Its distinguishing feature is that 0 ≤ D mod d < | d | irrespective of the signs of D and d . It is argued that the E- and F-definitions are superior to all other ones in regularity and useful mathematical properties and hence deserve serious consideration as the standard convention at the applications and language level. It is also shown that these definitions are the most suitable ones for describing number representation systems and the realization of arithmetic operations at the architecture and hardware level.


title: A Self-Applicable Partial Evaluator for the Lambda Calculus: Correctness and Pragmatics

abstract: We describe theoretical and a few practical aspects of an implemented self-applicable partial evaluator for the untyped lambda calculus with constants, conditionals, and a fixed point operator. The purpose of this paper is first to announce the existence of (and to describe) a partial evaluator that is both higher-order and self-applicable; second to describe a surprisingly simple solution to the central problem of binding time analysis, and third to prove that the partial evaluator yields correct answers. While λ-mix (the name of our system) seems to have been the first higher-order self-applicable partial evaluator to run on a computer, it was developed mainly for research purposes. Two recently developed systems are much more powerful for practical use, but also much more complex: Similix[3,5] and Schism[7]. Our partial evaluator is surprisingly simple, completely automatic, and has been implemented in a side effect-free subset of Scheme. It has been used to compile, generate compilers and generate a compiler generator.


title: Denotational Semantics of a Goal-Directed Language

abstract: Goal-directed evaluation is a very expressive programming language paradigm that is supported in relatively few languages. It is characterized by evaluation of expressions in an attempt to meet some goal, with resumption of previous expressions on failure. This paradigm is found in SNOBL4 in its pattern-matching facilities, and in Icon as a general part of the language. This paper presents a denotational semantics of Icon and shows how Icon is in fact a combination of two distinct paradigms, goal-directed evaluation and functional application. The two paradigms are not supported separately in different contexts, but integrated fully into a single evaluation mechanism.


title: Subsequence References: First-Class Values for Substrings

abstract: Arrays of characters are a basic data type in many programming languages, but strings and substrings are seldom accorded first-class status as parameters and return values. Such status would enable a routine that calls a search function to readily access context on both sides of a return value. To enfranchise substrings, this paper describes a new data type for substrings as a special case of one for general subsequences. The key idea is that values are not sequences or references to positions in sequences, but rather references to subsequences. Primitive operations on the data type are constants, concatenation, and four new functions— base , start , next , and extent —which map subsequence references to subsequence references. This paper informally presents the data type, demonstrates its convenience for defining search functions, and shows how it can be concisely implemented. Examples are given in Ness, a language incorporating the new data type, which is implemented as part of the Andrew User Interface System.


title: Incremental Generation of Lexical Scanners

authors:
Jan Heering
Paul Klint
J. Rekers

abstract: It is common practice to specify textual patterns by means of a set of regular expressions and to transform this set into a finite automaton to be used for the scanning of input strings. In many applications, the cost of this preprocessing phase can be amortized over many uses of the constructed automaton. In this paper new techniques for lazy and incremental scanner generation are presented. The lazy technique postpones the construction of parts of the automaton until they are really needed during the scanning of input. The incremental technique allows modifications to the original set of regular expressions to be made and reuses major parts of the previous automaton. This is interesting in applications such as environments for the interactive development of language definitions in which modifications to the definition of lexical syntax and the uses of the generated scanners alternate frequently.


title: Computer-Assisted Microanalysis of Parallel Programs

authors:
Timothy J. Hickey
Jacques Cohen
Hitofumi Hotta
Thierry PetitJean

abstract: This paper consists of two parts: the first provides the theoretical foundations for analyzing parallel programs and illustrates how the theory can be applied to estimate the execution time of a class of parallel programs being executed on a MIMD computer. The second part describes a program analysis system, based on the theoretical model, which allows a user to interactively analyze the results of executing (or simulating the execution) of such parallel programs. Several examples illustrating the use of the tool are presented. A novel contribution is the separation (both at the conceptual and the implementation levels) of the machine-independent and the machine-dependent parts of the analysis. This separation enables the users of the system to establish speed-up curves for machines having varying characteristics.


title: The CLP(R) Language and System

authors:
Joxan Jaffar
Spiro Michaylov
Peter J. Stuckey
Roland H. C. Yap


title: An Object-Based Programming Model for Shared Data

authors:
Gail E. Kaiser
Brent Hailpern

abstract: The classical object model supports private data within objects and clean interfaces between objects, and by definition does not permit sharing of data among arbitrary objects. This is a problem for real-world applications, such as advanced financial services and integrated network management, where the same data logically belong to multiple objects and may be distributed over multiple nodes on the network. Rather than give up the advantages of encapsulated objects in modeling real-world entities, we propose a new object model that supports shared data in a distributed environment. The key is separating distribution of computation units from information-hiding concerns. Minimal units of data and control, called facets , may be shared among multiple objects and are grouped into processes . Thus, a single object, or information-hiding unit, may be distributed among multiple processes, or computation units. In other words, different facets of the same object may reside in different address spaces on different machines. We introduce our new object model, describe a motivating example from the financial domain, and then explain facets, objects, and processes, followed by timing and synchronization concerns.


title: Type Matching, Type-Graphs, and the Schanuel Conjecture

authors:
Jacob Katzenelson
Shlomit S. Pinter
Eugen Schenfeld

abstract: This work considers type systems that are defined by type-graphs (tgraphs), which are rooted directed graphs with order among the edges leaving each node. Tgraphs are uniquely mapped into polynomials which, in turn, are each evaluated at a special point to yield an irrational number named the tgraph's magic number . This special point is chosen using the Schanuel conjecture. It is shown that each tgraph can be uniquely represented by this magic number; namely, types are equal if and only if the corresponding magic numbers are equal. Since irrational numbers require infinite precision, the algorithm for generating magic numbers is carried out using a double-precision floating-point approximation. This approximation is viewed as a hashing scheme, mapping the infinite domain of the irrational numbers into finite computer words. The proposed hashing scheme was investigated experimentally, with the conclusion that it is a good and practical hashing method. In tests involving over a million randomly chosen tgraphs, we have not encountered a single collision. We conclude that this method for representation and management of types is practical, and offers novel possibilities for enforcing strict type matching at link time among separately compiled modules.


title: Cache Behavior of Combinator Graph Reduction

authors:
Philip J. Koopman Jr.
Peter Lee
Daniel P. Siewiorek

abstract: The results of cache-simulation experiments with an abstract machine for reducing combinator graphs are presented. The abstract machine, called TIGRE, exhibits reduction rates that, for similar kinds of combinator graphs on similar kinds of hardware, compare favorably with previously reported techniques. Furthermore, TIGRE maps easily and efficiently onto standard computer architectures, particularly those that allow a restricted form of self-modifying code. This provides some indication that the conventional "stored program" organization of computer systems is not necessarily an inappropriate one for functional programming language implementations. This is not to say, however, that present day computer systems are well equipped to reduce combinator graphs. In particular, the behavior of the cache memory has a significant effect on performance. In order to study and quantify this effect, trace-driven cache simulations of a TIGRE graph reducer running on a reduced instruction-set computer are conducted. The results of these simulations are presented with the following hardware-cache parameters varied: cache size, block size, associativity, memory update policy, and write-allocation policy. To begin with, the cache organization of a commercially available system is used and then the performance sensitivity with respect to variations of each parameter are measured. From the results of the simulation study, a conclusion is made that combinator-graph reduction using TIGRE runs most efficiently when using a cache memory with an allocate-on-write-miss strategy, moderately large block size (preferably with subblock placement), and copy-back memory updates.


title: A Model Parametric Real-Time Logic

authors:
Angelo Morzenti
Dino Mandrioli
Carlo Ghezzi

abstract: TRIO is a formal notation for the logic-based specification of real-time systems. In this paper the language and its straightforward model-theoretic semantics are briefly summarized. Then the need for assigning a consistent meaning to TRIO specifications is discussed, with reference to a variety of underlying time structures such as infinite-time structures (both dense and discrete) and finite-time structures. The main motivation is the ability to validate formal specifications. A solution to this problem is presented, which gives a new, model-parametric semantics to the language. An algorithm for constructively verifying the satisfiability of formulas in the decidable cases is defined, and several important temporal properties of specifications are characterized.


title: M-Lisp: A Representation-Independent Dialect of Lisp with Reduction Semantics

abstract: In this paper we introduce M-LISP, a dialect of LISP designed with an eye toward reconciling LISP's metalinguistic power with the structural style of operational semantics advocated by Plotkin [28]. We begin by reviewing the original definition of LISP [20] in an attempt to clarify the source of its metalinguistic power. We find that it arises from a problematic clause in this definition. We then define the abstract syntax and operational semantics of M-LISP, essentially a hybrid of M-expression LISP and Scheme. Next, we tie the operational semantics to the corresponding equational logic. As usual, provable equality in the logic implies operational equality. Having established this framework we then extend M-LISP with the metalinguistic eval and reify operators (the latter is a nonstrict operator that converts its argument to its metalanguage representation). These operators encapsulate the matalinguistic representation conversions that occur globally in S-expression LISP. We show that the naive versions of these operators render LISP's equational logic inconsistent. On the positive side, we show that a naturally restricted form of the eval operator is confluent and therefore a conservative extension of M-LISP. Unfortunately, we must weaken the logic considerably to obtain a consistent theory of reification.


title: Incremental Global Reoptimization of Programs

authors:
Lori L. Pollock
Mary Lou Soffa

abstract: Although optimizing compilers have been quite successful in producing excellent code, two factors that limit their usefulness are the accompanying long compilation times and the lack of good symbolic debuggers for optimized code. One approach to attaining faster recompilations is to reduce the redundant analysis that is performed for optimization in response to edits, and in particulars, small maintenance changes, without affecting the quality of the generated code. Although modular programming with separate compilation aids in eliminating unnecessary recompilation and reoptimization, recent studies have discovered that more efficient code can be generated by collapsing a modular program through procedure inlining. To avoid having to reoptimize the resultant large procedures, this paper presents techniques for incrementally incorporating changes into globally optimized code. An algorithm is given for determining which optimizations are no longer safe after a program change, and for discovering which new optimizations can be performed in order to maintain a high level of optimization. An intermediate representation is incrementally updated to reflect the current optimizations in the program. Analysis is performed in response to changes rather than in preparation for possible changes, so analysis is not wasted if an edit has no far-reaching effects. The techniques developed in this paper have also been exploited to improve on the current techniques for symbolic debugging of optimized code.


title: A Stepwise Refinement Heuristic for Protocol Construction

authors:
A. Udaya Shankar
Simon S. Lam

abstract: A stepwise refinement heuristic to construct distributed systems is presented. The heuristic is based on a conditional refinement relation between system specifications, and a “Marking”. It is applied to construct four sliding window protocols that provide reliable data transfer over unreliable communication channels. The protocols use modulo- N sequence numbers. The first protocol is for channels that can only lose messages in transit. By refining this protocol, we obtain three protocols for channels that can lose, reorder, and duplicate messages in transit. The protocols herein are less restrictive and easier to implement than sliding window protocols previously studied in the protocol verification literature.


title: Epochs

abstract: To date, the implementation of message passing languages has required hte communications variables (sometimes called ports) either to be limited to the number of physical communications registers in the machine or to be mapped to memory. Neither solution is satisfactory. Limiting the number of variables decreases modularity and efficiency of parallel programs. Mapping variables to memory increases the cost of communications and the granularity of parallelism. We present here a new programming language construct called epochs . Epochs are a scoping mechanism within which the programmer can declare communications variables, which are live only during the scope of that epoch. To limit the range of time a register has to be allocated for a communications variable, the compiler ensures that all processors enter an epoch simultaneously. The programming style engendered fits somewhere between the SIMD data parallel and the MIMD process spawning models. We describe an implementation for epochs including an efficient synchronization mechanism, a means of statically binding registers to communications variables, and a method of fusing epochs to reduce synchronization overhead.


title: An Adaptive Tenuring Policy for Generation Scavengers

authors:
David M. Ungar
Frank Jackson

abstract: One of the more promising automatic storage reclamation techniques, generation scavenging, suffers poor performance if many objects live for a fairly long time and then die. We have investigated the severity of this problem by simulating a two-generation scavenger using traces taken from actual 4-h sessions. There was a wide variation in the sample runs, with garbage-collection overhead ranging from insignificant, during three of the runs, to severe, during a single run. All runs demonstrated that performance could be improved with two techniques: segregating large bitmaps and strings, and adapting the scavenger's tenuring policy according to demographic feedback. We therefore incorporated these ideas into a commercial Smalltalk implementation. These two improvements deserve consideration for any storage reclamation strategy that utilizes a generation scavenger.


title: Experience with a Software-Defined Machine Architecture

abstract: We have built a system in which the compiler back end and the linker work together to present an abstract machine at a considerably higher level than the actual machine. The intermediate language translated by the back end is the target language of all high-level compilers and is also the only assembly language generally available. This lets us do intermodule register allocation, which would be harder if some of the code in the program had come from a traditional assembler, out of sight of the optimizer. We do intermodule register allocation and pipeline instruction scheduling at link time, using information gathered by the compiler back end. The mechanism for analyzing and modifying the program at link time is also useful in a wide array of instrumentation tools.


title: Trace-Based Network Proof Systems: Expressiveness and Completeness

authors:
Jennifer Widom
David Gries
Fred B. Schneider

abstract: We consider incomplete trace-based network proof systems for safety properties, identifying extensions that are necessary and sufficient to achieve relative completeness. We investigate the expressiveness required of any trace logic to encode these extensions.


title: A Calculus for Access Control in Distributed Systems

authors:
Martín Abadi
Michael Burrows
Butler W. Lampson
Gordon D. Plotkin

abstract: We study some of the concepts, protocols, and algorithms for access control in distributed systems, from a logical perspective. We account for how a principal may come to believe that another principal is making a request, either on his own or on someone else's behalf. We also provide a logical language for accesss control lists and theories for deciding whether requests should be granted.


title: Composing Specifications

authors:
Martín Abadi
Leslie Lamport

abstract: A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle because a component need behave correctly only when its environment does, and each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.


title: Lazy Caching

authors:
Yehuda Afek
Geoffrey M. Brown
Michael Merritt

abstract: This paper examines cache consistency conditions for multiprocessor shared memory systems. It states and motivates a weaker condition than is normally implemented. An algorithm is presented that exploits the weaker condition to achieve greater concurrency. The algorithm is shown to satisfy the weak consistency condition. Other properties of the algorithm and possible extensions are discussed.


title: Subtyping Recursive Types

authors:
Roberto M. Amadio
Luca Cardelli

abstract: We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, we relate various definitions of type equivalence and subtyping that are induced by a model, an ordering on infinite trees, an algorithm, and a set of type rules. We show soundness and completeness among the rules, the algorithm, and the tree semantics. We also prove soundness and a restricted form of completeness for the model. To address the second question, we show that to every pair of types in the subtype relation we can associate a term whose denotation is the uniquely determined coercion map between the two types. Moreover, we derive an algorithm that, when given a term with implicit coercions, can infer its least type whenever possible.


title: A General Framework for Semantics-Based Bottom-Up Abstract Interpretation of Logic Programs

authors:
Roberto Barbuti
Roberto Giacobazzi
Giorgio Levi

abstract: The theory of abstract interpretation provides a formal framework to develop advanced dataflow analysis tools. The idea is to define a nonstandard semantics which is able to compute, in finite time, an approximated model of the program. In this paper, we define an abstract interpretation framework based on a fixpoint approach to the semantics. This leads to the definition, by means of a suitable set of operators, of an abstract fixpoint characterization of a model associated with the program. Thus, we obtain a specializable abstract framework for bottom-up abstract interpretations of definite logic programs. The specialization of the framework is shown on two examples, namely, gound-dependence analysis and depth-kanalysis.


title: Reasoning About Naming Systems

authors:
Mic Bowman
Saumya K. Debray
Larry L. Peterson

abstract: This paper defines a simple model, called a preference hierarchy, that provides a framework for using the information available to a naming system to compute the object(s) identified by a given name. The preference hierarchy therefore serves as a formal tool for designing and reasoning about naming systems.


title: Interprocedural Optimization: Eliminating Unnecessary Recompilation

authors:
Michael G. Burke
Linda Torczon

abstract: While efficient new algorithms for interprocedural data-flow analysis have made these techniques practical for use in production compilation systems,a new problem has arisen: collecting and using interprocedural information in a compiler introduces subtle dependence among the proceduresof a program.If the compiler dependson interprocedural information to optimize a given module, a subsequentediting changeto another module in the program may changethe interprocedural information and necessitaterecompilation.To avoid having to recompile every module in a program in responseto a single editing changeto one module, we have developed techniques to more precisely determine which compilations have actually been invalidated by a changeto the program's source.This paper presents a general recoi-npzlatton test to determine which proceduresmust be compiled in responseto a series of editing changes.Three different implementation strategies, which demonstrate the fundamental tradeoff between the cost of analysis and the precision of the resulting test, are also discussed.


title: Compiling Nested Data-Parallel Programs for Shared-Memory Multiprocessors

abstract: While data parallelism is well-suited from algorithmic, architectural, and linguistic considerations to serve as a basis for portable parallel programming, its characteristic fine-grained parallelism makes the efficient implementation of data-parallel languages on MIMD machines a challenging task. The design, implementation, and evaluation of an optimizing compiler are presented for an applicative nested data-parallel language called VCODE targeted at the Encore Multimax, a shared-memory multiprocessor. The source language supports nested aggregate data types; aggregate operations including elementwise forms, scans, reductions, and permutations; and conditionals and recursion for control flow. A small set of graph-theoretic compile-time optimizations reduce the overheads on MIMDmachines in several ways: by increasing the grain size of the output program, by reducing synchronization and storage requirements, and by improving locality of reference. The two key ideas behind these...


title: The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems

authors:
Rance Cleaveland
Joachim Parrow
Bernhard Steffen

abstract: The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth: a variety of different verification methods, including equivalence checking, preorder checking, and model checking, are supported for several different process semantics. One experience from our work is that a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.


title: Parameterized Partial Evaluation

authors:
Charles Consel
Siau-Cheng Khoo

abstract: article Free AccessParameterized partial evaluation Authors: Charles Consel Yale University Yale UniversityView Profile , Siau Cheng Khoo Yale University Yale UniversityView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 15Issue 3pp 463–493https://doi.org/10.1145/169683.174155Published:01 July 1993Publication History 47citation352DownloadsMetricsTotal Citations47Total Downloads352Last 12 Months11Last 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 AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF


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

authors:
Max Copperman
Charles E. McDowell

abstract: When attempting to debug optimized programs, most debuggers may give misleading information about the value of variables at breakpoints.Hennessy proposed a set of algorithms for generating optimized code and determining when, in the generated code, the reported values would be misleading-and under certain circumstances actually recovering the "expected" value of the variable (i.e., one that would not be misleading).We point out where the assumptions made by Hennessy need to be revised due to advances in compiler and debugger technology, and give references for current work on this revised problem.


title: Cost Analysis of Logic Programs

authors:
Saumya K. Debray
Nai-Wei Lin

abstract: Cost analysis of programs has been studied in the context of imperative and functional programming languages. For logic programs, the problem is complicated by the fact that programs may be nondeterministic and produce multiple solutions. A related problem is that because failure of execution is not an abnormal situation, it is possible to write programs where implicit failures have to be dealt with explicitly in order to get meaningful results. This paper addresses these problems and develops a method for (semi-)automatic analysis of the worst-case cost of a large class of logic programs. The primary contribution of this paper is the development of techniques to deal with nondeterminism and the generation of multiple solutions via backtracking. Applications include program transformation and synthesis, software engineering, and in parallelizing compilers. Categories and Subject Descriptors: D.1 [Software]: Programming Techniques; D.1.6 [Program- ming Techniques]: Logic Progra...


title: An Elimination Algorithm for Bidirectional Data Flow Problems Using Edge Placement

authors:
Dhananjay M. Dhamdhere
Harish Patil

abstract: Bidirectional data flow problems, useful in a wide range of optimizing transformations, are conventionally solved using the iterative approach.Thm paper shows that use of the edge placement technique makes bidirectional data flow problems amenable to effkient solution.An elimination algorithm for bidirectional data flow problems using edge placement is presented, and its complexity is shown to be ldentlcal to the complexity of elimination algorithms for unidirectional data flows.


title: A Formal Definition of Priority in CSP

abstract: The process models of Ada and occam are formally based on the CSP process algebra. However, for fine-tuning real-time performance, they include “prioritized” constructs that have no counterparts in CSP. These constructs therefore lack any formal definition, a situation that leaves room for misunderstandings. We extend CSP with a formal definition of the notion of priority. The definition is then used to assess the transputer implementation of priority in occam and the definition of priority in Ada.


title: A Correction to the Denotational Semantics for the Prolog of Nicholson and Foo

authors:
Alan Finlay
Lloyd Allison

abstract: article Free Access Share on Technical correspondence: a correction to the denotational semantics for the Prolog of Nicholson and Foo Authors: Alan Finlay Monash Univ. Monash Univ.View Profile , Lloyd Allison Monash Univ. Monash Univ.View Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 15Issue 1Jan. 1993 pp 206–208https://doi.org/10.1145/151646.151652Published:01 January 1993Publication History 0citation179DownloadsMetricsTotal Citations0Total Downloads179Last 12 Months5Last 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: An Alternative Solution to a Problem on Self-Stabilization

abstract: Dijkstra [4, 5] introduced the problem of self-stabilization in distributed systems as an interesting exercise for achieving global convergence through local actions. In [4] he presented three solutions to a specific version of the self-stabilization problem, one of which was proved in [6]. This paper presents an alternative solution of his self-stabilization problem with four-state machines.


title: Analysis of Or-Parallel Execution Models

authors:
Gopal Gupta
Bharat Jayaraman

abstract: We discuss fundamental limitations of or-parallel execution models of nondeterministic programming languages. Or-parallelism corresponds to the execution of different nondeterministic computational paths in parallel. A natural way to represent the state of (parallel) execution of a nondeterministic program is by means of an or-parallel tree. We identify three important criteria that underlie the design of or-parallel implementations based on the or-parallel tree: constant-time access to variables, constant-time task creation, and constant-time task switching, where the term constant-time means that the time for these operations is independent of the number of nodes in the or-parallel tree, as well as the size of each node. We prove that all three criteria cannot be simultaneously satisfied by any or-parallel execution model based on a finite number of processors but unbounded memory. We discuss in detail the application of our result to the class of logic programming languages and show how our result can serve as a useful way to categorize the various or-parallel methods proposed in this field. We also discuss the suitability of different or-parallel implemenation strategies for different parallel architectures.


title: On the Type Structure of Standard ML

authors:
Robert Harper
John C. Mitchell

abstract: Standard ML is a useful programming language with a polymorphic type system and a flexible module facility.One notable feature of the core expression language of ML is that it is implicdy typed: no explicit type information need be supplied by the programmer.In contrast, the module language of ML is explicitly typed; in particular, the types of parameters in parametric modules must be supplied by the programmer.We study the type structure of Standard ML by giving an explicitly-typed, polymorphic function calculus that captures many of the essential aspects of both the core and module language.In this setting, implicitly-typed core language expressions are regarded as a convenient short-hand for an explicitly-typed counterpart in our function calculus.In contrast to the Girard-Reynolds polymorphic calculus, our function calculus is


title: Type Inference with Polymorphic Recursion

abstract: Henglein(1) The resulting typing discipline cannot be explained in a syntax-directed fashion, but is rather reminiscent of data-flow oriented reasoning.This


title: A Methodology for Implementing Highly Concurrent Objects

abstract: A concurrent object is a data structure shared by concurrent processes. Conventional techniques for implementing concurrent objects typically rely on critical sections ; ensuring that only one process at a time can operate on the object. Nevertheless, critical sections are poorly suited for asynchronous systems: if one process is halted or delayed in a critical section, other, nonfaulty processes will be unable to progress. By contrast, a concurrent object implementation is lock free if it always guarantees that some process will complete an operation in a finite number of steps, and it is wait free if it guarantees that each process will complete an operation in a finite number of steps. This paper proposes a new methodology for constructing lock-free and wait-free implementations of concurrent objects. The object's representation and operations are written as stylized sequential programs, with no explicit synchronization. Each sequential operation is atutomatically transformed into a lock-free or wait-free operation using novel synchronization and memory management algorithms. These algorithms are presented for a multiple instruction/multiple data (MIMD) architecture in which n processes communicate by applying atomic read, write, load_linked, and store_conditional operations to a shared memory.


title: Leader Election in Uniform Rings

abstract: article Free Access Share on Leader election in uniform rings Author: Shing-Tsaan Huang National Tsing-Hua University, Taiwan National Tsing-Hua University, TaiwanView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 15Issue 301 July 1993pp 563–573https://doi.org/10.1145/169683.174161Published:01 July 1993Publication History 57citation803DownloadsMetricsTotal Citations57Total Downloads803Last 12 Months27Last 6 weeks3 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: A Superimposition Control Construct for Distributed Systems

abstract: article Free Access Share on A superimposition control construct for distributed systems Author: Shmuel Katz Technion–Israel Institute of Technology, Haifa, Israel Technion–Israel Institute of Technology, Haifa, IsraelView Profile Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 15Issue 2April 1993 pp 337–356https://doi.org/10.1145/169701.169682Published:01 April 1993Publication History 122citation463DownloadsMetricsTotal Citations122Total Downloads463Last 12 Months32Last 6 weeks4 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: Type Reconstruction in the Presence of Polymorphic Recursion

authors:
A. J. Kfoury
Jerzy Tiuryn
Pawel Urzyczyn

abstract: We study the problem of type-checking functional programs in three extensions of ML.One distinguishing feature of these extensions is that they allow recursive definitions to be polymorphically typed.Although the motivation for these extensions comes from pragmatic considera-


title: Mathematical Foundations of Time Warp Systems

authors:
Jonathan I. Leivent
Ronald J. Watro

abstract: We develop a simple formal model of the Time Warp approach to distributed computation, prove several important properties of the model, and devise some extensions to Time Warp that provide improved termination behavior. Our model consists of processes that communicate solely via message passing. One of the basic process steps is a rollback operation that includes message retraction via transmission of antimessages. In the model, we consider three problems: safety, progress, and termination. By safety, we mean that for a given system of processes, if a run of the system terminates, then the final system state of the run is identical to the final system state of a rollback-free run. We give premises that imply safety, and a counterexample that shows how safety can fail. By progress, we mean that, as a run of a system proceeds, the minimum timestamp of an unprocessed message always eventually increases. We state three axioms that imply the progress property. By termination, we mean that, if all rollback-free runs of a system terminate, then all runs terminate. The termination property is generally false in existing implementations of Time Warp systems due to the possibility of Time Warp vortices. We define additional mechanisms that can guarantee the termination property for most Time Warp applications.


title: Procedural Implementation of Algebraic Specification

abstract: An implementation of an algebraic specification in an imperative programming language consists of a representation type, together with an invariant and an equivalence relation over it, and a procedure for each operator in the specification. A formal technique is developed to check the correctness of an implementation with respect to its specification. Here “correctness” means that the implementation satisfies the axioms and preserves the behavior of the specification. Within legal representing value space, a correct implementation behaves like a desirable model of the specification. A notion of implementation refinement is also proposed, and it is shown that the correctness relation between implementations and specifications is preserved by implementation refinement. In the extreme case the procedures in an implementation may be pre-post-condition pairs. Such abstract implementations can be refined into executable code by refining the abstract procedures in it. In this way a formal link between the algebraic and the pre- post-condition specification techniques is established.


title: Defining Context-Dependent Syntax Without Using Contexts

abstract: A method for defining context-dependent syntax is presented.The method, like many others,


title: Scheduling Time-Critical Instructions on RISC Machines

authors:
Krishna V. Palem
Barbara B. Simons

abstract: We present a polynomial time algorithm for constructing a minimum completion time schedule of instructions from a basic block on RISC machines such as the Sun SPARC, the IBM 801, the Berkeley RISC machine, and the HP Precision Architecture. Our algorithm can be used as a heuristic for RISC processors with longer pipelines, for which there is no known optimal algorithm. Our algorithm can also handle time-critical instructions, which are instructions that have to be completed by a specific time. Time-critical instructions occur in some real-time computations, and can also be used to make shared resources such as registers quickly available for reuse. We also prove that in the absence of time-critical constraints, a greedy scheduling algorithm always produces a schedule for a target machine with multiple identical pipelines that has a length less than twice that of an optimal schedule. The behavior of the heuristic is of interest because, as we show, the instruction scheduling problem becomes NP-hard for arbitrary length pipelines, even when the basic block of code being input consists of only several independent streams of straightline code, and there are no time-critical constraints. Finally, we prove that the problem becomes NP-hard even for small pipelines, no time-critical constraints, and input of several independent streams of straightline code if either there is only a single register or if no two instructions are allowed to complete simultaneously because of some shared resource such as a bus.


title: The Design of the E Programming Language

authors:
Joel E. Richardson
Michael J. Carey
Daniel T. Schuh

abstract: E is an extension of C++ designed for writing software systems to support persistent applica- tions.Originally designed as a language for implementing database systems, E has evolved into a general persistent programming language E was the first C++ extension to support transparent persistence, the first C++ implementation to support generic classes, and remains the only C++ extension to provide general-purpose lterators, In addition to its contributions to the C + + programming domain, work on E has made several contributions to the field of persmtent languages in general, including several distinct implementations of persistence.Thm paper describes the main features of E and shows through examples how E addresses many of the problems that arise in building persistent systems.


title: The Derivation of Distributed Termination Detection Algorithms from Garbage Collection Schemes

authors:
Gerard Tel
Friedemann Mattern

abstract: It is shown that the termination detection problem for distributed computations can be modeled as an instance of the garbage collection problem. Consequently, algorithms for the termination detection problem are obtained by applying transformations to garbage collection algorithms. The transformation can be applied to collectors of the “mark-and-sweep” type as well as to reference-counting protocol of Lermen and Maurer, the weighted-reference-counting protocol, the local-reference-counting protocol, and Ben-Ari's mark-and-sweep collector into termination detection algorithms. Known termination detection algorithms as well as new variants are obtained.


title: An Old-Fashined Recipe for Real-Time

authors:
Martín Abadi
Leslie Lamport

abstract: Traditional methods for specifying and reasoning about concurrent systems work for real-time systems. Using TLA (the temporal logic of actions), we illustrate how they work with the examples of a queue and of a mutual-exclusion protocol. In general, two problems must be addressed: avoiding the real-time programming version of Zeno's paradox, and coping with circularities when composing real-time assumption/guarantee specifications. Their solutions rest on properties of machine closure and realizability.


title: A Bounded First-In, First-Enabled Solution to the l-Exclusion Problem

authors:
Yehuda Afek
Danny Dolev
Eli Gafni
Michael Merritt
Nir Shavit

abstract: This article presents a solution to the first-come, first-enabled ℓ-exclusion problem of Fischer et al. [1979]. Unlike their solution, this solution does not use powerful read-modify-write synchronization primitives and requires only bounded shared memory. Use of the concurrent timestamp system of Dolev and Shavir [1989] is key in solving the problem within bounded shared memory.


title: Functions as Passive Constraints in LIFE

authors:
Hassan Aït-Kaci
Andreas Podelski

abstract: LIFE is a programming language proposing to integrate logic programming, functional programming, and object-oriented programming. It replaces first-order terms with ψ-terms, data structures that allow computing with partial information. These are approximation structures denoting sets of values. LIFE further enriches the expressiveness of ψ-terms with functional dependency constraints. We must explain the meaning and use of functions in LIFE declaratively, as solving partial information constraints. These constraints do not attempt to generate their solutions but behave as demons filtering out anything else. In this manner, LIFE functions act as declarative coroutines. We need to show that the ψ-term's approximation semantics is congruent with an operational semantics viewing functional reduction as an effective enforcing of passive constraints. In this article, we develop a general formal framework for entailment and disentailment of constraints based on a technique called relative simplification. We study its operational and semantical properties, and we use it to account for functional application over ψ-terms in LIFE.


title: Axiomatic Bootstrapping: A Guide for Compiler Hackers

abstract: If a compiler for language L is implemented in L , then it should be able to compile itself. But for systems used interactively commands are compiled and immediately executed, and these commands may invoke the compiler; so there is the question of how ever to cross-compile for another architecture. Also, where the compiler writes binary files of static type information that must then be read in by the bootstrapped interactive compiler, how can one ever change the format of digested type information in binary files? Here I attempt an axiomatic clarification of the bootstrapping technique, using Standard ML of New Jersey as a case study. This should be useful to implementors of any self-applicable interactive compiler with nontrivial object-file and runtime-system compatibility problems.


title: On the Occur-Check-Free Prolog Programs

authors:
Krzysztof R. Apt
Alessandro Pellegrini

abstract: In most PROLOG implementations, for efficiency occur-check is omitted from the unification algorithm. This paper provides natural syntactic conditions that allow the occur-check to be safely omitted. The established results apply to most well-known PROLOG programs, including those that use difference lists, and seem to explain why this omission does not lead in practice to any complications. When applying these results to general programs, we show their usefulness for proving absence of floundering. Finally, we propose a program transformation that transforms every program into a program for which only the calls to the built-in unification predicate need to be resolved by a unification algorithm with the occur-check.


title: Some Comments on "A Denotational Semantics for Prolog"

authors:
Bijan Arbab
Daniel M. Berry

abstract: Two independently derived denotational semantics for Prolog are contrasted, Arbab and Berry's for the full language and Nicholson and Foo's for a databaseless language. Using the ideas suggested by the former, the latter can be easily extended to include the database operations.


title: Fixpoint Computation for Polyvariant Static Analyses of Higher-Order Applicative Programs

authors:
J. Michael Ashley
Charles Consel

abstract: This paper presents an optimized general-purpose algorithm for polyvariant, static analyses of higher-order applicative programs. A polyvariant analysis is a very accurate form of analysis that produces many more abstract descriptions for a program than does a conventional analysis. It may also compute intermediate abstract descriptions that are irrelevant to the final result of the analysis. The optimized algorithm addresses this overhead while preserving the accuracy of the analysis. The algorithm is also parameterized over both the abstract domain and degree of polyvariance. We have implemented an instance of our algorithm and evaluated its performance compared to the unoptimized algorithm. Our implementation runs significantly faster on average than the other algorithm for benchmarks reported here.