OpenRaiser/Intern-Atlas huggingface dataset:
Safe Non-blocking Synchronization in Ada 202x
Venue: arXiv cs.PL 2018
Year: 2018

The mutual-exclusion property of locks stands in the way to scalability of parallel programs on many-core architectures. Locks do not allow progress guarantees, because a task may fail inside a critical section and keep holding a lock that blocks other tasks from accessing shared data. With non-blocking synchronization, the drawbacks of locks are avoided by synchronizing access to shared data by atomic read-modify-write operations. To incorporate non-blocking synchronization in Ada~202x, programmers must be able to reason about the behavior and performance of tasks in the absence of protected objects and rendezvous. We therefore extend Ada's memory model by synchronized types, which support the expression of memory ordering operations at a sufficient level of detail. To mitigate the complexity associated with non-blocking synchronization, we propose concurrent objects as a novel high-level language construct. Entities of a concurrent object execute in parallel, due to a fine-grained, optimistic synchronization mechanism. Synchronization is framed by the semantics of concurrent entry execution. The programmer is only required to label shared data accesses in the code of concurrent entries. Labels constitute memory-ordering operations expressed through attributes. To the best of our knowledge, this is the first approach to provide a non-blocking synchronization construct as a first-class citizen of a high-level programming language. We illustrate the use of concurrent objects by several examples.
Random Polyhedral Scenes: An Image Generator for Active Vision System Experiments
Venue: arXiv cs.CV 2018
Year: 2018

We present a Polyhedral Scene Generator system which creates a random scene based on a few user parameters, renders the scene from random view points and creates a dataset containing the renderings and corresponding annotation files. We hope that this generator will enable research on how a program could parse a scene if it had multiple viewpoints to consider. For ambiguous scenes, typically people move their head or change their position to see the scene from different angles as well as seeing how it changes while they move; this research field is called active perception. The random scene generator presented is designed to support research in this field by generating images of scenes with known complexity characteristics and with verifiable properties with respect to the distribution of features across a population. Thus, it is well-suited for research in active perception without the requirement of a live 3D environment and mobile sensing agent, including comparative performance evaluations. The system is publicly available at https://polyhedral.eecs.yorku.ca.
Harmonizing Signals and Events with a Lightweight Extension to Java
Venue: arXiv cs.PL 2018
Year: 2018

The current demands for seamless connections with the surrounding environment make software more reactive. For example, such demands are evident in systems consisting of the Internet of Things. Such systems include a set of reactive values that are periodically updated in response to external or internal events to form a dataflow in the sense that such updates are propagated to other reactive values. Two effective approaches for realizing such reactive values have been proposed: the event mechanisms in event-based programming and the signals in functional-reactive programming. These two approaches are now becoming mixed in several languages such as Flapjax and REScala, which makes these languages notably expressive for modularizing the implementation of reactive software. For example, REScala provides a rich API that consists of functions converting events to signals and vice versa. In this paper, we explore another, simpler approach in the design space of reactive programming languages: the event mechanism is harmonized with signals, resulting in a simplified programming interface that is mostly based on signals. Based on this approach, we realize SignalJ, a simple extension of Java with events and signals. Our notable findings are (1) an event can be represented as an update of a signal and (2) such an effectful signal can be represented using annotations instead of introducing types and constructors for signals to further simplify the language. Another contribution of this paper is the formal model of SignalJ. As both mechanisms of events and signals may interfere with each other, this mixing sometimes results in surprising behavior. For example, the functional behavior of signals is affected by the imperative features of events. Thus, understanding the formal model of this mixing is actually important. The core calculus, Featherweight SignalJ (FSJ), was developed as an extension of Featherweight Java, and proofs are provided to ensure the soundness of FSJ.
Incremental Training of Deep Convolutional Neural Networks
Venue: arXiv cs.LG 2018
Year: 2018

We propose an incremental training method that partitions the original network into sub-networks, which are then gradually incorporated in the running network during the training process. To allow for a smooth dynamic growth of the network, we introduce a look-ahead initialization that outperforms the random initialization. We demonstrate that our incremental approach reaches the reference network baseline accuracy. Additionally, it allows to identify smaller partitions of the original state-of-the-art network, that deliver the same final accuracy, by using only a fraction of the global number of parameters. This allows for a potential speedup of the training time of several factors. We report training results on CIFAR-10 for ResNet and VGGNet.
Canonical Correlation Analysis of Datasets with a Common Source Graph
Venue: arXiv cs.LG 2018
Year: 2018

