OpenRaiser/Intern-Atlas huggingface dataset:
Let's HPC: A web-based interactive platform to aid High Performance Computing education
Venue: arXiv cs.CY 2017
Year: 2017

Let's HPC (www.letshpc.org) is an open-access online platform to supplement conventional classroom oriented High Performance Computing (HPC) and Parallel & Distributed Computing (PDC) education. The web based platform provides online plotting and analysis tools which allow users to learn, evaluate, teach and see the performance of parallel algorithms from a system's viewpoint. The user can quantitatively compare and understand the importance of numerous deterministic as well as non-deterministic factors of both the software and the hardware that impact the performance of parallel programs. At the heart of this platform is a database archiving the performance and execution environment related data of standard parallel algorithms executed on different computing architectures using different programming environments, this data is contributed by various stakeholders in the HPC community. The plotting and analysis tools of our platform can be combined seamlessly with the database to aid self-learning, teaching, evaluation and discussion of different HPC related topics. Instructors of HPC/PDC related courses can use the platform's tools to illustrate the importance of proper analysis in understanding factors impacting performance, to encourage peer learning among students, as well as to allow students to prepare a standard lab/project report aiding the instructor in uniform evaluation. The platform's modular design enables easy inclusion of performance related data from contributors as well as addition of new features in the future.
Constraint programming for planning test campaigns of communications satellites
Venue: arXiv cs.AI 2017
Year: 2017

The payload of communications satellites must go through a series of tests to assert their ability to survive in space. Each test involves some equipment of the payload to be active, which has an impact on the temperature of the payload. Sequencing these tests in a way that ensures the thermal stability of the payload and minimizes the overall duration of the test campaign is a very important objective for satellite manufacturers. The problem can be decomposed in two sub-problems corresponding to two objectives: First, the number of distinct configurations necessary to run the tests must be minimized. This can be modeled as packing the tests into configurations, and we introduce a set of implied constraints to improve the lower bound of the model. Second, tests must be sequenced so that the number of times an equipment unit has to be switched on or off is minimized. We model this aspect using the constraint Switch, where a buffer with limited capacity represents the currently active equipment units, and we introduce an improvement of the propagation algorithm for this constraint. We then introduce a search strategy in which we sequentially solve the sub-problems (packing and sequencing). Experiments conducted on real and random instances show the respective interest of our contributions.
Nonsmooth Analysis and Subgradient Methods for Averaging in Dynamic Time Warping Spaces
Venue: arXiv cs.CV 2017
Year: 2017

Time series averaging in dynamic time warping (DTW) spaces has been successfully applied to improve pattern recognition systems. This article proposes and analyzes subgradient methods for the problem of finding a sample mean in DTW spaces. The class of subgradient methods generalizes existing sample mean algorithms such as DTW Barycenter Averaging (DBA). We show that DBA is a majorize-minimize algorithm that converges to necessary conditions of optimality after finitely many iterations. Empirical results show that for increasing sample sizes the proposed stochastic subgradient (SSG) algorithm is more stable and finds better solutions in shorter time than the DBA algorithm on average. Therefore, SSG is useful in online settings and for non-small sample sizes. The theoretical and empirical results open new paths for devising sample mean algorithms: nonsmooth optimization methods and modified variants of pairwise averaging methods.
Security Analysis of Cache Replacement Policies
Venue: arXiv cs.CR 2017
Year: 2017

Modern computer architectures share physical resources between different programs in order to increase area-, energy-, and cost-efficiency. Unfortunately, sharing often gives rise to side channels that can be exploited for extracting or transmitting sensitive information. We currently lack techniques for systematic reasoning about this interplay between security and efficiency. In particular, there is no established way for quantifying security properties of shared caches. In this paper, we propose a novel model that enables us to characterize important security properties of caches. Our model encompasses two aspects: (1) The amount of information that can be absorbed by a cache, and (2) the amount of information that can effectively be extracted from the cache by an adversary. We use our model to compute both quantities for common cache replacement policies (FIFO, LRU, and PLRU) and to compare their isolation properties. We further show how our model for information extraction leads to an algorithm that can be used to improve the bounds delivered by the CacheAudit static analyzer.
Learning to Decode for Future Success
Venue: arXiv cs.CL 2017
Year: 2017

