Running programs backwards: The logical inversion of imperative computation

Imperative programs can be inverted directly from their forward-directed program code with the use of logical inference. The relational semantics of imperative computations treats programs as logical relations over the observable state of the environment, which is taken to be the state of the variables in memory. Program relations denote both forward and backward computations, and the direction of the computation depends upon the instantiation pattern of arguments in the relation. This view of inversion has practical applications when the relational semantics is treated as a logic program. Depending on the logic programming inference scheme used, execution of this relational program can compute the inverse of the imperative program. A number of nontrivial imperative computations can be inverted with minimal logic programming tools.     

Programming Languages For Interactive Computing

Traditional programming languages are algorithmic: they are best suited to writing programs that acquire all their inputs before executing and only produce a result on termination. By contrast most applications are interactive: they maintain ongoing interactions with their environments. Modern systems address this incompatibility by manually extending the execution model of the host language to support interaction, usually by embedding an event-driven state management scheme which executes fragments of imperative code in response to interactions, the job of each executed fragment being to restore the internal consistency of the computation. The downside of this approach to interaction is that it relies heavily on mutable stores and side-effects and mixes application logic in with behaviour which is more properly the responsibility of an execution model. I describe a programming model called declarative interaction which supports interaction directly. The distinguishing feature of the model is its modal construal of state and interaction.     

Evaluating the performance of a SISAL implementation of the abingdon cross image processing benchmark

There are many paradigms being promoted and explored for programming parallel computers, including modified sequential languages, new imperative languages and applicative languages. SISAL is an applicative language which has been designed by a consortium of industrial and research organizations for the specification and execution of parallel programs. It allows programs to be written with little concern for the structure of the underlying machine, thus the programmer is free to explore different ways of expressing the parallelism. A major problem with applicative languages has been their poor efficiency at handling large data structures. To counter this problem SISAL includes some advanced memory management techniques for reducing the amount of data copying that occurs. In this paper we discuss the implementation of some image processing benchmarks in SISAL and C to evaluate the effectiveness of the memory management code. In general, the SISAL program was easier to code than the C (augmented with the PARMACS macros) because we were not concerned with the parallel implementation details. We found that the SISAL performance was in general comparable to C, and that it could be brought in line with an efficient parallel C implementation by some programmer-specified code transformations.     

Yacc in sasl — an exercise in functional programming

Among the advantages claimed for a purely functional programming style is ease of designing and implementing large programs. However, little experience of actually doing so has been gained so far. The experience of writing a particular medium sized program in a functional language is described here, with particular emphasis on the differences in programming style that were appropriate. This is compared with the experience of writing a very similar program in an imperative language. The main conclusions appear to be that the functional version was significantly easier to write, and was considerably smaller, though not by as large a factor as is sometimes claimed; that strong typing is, if anything, more desirable than in imperative systems; and that the question of debugging functional programs needs further research attention.     

Compiler to interpreter: experiences with a distributed programming language

One interpretive approach for handling concurrency is to provide an interpreter instance for each executing language‐level process. Such an approach has mainly been applied to concurrent implementations of logic and functional languages. This paper describes the use of this approach in constructing an interpreter for an imperative, distributed programming language from an existing compiler and run‐time support system (RTS). Primary design goals were to exploit the existing compiler to the extent possible as well as to have minimal impact on the RTS used to support concurrency. We have been successful in meeting these goals. Additionally, performance results show our interpreter's execution times compare favorably to the times required for compilation, linkage, and execution of small programs or programs with a significant number of calls to the RTS; on such programs, our interpreter's performance also compares favorably to that of the standard Java implementation. However, for larger programs and programs with fewer calls to the underlying RTS, the conventional compiler‐based implementation outperforms the interpreter implementation. For many distributed programs in which network costs dominate, the performances of the two implementations differ little. Copyright © 2001 John Wiley & Sons, Ltd.     

Compiler Optimization Correctness by Temporal Logic

Rewrite rules with side conditions can elegantly express many classical compiler optimizations for imperative programming languages. In this paper, programs are written in an intermediate language and transformation-enabling side conditions are specified in a temporal logic suitable for describing program data flow.The purpose of this paper is to show how such transformations may be proven correct. Our methodology is illustrated by three familiar optimizations: dead code elimination, constant folding, and code motion. A transformation is correct if whenever it can be applied to a program, the original and transformed programs are semantically equivalent, i.e., they compute the same input-output function. The proofs of semantic equivalence inductively show that a transformation-specific bisimulation relation holds between the original and transformed program computations.     

An assessment of modula