Canonical correlation analysis (CCA) is a powerful technique for discovering whether or not hidden sources are commonly present in two (or more) datasets. Its well-appreciated merits include dimensionality reduction, clustering, classification, feature selection, and data fusion. The standard CCA however, does not exploit the geometry of the common sources, which may be available from the given data or can be deduced from (cross-) correlations. In this paper, this extra information provided by the common sources generating the data is encoded in a graph, and is invoked as a graph regularizer. This leads to a novel graph-regularized CCA approach, that is termed graph (g) CCA. The novel gCCA accounts for the graph-induced knowledge of common sources, while minimizing the distance between the wanted canonical variables. Tailored for diverse practical settings where the number of data is smaller than the data vector dimensions, the dual formulation of gCCA is also developed. One such setting includes kernels that are incorporated to account for nonlinear data dependencies. The resultant graph-kernel (gk) CCA is also obtained in closed form. Finally, corroborating image classification tests over several real datasets are presented to showcase the merits of the novel linear, dual, and kernel approaches relative to competing alternatives.
Evolutionary Multi-objective Optimization of Real-Time Strategy Micro
Venue: arXiv cs.NE 2018
Year: 2018

We investigate an evolutionary multi-objective approach to good micro for real-time strategy games. Good micro helps a player win skirmishes and is one of the keys to developing better real-time strategy game play. In prior work, the same multi-objective approach of maximizing damage done while minimizing damage received was used to evolve micro for a group of ranged units versus a group of melee units. We extend this work to consider groups composed from two types of units. Specifically, this paper uses evolutionary multi-objective optimization to generate micro for one group composed from both ranged and melee units versus another group of ranged and melee units. Our micro behavior representation uses influence maps to represent enemy spatial information and potential fields generated from distance, health, and weapons cool down to guide unit movement. Experimental results indicate that our multi-objective approach leads to a Pareto front of diverse high-quality micro encapsulating multiple possible tactics. This range of micro provided by the Pareto front enables a human or AI player to trade-off among short term tactics that better suit the player's longer term strategy - for example, choosing to minimize friendly unit damage at the cost of only lightly damaging the enemy versus maximizing damage to the enemy units at the cost of increased damage to friendly units. We believe that our results indicate the usefulness of potential fields as a representation, and of evolutionary multi-objective optimization as an approach, for generating good micro.
Ten Diverse Formal Models for a CBTC Automatic Train Supervision System
Venue: arXiv cs.SE 2018
Year: 2018

Communications-based Train Control (CBTC) systems are metro signalling platforms, which coordinate and protect the movements of trains within the tracks of a station, and between different stations. In CBTC platforms, a prominent role is played by the Automatic Train Supervision (ATS) system, which automatically dispatches and routes trains within the metro network. Among the various functions, an ATS needs to avoid deadlock situations, i.e., cases in which a group of trains block each other. In the context of a technology transfer study, we designed an algorithm for deadlock avoidance in train scheduling. In this paper, we present a case study in which the algorithm has been applied. The case study has been encoded using ten different formal verification environments, namely UMC, SPIN, NuSMV/nuXmv, mCRL2, CPN Tools, FDR4, CADP, TLA+, UPPAAL and ProB. Based on our experience, we observe commonalities and differences among the modelling languages considered, and we highlight the impact of the specific characteristics of each language on the presented models.
An Experiment in Ping-Pong Protocol Verification by Nondeterministic Pushdown Automata
Venue: arXiv cs.PL 2018
Year: 2018

An experiment is described that confirms the security of a well-studied class of cryptographic protocols (Dolev-Yao intruder model) can be verified by two-way nondeterministic pushdown automata (2NPDA). A nondeterministic pushdown program checks whether the intersection of a regular language (the protocol to verify) and a given Dyck language containing all canceling words is empty. If it is not, an intruder can reveal secret messages sent between trusted users. The verification is guaranteed to terminate in cubic time at most on a 2NPDA-simulator. The interpretive approach used in this experiment simplifies the verification, by separating the nondeterministic pushdown logic and program control, and makes it more predictable. We describe the interpretive approach and the known transformational solutions, and show they share interesting features. Also noteworthy is how abstract results from automata theory can solve practical problems by programming language means.
Smoothed Online Convex Optimization in High Dimensions via Online Balanced Descent
Venue: arXiv cs.LG 2018
Year: 2018

