Search

Computation via biological devices has been the subject of close scrutiny since von Neumann’s early work some 60 years ago. In spite of the many relevant works in this field, the notion of programming biological devices seems to be, at best, ill-defined. While many devices are claimed or proved to be computationally universal in some sense, the full step to a bona fide programming language is rarely taken, and one question is noticeable by its absence: If the device is universal, where are the programs? We begin with an extensive review of the literature on programming-related biocomputing; and briefly identify some strengths and shortcomings from a programming perspective. To show concretely what one could see as programming in biocomputing, we outline (from recent work) a computation model and a small programming language that are biologically more plausible than existing silicon-inspired models. Whether or not the model is biologically plausible in an absolute sense, we believe it sets a standard for a biological device that can be both universal and programmable.

CUTE, a Concolic Unit Testing Engine for C and Java, is a tool to systematically and automatically test sequential C programs (including pointers) and concurrent Java programs. CUTE combines concrete and symbolic execution in a way that avoids redundant test cases as well as false warnings. The tool also introduces a race-flipping technique to efficiently test and model check concurrent programs with data inputs., The original document contains color images. Supported in part by NSF.

The goal of this project was to develop new techniques for the construction, description, and analysis of multi-agent systems. The characteristics of systems being addressed include a high degree of non-determinism (resulting form a large number of interactions) and unpredictability of the environment in which the agents operate. Specifically, we implemented tools for building robust and dependable large-scale multi-agent systems and studied methods for predicting and analyzing the behaviors of such systems. The project developed coordination methods for systems consisting of large numbers of agents., The original document contains color images. Sponsored in part by DARPA.

An automated and configurable technique for runtime safety analysis of multithreaded programs is presented, which is able to predict safety violations from successful executions. Based on a user provided safety formal specification, the program is automatically instrumented to emit relevant state update events to an observer, which further checks them against the safety specification. The events are stamped with dynamic vector clocks, enabling the observer to infer a causal partial order on the state updates. All event traces that are consistent with this partial order, including the actual execution trace, are analyzed on-line and in parallel, and a warning is issued whenever there is a trace violating the specification. This technique can be therefore seen as a bridge between testing and model checking. To further increase scalability, a window in the state space can be specified, allowing the observer to infer the most probable runs. If the size of the window is 1 then only the received execution trace is analyzed, like in testing; if the size of the window is then all the execution traces are analyzed, such as in model checking., Sponsored in part by ONR Grant No. N00014-02-1-0715 and by NSF/NASA Joint Grant No. CCR-0234524.

In unit testing, a program is decomposed into units which are collections of functions. A part of unit can be tested by generating inputs for a single entry function. The entry function may contain pointer arguments, in which case the inputs to the unit are memory graphs. The paper addresses the problem of automating unit testing with memory graphs as inputs. The approach used builds on previous work combining symbolic and concrete execution, and more specifically, using such a combination to generate test inputs to explore all feasible execution paths. The current work develops a method to represent and track constraints that capture the behavior of a symbolic execution of a unit with memory graphs as inputs. Moreover, an efficient constraint solver is proposed to facilitate incremental generation of such test inputs. Finally, CUTE, a tool implementing the method is described together with the results of applying CUTE to real-world examples of C code.

A process which computes the physical locations of nodes in a wireless sensor network is called localization. Self-localization is critical for large-scale sensor networks because manual or assisted localization is often impractical due to time requirements, economic constraints or inherent limitations of deployment scenarios. We have developed a service for reliably localizing wireless sensor networks in environments conducive to ranging errors by using a custom hardware-software solution for acoustic ranging and a family of self-localization algorithms. The ranging solution improves on previous work, extending the practical measurement range threefold "20-30m" while maintaining a distance-invariant median measurement error of about 1% of maximum range "33cm". The localization scheme is based on least squares scaling with soft constraints. Evaluation using ranging results obtained from sensor network field experiments shows that the localization scheme is resilient against large-magnitude ranging errors and sparse range measurements, both of which are common in large-scale outdoor sensor network deployments.

A foundational model of concurrency is developed in this thesis. We examine issues in the design of parallel systems and show why the actor model is suitable for exploiting large-scale parallelism. Concurrency in actors is constrained only by the availability of hardware resources and by the logical dependence inherent in the computation. Unlike dataflow and functional programming, however, actors are dynamically reconfigurable and can model shared resources with changing local state. Concurrency is spawned in actors using asynchronous message-passing, pipelining, and the dynamic creation of actors. This thesis deals with some central issues in distributed computing. Specifically, problems of divergence and deadlock are addressed. For example, actors permit dynamic deadlock detection and removal. The problem of divergence is contained because independent transactions can execute concurrently and potentially infinite processes are nevertheless available for interaction.

This paper addressed linguistic issues that arise in providing support for shared resources in large scale concurrent systems. Our work is based on the Actor Model of computation which unifies the lambda calculus, the sequential stored-program and the object-oriented models of computation. We show how receptionist can be used to regulate the se of shared resources by scheduling their access and providing protection against unauthorized or accidental access. A shared financial account is an example of the kind of resource that needs a receptionist. Issues involved in the implementation of scheduling policies for shared resources are also addressed. The modularity problems involved in implementing servers which multiplex the use of physical devices illustrated how delegation aids in the implementation of parallel problem solving systems for communities of actors.

We argue that the ability to model shared objects with changing local states, dynamic reconfigurability, and inherent parallelism are desirable properties of any model of concurrency. The actor model addresses these issues in a uniform framework. This paper briefly describes the concurrent programming language Act3 and the principles that have guided its development. Act3 advances the state of the art in programming languages by combining the advantages of object-oriented programming with those of functional programming. We also discuss considerations relevant to large-scale parallelism in the context of open systems, and define an abstract model which establishes the equivalence of systems defined by actor programs.