We introduce a simple, general strategy to manipulate the behavior of a neural decoder that enables it to generate outputs that have specific properties of interest (e.g., sequences of a pre-specified length). The model can be thought of as a simple version of the actor-critic model that uses an interpolation of the actor (the MLE-based token generation policy) and the critic (a value function that estimates the future values of the desired property) for decision making. We demonstrate that the approach is able to incorporate a variety of properties that cannot be handled by standard neural sequence decoders, such as sequence length and backward probability (probability of sources given targets), in addition to yielding consistent improvements in abstractive summarization and machine translation when the property to be optimized is BLEU or ROUGE scores.
Convex Parameterizations and Fidelity Bounds for Nonlinear Identification and Reduced-Order Modelling
Venue: arXiv cs.SY 2017
Year: 2017

Model instability and poor prediction of long-term behavior are common problems when modeling dynamical systems using nonlinear "black-box" techniques. Direct optimization of the long-term predictions, often called simulation error minimization, leads to optimization problems that are generally non-convex in the model parameters and suffer from multiple local minima. In this work we present methods which address these problems through convex optimization, based on Lagrangian relaxation, dissipation inequalities, contraction theory, and semidefinite programming. We demonstrate the proposed methods with a model order reduction task for electronic circuit design and the identification of a pneumatic actuator from experiment.
Variable-length codes for channels with memory and feedback: error-exponent upper bounds
Venue: arXiv cs.IT 2017
Year: 2017

The reliability function of memoryless channels with noiseless feedback and variable-length coding has been found to be a linear function of the average rate in the classic work of Burnashev. In this work we consider unifilar channels with noiseless feedback and study upper bounds for the channel reliability function with variable length codes. In unifilar channels the channel state is known to the transmitter but is unknown to the receiver. We generalize Burnashev's analysis and derive a similar expression which is linear in average rate and depends on the channel capacity, as well as an additional parameter which relates to a sequential binary hypothesis testing problem over this channel. This parameter is evaluated by setting up an appropriate Markov decision process (MDP). Furthermore, an upper bound for this parameter is derived using a simplified MDP. Numerical evaluation of the parameter for several binary input/state/output unifilar channels hints at the optimal transmission strategies. Such strategies are studied in a companion paper to provide lower (achievable) bounds on the channel reliability function.
Variable-length codes for channels with memory and feedback: error-exponent lower bounds
Venue: arXiv cs.IT 2017
Year: 2017

The reliability function of memoryless channels with noiseless feedback and variable-length coding has been found to be a linear function of the average rate in the classic work of Burnashev. In this work we consider unifilar channels with noiseless feedback and study specific transmission schemes, the performance of which provides lower bounds for the channel reliability function. In unifilar channels the channel state evolves in a deterministic fashion based on the previous state, input, and output, and is known to the transmitter but is unknown to the receiver. We consider a two-stage transmission scheme. In the first stage, both transmitter and receiver summarize their common information in an M-dimensional vector with elements in the state space of the unifilar channel and an M-dimensional probability mass function, with M being the number of messages. The second stage, which is entered when one of the messages is sufficiently reliable, is resolving a binary hypothesis testing problem. The analysis assumes the presence of some common randomness shared by the transmitter and receiver, and is based on the study of the log-likelihood ratio of the transmitted message posterior belief, and in particular on the study of its multi-step drift. Simulation results confirm that the bounds are tight compared to the upper bounds derived in a companion paper.
Variability-Aware Design for Energy Efficient Computational Artificial Intelligence Platform
Venue: arXiv cs.AR 2017
Year: 2017

Portable computing devices, which include tablets, smart phones and various types of wearable sensors, experienced a rapid development in recent years. One of the most critical limitations for these devices is the power consumption as they use batteries as the power supply. However, the bottleneck of the power saving schemes in both hardware design and software algorithm is the huge variability in power consumption. The variability is caused by a myriad of factors, including the manufacturing process, the ambient environment (temperature, humidity), the aging effects and etc. As the technology node scaled down to 28nm and even lower, the variability becomes more severe. As a result, a platform for variability characterization seems to be very necessary and helpful.
Towards the quality improvement of cross-platform mobile applications
Venue: arXiv cs.SE 2017
Year: 2017

During last ten years, the number of smartphones and mobile applications has been constantly growing. Android, iOS and Windows Mobile are three mobile platforms that cover almost all smartphones in the world in 2017. Developing a mobile app involves first to choose the platforms the app will run, and then to develop specific solutions (i.e., native apps) for each chosen platform using platform-related toolkits such as AndroidSDK. Across-platform mobile application is an app that runs on two or more mobile platforms. Several frameworks have been proposed to simplify the development of cross-platform mobile applications and to reduce development and maintenance costs.They are called cross-platform mobile app development frameworks.However, to our knowledge, the life-cycle and the quality of cross-platforms mobile applications built using those frameworks have not been studied in depth. Our main goal is to first study the processes of development and maintenance of mobile applications built using cross-platform mobile app development frameworks, focusing particularly on the bug-fixing activity. Then, we aim at defining tools for automated repairing bugs from cross-platform mobile applications.
Security and Privacy of performing Data Analytics in the cloud - A three-way handshake of Technology, Policy, and Management
Venue: arXiv cs.DC 2017
Year: 2017