We study Smoothed Online Convex Optimization, a version of online convex optimization where the learner incurs a penalty for changing her actions between rounds. Given a $Ω(\sqrt{d})$ lower bound on the competitive ratio of any online algorithm, where $d$ is the dimension of the action space, we ask under what conditions this bound can be beaten. We introduce a novel algorithmic framework for this problem, Online Balanced Descent (OBD), which works by iteratively projecting the previous point onto a carefully chosen level set of the current cost function so as to balance the switching costs and hitting costs. We demonstrate the generality of the OBD framework by showing how, with different choices of "balance," OBD can improve upon state-of-the-art performance guarantees for both competitive ratio and regret, in particular, OBD is the first algorithm to achieve a dimension-free competitive ratio, $3 + O(1/α)$, for locally polyhedral costs, where $α$ measures the "steepness" of the costs. We also prove bounds on the dynamic regret of OBD when the balance is performed in the dual space that are dimension-free and imply that OBD has sublinear static regret.
Automatic Stroke Lesions Segmentation in Diffusion-Weighted MRI
Venue: arXiv cs.CV 2018
Year: 2018

Diffusion-Weighted Magnetic Resonance Imaging (DWI) is widely used for early cerebral infarct detection caused by ischemic stroke. Manual segmentation is done by a radiologist as a common clinical process, nonetheless, challenges of cerebral infarct segmentation come from low resolution and uncertain boundaries. Many segmentation techniques have been proposed and proved by manual segmentation as gold standard. In order to reduce human error in research operation and clinical process, we adopt a semi-automatic segmentation as gold standard using Fluid-Attenuated Inversion-Recovery (FLAIR) Magnetic Resonance Image (MRI) from the same patient under controlled environment. Extensive testing is performed on popular segmentation algorithms including Otsu method, Fuzzy C-means, Hill-climbing based segmentation, and Growcut. The selected segmentation techniques have been validated by accuracy, sensitivity, and specificity using leave-one-out cross-validation to determine the possibility of each techniques first then maximizes the accuracy from the training set. Our experimental results demonstrate the effectiveness of selected methods.
The Effects of JPEG and JPEG2000 Compression on Attacks using Adversarial Examples
Venue: arXiv cs.CV 2018
Year: 2018

Adversarial examples are known to have a negative effect on the performance of classifiers which have otherwise good performance on undisturbed images. These examples are generated by adding non-random noise to the testing samples in order to make classifier misclassify the given data. Adversarial attacks use these intentionally generated examples and they pose a security risk to the machine learning based systems. To be immune to such attacks, it is desirable to have a pre-processing mechanism which removes these effects causing misclassification while keeping the content of the image. JPEG and JPEG2000 are well-known image compression techniques which suppress the high-frequency content taking the human visual system into account. JPEG has been also shown to be an effective method for reducing adversarial noise. In this paper, we propose applying JPEG2000 compression as an alternative and systematically compare the classification performance of adversarial images compressed using JPEG and JPEG2000 at different target PSNR values and maximum compression levels. Our experiments show that JPEG2000 is more effective in reducing adversarial noise as it allows higher compression rates with less distortion and it does not introduce blocking artifacts.
Handling Verb Phrase Anaphora with Dependent Types and Events
Venue: arXiv cs.CL 2018
Year: 2018

This paper studies how dependent typed events can be used to treat verb phrase anaphora. We introduce a framework that extends Dependent Type Semantics (DTS) with a new atomic type for neo-Davidsonian events and an extended @-operator that can return new events that share properties of events referenced by verb phrase anaphora. The proposed framework, along with illustrative examples of its use, are presented after a brief overview of the necessary background and of the major challenges posed by verb phrase anaphora.
Non-Linear Model Predictive Control with Adaptive Time-Mesh Refinement
Venue: arXiv cs.RO 2018
Year: 2018