Wirth has recently published a new programming language called Modula which he suggests is suitable for the programming of process control systems, computerized laboratory equipment and input/output device drivers. The authors have written a compiler for Modula running on a PDP-11 and generating object code for the same machine. Their experience in writing device drivers for a number of PDP-11 devices is reported, including simple mains frequency clocks, disks, CAMAC and a graphics processor. Some difficulties arose during the writing of these programs; these are investigated and solutions proposed, either within the existing language or by minor modifications to the language. The study shows the extent to which Modula meets the requirements for a general purpose real-time systems-implementations programming language; areas of deficiency are noted.     

A comparison of concurrent programming and cooperative multithreading

This paper presents a comparison of the cooperative multithreading model with the general concurrent programming model. It focuses on the execution time performance of a range of standard concurrent programming applications. The overall results are mixed. In some cases, programs written in the cooperative multithreading model outperform those written in the general concurrent programming model. The contributions of this paper are twofold. First, it presents a thorough analysis of the performances of applications in the different models, i.e. to explain the criteria that determine when a program in one model will outperform an equivalent program in the other. Second, it examines the tradeoffs in writing programs in the different programming styles. In some cases, better performance comes at the cost of more complicated code. Copyright © 2003 John Wiley & Sons, Ltd.     

Linear Approximation of Execution-Time Constraints

This paper defines an algorithm for predicting worst-case and best-case execution times, and determining execution-time constraints of control-flow paths through real-time programs using their partial correctness semantics. The algorithm produces a linear approximation of path traversal conditions, worst-case and best-case execution times and strongest postconditions for timed paths in abstract real-time programs. Also shown are techniques for determining the set of control-flow paths with decidable worst-case and best-case execution times. The approach is based on a weakest liberal precondition semantics and relies on supremum and infimum calculations similar to standard computations from linear programming and Presburger arithmetic. The methodology is applicable to any executable language with a predicate transformer semantics and hence provides a verification basis for both high-level language and assembly code execution-time analysis.     

基于Coq的矩阵代码生成技术

矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.     

A wide instruction word architecture for parallel execution of logic programs coded in BSL

This paper begins by describing BSL, a new logic programming language fundamentally different from Prolog. BSL is a nondeterministic Algol-class language whose programs have a natural translation to first order logic; executing a BSL program without free variables amounts to proving the corresponding first order sentence. A new approach is proposed for parallel execution of logic programs coded in BSL, that relies on advanced compilation techniques for extracting fine grain parallelism from sequential code. We describe a new “Very Long Instruction Word” (VLIW) architecture for parallel execution of BSL programs. The architecture, now being designed at the IBM Thomas J. Watson Research Center, avoids the synchronization and communication delays (normally associated with parallel execution of logic programs on multiprocessors), by determining data dependences between operations at compile time, and by coupling the processing elements very tightly, via a single central shared register file. A simulator for the architecture has been implemented and some simulation results are reported in the paper, which are encouraging.     

The Fork95 parallel programming language: Design, implementation, application

Fork95 is an imperative parallel programming language intended to express algorithms for synchronous shared memory machines (PRAMs). It is based on ANSI C and offers additional constructs to hierarchically divide processor groups into subgroups and manage shared and private address subspaces. Fork95 makes the assembly-level synchronicity of the underlying hardware available to the programmer at the language level. Nevertheless, it supports locally asynchronous computation where desired by the programmer. We present a one pass compiler, fcc, which compiles Fork95 and C programs to the SB-PRAM machine. The SB-PRAM is a lock-step synchronous, massively parallel multiprocessor currently being built at Saarbrücken University, with a physically shared memory and uniform memory access time. We examine three important types of parallel computation frequently used for the parallel solution of real-world problems. While farming and parallel divide-and-conquer are directly supported by Fork95 language constructs, pipelining can be easily expressed using existing language features; an additional language construct for pipelining is not required.     

A Structured Synchronization and Communication Model Fitting Irregular Data Accesses

In this paper, we present a parallel programming and execution model based on alogicalordering of control flows. We show that it is possible to provide a unifying framework consisting of a synchronous programming model, thereby facilitating the mastery of programs, and an asynchronous execution model yielding efficient executions. Our approach is based on a SPMD and task parallel programming language, called –Chan. Communications take place through channels and rely on explicit send/receive instructions. In contrast to classical message passing models, synchronizations and communications are dissociated. We show that it is possible to perform a data-driven automatic translation of sequential and arbitrary DOACROSS loops into –Chan, by using nonmatching send/receive instructions. Our parallelization technique allows us to handle irregular control and leads to optimizations of communications in irregular computations.     

Debugging mixed‐environment programs with Blink

