Translation validators are static analyzers that attempt to verify that program transformations preserve the semantics of the transformed program. Normalizing translation validators do so by trying to match the value-graphs of an original function and it's transformed counterpart. In this paper, we present the design of such a validator for LLVM's intra-procedural optimizations, a design that does not require any instrumentation of the optimizer, nor any rewriting of the source code to compile, and needs to run only once to validate a pipeline of optimizations. We present in details the results of our preliminary experiments on a set of benchmarks that include GCC, a perl interpretor, sqlite3, and other C programs.
Monad comprehensions are by now a mainstay of functional programming languages. In this paper we develop a theory of semantic optimization for monad comprehensions that goes beyond rewriting using the monad laws. A monad-with-zero comprehension do x X; y Y ; if P(x; y) then return F(x; y) else zero can be rewritten, so as to minimize the number of bindings, using constraints that are known to hold of X and Y . The soundness of this technique varies from monad to monad, and we characterize its soundness for monads expressible in functional programming languages by generalizing classical results from relational database theory. This technique allows the optimization of a wide class of languages, ranging from large-scale data-parallel languages such as DryadLINQ and Data Parallel Haskell to probabilistic languages such as IBAL and functional-logical languages like Curry.
In “Shape From Specular Flow: Is One Flow Enough?” (Vasilyev, et al., 2011 ) we show that mirror shape can often be reconstructed from the observation of a single specular flow. In this technical report we provide additional details that, due to space constraints, could not be included in the paper. First we provide a derivation of the linear system for the reflection field derivative in the direction orthogonal to the flow, ^ry. Second, we derive an expression for the determinant of this system which is independent of coordinate system. Third, we show that the sphere is reconstructable whenever the scene rotation is neither on the equator nor parallel to the view direction. Finally we provide additional details for the outline of the proof that reconstructability is a generic property and for our numerical investigation of the dimensionality of the variety described by the “bad” conditions.
Hybrid information-flow monitors use a combination of static analysis and dynamic mechanisms to provide precise strong information security guarantees. However, unlike purely static mechanisms for information security, hybrid information-flow monitors incur run-time overhead. We show how static analyses can be used to make hybrid informationflow monitors more efficient, in two ways.
First, a simple static analysis can determine when it is sound for a monitor to stop tracking the security level of certain variables. This potentially reduces run-time overhead of the monitor, particularly in applications where sensitive (i.e., confidential or untrusted) data is infrequently introduced to the system.
Second, we derive sufficient conditions for soundly incorporating a wide range of memory abstractions into informationflow monitors. This allows the selection of a memory abstraction that gives an appropriate tradeoff between efficiency and precision. It also facilitates the development of innovative and sound memory abstractions that use run-time security information maintained by the monitor.
We present and prove our results by extending the information-flow monitor of Russo and Sabelfeld (2010). These results bring us closer to efficient, sound, and precise enforcement of information security.
In current robotics research there is a vast body of work on algorithms and control methods for groups of decentralized cooperating robots, called a swarm or collective. These algorithms are generally meant to control collectives of hundreds or even thousands of robots; however, for reasons of cost, time, or complexity, they are generally validated in simulation only, or on a group of a few 10s of robots. To address this issue, this paper presents Kilobot, a low-cost robot designed to make testing collective algorithms on hundreds or thousands of robots accessible to robotics researchers. To enable the possibility of large Kilobot collectives where the number of robots is an order of magnitude larger than the largest that exist today, each robot is made with only $14 worth of parts and takes 5 minutes to assemble. Furthermore, the robot design allows a single user to easily oversee the operation of a large Kilobot collective, such as programming, powering on, and charging all robots, which would be difficult or impossible to do with many existing robotic systems. We demonstrate the capabilities of the Kilobot as a collective robot, using a 25 robot test collective to implement three popular swarm behaviors: foraging, formation control, and synchronization.
While the color image formats used by modern cameras provide visually pleasing images, they distort and discard a significant amount of signal that is useful for many applications. Existing methods for modeling physical world properties based on such narrow-gamut images use a deterministic, per-channel, one-to-one mapping to get back to wide-gamut physical scene colors, ignoring the uncertainty inherent in the process. Rather than fit a deterministic parametric model, we show that non-parametric Bayesian regression techniques, e.g. Gaussian Processes (GP), are well-suited to model this de-rendering process, and accurately capture the uncertainty in the transformation. We propose a probabilistic approach that outputs, for each low-gamut image color, a distribution over the wide-gamut scene colors that could have created it. Using a variety of different consumer camera models, we show that effective distributions can be learned by online local Gaussian process regression. Such distributions can be used to hallucinate estimates of RAW values corresponding to JPEG samples, creating “out-of-gamut” images, and also to improve robustness in related applications, e.g., when recovering three-dimensional shape via photometric stereo.
We describe a method of integrating Karhunen- Lo`eve Transform (KLT) into compressive sensing, which can as a result leverage KLT’s optimality in revealing the sparsity of a signal. We present two complementary results: (1) by using the KLT to find the optimal basis for decoding we can drastically reduce the number of measurements for compressive sensing used in applications such as spectrum sensing; (2) by using compressive sensing we can compute the KLT basis directly from measurements of the input signal, with substantially fewer samples than the Nyquist rate. For a non-stationary signal, we suggest strategies in addressing the trade-off of incurring additional measurements for updating a KLT basis or compensating an obsolete KLT basis in signal recovery. We validate our results with field experiments to detect multiple radio transmitters and sense the UHF spectrums using software-defined radios.