Proving correctness of coroutines without history variables

We examine the question of whether history variables are necessary in formal proofs of correctness for coroutines. History variables are special variables, which are added to a program to facilitate its proof by recording the sequence of states reached by the program during a computation; after the proof has been completed the history variables may be deleted. The use of such variables in correctness proofs was first suggested by Clint [CL73] in a paper entitled Program Proving: Coroutines; subsequently, history variables have been used by Owicki [OW76a] and Howard [HO75] in verifying concurrent programs and by Apt [APT77] in verifying sequential programs. We argue that recording the entire history of a computation in a single set of variables can actually complicate a correctness proof and should be avoided if possible. We propose a modification of Clint's axiom system and a strategy for constructing proofs that eliminates the need for history variables in verifying simple coroutines. Examples (including Clint's program Histo) are given to illustrate this technique of verifying coroutines, and our axiom system is shown to be sound and relatively complete with respect to an operational semantics for coroutines. Finally, we discuss extensions of the coroutine concept for which history variables do appear to be needed; we also discuss the question of whether such variables are necessary in verifying concurrent programs.The preparation of this paper was supported by NSF Grant MCS-75-08146.     

Declarative diagnosis of missing answers

This paper investigates algorithms for declarative diagnosis of missing answers in Prolog programs, especially programs which use coroutines. The logic of the problem is first presented, in the form of the simplest possible debugger. Next, we compare several previously published declarative debuggers based on Shapiro’s work. Examples showing incompleteness, incorrectness and equivalence of debuggers are given. Several enhancements to these debuggers are presented which can reduce the number and complexity of questions asked of the oracle, while still supporting coroutines. Although no debugger considered is best in all cases, the new algorithms are a practical contribution. Finally, we discuss diagnosis algorithms based more on Pereira’s work. These algorithms ask easier questions than Shapiro’s algorithms but rely on the standard left to right computation rule. We discuss possible ways to adapt these algorithms to handle coroutining. Completeness of debuggers is also discussed.     

Program proving: Jumps and functions

Summary Proof methods adequate for a wide range of computer programs have been expounded in [1] and [2]. This paper develops a method suitable for programs containing functions, and a certain kind Of jump. The method is illustrated by the proof of a useful and efficient program for table lookup by logarithmic search.     

A low-cost implementation of coroutines for C

We identify a set of primitive operations supporting coroutines, and demonstrate their usefulness. We then address their implementation in C according to a set of criteria aimed at maintaining simplicity, and achieve a satisfactory compromise between it and effectiveness. Our package for the PDP-11 under UNIX? allows users of coroutines in C programs to gain access to the primitives via an included definitions file and an object library; no penalty is imposed upon non-coroutine users.     

Reverse execution in a generalized control regime

The value of advanced control forms in programming languages is currently being recognized. A combination of control forms in a single environment can increase the expressive power of a system but may lead to difficulties in semantic definition and implementation. This paper describes an implementation for a control combination of backtracking and logical concurrent structures. In particular, we present a reversible execution implementation for backtracking across scheduled coroutines or processes as defined in Simula [1]. Such a control combination, particularly useful for debugging simulation programs, is incorporated as a basic feature in a debugging tool expecially designed for programs using scheduled processes.     

Bidirectional coroutines

The bidirectional coroutine is introduced as a mechanism for overcoming a shortcoming in the method of specification of the transfer of control between coroutines. An analogy is drawn between subroutines and coroutines by observing that coroutines, like subroutines, should not have to know with whom they are interacting. At present, most coroutine implementations require specific mention of the coroutine being resumed, or use a suspend mechanism in which case one coroutine acts as a slave (the suspending one) and the other as a master. In the second case, the slave need not know the identity of its master while the master must know the identity of its slave. For bidirectional coroutines, a coroutine need not know the identity of its master nor its slave. This is achieved by replacing the suspend primitive with two new primitives — resume master and resume slave.     

Experiences with coroutines in BCPL

This communication describes a typical application of BCPL coroutines in simplifying the implementation of a multi-event task, together with some problems encountered. The problems fall into two major groups: those associated with the routing of operating system messages to coroutines within a task, and those connected with data shared between coroutines. General solutions are suggested to these problems, which can occur in any program employing similar structures.     

Stable marriages by coroutines

The stable marriage problem is an appealing version of many pairing problems. A solution by coroutines is given, based on the recursive algorithm of McVitie and Wilson (1971). There are few published algorithms where coroutines are really useful but they solve this problem very naturally.     

Towards reasoning about Hoare relations

A logical framework is presented for defining semantics of programs that satisfy Hoare postulates. The two families of logical systems are given: modal systems and relational systems. In the modal systems semantics of Hoare-style programming languages is provided in terms of relations and sets, and in relational systems in terms of relations only. Proof theory for the given logics is presented.     

Implementing a simulation tool in a high-level language with no multitasking facilities

Ways to implement coroutines in a block-structured language with no multitasking facilities are presented. Coroutines are implemented as procedures. The reactivation points are kept in global variables, one variable for each procedure. Local variables whose values are required on re-entry are stored as STATIC objects. The variables or data of re-entrant coroutines are stored in an event list associated with each such coroutine. A procedure with several entries is a convenient mechanism to trap the primitive calls issued by the coroutines. This procedure returns to the master program by using a non-local GOTO. The implementation of the above in PL/I and C is described and a comparison is made with sequential Pascal. Ada includes constructs which satisfy most requirements.     

