OpenRaiser/Intern-Atlas huggingface dataset:
MessageGuard: A Browser-based Platform for Usable, Content-Based Encryption Research
Venue: arXiv cs.CR 2016
Year: 2016

This paper describes MessageGuard, a browser-based platform for research into usable content-based encryption. MessageGuard is designed to enable collaboration between security and usability researchers on long-standing research questions in this area. It significantly simplifies the effort required to work in this space and provides a place for research results to be shared, replicated, and compared with minimal confounding factors. MessageGuard provides ubiquitous encryption and secure cryptographic operations, enabling research on any existing web application, with realistic usability studies on a secure platform. We validate MessageGuard's compatibility and performance, and we illustrate its utility with case studies for Gmail and Facebook Chat.
Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings
Venue: arXiv cs.SC 2016
Year: 2016

In this paper, we present an algorithm for computing a fundamental matrix of formal solutions of completely integrable Pfaffian systems with normal crossings in several variables. This algorithm is a generalization of a method developed for the bivariate case based on a combination of several reduction techniques and is implemented in the computer algebra system Maple.
TLS in the wild: an Internet-wide analysis of TLS-based protocols for electronic communication
Venue: arXiv cs.CR 2016
Year: 2016

The majority of electronic communication today happens either via email or chat. Thanks to the use of standardised protocols electronic mail (SMTP, IMAP, POP3) and instant chat (XMPP, IRC) servers can be deployed in a decentralised but interoperable fashion. These protocols can be secured by providing encryption with the use of TLS---directly or via the STARTTLS extension---and leverage X.509 PKIs or ad hoc methods to authenticate communication peers. However, many combination of these mechanisms lead to insecure deployments. We present the largest study to date that investigates the security of the email and chat infrastructures. We used active Internet-wide scans to determine the amount of secure service deployments, and passive monitoring to investigate if user agents actually use this opportunity to secure their communications. We addressed both the client-to-server interactions as well as server-to-server forwarding mechanisms that these protocols offer, and the use of encryption and authentication methods in the process. Our findings shed light on an insofar unexplored area of the Internet. The truly frightening result is that most of our communication is poorly secured in transit.
Universally Near Optimal Online Power Control for Energy Harvesting Nodes
Venue: arXiv cs.IT 2016
Year: 2016

We consider online power control for an energy harvesting system with random i.i.d. energy arrivals and a finite size battery. We propose a simple online power control policy for this channel that requires minimal information regarding the distribution of the energy arrivals and prove that it is universally near-optimal for all parameter values. In particular, the policy depends on the distribution of the energy arrival process only through its mean and it achieves the optimal long-term average throughput of the channel within both constant additive and multiplicative gaps. Existing heuristics for online power control fail to achieve such universal performance. This result also allows us to approximate the long-term average throughput of the system with a simple formula, which sheds some light on the qualitative behavior of the throughput, namely how it depends on the distribution of the energy arrivals and the size of the battery.
Broadcast Coded Slotted ALOHA: A Finite Frame Length Analysis
Venue: arXiv cs.IT 2016
Year: 2016

We propose an uncoordinated medium access control (MAC) protocol, called all-to-all broadcast coded slotted ALOHA (B-CSA) for reliable all-to-all broadcast with strict latency constraints. In B-CSA, each user acts as both transmitter and receiver in a half-duplex mode. The half-duplex mode gives rise to a double unequal error protection (DUEP) phenomenon: the more a user repeats its packet, the higher the probability that this packet is decoded by other users, but the lower the probability for this user to decode packets from others. We analyze the performance of B-CSA over the packet erasure channel for a finite frame length. In particular, we provide a general analysis of stopping sets for B-CSA and derive an analytical approximation of the performance in the error floor (EF) region, which captures the DUEP feature of B-CSA. Simulation results reveal that the proposed approximation predicts very well the performance of B-CSA in the EF region. Finally, we consider the application of B-CSA to vehicular communications and compare its performance with that of carrier sense multiple access (CSMA), the current MAC protocol in vehicular networks. The results show that B-CSA is able to support a much larger number of users than CSMA with the same reliability.
Geometric approach to tracking and stabilization for a spherical robot actuated by internal rotors
Venue: arXiv cs.SY 2016
Year: 2016

This paper presents tracking control laws for two different objectives of a nonholonomic system - a spherical robot - using a geometric approach. The first control law addresses orientation tracking using a modified trace potential function. The second law addresses contact position tracking using a $right$ transport map for the angular velocity error. A special case of this is position and reduced orientation stabilization. Both control laws are coordinate free. The performance of the feedback control laws are demonstrated through simulations.
Spiking Analog VLSI Neuron Assemblies as Constraint Satisfaction Problem Solvers
Venue: arXiv cs.NE 2016
Year: 2016

