OpenRaiser/Intern-Atlas huggingface dataset:
Hoare-style Specifications as Correctness Conditions for Non-linearizable Concurrent Objects
Venue: arXiv cs.LO 2016
Year: 2016

Designing scalable concurrent objects, which can be efficiently used on multicore processors, often requires one to abandon standard specification techniques, such as linearizability, in favor of more relaxed consistency requirements. However, the variety of alternative correctness conditions makes it difficult to choose which one to employ in a particular case, and to compose them when using objects whose behaviors are specified via different criteria. The lack of syntactic verification methods for most of these criteria poses challenges in their systematic adoption and application. In this paper, we argue for using Hoare-style program logics as an alternative and uniform approach for specification and compositional formal verification of safety properties for concurrent objects and their client programs. Through a series of case studies, we demonstrate how an existing program logic for concurrency can be employed off-the-shelf to capture important state and history invariants, allowing one to explicitly quantify over interference of environment threads and provide intuitive and expressive Hoare-style specifications for several non-linearizable concurrent objects that were previously specified only via dedicated correctness criteria. We illustrate the adequacy of our specifications by verifying a number of concurrent client scenarios, that make use of the previously specified concurrent objects, capturing the essence of such correctness conditions as concurrency-aware linearizability, quiescent, and quantitative quiescent consistency. All examples described in this paper are verified mechanically in Coq.
Graph-Based Lossless Markov Lumpings
Venue: arXiv cs.IT 2016
Year: 2016

We use results from zero-error information theory to determine the set of non-injective functions through which a Markov chain can be projected without losing information. These lumping functions can be found by clique partitioning of a graph related to the Markov chain. Lossless lumping is made possible by exploiting the (sufficiently sparse) temporal structure of the Markov chain. Eliminating edges in the transition graph of the Markov chain trades the required output alphabet size versus information loss, for which we present bounds.
Links as a Service (LaaS): Feeling Alone in the Shared Cloud
Venue: arXiv cs.DC 2016
Year: 2016

The most demanding tenants of shared clouds require complete isolation from their neighbors, in order to guarantee that their application performance is not affected by other tenants. Unfortunately, while shared clouds can offer an option whereby tenants obtain dedicated servers, they do not offer any network provisioning service, which would shield these tenants from network interference. In this paper, we introduce Links as a Service, a new abstraction for cloud service that provides physical isolation of network links. Each tenant gets an exclusive set of links forming a virtual fat tree, and is guaranteed to receive the exact same bandwidth and delay as if it were alone in the shared cloud. Under simple assumptions, we derive theoretical conditions for enabling LaaS without capacity over-provisioning in fat-trees. New tenants are only admitted in the network when they can be allocated hosts and links that maintain these conditions. Using experiments on real clusters as well as simulations with real-life tenant sizes, we show that LaaS completely avoids the performance degradation caused by traffic from concurrent tenants on shared links. Compared to mere host isolation, LaaS can improve the application performance by up to 200%, at the cost of a 10% reduction in the cloud utilization.
Training Deep Networks with Structured Layers by Matrix Backpropagation
Venue: arXiv cs.CV 2016
Year: 2016

Deep neural network architectures have recently produced excellent results in a variety of areas in artificial intelligence and visual recognition, well surpassing traditional shallow architectures trained using hand-designed features. The power of deep networks stems both from their ability to perform local computations followed by pointwise non-linearities over increasingly larger receptive fields, and from the simplicity and scalability of the gradient-descent training procedure based on backpropagation. An open problem is the inclusion of layers that perform global, structured matrix computations like segmentation (e.g. normalized cuts) or higher-order pooling (e.g. log-tangent space metrics defined over the manifold of symmetric positive definite matrices) while preserving the validity and efficiency of an end-to-end deep training framework. In this paper we propose a sound mathematical apparatus to formally integrate global structured computation into deep computation architectures. At the heart of our methodology is the development of the theory and practice of backpropagation that generalizes to the calculus of adjoint matrix variations. The proposed matrix backpropagation methodology applies broadly to a variety of problems in machine learning or computational perception. Here we illustrate it by performing visual segmentation experiments using the BSDS and MSCOCO benchmarks, where we show that deep networks relying on second-order pooling and normalized cuts layers, trained end-to-end using matrix backpropagation, outperform counterparts that do not take advantage of such global layers.
Information-based Active SLAM via Topological Feature Graphs
Venue: arXiv cs.RO 2016
Year: 2016

