OpenRaiser/Intern-Atlas huggingface dataset:
On Verifying Causal Consistency
Venue: arXiv cs.LO 2016
Year: 2016

Causal consistency is one of the most adopted consistency criteria for distributed implementations of data structures. It ensures that operations are executed at all sites according to their causal precedence. We address the issue of verifying automatically whether the executions of an implementation of a data structure are causally consistent. We consider two problems: (1) checking whether one single execution is causally consistent, which is relevant for developing testing and bug finding algorithms, and (2) verifying whether all the executions of an implementation are causally consistent. We show that the first problem is NP-complete. This holds even for the read-write memory abstraction, which is a building block of many modern distributed systems. Indeed, such systems often store data in key-value stores, which are instances of the read-write memory abstraction. Moreover, we prove that, surprisingly, the second problem is undecidable, and again this holds even for the read-write memory abstraction. However, we show that for the read-write memory abstraction, these negative results can be circumvented if the implementations are data independent, i.e., their behaviors do not depend on the data values that are written or read at each moment, which is a realistic assumption.
Scala-gopher: CSP-style programming techniques with idiomatic Scala
Venue: arXiv cs.PL 2016
Year: 2016

Cala-gopher is a library-level Scala implementation of communication sequence process constructs: channels, selectors (similar to analogical constructs in Limbo or Go) transputers (similar to Occam proc) and a set of high-level operations on top of akka and SIP-22 async. The framework integrates CSP-style programming into standard Scala concurrency environment via idiomatic API. This allows usage of communication patterns, well known in Go world, but not easy expressable in mainstream scala concurrency frameworks, along with algebraic approach for composing computation builders. Besides, we want to discuss current implementation issues and future directions in the context of evolving of compiler and libraries ecosystem.
Towards Automatic Resource Bound Analysis for OCaml
Venue: arXiv cs.PL 2016
Year: 2016

This article presents a resource analysis system for OCaml programs. This system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and can derive bounds for time, memory allocations and energy usage. The derived bounds are multivariate resource polynomials which are functions of different size parameters that depend on the standard OCaml types. Bound inference is fully automatic and reduced to a linear optimization problem that is passed to an off-the-shelf LP solver. Technically, the analysis system is based on a novel multivariate automatic amortized resource analysis (AARA). It builds on existing work on linear AARA for higher-order programs with user-defined inductive types and on multivariate AARA for first-order programs with built-in lists and binary trees. For the first time, it is possible to automatically derive polynomial bounds for higher-order functions and polynomial bounds that depend on user-defined inductive types. Moreover, the analysis handles programs with side effects and even outperforms the linear bound inference of previous systems. At the same time, it preserves the expressivity and efficiency of existing AARA techniques. The practicality of the analysis system is demonstrated with an implementation and integration with Inria's OCaml compiler. The implementation is used to automatically derive resource bounds for 411 functions and 6018 lines of code derived from OCaml libraries, the CompCert compiler, and implementations of textbook algorithms. In a case study, the system infers bounds on the number of queries that are sent by OCaml programs to DynamoDB, a commercial NoSQL cloud database service.
Scalable Semi-Supervised Learning over Networks using Nonsmooth Convex Optimization
Venue: arXiv cs.LG 2016
Year: 2016

We propose a scalable method for semi-supervised (transductive) learning from massive network-structured datasets. Our approach to semi-supervised learning is based on representing the underlying hypothesis as a graph signal with small total variation. Requiring a small total variation of the graph signal representing the underlying hypothesis corresponds to the central smoothness assumption that forms the basis for semi-supervised learning, i.e., input points forming clusters have similar output values or labels. We formulate the learning problem as a nonsmooth convex optimization problem which we solve by appealing to Nesterovs optimal first-order method for nonsmooth optimization. We also provide a message passing formulation of the learning method which allows for a highly scalable implementation in big data frameworks.
Extensions and Limitations of the Neural GPU
Venue: arXiv cs.NE 2016
Year: 2016

The Neural GPU is a recent model that can learn algorithms such as multi-digit binary addition and binary multiplication in a way that generalizes to inputs of arbitrary length. We show that there are two simple ways of improving the performance of the Neural GPU: by carefully designing a curriculum, and by increasing model size. The latter requires a memory efficient implementation, as a naive implementation of the Neural GPU is memory intensive. We find that these techniques increase the set of algorithmic problems that can be solved by the Neural GPU: we have been able to learn to perform all the arithmetic operations (and generalize to arbitrarily long numbers) when the arguments are given in the decimal representation (which, surprisingly, has not been possible before). We have also been able to train the Neural GPU to evaluate long arithmetic expressions with multiple operands that require respecting the precedence order of the operands, although these have succeeded only in their binary representation, and not with perfect accuracy. In addition, we gain insight into the Neural GPU by investigating its failure modes. We find that Neural GPUs that correctly generalize to arbitrarily long numbers still fail to compute the correct answer on highly-symmetric, atypical inputs: for example, a Neural GPU that achieves near-perfect generalization on decimal multiplication of up to 100-digit long numbers can fail on $000000\dots002 \times 000000\dots002$ while succeeding at $2 \times 2$. These failure modes are reminiscent of adversarial examples.
Enerji İzleme Yazılımları için Merkezi ve Genel bir Mimari (A Centralized and Generic Architecture for Energy Monitoring Software)
Venue: arXiv cs.OH 2016
Year: 2016

