Abstract

Model checking is now a standard technology for verifying large and complex systems. While there are a range of tools and techniques to verify various properties of a system under consideration, in this work, we restrict our attention to safety checking procedures using explicit state space generation. The necessary hardware resources required in this approach depends on the model complexity and the resulting state transition graph that gets generated. This cannot be estimated apriori. For reasonably realistic models, the available main memory in even high end servers may not be sufficient. Hence, we have to use distributed safety verification approaches on a cluster of nodes. However, the problem of estimating the minimum number of nodes in the cluster for the verification procedure to complete successfully remains unsolved. In this paper, we propose a dynamically scalable model checker using an actor based architecture. Using the proposed approach, an end user can invoke a model checker hosted on a cloud platform in a push button fashion. Our safety verification procedures automatically expands the cluster by requesting more virtual machines from the cloud provider. Finally, the user gets to pay only for the hardware resources he rented for the duration of the verification procedure. We refer to this as Model Checking as Service. We approach this problem by proposing an asynchronous algorithm for safety checking in actor framework. The actor based approach allows for scaling the resources on a need basis and redistributes the work load transparently through state migration. We tested our approach by developing a distributed version of SpinJA model checker using Akka actor framework. We conducted our experiments on Google Cloud Engine (GCE) platform wherein we scale our resources automatically using the GCE API. On large models such as anderson.8 from BEEM benchmark suite, our approach reduced the model checking cost in dollars by 8.6x while reducing the wall clock time to complete the safety checking procedure 5.5x times.

Abstract

In this paper, we propose a fully parallel and pipelined architecture for stereo vision on FPGAs using Semi-Global Matching with Census Transform being used underneath. Further, we extend the above streaming architecture so that multiple pixels can be processed in a data parallel fashion. We expose this data parallelism through dependency relaxation. This establishes a trade-off between accuracy and throughput of the hardware. We tested the proposed architecture on Virtex-7 FPGA using KITTI 2012 and KITTI 2015 datasets. On images of resolution 1280x960, with 64 disparity levels, we are able to run our hardware design at 100 MHz. At this frequency, our design is able to process 322 frames per second which is 1.6 times faster than the state-of-the-art SGM implementation on FPGA. Our system can be scaled to a higher resolution image.

Abstract

Images when processed using various enhancement techniques often lead to edge degradation and other unwanted artifacts such as halos. These artifacts pose a major problem for photographic applications where they can denude the quality of an image. There is a plethora of edge-aware techniques proposed in the field of image processing. However, these require the application of complex optimization or post-processing methods. Local Laplacian Filtering is an edge-aware image processing technique that involves the construction of simple Gaussian and Laplacian pyramids. This technique can be successfully applied for detail smoothing, detail enhancement, tone mapping and inverse tone mapping of an image while keeping it artifact-free. The problem though with this approach is that it is computationally expensive. Hence, parallelization schemes using multi-core CPUs and GPUs have been proposed. As is well known, they are not power-efficient, and a well-designed hardware architecture on an FPGA can do better on the performance per watt metric. In this paper, we propose a hardware accelerator, which exploits fully the available parallelism in the Local Laplacian Filtering algorithm, while minimizing the utilization of on-chip FPGA resources. On Virtex-7 FPGA, we obtain a 7.5x speed-up to process a 1 MB image when compared to an optimized baseline CPU implementation. To the best of our knowledge, we are not aware of any other hardware accelerators proposed in the research literature for the Local Laplacian Filtering problem.

Abstract

Unlike CPUs and GPUs, it is possible to use custom fixed-point data types, specified as a tuple (α, β), on FPGAs. The parameters α and β denote the number of integral and fractional bitwidths respectively. The power and area savings while performing arithmetic operations on fixed-point data types are well known to be significant over using floating-point data types. In this paper, we propose a hybrid approach involving interval analysis and SMT solvers, for estimating integral bitwidths at different compute stages, in an image processing pipeline, specified using a domain-specific language (DSL) such as PolyMage. The DSL specification facilitates the compiler analysis to infer the underlying computational structure with ease. We also propose a simple and practical profile-driven greedy heuristic search technique for fractional bitwidth analysis. Using the Horn-Schunck Optical Flow benchmark program, we demonstrate where the conventional range analysis approaches fail, and how we overcome them using the hybrid technique proposed in this paper. The integral bitwidth estimates provided by the hybrid technique on the optical flow benchmark are up to 3x times better when compared with interval analysis.

Abstract

The formidable increase in the number of smaller and smarter embedded devices has compelled programmers to develop more and more specialized application programs for these systems. These resource intensive programs that have to be executed on limited memory systems make a strong case for compiler optimizations that reduce the executable size of programs. Standard compilers (like LLVM) offer an out-of-the-box -Oz optimization option—just a series of compiler optimization passes—that is specifically targeted for the reduction of the generated executable size. In this paper, we aim to analyze the effects of optimizations of LLVM compiler on the reduction of executable size. Specifically, we take the size of the executable as a metric and attempt to divide the -Oz series into logical groups and study their individual effects; while also study the effect of their combinations. Our preliminary study over SPEC CPU 2017 benchmarks gives us an insight into the comparative effect of the groups of passes on the executable size. Our work has potential to enable the user to tailor a custom series of passes so as to obtain the desired executable size