Active SLAM is the task of actively planning robot paths while simultaneously building a map and localizing within. Existing work has focused on planning paths with occupancy grid maps, which do not scale well and suffer from long term drift. This work proposes a Topological Feature Graph (TFG) representation that scales well and develops an active SLAM algorithm with it. The TFG uses graphical models, which utilize independences between variables, and enables a unified quantification of exploration and exploitation gains with a single entropy metric. Hence, it facilitates a natural and principled balance between map exploration and refinement. A probabilistic roadmap path-planner is used to generate robot paths in real time. Experimental results demonstrate that the proposed approach achieves better accuracy than a standard grid-map based approach while requiring orders of magnitude less computation and memory resources.
A Note on Bayesian Rationality and Correlated Equilibrium
Venue: arXiv cs.GT 2016
Year: 2016

Bayesian rationality in strategic games presumes that it is possible to translate strategic uncertainty into imperfect information. Correlated equilibrium is guided by the idea that players are Bayes rational, have a common prior, and choose their strategies independently. I show that an essential condition for Bayesian rationality is violated in every game with imperfect information. Moreover, without strategic uncertainty, players cannot choose their strategies independently. This means strategic independence requires strategic uncertainty. If we distinguish between strategic certainty and uncertainty, we are able to explain both the existence of the cooperative and the noncooperative solution of the prisoner's dilemma.
Asynchronous Distributed Optimization via Randomized Dual Proximal Gradient
Venue: arXiv cs.SY 2016
Year: 2016

In this paper we consider distributed optimization problems in which the cost function is separable, i.e., a sum of possibly non-smooth functions all sharing a common variable, and can be split into a strongly convex term and a convex one. The second term is typically used to encode constraints or to regularize the solution. We propose a class of distributed optimization algorithms based on proximal gradient methods applied to the dual problem. We show that, by choosing suitable primal variable copies, the dual problem is itself separable when written in terms of conjugate functions, and the dual variables can be stacked into non-overlapping blocks associated to the computing nodes. We first show that a weighted proximal gradient on the dual function leads to a synchronous distributed algorithm with local dual proximal gradient updates at each node. Then, as main paper contribution, we develop asynchronous versions of the algorithm in which the node updates are triggered by local timers without any global iteration counter. The algorithms are shown to be proper randomized block-coordinate proximal gradient updates on the dual function.
Phase Retrieval Using Feasible Point Pursuit: Algorithms and Cramér-Rao Bound
Venue: arXiv cs.IT 2016
Year: 2016

Reconstructing a signal from squared linear (rank-one quadratic) measurements is a challenging problem with important applications in optics and imaging, where it is known as phase retrieval. This paper proposes two new phase retrieval algorithms based on non-convex quadratically constrained quadratic programming (QCQP) formulations, and a recently proposed approximation technique dubbed feasible point pursuit (FPP). The first is designed for uniformly distributed bounded measurement errors, such as those arising from high-rate quantization (B-FPP). The second is designed for Gaussian measurement errors, using a least squares criterion (LS-FPP). Their performance is measured against state-of-the-art algorithms and the Cramér-Rao bound (CRB), which is also derived here. Simulations show that LS-FPP outperforms the state-of-art and operates close to the CRB. Compact CRB expressions, properties, and insights are obtained by explicitly computing the CRB in various special cases -- including when the signal of interest admits a sparse parametrization, using harmonic retrieval as an example.
Correlated Cascades: Compete or Cooperate
Venue: arXiv cs.SI 2016
Year: 2016

In real world social networks, there are multiple cascades which are rarely independent. They usually compete or cooperate with each other. Motivated by the reinforcement theory in sociology we leverage the fact that adoption of a user to any behavior is modeled by the aggregation of behaviors of its neighbors. We use a multidimensional marked Hawkes process to model users product adoption and consequently spread of cascades in social networks. The resulting inference problem is proved to be convex and is solved in parallel by using the barrier method. The advantage of the proposed model is twofold; it models correlated cascades and also learns the latent diffusion network. Experimental results on synthetic and two real datasets gathered from Twitter, URL shortening and music streaming services, illustrate the superior performance of the proposed model over the alternatives.
A System for Precise End-to-End Delay Measurements in Video Communication
Venue: arXiv cs.MM 2016
Year: 2016

Low delay video transmission is becoming increasingly important. Delay critical, video enabled applications range from teleoperation scenarios such as controlling drones or telesurgery to autonomous control through computer vision algorithms applied on real-time video. To judge the quality of the video transmission in such a system, it is important to be able to precisely measure the end-to-end (E2E) delay of the transmitted video. We present a low-complexity system that automatically takes pairwise independent measurements of E2E delay. The precision can be far below the millisecond order, mainly limited by the sampling rate of the measurement system. In our implementation, we achieve a precision of 0.5 milliseconds with a sampling rate of 2kHz.
From Network Traces to System Responses: Opaquely Emulating Software Services
Venue: arXiv cs.SE 2016
Year: 2016