There is need for several software systems within the energy domain and corresponding systems are being developed to satisfy these needs. These systems include energy monitoring, information, wide area monitoring and control systems, and SCADA systems. Energy monitoring systems are one of the most important and common systems among them. In this study, after briefly reviewing several of the software systems within the energy domain, a centralized and generic software architecture for energy monitoring systems is presented. Next, sample projects are described in which energy monitoring systems based on this architecture have been implemented. We envisage that this study will be an important resource for software projects in the energy domain.
A FOFE-based Local Detection Approach for Named Entity Recognition and Mention Detection
Venue: arXiv cs.CL 2016
Year: 2016

In this paper, we study a novel approach for named entity recognition (NER) and mention detection in natural language processing. Instead of treating NER as a sequence labelling problem, we propose a new local detection approach, which rely on the recent fixed-size ordinally forgetting encoding (FOFE) method to fully encode each sentence fragment and its left/right contexts into a fixed-size representation. Afterwards, a simple feedforward neural network is used to reject or predict entity label for each individual fragment. The proposed method has been evaluated in several popular NER and mention detection tasks, including the CoNLL 2003 NER task and TAC-KBP2015 and TAC-KBP2016 Tri-lingual Entity Discovery and Linking (EDL) tasks. Our methods have yielded pretty strong performance in all of these examined tasks. This local detection approach has shown many advantages over the traditional sequence labelling methods.
QoE-based MAC Layer Optimization for Video Teleconferencing over WiFi
Venue: arXiv cs.MM 2016
Year: 2016

In IEEE 802.11, the retry limit is set the same value for all packets. In this paper, we dynamically classify video teleconferencing packets based on the type of the video frame that a packet carries and the packet loss events that have happened in the network, and assign them different retry limits. We consider the IPPP video encoding structure with instantaneous decoder refresh (IDR) frame insertion based on packet loss feedback. The loss of a single frame causes error propagation for a period of time equal to the packet loss feedback delay. To optimize the video quality, we propose a method to concentrate the packet losses to small segments of the entire video sequence, and study the performance by an analytic model. Our proposed method is implemented only on the stations interested in enhanced video quality, and is compatible with unmodified IEEE 802.11 stations and access points in terms of performance. Simulation results show that the performance gain can be significant compared to the IEEE 802.11 standard without negatively affecting cross traffic.
A Decision Support System for Inbound Marketers: An Empirical Use of Latent Dirichlet Allocation Topic Model to Guide Infographic Designers
Venue: arXiv cs.HC 2016
Year: 2016

Infographic is a type of information presentation that inbound marketers use. I suggest a method that can allow the infographic designers to benchmark their design against the previous viral infographics to measure whether a given design decision can help or hurt the probability of the design becoming viral.
Runtime Template Instantiation for C++
Venue: arXiv cs.SE 2016
Year: 2016

Performance, genericity and flexibility are three valuable qualities for scientific environments that tend to be antagonistic. C++ provides excellent support for both performances and genericity thanks to its support for (class and function) templates. However, a C++ templated library can hardly be qualified as flexible: data of unexpected types cannot enter the system, which hinders user interactions. This paper describes the approach that was taken in the Vcsn platform to add flexibility on top of C++ templates, including runtime template instantiation.
Bayesian Heuristics for Group Decisions
Venue: arXiv cs.MA 2016
Year: 2016