The contraction of control implementations

The implementation of a high level language which provides higher control forms such as concurrency and coroutines along with the more traditional recursive procedures is obligated to support all control forms in a reasonably efficient manner. In particular, the implementation of a general purpose language (such as Simula or Ada) should contract gracefully into a scheme incurring overhead approximately the same amount as a simple stack when presented with programs which employ control forms no more general than recursive procedures. This study is a quantitative investigation into the contraction of implementations capable of supporting higher control forms into an environment in which recursive procedures are the most complex control form. A technique called the stack-heap is shown to contract most fully.     

Coroutine behaviour and implementation

Algorithms using retentive control are currently being developed in operating systems, simulation, artificial intelligence and language implementation. This paper investigates two aspects of a form of retentive control, namely coroutines. The behaviour of coroutines and language primitives that express the operations on coroutines are explored by surveying the literature for coroutine usage. Secondly, the area of control implementation of coroutines is investigated by considering the Bobrow and Wegbreit spaghetti stack as a viable data structure for managing run-time storage. Changes in the basic model of the spaghetti stack, tailoring its use in a strictly coroutine environment with subsequent implementation alternatives, are explored. An investigation through experimentation is made of the effect control-related aspects of coroutines have on the revised spaghetti stack models. An analysis of the empirical results obtained provides a useful barometer for selecting appropriate storage management schemes based on coroutine design and usage.     

Using coroutines in pascal

Coroutines are routines which communicate with each other in a more general way than that provided by the normal subroutine mechanism. Although they have many potential applications, their use has been restricted by their lack of availability in common high-level languages. This paper discusses some of the issues involved in implementing coroutines, and proposes an implementation written in Pascal which may be incorporated into a Pascal program to give coroutine facilities. Use of the system is illustrated by two solutions to the N-Queens problem by different coroutine strategies. The basic system is then extended to allow more advanced use of coroutines.     

A proof technique for communicating sequential processes

Summary Proof rules are presented for an extension of Hoare's Communicating Sequential Processes. The rules deal with total correctness; all programs terminate in the absence of deadlock. The commands send and receive are treated symmetrically, simplifying the rules and allowing send to appear in guards. Also given are sufficient conditions for showing that a program is deadlock-free. An extended example illustrates the use of the technique.This research was supported in part by the National Science Foundation under grant MCS-7622360.     

An application of coroutines and backtracking in interactive systems

A software structure well-suited for the programming of interactive recognition and translation systems is described. This structure makes use of coroutines and backtracking in a highly coordinated and integrated fashion. A set of coroutine and backtracking primitives that supports this approach is defined. An example of the use of this approach is given.     

Proving weak properties of rewriting

In rule-based programming, properties of programs, such as termination, are in general considered in their strong acceptance, i.e., on every computation branch. But in practice, they may hold in their weak acceptance only, i.e., on at least one computation branch. Moreover, weak properties are often enough to ensure that programs give the expected result. There are very few results to handle weak properties of rewriting. We address here two of them: termination and reducibility to a constructor form, in a unified framework allowing us to prove them inductively. Proof trees are developed, which simulate rewriting trees by narrowing and abstracting subterms. Our technique is constructive in the sense that proof trees can be used to infer an evaluation strategy for any given input: the right computation branch is developed without using a costly breadth-first strategy nor backtracking.     

Note sulla derivata di un programma

In this paper, we consider while-program-schemata, as defined, for example, in [1] [2] [3], interpreted over a domain of functions and predicates over the real numbers. We observe that the (real) functions computed by programs of this kind are representable by (non recursive) Algol-like expressions which are, in general, too complicated to be treated with the methods of classical mathematical analysis. As an example of how to extend classical analytical concepts to functions computed by programs, we give a method for constructing in an algorithmic way a program which computes the derivative of the function computed by a given program, if such a derivative exists. A simple example is given.     

Combining Proof Plans with Partial Order Planning for Imperative Program Synthesis

The structured programming literature provides methods and a wealth of heuristic knowledge for guiding the construction of provably correct imperative programs. We investigate these methods and heuristics as a basis for mechanizing program synthesis. Our approach combines proof planning with conventional partial order planning. Proof planning is an automated theorem proving technique which uses high-level proof plans to guide the search for proofs. Proof plans are structured in terms of proof methods, which encapsulate heuristics for guiding proof search. We demonstrate that proof planning provides a local perspective on the synthesis task. In particular, we show that proof methods can be extended to represent heuristics for guiding program construction. Partial order planning complements proof planning by providing a global perspective on the synthesis task. This means that it allows us to reason about the order in which program fragments are composed. Our hybrid approach has been implemented in a semi-automatic system called Bertha. Bertha supports partial correctness and has been tested on a wide range of non-trivial programming examples.     

Preventing massive automated access to web resources

Automated web tools are used to achieve a wide range of different tasks, some of which are legal activities, whilst others are considered attacks to the security and data integrity of online services. Effective solutions to counter the threat represented by such programs are therefore required. In this work, we present MosaHIP, a Mosaic-based Human Interactive Proof (HIP), which is able to prevent massive automated access to web resources. Properties of the proposed solution grant an improved security over usual text-based and image-based HIPs, whereas the user-friendliness of the system alleviates the user from the discomfort of typing any text before accessing to a web content. Experimental evidence of the effectiveness of the proposed technique is given by submitting our system to a series of tests simulating possible bot attacks.