Enterprise software systems make complex interactions with other services in their environment. Developing and testing for production-like conditions is therefore a challenging task. Prior approaches include emulations of the dependency services using either explicit modelling or record-and-replay approaches. Models require deep knowledge of the target services while record-and-replay is limited in accuracy. We present a new technique that improves the accuracy of record-and-replay approaches, without requiring prior knowledge of the services. The approach uses multiple sequence alignment to derive message prototypes from recorded system interactions and a scheme to match incoming request messages against message prototypes to generate response messages. We introduce a modified Needleman-Wunsch algorithm for distance calculation during message matching, wildcards in message prototypes for high variability sections, and entropy-based weightings in distance calculations for increased accuracy. Combined, our new approach has shown greater than 99% accuracy for four evaluated enterprise system messaging protocols.
Multi-Objective Resource Allocation in Full-Duplex SWIPT Systems
Venue: arXiv cs.IT 2016
Year: 2016

In this paper, we investigate the resource allocation algorithm design for full-duplex simultaneous wireless information and power transfer (FD-SWIPT) systems. The considered system comprises a FD radio base station, multiple single-antenna half-duplex (HD) users, and multiple energy harvesters equipped with multiple antennas. We propose a multi-objective optimization framework to study the trade-off between uplink transmit power minimization, downlink transmit power minimization, and total harvested energy maximization. The considered optimization framework takes into account heterogeneous quality of service requirements for uplink and downlink communication and wireless power transfer. The non-convex multi-objective optimization problem is transformed into an equivalent rank-constrained semidefinite program (SDP) and solved optimally by SDP relaxation. The solution of the proposed framework results in a set of Pareto optimal resource allocation policies. Numerical results unveil an interesting trade-off between the considered conflicting system design objectives and reveal the improved power efficiency facilitated by FD in SWIPT systems compared to traditional HD systems.
The Stellar Transformation: From Interconnection Networks to Datacenter Networks
Venue: arXiv cs.DC 2016
Year: 2016

The first dual-port server-centric datacenter network, FiConn, was introduced in 2009 and there are several others now in existence; however, the pool of topologies to choose from remains small. We propose a new generic construction, the stellar transformation, that dramatically increases the size of this pool by facilitating the transformation of well-studied topologies from interconnection networks, along with their networking properties and routing algorithms, into viable dual-port server-centric datacenter network topologies. We demonstrate that under our transformation, numerous interconnection networks yield datacenter network topologies with potentially good, and easily computable, baseline properties. We instantiate our construction so as to apply it to generalized hypercubes and obtain the datacenter networks GQ*. Our construction automatically yields routing algorithms for GQ* and we empirically compare GQ* (and its routing algorithms) with the established datacenter networks FiConn and DPillar (and their routing algorithms); this comparison is with respect to network throughput, latency, load balancing, fault-tolerance, and cost to build, and is with regard to all-to-all, many all-to-all, butterfly, and random traffic patterns. We find that GQ* outperforms both FiConn and DPillar (sometimes significantly so) and that there is substantial scope for our stellar transformation to yield new dual-port server-centric datacenter networks that are a considerable improvement on existing ones.
Safety technology for train based on multi-sensors and braking system
Venue: arXiv cs.IT 2016
Year: 2016

This work deals with integration and transmission of safety information for smart railway vehicles and control and design of cooperative emergency brake systems for high speed trains. Due to increased speed of high-speed train, safety of passengers is becoming more critical. From this perspective, three different approaches to ensure the safety of passengers are useful. These approaches are based on integrated use of multi-sensors and emergency brake system. Methodology for integrated use of sensors to obtain situation-aware safety related information and for enhanced braking is to be discussed in details in this work
On the Complexity of Inner Product Similarity Join
Venue: arXiv cs.DS 2016
Year: 2016

A number of tasks in classification, information retrieval, recommendation systems, and record linkage reduce to the core problem of inner product similarity join (IPS join): identifying pairs of vectors in a collection that have a sufficiently large inner product. IPS join is well understood when vectors are normalized and some approximation of inner products is allowed. However, the general case where vectors may have any length appears much more challenging. Recently, new upper bounds based on asymmetric locality-sensitive hashing (ALSH) and asymmetric embeddings have emerged, but little has been known on the lower bound side. In this paper we initiate a systematic study of inner product similarity join, showing new lower and upper bounds. Our main results are: * Approximation hardness of IPS join in subquadratic time, assuming the strong exponential time hypothesis. * New upper and lower bounds for (A)LSH-based algorithms. In particular, we show that asymmetry can be avoided by relaxing the LSH definition to only consider the collision probability of distinct elements. * A new indexing method for IPS based on linear sketches, implying that our hardness results are not far from being tight. Our technical contributions include new asymmetric embeddings that may be of independent interest. At the conceptual level we strive to provide greater clarity, for example by distinguishing among signed and unsigned variants of IPS join and shedding new light on the effect of asymmetry.
Lempel-Ziv Computation In Compressed Space (LZ-CICS)
Venue: arXiv cs.DS 2016
Year: 2016

