Browsing by Author "Gerber, Richard"
Now showing 1 - 16 of 16
Results Per Page
Sort Options
Item Automated Techniques for Designing Embedded Signal Processors on Distributed Platforms(1998-11-04) Kang, Dong-In; Gerber, Richard; Golubchik, LeanaIn this paper, we present a performance-based technique to help synthesize high-bandwidth radar processors on commodity platforms. This problem is innately complex, for a number of reasons. Contemporary radars are very compute-intensive: they have high pulse rates, and they sample a large amount of range readings at each pulse. Indeed, modern radar processors can require CPU loads of in high-gigaflop to tera-flop ranges, performance which is only achieved by exploiting the radar's inherent data parallelism. Next-generation radars are slated to operate on scalable clusters of commodity systems. Throughput is only one problem. Since radars are usually embedded within larger real-time applications, they also must adhere to latency (or deadline) constraints. Building an embedded radar processor on a network of workstations (or a NOW) involves partitioning load in a balanced fashion, accounting for stochastic effects injected on all software-based systems, synthesizing runtime parameters for the on-line schedulers and drivers, and meeting the latency and throughput constraints. In this paper, we show how performance analysis can be used as an effective tool in the design loop; specifically, our method uses analytic approximation techniques to help synthesize efficient designs for radar processing systems. In our method, the signal-processor's topology is represented via a simple flow-graph abstraction, and the per-unit load requirements are modeled stochastically, to account for second-order effects like cache memory behavior, DMA interference, pipeline stalls, etc. Our design algorithm accepts the following inputs: (a)~the system topology, including the thread-to-CPU mapping, where multi-threading is assumed to be used; (b) the per-task load models; and (c) the required pulse rate and latency constraints. As output, it produces the proportion of load to allocate to each task, set at manageable time resolutions for the local schedulers; an optimal service interval over which all load proportions should be guaranteed; an optimal sampling frequency; and some reconfiguration schemes to accommodate single-node failures. Internally, the design algorithms use analytic approximations to quickly estimate output rates and propagation delays for candidate solutions. When the system is synthesized, its results are checked via a simulation model, which removes many of the analytic approximations. We show how our system synthesizes a real-time synthetic aperture radar, under a variety of loading conditions. Also cross-referenced as UMIACS TR # 98-57Item Benchmarking Digital Video: Measurements, Analysis, Improvements and Lessons Learned(1998-10-15) Gerber, Richard; Gharai, Ladan(Also cross-referenced as UMIACS-TR-95-60)Item Compiler Support for Real-Time Programs(1998-10-15) Gerber, Richard; Hong, SeongsooWe present a compiler-based approach to automatically assist in constructing real-time systems. In this approach, source programs are written in TCEL (or Time Constrained Event Language) which possesses high-level timing constructs, and whose semantics characterizes time-constrained relationships between observable events. A TCEL program infers only those timing constraints necessary to achieve real-time correctness, without over-constraining the system. We exploit this looser semantics to help transform programs to automatically achieve schedulability. In this article we present two such transformations. The first is trace-scheduling, which we use to achieve consistency between a program's worst-case execution time and its real-time requirements. The second is program-slicing, which we use to automatically tune application programs driven by rate-monotonic scheduling. (Also cross-referenced as UMIACS-TR-94-15)Item Compiling Real-Time Programs with Timing Constraint Refinement and Structural Code Motion(1998-10-15) Gerber, Richard; Hong, SeongsooWe present a programming language called TCEL (Time-Constrained Event Language), whose semantics is based on time-constrained relationships between observable events. Such a semantics infers only those timing constraints necessary to achieve real-time correctness, without over-constraining the system. Moreover, an optimizing compiler can exploit this looser semantics to help tune the code, so that its worst-case execution time is consistent with its real-time requirements. In this paper we describe such a transformation system, which works in two phases. First the TCEL source code is translated into an intermediate representation. Then an instruction-scheduling algorithm rearranges selected unobservable operations, and synthesizes tasks guaranteed to respect the original event-based constraints. (Also cross-referenced as UMIACS-TR-94-90)Item Composite Model Checking with Type Specific Symbolic Encodings(1998-10-15) Bultan, Tevfik; Gerber, RichardWe present a new symbolic model checking technique, which analyzes temporal properties in multi-typed transition systems. Specifically, the method uses multiple type-specific data encodings to represent system states, and it carries out fixpoint computations via the corresponding type-specific symbolic operations. In essence, different symbolic encodings are unified into one composite model checker. Any type-specific language can be included in this framework -- provided that the language is closed under Boolean connectives, propositions can be checked for satisfiability, and relational images can be computed. Our technique relies on conjunctive partitioning of transition relations of atomic events based on variable types involved, which allows independent computation of one-step pre- and post-conditions for each variable type. In this paper we demonstrate the effectiveness of our method on a nontrivial data-transfer protocol, which contains a mixture of integer and Boolean-valued variables. The protocol operates over an unreliable channel that can lose, duplicate or reorder messages. Moreover, the protocol's send and receive window sizes are not specified in advance; rather, they are represented as symbolic constants. The resulting system was automatically verified using our composite model checking approach, in concert with a conservative approximation technique. (Also cross-referenced as UMIACS-TR-98-07)Item Compositional Verification by Model Checking for Counter-Examples(1998-10-15) Tevfik Bultan ,; Fischer, Jeffrey; Gerber, RichardMany concurrent systems are required to maintain certain safety and liveness properties. One emerging method of achieving confidence in such systems is to statically verify them using "model checking". In this approach an abstract, finite-state model of the system is constructed; then an automatic check is made to ensure that the requirements are satisfied by the model. In practice, however, this method is limited by the "state space explosion problem". We have developed a compositional method that directly addresses this problem in the context of multi-tasking programs. Our solution depends on three key space-saving ingredients: (1) checking for counter-examples, which leads to simpler search algorithms; (2) automatic extraction of interfaces, which allows a refinement of the finite model -- even before its communicating partners have been compiled; and (3) using propositional "strengthening assertions" for the sole purpose of reducing state space. In this paper we present our compositional approach, and describe the software tools that support it. (Also cross-referenced as UMIACS-TR-95-98)Item End-to-End Design of Real-Time Systems(1998-10-15) Gerber, Richard; Kang, Dong-in; Hong, Seongsoo; Saksena, Manas(Also cross-referenced as UMIACS-TR-95-61)Item Experiments with Digital Video Playback(1998-10-15) Gerber, Richard; Gharai, LadanIn this paper we describe our experiments on digital video applications, concentrating on the static and dynamic tradeoffs involved in video playback. Our results were extracted from a controlled series 272 tests, which we ran in three stages. In the first stage of 120 tests, we used a simple player-monitor tool to evaluate the effects of various static parameters: compression type, frame size, digitized rate, spatial quality and keyframe distribution. The tests were carried out on two Apple Macintosh platforms: at the lower end a Quadra 950, and at the higher end, a Power PC 7100/80. Our quantitative metrics included average playback rate, as well as the rate's variance over one-second intervals. The first set of experiments unveiled several anomalous latencies. To track them down we ran an additional 120 tests, whose analysis led us to find the locus of the system's bottlenecks. They also let us conclude that a software-only solution was sufficient for good video playback on the systems under observation - provided that the operating system is tuned accordingly. In the next step we attempted to achieve this goal, by implementing our own video playback software and accompanying device-level handlers. Our emphasis was on achieving a controlled, deterministic coordination between the various system components. An additional set of 32 experiments were carried out on our platforms, which showed significant improvements in our quantitative performance measurements, as well as in visual quality. (Also cross-referenced as UMIACS-TR-95-103)Item Guaranteeing End-to-End Timing Constraints by Calibrating Intermediate Processes(1998-10-15) Gerber, Richard; Hong, Seongsoo; Saksena, ManasThis paper presents a comprehensive design methodology for guaranteeing end-to-end requirements of real-time systems. Applications are structured as a set of process components connected by asynchronous channels, in which the endpoints are the system's external inputs and outputs. Timing constraints are then postulated between these inputs and outputs; they express properties such as end-to-end propagation delay, temporal input-sampling correlation, and allowable separation times between updated output values. The automated design method works as follows: First the end-to-end requirements are transformed into a set of intermediate rate constraints on the tasks, and new tasks are created to correlate related inputs. The intermediate constraints are then solved by an optimization algorithm, whose objective is to minimize CPU utilization. If the algorithm fails, a restructuring tool attempts to eliminate bottlenecks by transforming the application, which is then re-submitted into the assignment algorithm. The final result is a schedulable set of fully periodic tasks, which collaboratively maintain the end-to-end constraints. (Also cross-referenced as UMIACS-TR-94-58)Item Languages and Tools for Real-Time Systems: Problems, Solutions and Opportunities(1998-10-15) Gerber, RichardThis report summarizes two talks I gave at the ACM SIGPLAN Workshop on Language, Compiler, and Tool Support for Real-Time Systems, which took place on June 21, 1994, in in Orlando, Florida. The workshop was held in concert with ACM SIGPLAN Conference on Programming Languages Design and Implementation. The first talk ("Statements about Real-Time: Truth or Bull?") was given in the early morning. At the behest of the workshop's organizers, its primary function was to seed the ongoing discourse and provoke some debate. Besides asking controversial questions, and positing opinions, the talk also identified some several fertile research areas that might interest PLDI attendees . The second talk ("Languages and Transformations: Some Solutions") was more technical, and it reviewed our research on program optimizations for real-time domains. However, I tried as much as possible to revisit the research problems raised in the morning talk, and present some possible approaches to them. The following paragraphs contain the text from my viewgraphs, laced with some commentary. Since so much work has been done in real-time systems - and even more in programming languages - my references are by necessity incomplete. (Also cross-referenced as UMIACS-TR-94-117)Item Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results(1998-10-15) Bultan, Tevfik; Gerber, Richard; Pugh, WilliamModel checking is a powerful technique for analyzing large, finite-state systems. In an infinite-state system, however, many basic properties are undecidable. In this paper, we present a new symbolic model checker which conservatively evaluates safety and liveness properties on infinite-state programs. We use Presburger formulas to symbolically encode a program's transition system, as well as its model-checking computations. All fixpoint calculations are executed symbolically, and their convergence is guaranteed by using approximation techniques. We demonstrate the promise of this technology on some well-known infinite-state concurrency problems. (Also cross-referenced as UMIACS-TR-98-07)Item Multi-platform Simulation of Video Playout Performance(1998-10-15) Gharai, Ladan; Gerber, RichardWe describe a video playout and simulation package, including (1) a multi-threaded player, which maximizes performance via asynchronous streaming and selective IO-prefetching; (2) a compositional simulator, which predicts playout performance for multiple platforms via eleven key deterministic and stochastic time-generating functions; and (3) a set of profiling tools, which allows one to extend the rang of target platforms by benchmarking new components, and converting the results into distribution functions that the simulator can access. Using this system, a developer can quickly estimate a video's performance on a wide spectrum of target platforms - without ever having to actually assemble them. (Also cross-referenced as UMIACS-TR-97-11)Item Parametric Design Synthesis of Distributed Embedded Systems(1998-10-15) Kang, Dong-In; Gerber, Richard; Saksena, ManasThis paper presents a design synthesis method for distributed embedded systems. In such systems, computations can flow through long pipelines of interacting software components, hosted on a variety of resources, each of which is managed by a local scheduler. Our method automatically calibrates the local resource schedulers to achieve the system's global end-to-end performance requirements. A system is modeled as a set of distributed task chains (or pipelines), where each task represents an activity requiring nonzero load from some CPU or network resource. Task load requirements can vary stochastically, due to second-order effects like cache memory behavior, DMA interference, pipeline stalls, bus arbitration delays, transient head-of-line blocking, etc. We aggregate these effects -- along with a task's per-service load demand -- and model them via a single random variable, ranging over an arbitrary discrete probability distribution. Load models can be obtained via profiling tasks in isolation, or simply by using an engineer's hypothesis about the system's projected behavior. The end-to-end performance requirements are posited in terms of throughput and delay constraints. Specifically, a pipeline's delay constraint is an upper bound on the total latency a computatation can accumulate, from input to output. The corresponding throughput constraint mandates the pipeline's minimum acceptable output rate -- counting only outputs which meet their delay constraints. Since per-component loads can be generally distributed, and since resources host stages from multiple pipelines, meeting all of the system's end-to-end constraints is a nontrivial problem. Our approach involves solving two sub-problems in tandem: (A)~finding an optimal proportion of load to allocate each task and channel; and (B)~deriving the best combination of service intervals over which all load proportions can be guaranteed. The design algorithms use analytic approximations to quickly estimate output rates and propagation delays for candidate solutions. When all parameters are synthesized, the estimated end-to-end performance metrics are re-checked by simulation. The per-component load reservations can then be increased, with the synthesis algorithms re-run to improve performance. At that point the system can be configured according to the synthesized scheduling parameters -- and then re-validated via on-line profiling. In this paper we demonstrate our technique on an example system, and compare the estimated performance to its simulated on-line behavior. (Also cross-referenced as UMIACS-TR-98-18)Item Slicing Real-Time Programs for Enhanced Schedulability(1998-10-15) Gerber, Richard; Hong, Seongsoo(Also cross-referenced as UMIACS-TR-95-62)Item Symbolic Model Checking of Infinite State Programs Using Presburger Artihmetic(1998-10-15) Bultan, Tevfik; Gerber, Richard; Pugh, WilliamModel checking is a powerful technique for analyzing large, finite-state systems. In an infinite transition system, however, many basic properties are undecidable. In this paper we present a new symbolic model checker which conservatively evaluates safety and liveness properties on infinite-state programs. We use Presburger formulas to symbolically encode a program's transition system, as well as its model-checking computations. All fixpoint calculations are executed symbolically, and their convergence is guaranteed by using approximation techniques. We demonstrate the promise of this technology on some well-known infinite-state concurrency problems. (Also cross-referenced as UMIACS-TR-96-66)Item Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach(1998-10-15) Bultan, Tevfik; Gerber, Richard; League, ChristopherSymbolic model checking has proved highly successful for large finite-state systems, in which states can be compactly encoded using binary decision diagrams (BDDs) or their variants. The inherent limitation of this approach is that it cannot be applied to systems with an infinite number of states -- even those with a single unbounded integer. Alternatively, we recently proposed a model checker for integer-based systems that uses Presburger constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency problems, it proved inefficient in its treatment of Boolean and (unordered) enumerated types -- which possess no natural mapping to the Euclidean coordinate space. In this paper we describe a model checker which combines the strengths of both approaches. We use a composite model, in which a formula's valuations are encoded in a mixed BDD-Presburger form, depending on the variables used. We demonstrate our technique's effectiveness on a nontrivial requirements specification, which includes a mixture of Booleans, integers and enumerated types. (Also cross-referenced as UMIACS-TR-97-62)