Solving constraint satisfaction problems (CSPs) is a notoriously expensive computational task. Recently, it has been proposed that efficient stochastic solvers can be obtained through appropriately configured spiking neural networks performing Markov Chain Monte Carlo (MCMC) sampling. The possibility to run such models on massively parallel, low-power neuromorphic hardware holds great promise; however, previously proposed networks are based on probabilistically spiking neurons, and thus rely on random number generators or external noise sources to achieve the necessary stochasticity, leading to significant overhead in the implementation. Here we show how stochasticity can be achieved by implementing deterministic models of integrate and fire neurons using subthreshold analog circuits that are affected by thermal noise. We present an efficient implementation of spike-based CSP solvers using a reconfigurable neural network VLSI device, and the device's intrinsic noise as a source of randomness. To illustrate the overall concept, we implement a generic Sudoku solver based on our approach and demonstrate its operation. We establish a link between the neuron parameters and the system dynamics, allowing for a simple temperature control mechanism.
Parameterized Algorithms for Constraint Satisfaction Problems Above Average with Global Cardinality Constraints
Venue: arXiv cs.DS 2016
Year: 2016

Given a constraint satisfaction problem (CSP) on $n$ variables, $x_1, x_2, \dots, x_n \in \{\pm 1\}$, and $m$ constraints, a global cardinality constraint has the form of $\sum_{i = 1}^{n} x_i = (1-2p)n$, where $p \in (Ω(1), 1 - Ω(1))$ and $pn$ is an integer. Let $AVG$ be the expected number of constraints satisfied by randomly choosing an assignment to $x_1, x_2, \dots, x_n$, complying with the global cardinality constraint. The CSP above average with the global cardinality constraint problem asks whether there is an assignment (complying with the cardinality constraint) that satisfies more than $(AVG+t)$ constraints, where $t$ is an input parameter. In this paper, we present an algorithm that finds a valid assignment satisfying more than $(AVG+t)$ constraints (if there exists one) in time $(2^{O(t^2)} + n^{O(d)})$. Therefore, the CSP above average with the global cardinality constraint problem is fixed-parameter tractable.
adaQN: An Adaptive Quasi-Newton Algorithm for Training RNNs
Venue: arXiv cs.LG 2016
Year: 2016

Recurrent Neural Networks (RNNs) are powerful models that achieve exceptional performance on several pattern recognition problems. However, the training of RNNs is a computationally difficult task owing to the well-known "vanishing/exploding" gradient problem. Algorithms proposed for training RNNs either exploit no (or limited) curvature information and have cheap per-iteration complexity, or attempt to gain significant curvature information at the cost of increased per-iteration cost. The former set includes diagonally-scaled first-order methods such as ADAGRAD and ADAM, while the latter consists of second-order algorithms like Hessian-Free Newton and K-FAC. In this paper, we present adaQN, a stochastic quasi-Newton algorithm for training RNNs. Our approach retains a low per-iteration cost while allowing for non-diagonal scaling through a stochastic L-BFGS updating scheme. The method uses a novel L-BFGS scaling initialization scheme and is judicious in storing and retaining L-BFGS curvature pairs. We present numerical experiments on two language modeling tasks and show that adaQN is competitive with popular RNN training algorithms.
Systematic and Realistic Testing in Simulation of Control Code for Robots in Collaborative Human-Robot Interactions
Venue: arXiv cs.RO 2016
Year: 2016

Industries such as flexible manufacturing and home care will be transformed by the presence of robotic assistants. Assurance of safety and functional soundness for these robotic systems will require rigorous verification and validation. We propose testing in simulation using Coverage-Driven Verification (CDV) to guide the testing process in an automatic and systematic way. We use a two-tiered test generation approach, where abstract test sequences are computed first and then concretized (e.g., data and variables are instantiated), to reduce the complexity of the test generation problem. To demonstrate the effectiveness of our approach, we developed a testbench for robotic code, running in ROS-Gazebo, that implements an object handover as part of a human-robot interaction (HRI) task. Tests are generated to stimulate the robot's code in a realistic manner, through stimulating the human, environment, sensors, and actuators in simulation. We compare the merits of unconstrained, constrained and model-based test generation in achieving thorough exploration of the code under test, and interesting combinations of human-robot interactions. Our results show that CDV combined with systematic test generation achieves a very high degree of automation in simulation-based verification of control code for robots in HRI.
Strong Scaling for Numerical Weather Prediction at Petascale with the Atmospheric Model NUMA
Venue: arXiv cs.DC 2016
Year: 2016