We propose a model of inference and heuristic decision-making in groups that is rooted in the Bayes rule but avoids the complexities of rational inference in partially observed environments with incomplete information, which are characteristic of group interactions. Our model is also consistent with a dual-process psychological theory of thinking: the group members behave rationally at the initiation of their interactions with each other (the slow and deliberative mode); however, in the ensuing decision epochs, they rely on a heuristic that replicates their experiences from the first stage (the fast automatic mode). We specialize this model to a group decision scenario where private observations are received at the beginning, and agents aim to take the best action given the aggregate observations of all group members. We study the implications of the information structure together with the properties of the probability distributions which determine the structure of the so-called "Bayesian heuristics" that the agents follow in our model. We also analyze the group decision outcomes in two classes of linear action updates and log-linear belief updates and show that many inefficiencies arise in group decisions as a result of repeated interactions between individuals, leading to overconfident beliefs as well as choice-shifts toward extremes. Nevertheless, balanced regular structures demonstrate a measure of efficiency in terms of aggregating the initial information of individuals. These results not only verify some well-known insights about group decision-making but also complement these insights by revealing additional mechanistic interpretations for the group declension-process, as well as psychological and cognitive intuitions about the group interaction model.
Probabilistic Modeling of Progressive Filtering
Venue: arXiv cs.AI 2016
Year: 2016

Progressive filtering is a simple way to perform hierarchical classification, inspired by the behavior that most humans put into practice while attempting to categorize an item according to an underlying taxonomy. Each node of the taxonomy being associated with a different category, one may visualize the categorization process by looking at the item going downwards through all the nodes that accept it as belonging to the corresponding category. This paper is aimed at modeling the progressive filtering technique from a probabilistic perspective, in a hierarchical text categorization setting. As a result, the designer of a system based on progressive filtering should be facilitated in the task of devising, training, and testing it.
CogALex-V Shared Task: ROOT18
Venue: arXiv cs.CL 2016
Year: 2016

In this paper, we describe ROOT 18, a classifier using the scores of several unsupervised distributional measures as features to discriminate between semantically related and unrelated words, and then to classify the related pairs according to their semantic relation (i.e. synonymy, antonymy, hypernymy, part-whole meronymy). Our classifier participated in the CogALex-V Shared Task, showing a solid performance on the first subtask, but a poor performance on the second subtask. The low scores reported on the second subtask suggest that distributional measures are not sufficient to discriminate between multiple semantic relations at once.
Learning Identity Mappings with Residual Gates
Venue: arXiv cs.CV 2016
Year: 2016

We propose a new layer design by adding a linear gating mechanism to shortcut connections. By using a scalar parameter to control each gate, we provide a way to learn identity mappings by optimizing only one parameter. We build upon the motivation behind Residual Networks, where a layer is reformulated in order to make learning identity mappings less problematic to the optimizer. The augmentation introduces only one extra parameter per layer, and provides easier optimization by making degeneration into identity mappings simpler. We propose a new model, the Gated Residual Network, which is the result when augmenting Residual Networks. Experimental results show that augmenting layers provides better optimization, increased performance, and more layer independence. We evaluate our method on MNIST using fully-connected networks, showing empirical indications that our augmentation facilitates the optimization of deep models, and that it provides high tolerance to full layer removal: the model retains over 90% of its performance even after half of its layers have been randomly removed. We also evaluate our model on CIFAR-10 and CIFAR-100 using Wide Gated ResNets, achieving 3.65% and 18.27% error, respectively.
Managing Quality Requirements Using Activity-Based Quality Models
Venue: arXiv cs.SE 2016
Year: 2016

Managing requirements on quality aspects is an important issue in the development of software systems. Difficulties arise from expressing them appropriately what in turn results from the difficulty of the concept of quality itself. Building and using quality models is an approach to handle the complexity of software quality. A novel kind of quality models uses the activities performed on and with the software as an explicit dimension. These quality models are a well-suited basis for managing quality requirements from elicitation over refinement to assurance. The paper proposes such an approach and shows its applicability in an automotive case study.
Goal-Driven Unfolding of Petri Nets
Venue: arXiv cs.LO 2016
Year: 2016

Unfoldings provide an efficient way to avoid the state-space explosion due to interleavings of concurrent transitions when exploring the runs of a Petri net. The theory of adequate orders allows one to define finite prefixes of unfoldings which contain all the reachable markings. In this paper we are interested in reachability of a single given marking, called the goal. We propose an algorithm for computing a finite prefix of the unfolding of a 1-safe Petri net that preserves all minimal configurations reaching this goal. Our algorithm combines the unfolding technique with on-the-fly model reduction by static analysis aiming at avoiding the exploration of branches which are not needed for reaching the goal. We present some experimental results.
Learning heat diffusion graphs
Venue: arXiv cs.LG 2016
Year: 2016