Programmers build large‐scale systems with multiple languages to leverage legacy code and languages best suited to their problems. For instance, the same program may use Java for ease of programming and C to interface with the operating system. These programs pose significant debugging challenges, because programmers need to understand and control code across languages, which often execute in different environments. Unfortunately, traditional multilingual debuggers require a single execution environment. This paper presents a novel composition approach to building portable mixed‐environment debuggers, in which an intermediate agent interposes on language transitions, controlling and reusing single‐environment debuggers. We implement debugger composition in Blink, a debugger for Java, C, and the Jeannie programming language. We show that Blink is (i) simple: it requires modest amounts of new code; (ii) portable: it supports multiple Java virtual machines, C compilers, operating systems, and component debuggers; and (iii) powerful: composition eases debugging, while supporting new mixed‐language expression evaluation and Java native interface bug diagnostics. To demonstrate the generality of interposition, we build prototypes and demonstrate debugger language transitions with C for five of six other languages (Caml, Common Lisp, C#, Perl 5, Python, and Ruby) without modifications to their debuggers. Using real‐world case studies, we show that diagnosing language interface errors require prior single‐environment debuggers to restart execution multiple times, whereas Blink directly diagnoses them with one execution. Copyright © 2014 John Wiley & Sons, Ltd.     

IAda: A language for robot programming based on Ada

We present a programming language for robots which we have implemented based on the Ada language. It is an interpreted language which permits dynamic configuration of software. It manipulates Ada tasks and subroutines. One of the Ada tasks is an inference engine of a logic programming language adapted to real-time constraints. We show how the conjunction of Ada tasks, to perform perception and action functions on the robot, to logic programs, for the control of these tasks, both manipulated by the IAda language, gives a powerful environment for robot programming.     

Applications experience in Jade

This paper presents our experience developing applications in Jade, a portable, implicitly parallel programming language designed for exploiting task-level concurrency. Jade programmers start with a program written in a standard serial, imperative language, and then use Jade constructs to describe how parts of the program access data. The Jade implementation analyzes this information to automatically extract the concurrency and execute the program in parallel. The resulting parallel execution is guaranteed to preserve the semantics of the serial program. We have implemented Jade as an extension to C on shared-memory multiprocessors, a homogeneous message-passing machine and networks of heterogeneous workstations. To evaluate Jade, we obtained several complete scientific and engineering applications and parallelized them using Jade. We then executed these applications on several computational platforms. We use this applications experience to evaluate Jade with respect to two properties: how well Jade supports the process of writing parallel programs and how well the resulting programs perform. Our applications experience shows that the current version of Jade is a qualified success. For all but one application the use of Jade entails limited programming overhead. The coarse-grain computations perform very well, with the dynamic Jade overhead having no significant impact on the performance. The finer-grain computations suffer from some Jade-specific performance problems, but some of these could be eliminated with a more advanced Jade implementation. © 1998 John Wiley & Sons, Ltd.     

Assessment of programming language learning based on peer code review model: Implementation and experience report

The traditional assessment approach, in which one single written examination counts toward a student’s total score, no longer meets new demands of programming language education. Based on a peer code review process model, we developed an online assessment system called EduPCR and used a novel approach to assess the learning of computer programming languages. Using this approach, students peer review programs written by other students, share ideas and make suggestions to achieve an objective of collaborative and interactive learning. Teachers assess and give scores to students based on their performance in writing, reviewing and revising programs and their abidance to a peer code review process. After using this approach in two courses in two consecutive semesters, we observed significant improvements of student learning in various aspects. We also conducted two questionnaire surveys and two interviews. The survey data and the interview report indicated that this assessment approach demonstrates high practical values in assessing student learning outcomes in programming languages. Additionally, this approach leads to several interesting research topics for future research in this field.     

A set‐oriented method definition language for object databases and its semantics

In this paper we propose a set‐oriented rule‐based method definition language for object‐oriented databases. Most existing object‐oriented database systems exploit a general‐purpose imperative object‐oriented programming language as the method definition language. Because methods are written in a general‐purpose imperative language, it is difficult to analyze their properties and to optimize them. Optimization is important when dealing with a large amount of objects as in databases. We therefore believe that the use of an ad hoc, set‐oriented language can offer some advantages, at least at the specification level. In particular, such a language can offer an appropriate framework to reason about method properties. In this paper, besides defining a set‐oriented rule‐based language for method definition, we formally define its semantics, addressing the problems of inconsistency and non‐determinism in set‐oriented updates. Moreover, we characterize some relevant properties of methods, such as conflicts among method specifications in sibling classes and behavioral refinement in subclasses. Copyright © 2003 John Wiley & Sons, Ltd.