Numerical weather prediction (NWP) has proven to be computationally challenging due to its inherent multiscale nature. Currently, the highest resolution NWP models use a horizontal resolution of about 10km. In order to increase the resolution of NWP models highly scalable atmospheric models are needed. The Non-hydrostatic Unified Model of the Atmosphere (NUMA), developed by the authors at the Naval Postgraduate School, was designed to achieve this purpose. NUMA is used by the Naval Research Laboratory, Monterey as the engine inside its next generation weather prediction system NEPTUNE. NUMA solves the fully compressible Navier-Stokes equations by means of high-order Galerkin methods (both spectral element as well as discontinuous Galerkin methods can be used). Mesh generation is done using the p4est library. NUMA is capable of running middle and upper atmosphere simulations since it does not make use of the shallow-atmosphere approximation. This paper presents the performance analysis and optimization of the spectral element version of NUMA. The performance at different optimization stages is analyzed using a theoretical performance model as well as measurements via hardware counters. Machine independent optimization is compared to machine specific optimization using BG/Q vector intrinsics. By using vector intrinsics the main computations reach 1.2 PFlops on the entire machine Mira (12% of the theoretical peak performance). The paper also presents scalability studies for two idealized test cases that are relevant for NWP applications. The atmospheric model NUMA delivers an excellent strong scaling efficiency of 99% on the entire supercomputer Mira using a mesh with 1.8 billion grid points. This allows to run a global forecast of a baroclinic wave test case at 3km uniform horizontal resolution and double precision within the time frame required for operational weather prediction.
"Pale as death" or "pâle comme la mort" : Frozen similes used as literary clichés
Venue: arXiv cs.CL 2016
Year: 2016

The present study is focused on the automatic identification and description of frozen similes in British and French novels written between the 19 th century and the beginning of the 20 th century. Two main patterns of frozen similes were considered: adjectival ground + simile marker + nominal vehicle (e.g. happy as a lark) and eventuality + simile marker + nominal vehicle (e.g. sleep like a top). All potential similes and their components were first extracted using a rule-based algorithm. Then, frozen similes were identified based on reference lists of existing similes and semantic distance between the tenor and the vehicle. The results obtained tend to confirm the fact that frozen similes are not used haphazardly in literary texts. In addition, contrary to how they are often presented, frozen similes often go beyond the ground or the eventuality and the vehicle to also include the tenor.
Hierarchical Codebook Design for Beamforming Training in Millimeter-Wave Communication
Venue: arXiv cs.IT 2016
Year: 2016

In millimeter-wave communication, large antenna arrays are required to achieve high power gain by steering towards each other with narrow beams, which poses the problem to efficiently search the best beam direction in the angle domain at both Tx and Rx sides. As the exhaustive search is time consuming, hierarchical search has been widely accepted to reduce the complexity, and its performance is highly dependent on the codebook design. In this paper, we propose two basic criteria for the hierarchical codebook design, and devise an efficient hierarchical codebook by jointly exploiting sub-array and deactivation (turning-off) antenna processing techniques, where closed-form expressions are provided to generate the codebook. Performance evaluations are conducted under different system and channel models. Results show superiority of the proposed codebook over the existing alternatives.
Profinite Monads, Profinite Equations, and Reiterman's Theorem
Venue: arXiv cs.FL 2016
Year: 2016

Profinite equations are an indispensable tool for the algebraic classification of formal languages. Reiterman's theorem states that they precisely specify pseudovarieties, i.e. classes of finite algebras closed under finite products, subalgebras and quotients. In this paper Reiterman's theorem is generalised to finite Eilenberg-Moore algebras for a monad T on a variety D of (ordered) algebras: a class of finite T-algebras is a pseudovariety iff it is presentable by profinite (in-)equations. As an application, quasivarieties of finite algebras are shown to be presentable by profinite implications. Other examples include finite ordered algebras, finite categories, finite infinity-monoids, etc.
The Goldilocks Principle: Reading Children's Books with Explicit Memory Representations
Venue: arXiv cs.CL 2016
Year: 2016