Effective information analysis generally boils down to properly identifying the structure or geometry of the data, which is often represented by a graph. In some applications, this structure may be partly determined by design constraints or pre-determined sensing arrangements, like in road transportation networks for example. In general though, the data structure is not readily available and becomes pretty difficult to define. In particular, the global smoothness assumptions, that most of the existing works adopt, are often too general and unable to properly capture localized properties of data. In this paper, we go beyond this classical data model and rather propose to represent information as a sparse combination of localized functions that live on a data structure represented by a graph. Based on this model, we focus on the problem of inferring the connectivity that best explains the data samples at different vertices of a graph that is a priori unknown. We concentrate on the case where the observed data is actually the sum of heat diffusion processes, which is a quite common model for data on networks or other irregular structures. We cast a new graph learning problem and solve it with an efficient nonconvex optimization algorithm. Experiments on both synthetic and real world data finally illustrate the benefits of the proposed graph learning framework and confirm that the data structure can be efficiently learned from data observations only. We believe that our algorithm will help solving key questions in diverse application domains such as social and biological network analysis where it is crucial to unveil proper geometry for data understanding and inference.
Protein Secondary Structure Prediction Using Deep Multi-scale Convolutional Neural Networks and Next-Step Conditioning
Venue: arXiv cs.LG 2016
Year: 2016

Recently developed deep learning techniques have significantly improved the accuracy of various speech and image recognition systems. In this paper we adapt some of these techniques for protein secondary structure prediction. We first train a series of deep neural networks to predict eight-class secondary structure labels given a protein's amino acid sequence information and find that using recent methods for regularization, such as dropout and weight-norm constraining, leads to measurable gains in accuracy. We then adapt recent convolutional neural network architectures--Inception, ReSNet, and DenseNet with Batch Normalization--to the problem of protein structure prediction. These convolutional architectures make heavy use of multi-scale filter layers that simultaneously compute features on several scales, and use residual connections to prevent underfitting. Using a carefully modified version of these architectures, we achieve state-of-the-art performance of 70.0% per amino acid accuracy on the public CB513 benchmark dataset. Finally, we explore additions from sequence-to-sequence learning, altering the model to make its predictions conditioned on both the protein's amino acid sequence and its past secondary structure labels. We introduce a new method of ensembling such a conditional model with our convolutional model, an approach which reaches 70.6% Q8 accuracy on CB513. We argue that these results can be further refined for larger boosts in prediction accuracy through more sophisticated attempts to control overfitting of conditional models. We aim to release the code for these experiments as part of the TensorFlow repository.
Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings
Venue: arXiv cs.PL 2016
Year: 2016

The C and C++ high-level languages provide programmers with atomic operations for writing high-performance concurrent code. At the assembly language level, C and C++ atomics get mapped down to individual instructions or combinations of instructions by compilers, depending on the ordering guarantees and synchronization instructions provided by the underlying architecture. These compiler mappings must uphold the ordering guarantees provided by C/C++ atomics or the compiled program will not behave according to the C/C++ memory model. In this paper we discuss two counterexamples to the well-known trailing-sync compiler mappings for the Power and ARMv7 architectures that were previously thought to be proven correct. In addition to the counterexamples, we discuss the loophole in the proof of the mappings that allowed the incorrect mappings to be proven correct. We also discuss the current state of compilers and architectures in relation to the bug.
Quasi-Recurrent Neural Networks
Venue: arXiv cs.NE 2016
Year: 2016

Recurrent neural networks are a powerful tool for modeling sequential data, but the dependence of each timestep's computation on the previous timestep's output limits parallelism and makes RNNs unwieldy for very long sequences. We introduce quasi-recurrent neural networks (QRNNs), an approach to neural sequence modeling that alternates convolutional layers, which apply in parallel across timesteps, and a minimalist recurrent pooling function that applies in parallel across channels. Despite lacking trainable recurrent layers, stacked QRNNs have better predictive accuracy than stacked LSTMs of the same hidden size. Due to their increased parallelism, they are up to 16 times faster at train and test time. Experiments on language modeling, sentiment classification, and character-level neural machine translation demonstrate these advantages and underline the viability of QRNNs as a basic building block for a variety of sequence tasks.
Leveraging Social Communities for Optimizing Cellular Device-to-Device Communications
Venue: arXiv cs.IT 2016
Year: 2016

Device-to-device (D2D) communications over licensed wireless spectrum has been recently proposed as a promising technology to meet the capacity crunch of next generation cellular networks. However, due to the high mobility of cellular devices, establishing and ensuring the success of D2D transmission becomes a major challenge. To this end, in this paper, a novel framework is proposed to enable devices to form multi-hop D2D connections in an effort to maintain sustainable communication in the presence of device mobility. To solve the problem posed by device mobility, in contrast to existing works, which mostly focus on physical domain information, a durable community based approach is introduced taking social encounters into context. It is shown that the proposed scheme can derive an optimal solution for time sensitive content transmission while also minimizing the cost that the base station pays in order to incentivize users to participate in D2D. Simulation results show that the proposed social community aware approach yields significant performance gain, in terms of the amount of traffic offloaded from the cellular network to the D2D tier, compared to the classical social-unaware methods.