arXiv subjects

Satoshi Matsuoka

Publications and source records attributed to Satoshi Matsuoka.

46 records · Page 3Linked to original sources

arXiv2018

High-performance sparse matrix-matrix products on Intel KNL and multicore architectures

Sparse matrix-matrix multiplication (SpGEMM) is a computational primitive that is widely used in areas ranging from traditional numerical applications to recent big data analysis and machine learning. Although many SpGEMM algorithms have been proposed, hardware specific optimizations for multi- and many-core processors are lacking and a detailed analysis of their performance under various use cases and matrices is not available. We firstly identify and mitigate multiple bottlenecks with memory management and thread scheduling on Intel Xeon Phi (Knights Landing or KNL). Specifically targeting multi- and many-core processors, we develop a hash-table-based algorithm and optimize a heap-based shared-memory SpGEMM algorithm. We examine their performance together with other publicly available codes. Different from the literature, our evaluation also includes use cases that are representative of real graph algorithms, such as multi-source breadth-first search or triangle counting. Our hash-table and heap-based algorithms are showing significant speedups from libraries in the majority of the cases while different algorithms dominate the other scenarios with different matrix size, sparsity, compression factor and operation type. We wrap up in-depth evaluation results and make a recipe to give the best SpGEMM algorithm for target scenario. A critical finding is that hash-table-based SpGEMM gets a significant performance boost if the nonzeros are not required to be sorted within each row of the output matrix.

cs.DC↗

arXiv2018

μ-cuDNN: Accelerating Deep Learning Frameworks with Micro-Batching

NVIDIA cuDNN is a low-level library that provides GPU kernels frequently used in deep learning. Specifically, cuDNN implements several equivalent convolution algorithms, whose performance and memory footprint may vary considerably, depending on the layer dimensions. When an algorithm is automatically selected by cuDNN, the decision is performed on a per-layer basis, and thus it often resorts to slower algorithms that fit the workspace size constraints. We present μ-cuDNN, a transparent wrapper library for cuDNN, which divides layers' mini-batch computation into several micro-batches. Based on Dynamic Programming and Integer Linear Programming, μ-cuDNN enables faster algorithms by decreasing the workspace requirements. At the same time, μ-cuDNN keeps the computational semantics unchanged, so that it decouples statistical efficiency from the hardware efficiency safely. We demonstrate the effectiveness of μ-cuDNN over two frameworks, Caffe and TensorFlow, achieving speedups of 1.63x for AlexNet and 1.21x for ResNet-18 on P100-SXM2 GPU. These results indicate that using micro-batches can seamlessly increase the performance of deep learning, while maintaining the same memory footprint.

cs.LG↗

arXiv2018

Combined Spatial and Temporal Blocking for High-Performance Stencil Computation on FPGAs Using OpenCL

Recent developments in High Level Synthesis tools have attracted software programmers to accelerate their high-performance computing applications on FPGAs. Even though it has been shown that FPGAs can compete with GPUs in terms of performance for stencil computation, most previous work achieve this by avoiding spatial blocking and restricting input dimensions relative to FPGA on-chip memory. In this work we create a stencil accelerator using Intel FPGA SDK for OpenCL that achieves high performance without having such restrictions. We combine spatial and temporal blocking to avoid input size restrictions, and employ multiple FPGA-specific optimizations to tackle issues arisen from the added design complexity. Accelerator parameter tuning is guided by our performance model, which we also use to project performance for the upcoming Intel Stratix 10 devices. On an Arria 10 GX 1150 device, our accelerator can reach up to 760 and 375 GFLOP/s of compute performance, for 2D and 3D stencils, respectively, which rivals the performance of a highly-optimized GPU implementation. Furthermore, we estimate that the upcoming Stratix 10 devices can achieve a performance of up to 3.5 TFLOP/s and 1.6 TFLOP/s for 2D and 3D stencil computation, respectively.

cs.DC↗

arXiv2016

Strong Typed Böhm Theorem and Functional Completeness on the Linear Lambda Calculus

In this paper, we prove a version of the typed Böhm theorem on the linear lambda calculus, which says, for any given types A and B, when two different closed terms s1 and s2 of A and any closed terms u1 and u2 of B are given, there is a term t such that t s1 is convertible to u1 and t s2 is convertible to u2. Several years ago, a weaker version of this theorem was proved, but the stronger version was open. As a corollary of this theorem, we prove that if A has two different closed terms s1 and s2, then A is functionally complete with regard to s1 and s2. So far, it was only known that a few types are functionally complete.