In this paper, we present a novel solution for real-time, Non-Linear Model Predictive Control (NMPC) exploiting a time-mesh refinement strategy. The proposed controller formulates the Optimal Control Problem (OCP) in terms of flat outputs over an adaptive lattice. In common approximated OCP solutions, the number of discretization points composing the lattice represents a critical upper bound for real-time applications. The proposed NMPC-based technique refines the initially uniform time horizon by adding time steps with a sampling criterion that aims to reduce the discretization error. This enables a higher accuracy in the initial part of the receding horizon, which is more relevant to NMPC, while keeping bounded the number of discretization points. By combining this feature with an efficient Least Square formulation, our solver is also extremely time-efficient, generating trajectories of multiple seconds within only a few milliseconds. The performance of the proposed approach has been validated in a high fidelity simulation environment, by using an UAV platform. We also released our implementation as open source C++ code.
Are There Functionally Similar Code Clones in Practice?
Venue: arXiv cs.SE 2018
Year: 2018

Having similar code fragments, also called clones, in software systems can lead to unnecessary comprehension, review and change efforts. Syntactically similar clones can often be encountered in practice. The same is not clear for only functionally similar clones (FSC). We conducted an exploratory survey among developers to investigate whether they encounter functionally similar clones in practice and whether there is a difference in their inclination to remove them to syntactically similar clones. Of the 34 developers answering the survey, 31 have experienced FSC in their professional work, and 24 have experienced problems caused by FSCs. We found no difference in the inclination and reasoning for removing FSCs and syntactically similar clones. FSCs exist in practice and should be investigated to bring clone detectors to the same quality as for syntactically similar clones, because being able to detect them allows developers to manage and potentially remove them.
Normalization of Neural Networks using Analytic Variance Propagation
Venue: arXiv cs.LG 2018
Year: 2018

We address the problem of estimating statistics of hidden units in a neural network using a method of analytic moment propagation. These statistics are useful for approximate whitening of the inputs in front of saturating non-linearities such as a sigmoid function. This is important for initialization of training and for reducing the accumulated scale and bias dependencies (compensating covariate shift), which presumably eases the learning. In batch normalization, which is currently a very widely applied technique, sample estimates of statistics of hidden units over a batch are used. The proposed estimation uses an analytic propagation of mean and variance of the training set through the network. The result depends on the network structure and its current weights but not on the specific batch input. The estimates are suitable for initialization and normalization, efficient to compute and independent of the batch size. The experimental verification well supports these claims. However, the method does not share the generalization properties of BN, to which our experiments give some additional insight.
Stability and Dynamic Control of Underlay Mobile Edge Networks
Venue: arXiv cs.IT 2018
Year: 2018

This paper studies the stability and dynamic control of underlay mobile edge networks. First, the stability region for a multiuser edge network is obtained under the assumption of full channel state information. This result provides a benchmark figure for comparing performance of the proposed algorithms. Second, a centralized joint flow control and scheduling algorithm is proposed to stabilize the queues of edge devices while respecting the average and instantaneous interference power constraints at the core access point. This algorithm is proven to converge to a utility point arbitrarily close to the maximum achievable utility within the stability region. Finally, more practical implementation issues such as distributed scheduling are examined by designing efficient scheduling algorithms taking advantage of communications diversity. The proposed distributed solutions utilize mini slots for contention resolution and achieve a certain fraction of the utility optimal point. The performance lower bounds for distributed algorithms are determined analytically. The detailed simulation study is performed to pinpoint the cost of distributed control for mobile edge networks with respect to centralized control.
Implementation of an Improved Coulomb-Counting Algorithm Based on a Piecewise SOC-OCV Relationship for SOC Estimation of Li-IonBattery
Venue: arXiv cs.SY 2018
Year: 2018

Considering the expanding useofembedded devices equipped with rechargeable batteries, especially Li-ionbatteries that have higher power and energy density, the battery management systemis becomingincreasingly important. Infact, theestimationaccuracy of the amount of the remaining charges is critical as it affects the device operational autonomy.Therefore, the battery State-Of-Charge (SOC) is defined to indicate its estimated available charge. In this paper, a solution isproposed for Li-ion battery SOC estimation based on an enhanced Coulomb-counting algorithm to be implemented formultimedia applications.However,the Coulomb-counting algorithm suffers from cumulative errors due to the initial SOC andtheerrors ofmeasurements uncertainties,thereforeto overcome these limitations,we use the Open-CircuitVoltage (OCV),thushavinga piecewise linear SOC-OCV relationship andperformingperiodic re-calibration of the battery capacity. Thissolutionis implementedand validated on a hardware platform based onthePIC18F MCU family. The measured resultsarecorrelated withthetheoretical ones; they have shown a reliable estimation since accuracy is less than 2%.