We show that both the Lempel Ziv 77- and the 78-factorization of a text of length $n$ on an integer alphabet of size $σ$ can be computed in $O(n \lg \lg σ)$ time (linear time if we allow randomization) using $O(n \lg σ)$ bits of working space. Given that a compressed representation of the suffix tree is loaded into RAM, we can compute both factorizations in $O(n)$ time using $z \lg n + O(n)$ bits of space, where $z$ is the number of factors.
A Shifting Bloom Filter Framework for Set Queries
Venue: arXiv cs.DS 2016
Year: 2016

Set queries are fundamental operations in computer systems and applications.This paper addresses the fundamental problem of designing a probabilistic data structure that can quickly process set queries using a small amount of memory. We propose a Shifting Bloom Filter (ShBF) framework for representing and querying sets. We demonstrate the effectiveness of ShBF using three types of popular set queries: membership, association, and multiplicity queries. The key novelty of ShBF is on encoding the auxiliary information of a set element in a location offset. In contrast, prior BF based set data structures allocate additional memory to store auxiliary information. To evaluate ShBF in comparison with prior art, we conducted experiments using real-world network traces. Results show that ShBF significantly advances the state-of-the-art on all three types of set queries.
ZMP support areas for multi-contact mobility under frictional constraints
Venue: arXiv cs.RO 2016
Year: 2016

We propose a method for checking and enforcing multi-contact stability based on the Zero-tilting Moment Point (ZMP). The key to our development is the generalization of ZMP support areas to take into account (a) frictional constraints and (b) multiple non-coplanar contacts. We introduce and investigate two kinds of ZMP support areas. First, we characterize and provide a fast geometric construction for the support area generated by valid contact forces, with no other constraint on the robot motion. We call this set the full support area. Next, we consider the control of humanoid robots using the Linear Pendulum Mode (LPM). We observe that the constraints stemming from the LPM induce a shrinking of the support area, even for walking on horizontal floors. We propose an algorithm to compute the new area, which we call pendular support area. We show that, in the LPM, having the ZMP in the pendular support area is a necessary and sufficient condition for contact stability. Based on these developments, we implement a whole-body controller and generate feasible multi-contact motions where an HRP-4 humanoid locomotes in challenging multi-contact scenarios.
The social dilemma of autonomous vehicles
Venue: arXiv cs.CY 2016
Year: 2016

Autonomous Vehicles (AVs) should reduce traffic accidents, but they will sometimes have to choose between two evils-for example, running over pedestrians or sacrificing itself and its passenger to save them. Defining the algorithms that will help AVs make these moral decisions is a formidable challenge. We found that participants to six MTurk studies approved of utilitarian AVs (that sacrifice their passengers for the greater good), and would like others to buy them, but they would themselves prefer to ride in AVs that protect their passengers at all costs. They would disapprove of enforcing utilitarian AVs, and would be less willing to buy such a regulated AV. Accordingly, regulating for utilitarian algorithms may paradoxically increase casualties by postponing the adoption of a safer technology.
Topological lower bounds for arithmetic networks
Venue: arXiv cs.CC 2016
Year: 2016

We prove a complexity lower bound on deciding membership in a semialgebraic set for arithmetic networks in terms of the sum of Betti numbers with respect to "ordinary" (singular) homology. This result complements a similar lower bound by Montana, Morais and Pardo for locally close semialgebraic sets in terms of the sum of Borel-Moore Betti numbers. We also prove a lower bound in terms of the sum of Betti numbers of the projection of a semialgebraic set to a coordinate subspace.
Hybrid Dialog State Tracker
Venue: arXiv cs.CL 2016
Year: 2016

This paper presents a hybrid dialog state tracker that combines a rule based and a machine learning based approach to belief state tracking. Therefore, we call it a hybrid tracker. The machine learning in our tracker is realized by a Long Short Term Memory (LSTM) network. To our knowledge, our hybrid tracker sets a new state-of-the-art result for the Dialog State Tracking Challenge (DSTC) 2 dataset when the system uses only live SLU as its input.
Honeypot-powered Malware Reverse Engineering
Venue: arXiv cs.CR 2016
Year: 2016

Honeypots, i.e. networked computer systems specially designed and crafted to mimic the normal operations of other systems while capturing and storing information about the interactions with the world outside, are a crucial technology into the study of cyber threats and attacks that propagate and occur through networks. Among them, high interaction honeypots are considered the most efficient because the attacker (whether automated or not) perceives realistic interactions with the target machine. In the case of automated attacks, propagated by malwares, currently available honeypots alone are not specialized enough to allow the analysis of their behaviors and effects on the target system. The research presented in this paper shows how high interaction honeypots can be enhanced by powering them with specific features that improve the reverse engineering activities needed to effectively analyze captured malicious entities.