cs.LO↗

arXiv2013

A New Proof of P-time Completeness of Linear Lambda Calculus

We give a new proof of P-time completeness of Linear Lambda Calculus, which was originally given by H. Mairson in 2003. Our proof uses an essentially different Boolean type from the type Mairson used. Moreover the correctness of our proof can be machined-checked using an implementation of Standard ML.

cs.LO↗

arXiv2010

A Coding Theoretic Study on MLL proof nets

Coding theory is very useful for real world applications. A notable example is digital television. Basically, coding theory is to study a way of detecting and/or correcting data that may be true or false. Moreover coding theory is an area of mathematics, in which there is an interplay between many branches of mathematics, e.g., abstract algebra, combinatorics, discrete geometry, information theory, etc. In this paper we propose a novel approach for analyzing proof nets of Multiplicative Linear Logic (MLL) by coding theory. We define families of proof structures and introduce a metric space for each family. In each family, 1. an MLL proof net is a true code element; 2. a proof structure that is not an MLL proof net is a false (or corrupted) code element. The definition of our metrics reflects the duality of the multiplicative connectives elegantly. In this paper we show that in the framework one error-detecting is possible but one error-correcting not. Our proof of the impossibility of one error-correcting is interesting in the sense that a proof theoretical property is proved using a graph theoretical argument. In addition, we show that affine logic and MLL + MIX are not appropriate for this framework. That explains why MLL is better than such similar logics.

cs.LO↗

arXiv2005

Weak Typed Boehm Theorem on IMLL

In the Boehm theorem workshop on Crete island, Zoran Petric called Statman's ``Typical Ambiguity theorem'' typed Boehm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus. In this paper, we study the linear version of the typed Boehm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit 1 (for short IMLL) weak typed Boehm theorem holds. The system IMLL exactly corresponds to the linear lambda calculus without exponentials, additives and logical constants. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner.

cs.LO↗

arXiv2004

P-time Completeness of Light Linear Logic and its Nondeterministic Extension

In CSL'99 Roversi pointed out that the Turing machine encoding of Girard's seminal paper "Light Linear Logic" has a flaw. Moreover he presented a working version of the encoding in Light Affine Logic, but not in Light Linear Logic. In this paper we present a working version of the encoding in Light Linear Logic. The idea of the encoding is based on a remark of Girard's tutorial paper on Linear Logic. The encoding is also an example which shows usefulness of additive connectives. Moreover we also consider a nondeterministic extension of Light Linear Logic. We show that the extended system is NP-complete in the same meaning as P-completeness of Light Linear Logic.

cs.LO↗

arXiv2004

Nondeterministic Linear Logic

In this paper, we introduce Linear Logic with a nondeterministic facility, which has a self-dual additive connective. In the system the proof net technology is available in a natural way. The important point is that nondeterminism in the system is expressed by the process of normalization, not by proof search. Moreover we can incorporate the system into Light Linear Logic and Elementary Linear Logic developed by J.-Y.Girard recently: Nondeterministic Light Linear Logic and Nondeterministic Elementary Linear Logic are defined in a very natural way.

cs.LO↗

arXiv2003

Worldwide Fast File Replication on Grid Datafarm

The Grid Datafarm architecture is designed for global petascale data-intensive computing. It provides a global parallel filesystem with online petascale storage, scalable I/O bandwidth, and scalable parallel processing, and it can exploit local I/O in a grid of clusters with tens of thousands of nodes. One of features is that it manages file replicas in filesystem metadata for fault tolerance and load balancing. This paper discusses and evaluates several techniques to support long-distance fast file replication. The Grid Datafarm manages a ranked group of files as a Gfarm file, each file, called a Gfarm file fragment, being stored on a filesystem node, or replicated on several filesystem nodes. Each Gfarm file fragment is replicated independently and in parallel using rate-controlled HighSpeed TCP with network striping. On a US-Japan testbed with 10,000 km distance, we achieve 419 Mbps using 2 nodes on each side, and 741 Mbps using 4 nodes out of 893 Mbps with two transpacific networks.

cs.PF↗