Cloud platform came into existence primarily to accelerate IT delivery and to promote innovation. To this point, it has performed largely well to the expectations of technologists, businesses and customers. The service aspect of this technology has paved the road for a faster set up of infrastructure and related goals for both startups and established organizations. This has further led to quicker delivery of many user-friendly applications to the market while proving to be a commercially viable option to companies with limited resources. On the technology front, the creation and adoption of this ecosystem has allowed easy collection of massive data from various sources at one place, where the place is sometimes referred as just the cloud. Efficient data mining can be performed on raw data to extract potentially useful information, which was not possible at this scale before. Targeted advertising is a common example that can help businesses. Despite these promising offerings, concerns around security and privacy of user information suppressed wider acceptance and an all-encompassing deployment of the cloud platform. In this paper, we discuss security and privacy concerns that occur due to data exchanging hands between a cloud servicer provider (CSP) and the primary cloud user - the data collector, from the content generator. We offer solutions that encompass technology, policy and sound management of the cloud service asserting that this approach has the potential to provide a holistic solution.
Improved Descriptors for Patch Matching and Reconstruction
Venue: arXiv cs.CV 2017
Year: 2017

We propose a convolutional neural network (ConvNet) based approach for learning local image descriptors which can be used for significantly improved patch matching and 3D reconstructions. A multi-resolution ConvNet is used for learning keypoint descriptors. We also propose a new dataset consisting of an order of magnitude more number of scenes, images, and positive and negative correspondences compared to the currently available Multi-View Stereo (MVS) [18] dataset. The new dataset also has better coverage of the overall viewpoint, scale, and lighting changes in comparison to the MVS dataset. We evaluate our approach on publicly available datasets, such as Oxford Affine Covariant Regions Dataset (ACRD) [12], MVS [18], Synthetic [6] and Strecha [15] datasets to quantify the image descriptor performance. Scenes from the Oxford ACRD, MVS and Synthetic datasets are used for evaluating the patch matching performance of the learnt descriptors while the Strecha dataset is used to evaluate the 3D reconstruction task. Experiments show that the proposed descriptor outperforms the current state-of-the-art descriptors in both the evaluation tasks.
Detecting Hierarchical Ties Using Link-Analysis Ranking at Different Levels of Time Granularity
Venue: arXiv cs.SI 2017
Year: 2017

Social networks contain implicit knowledge that can be used to infer hierarchical relations that are not explicitly present in the available data. Interaction patterns are typically affected by users' social relations. We present an approach to inferring such information that applies a link-analysis ranking algorithm at different levels of time granularity. In addition, a voting scheme is employed for obtaining the hierarchical relations. The approach is evaluated on two datasets: the Enron email data set, where the goal is to infer manager-subordinate relationships, and the Co-author data set, where the goal is to infer PhD advisor-advisee relations. The experimental results indicate that the proposed approach outperforms more traditional approaches to inferring hierarchical relations from social networks.
Deep Network Guided Proof Search
Venue: arXiv cs.AI 2017
Year: 2017

Deep learning techniques lie at the heart of several significant AI advances in recent years including object recognition and detection, image captioning, machine translation, speech recognition and synthesis, and playing the game of Go. Automated first-order theorem provers can aid in the formalization and verification of mathematical theorems and play a crucial role in program analysis, theory reasoning, security, interpolation, and system verification. Here we suggest deep learning based guidance in the proof search of the theorem prover E. We train and compare several deep neural network models on the traces of existing ATP proofs of Mizar statements and use them to select processed clauses during proof search. We give experimental evidence that with a hybrid, two-phase approach, deep learning based guidance can significantly reduce the average number of proof search steps while increasing the number of theorems proved. Using a few proof guidance strategies that leverage deep neural networks, we have found first-order proofs of 7.36% of the first-order logic translations of the Mizar Mathematical Library theorems that did not previously have ATP generated proofs. This increases the ratio of statements in the corpus with ATP generated proofs from 56% to 59%.
Optimal Context Aware Transmission Strategy for non-Orthogonal D2D Communications
Venue: arXiv cs.NI 2017
Year: 2017