Abstract

High-level synthesis (HLS) has received significant attention in recent years, improving programmability for FPGAs. PolyMage is a domain-specific language (DSL) for image processing pipelines that also has a HLS backend to translate the input DSL into an equivalent circuit that can be synthesized on FPGAs, while leveraging an HLS suite. The data at each stage of a pipeline is stored using a fixed-point data type (alpha,beta) where alpha and beta denote the number of integral and fractional bits. The power and area savings while performing arithmetic operations on fixed-point data type is known to be significant over using floating point. In this paper, we first propose an interval-arithmetic based range analysis (alpha-analysis) algorithm to estimate the number of bits required to store the integral part of the data at each stage of an image processing pipeline. The analysis algorithm uses the homogeneity of pixel signals at each stage to cluster them and perform a combined range analysis. Secondly, we propose a software architecture for easily deploying any kind of interval/affine arithmetic based range analyses in the DSL compiler. Thirdly, we propose a new range analysis technique using Satisfiability Modulo Theory (SMT) solvers, and show that the range estimates obtained through it are very close to the lower bounds obtained through profile-driven analysis.We evaluated our bitwidth analysis algorithms on four image processing benchmarks listed in the order of increasing complexity: Unsharp Mask, Down-Up Sampling, Harris Corner Detection and Horn-Schunck Optical Flow. For example, on Optical Flow, the interval analysis based approach showed an 1.4x and 1.14x improvement on area and power metrics over floating-point representation respectively; whereas the SMT solver based approach showed 2.49x and 1.58x improvement on area and power metrics when compared to interval analysis.

Abstract

High-level synthesis (HLS) has received significant attention in recent years, improving programmability for FPGAs. PolyMage is a domain-specific language (DSL) for image processing pipelines that also has a HLS backend to translate the input DSL into an equivalent circuit that can be synthesized on FPGAs, while leveraging an HLS suite. The data at each stage of a pipeline is stored using a fixed-point data type (alpha,beta) where alpha and beta denote the number of integral and fractional bits. The power and area savings while performing arithmetic operations on fixed-point data type is known to be significant over using floating point. In this paper, we first propose an interval-arithmetic based range analysis (alpha-analysis) algorithm to estimate the number of bits required to store the integral part of the data at each stage of an image processing pipeline. The analysis algorithm uses the homogeneity of pixel signals at each stage to cluster them and perform a combined range analysis. Secondly, we propose a software architecture for easily deploying any kind of interval/affine arithmetic based range analyses in the DSL compiler. Thirdly, we propose a new range analysis technique using Satisfiability Modulo Theory (SMT) solvers, and show that the range estimates obtained through it are very close to the lower bounds obtained through profile-driven analysis.We evaluated our bitwidth analysis algorithms on four image processing benchmarks listed in the order of increasing complexity: Unsharp Mask, Down-Up Sampling, Harris Corner Detection and Horn-Schunck Optical Flow. For example, on Optical Flow, the interval analysis based approach showed an 1.4x and 1.14x improvement on area and power metrics over floating-point representation respectively; whereas the SMT solver based approach showed 2.49x and 1.58x improvement on area and power metrics when compared to interval analysis.

Abstract

In this paper, we study how an oligopolist influences the coalition structure in federated cloud markets. Specifically, we use cooperative game theory to model the circumstances under which a cloud provider prefers to join a cloud federation vis-a-vis consider taking a price offer made by an oligopolist

Abstract

In this paper, we propose a multi-cloud marketplace model for Infrastructure-as-a-Service (IaaS) layer with multiple cloud providers, intermediate brokers and end users. The brokers service end users subscribed to them by aggregating resources (virtual machines) from cloud providers while maximizing their profits. Similarly cloud providers (producers) allocate their supply of virtual machines to brokers (consumers) so as to maximize their profits. We define the notion of social welfare in this market structure and study two trading schemes. The first scheme involves centralized control which aims at maximizing social welfare but may contain unstable producer-consumer pairs who have an incentive to deviate from the current allocation. The second scheme eliminates such unstable pairs by using a generalization of stable matching algorithm but may lead to sub-optimal social welfare. The stable matching algorithm we proposed in this paper is a particular way of generalizing the original Gale-Shapley algorithm

Abstract

Time-sharing, which allows for multiple users to use a shared resource, is an important and fundamental aspect of modern computing systems. However, accelerators such as GPUs, that come without a native operating system do not support time sharing. The inability of accelerators to support time-sharing limits their applicability especially as they are getting deployed in Platform-as-a-Service and Resource-as-a-Service environments. In the former, elastic demands may require preemption where as in the latter, fine-grained economic models of service cost can be supported with time sharing. In this paper, we extend the concept of time sharing to the GPGPU computational space using a cooperative multitasking approach. Our technique is applicable to any GPGPU program written in Compute Unified Device Architecture (CUDA) API provided for C/C++ programming languages. With minimal support from the programmer, our framework incorporates process scheduling, light-weight memory management, and multiGPU support. Our framework provides an abstraction where, in a round-robin manner, every workload can use a GPU(s) over a time quantum exclusively. We demonstrate the applicability of our scheduling framework by running many workloads concurrently in a time sharing manner