We introduce a new test of how well language models capture meaning in children's books. Unlike standard language modelling benchmarks, it distinguishes the task of predicting syntactic function words from that of predicting lower-frequency words, which carry greater semantic content. We compare a range of state-of-the-art models, each with a different way of encoding what has been previously read. We show that models which store explicit representations of long-term contexts outperform state-of-the-art neural language models at predicting semantic content words, although this advantage is not observed for syntactic function words. Interestingly, we find that the amount of text encoded in a single memory representation is highly influential to the performance: there is a sweet-spot, not too big and not too small, between single words and full sentences that allows the most meaningful information in a text to be effectively retained and recalled. Further, the attention over such window-based memories can be trained effectively through self-supervision. We then assess the generality of this principle by applying it to the CNN QA benchmark, which involves identifying named entities in paraphrased summaries of news articles, and achieve state-of-the-art performance.
Low Complexity Antenna Selection for Low Target Rate Users in Dense Cloud Radio Access Networks
Venue: arXiv cs.IT 2016
Year: 2016

We propose a low complexity antenna selection algorithm for low target rate users in cloud radio access networks. The algorithm consists of two phases: In the first phase, each remote radio head (RRH) determines whether to be included in a candidate set by using a predefined selection threshold. In the second phase, RRHs are randomly selected within the candidate set made in the first phase. To analyze the performance of the proposed algorithm, we model RRHs and users locations by a homogeneous Poisson point process, whereby the signal-to-interference ratio (SIR) complementary cumulative distribution function is derived. By approximating the derived expression, an approximate optimum selection threshold that maximizes the SIR coverage probability is obtained. Using the obtained threshold, we characterize the performance of the algorithm in an asymptotic regime where the RRH density goes to infinity. The obtained threshold is then modified depending on various algorithm options. A distinguishable feature of the proposed algorithm is that the algorithm complexity keeps constant independent to the RRH density, so that a user is able to connect to a network without heavy computation at baseband units.
Iterative compilation on mobile devices
Venue: arXiv cs.PL 2016
Year: 2016

The abundance of poorly optimized mobile applications coupled with their increasing centrality in our digital lives make a framework for mobile app optimization an imperative. While tuning strategies for desktop and server applications have a long history, it is difficult to adapt them for use on mobile phones. Reference inputs which trigger behavior similar to a mobile application's typical are hard to construct. For many classes of applications the very concept of typical behavior is nonexistent, each user interacting with the application in very different ways. In contexts like this, optimization strategies need to evaluate their effectiveness against real user input, but doing so online runs the risk of user dissatisfaction when suboptimal optimizations are evaluated. In this paper we present an iterative compiler which employs a novel capture and replay technique in order to collect real user input and use it later to evaluate different transformations offline. The proposed mechanism identifies and stores only the set of memory pages needed to replay the most heavily used functions of the application. At idle periods, this minimal state is combined with different binaries of the application, each one build with different optimizations enabled. Replaying the targeted functions allows us to evaluate the effectiveness of each set of optimizations for the actual way the user interacts with the application. For the BEEBS benchmark suite, our approach was able to improve performance by up to 57%, while keeping the slowdown experienced by the user on average at 0.8%. By focusing only on heavily used functions, we are able to conserve storage space by between two and three orders of magnitude compared to typical capture and replay implementations.
Reducing the Training Time of Neural Networks by Partitioning
Venue: arXiv cs.NE 2016
Year: 2016

This paper presents a new method for pre-training neural networks that can decrease the total training time for a neural network while maintaining the final performance, which motivates its use on deep neural networks. By partitioning the training task in multiple training subtasks with sub-models, which can be performed independently and in parallel, it is shown that the size of the sub-models reduces almost quadratically with the number of subtasks created, quickly scaling down the sub-models used for the pre-training. The sub-models are then merged to provide a pre-trained initial set of weights for the original model. The proposed method is independent of the other aspects of the training, such as architecture of the neural network, training method, and objective, making it compatible with a wide range of existing approaches. The speedup without loss of performance is validated experimentally on MNIST and on CIFAR10 data sets, also showing that even performing the subtasks sequentially can decrease the training time. Moreover, we show that larger models may present higher speedups and conjecture about the benefits of the method in distributed learning systems.
Fault Diagnosis of Rolling Element Bearings with a Spectrum Searching Method
Venue: arXiv cs.SD 2016
Year: 2016

Rolling element bearing faults in rotating systems are observed as impulses in the vibration signals, which are usually buried in noises. In order to effectively detect the fault of bearings, a novel spectrum searching method is proposed. The structural information of spectrum (SIOS) on a predefined basis is constructed through a searching algorithm, such that the harmonics of impulses generated by faults can be clearly identified and analyzed. Local peaks of the spectrum are located on a certain bin of the basis, and then the SIOS can interpret the spectrum via the number and energy of harmonics related to frequency bins of the basis. Finally bearings can be diagnosed based on the SIOS by identifying its dominant components. Mathematical formulation is developed to guarantee the correct construction of the SISO through searching. The effectiveness of the proposed method is verified with a simulation signal and a benchmark study of bearings.