The increasing traffic demand in cellular networks has recently led to the investigation of new strategies to save precious resources like spectrum and energy. A possible solution employs direct device-to-device (D2D) communications, which is particularly promising when the two terminals involved in the communications are located in close proximity. The D2D communications should coexist with other transmissions, so they must be careful scheduled in order to avoid harmful interference impacts. In this paper, we analyze how a distributed context-awareness, obtained by observing few local channel and topology parameters, can be used to adaptively exploit D2D communications. We develop a rigorous theoretical analysis to quantify the balance between the gain offered by a D2D transmission, and its impact on the other network communications. Based on this analysis, we derive two theorems that define the optimal strategy to be employed, in terms of throughput maximization, when a single or multiple transmit power levels are available for the D2D communications. We compare this strategy to the state-of-the-art in the same network scenario, showing how context awareness can be exploited to achieve a higher sum throughput and an improved fairness.
A New Wiretap Channel Model and its Strong Secrecy Capacity
Venue: arXiv cs.IT 2017
Year: 2017

In this paper, a new wiretap channel model is proposed, where the legitimate transmitter and receiver communicate over a discrete memoryless channel. The wiretapper has perfect access to a fixed-length subset of the transmitted codeword symbols of her choosing. Additionally, she observes the remainder of the transmitted symbols through a discrete memoryless channel. This new model subsumes the classical wiretap channel and wiretap channel II with noisy main channel as its special cases. The strong secrecy capacity of the proposed channel model is identified. Achievability is established by solving a dual secret key agreement problem in the source model, and converting the solution to the original channel model using probability distribution approximation arguments. In the dual problem, a source encoder and decoder, who observe random sequences independent and identically distributed according to the input and output distributions of the legitimate channel in the original problem, communicate a confidential key over a public error-free channel using a single forward transmission, in the presence of a compound wiretapping source who has perfect access to the public discussion. The security of the key is guaranteed for the exponentially many possibilities of the subset chosen at wiretapper by deriving a lemma which provides a doubly-exponential convergence rate for the probability that, for a fixed choice of the subset, the key is uniform and independent from the public discussion and the wiretapping source's observation. The converse is derived by using Sanov's theorem to upper bound the secrecy capacity of the new wiretap channel model by the secrecy capacity when the tapped subset is randomly chosen by nature.
Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural Code
Venue: arXiv cs.PL 2017
Year: 2017

The current trends in next-generation exascale systems go towards integrating a wide range of specialized (co-)processors into traditional supercomputers. Due to the efficiency of heterogeneous systems in terms of Watts and FLOPS per surface unit, opening the access of heterogeneous platforms to a wider range of users is an important problem to be tackled. However, heterogeneous platforms limit the portability of the applications and increase development complexity due to the programming skills required. Program transformation can help make programming heterogeneous systems easier by defining a step-wise transformation process that translates a given initial code into a semantically equivalent final code, but adapted to a specific platform. Program transformation systems require the definition of efficient transformation strategies to tackle the combinatorial problem that emerges due to the large set of transformations applicable at each step of the process. In this paper we propose a machine learning-based approach to learn heuristics to define program transformation strategies. Our approach proposes a novel combination of reinforcement learning and classification methods to efficiently tackle the problems inherent to this type of systems. Preliminary results demonstrate the suitability of this approach.
Interactive Proof Presentations with Cobra
Venue: arXiv cs.LO 2017
Year: 2017

We present Cobra, a modern proof presentation framework, leveraging cutting-edge presentation technology together with a state of the art interactive theorem prover to present formalized mathematics as active documents. Cobra provides both an easy way to present proofs and a novel approach to auditorium interaction. The presentation is checked live by the theorem prover, and moreover allows for live changes both by the presenter and the audience.
Throughput Maximization for Wireless Powered Communications Harvesting from Non-dedicated Sources
Venue: arXiv cs.NI 2017
Year: 2017

We consider the wireless powered communications where users harvest energy from non-dedicated sources. The user follows a harvest-then-transmit protocol: in first phase of a slot time the source node harvests energy from a nearby conventional Access Point, then transmit information to its destination node or relay node in the second phase. We obtain the optimal\textit{ harvesting ratio} to maximize the expected throughput for direct transmission (DT )and decode forward (DF) relay under outage constraint, respectively. Our results reveal that the optimal harvest ratio for DT is dominated by the outage constraint while for DF relay, by the data causality .