日本ソフトウェア科学会第 36 回大会 (2019 年度) 講演論文集

Verification of memory access for deep learningcompilers
Tung D. Le

小川 愛理

Swagath Venkataramani

井上 拓

石崎 一明

小原 盛幹

The succeed of deep learning recently leads to the emergence of many deep-learning-specialized acceleratorsthat are designed as a distributed system with shared hierarchical memory. On the software side, compilers
must take into account this complexity and ensure that the generated assembly program is correct. In
this paper, we tackle the problem of verifying memory accesses or data transfers in an assembly program
generated by our deep learning compiler, and report some preliminary results. Given an assembly program
generated by the compiler from a source program, and a correct assembly simulator, we first run the simulator to simulate the execution of the assembly program in order to generate a sequence of data transfers.
We then verify the sequence of data transfers against a correct sequence that is generated directly from thesource program. We propose a novel data structure, called address tensor, that can capture both informationof input data from the source program and addresses in the assembly program. Address tensors are very
convenient to correctly generate a sequence of data transfers from the source program.They are also flexible
enough to adapt to new data transfer strategies in the compiler. Our verification has been using during thedevelopment of the compiler, which helps us quickly find bugs and validate generated assembly programs.

signed for deep learning but high performance com-

1 Introduction

puting in general. This leads to the emergence ofDeep learning has been emerging as an eﬃcientmany deep-learning-specialized accelerators such as

tool for solving many important problems in com-

TPU [4], RAPID AI accelerator [2]. Such accelera-

puter vision, speech recognition, and natural lan-tors have much better performance with low power

guage processing. It has been applied to traditional

consumption.

fields like software engineering as well as program-

Deep learning accelerators often have thousands

ming languages. The recent succeed of deep learn-of small dedicated compute units with software-

ing mainly comes from two things: a lot of labeledcontrolled shared hierarchical memory, which helps

data and a lot of convenient compute power suchdata move around the units in the fastest way andas GPUs. Thought GPUs are very fast for training

helps maximize parallelism. Though such a hard-

deep neural networks, they were not originally de-ware design significantly accelerates deep learning∗ Verification of memory access for deep learning com-

applications, its flexibility in memory management

pilers.
This is an unrefereed paper. Copyrights belong to
the Author(s).
Tung D. Le, Eri Ogawa, Hiroshi Inoue, Kazuaki
Ishizaki, Moriyoshi Ohara, IBM 東京基礎研究所, IBM
Research, Tokyo.
Swagath Venkataramani, IBM TJ Watson ResearchCenter, Yorktown Heights, NY.

by software makes a burden of software stack, especially, a compiler, taking care of all data transfers among many units, e.g. how to partition data
among units, when to transfer and where to sendor store the data to. It is often the case that small
units has limited capacity such instruction sets, andthe compiler needs to do a lot of optimizations,which causes diﬃculty in verifying that the compiler correctly generated all of the data transfers.
In this paper we tackle the problem of verifying
memory accesses or data transfers generated by acompiler in DEEPTOOLS [8]—a software stack for
RAPID AI accelerator [2]. In particular, we propose a method to verify correctness of the orderof chunks of data transferred among memory levelsin the accelerator, under a consumption that theAI accelerator’s hierarchical memory is softwarecontrolled.

We propose a novel data structure,

called address tensor, that can capture both information of input data from a source program of
the compiler and addresses in a generated assembly code. Address tensors are very convenient to

図1

Architecture of the RAPID AI

generate a correct sequence of data transfers fromAccelerator

the source program. They are also flexible enoughto adapt to new data transfer strategies in the

Input program

compiler. Our verification has been using during
the development of the compiler, which helps us

DL framework(e.g. TensorFlow)quickly find bugs and validate generated assembly
programs.
The rest of the paper is organized as follows: Sec-

Hardwareconfigtion 2 gives an overview of the target compiler as

Schedulerwell as the software stack and RAPID AI accelerRAPIDDSC

ator. Section 3 describes our verification method,
how it is positioned in the software stack. It also
describes the design of address tensor in detail, andComputation
kernelssome preliminary results. Section 4 concludes theCompiler

Assembly code

paper and discusses future works.

2 Target Compiler

Simulator

This section presents the overview of a compiler [6] for RAPID AI accelerator developed by

図2

DEEPTOOLS Software Stack

IBM Research [2]. Before discussing the compiler,
we quickly give an overview of the architecture of

2. 1 Hardware and Software Architecture

the RAPID AI accelerator and the DEEPTOOLS

2. 1. 1 Hardware Architecture

software stack [8] in which compiler is one of its

The RAPID AI accelerator [2], being developed

components.

by IBM Research, consists of an array of processing

RAPID AI accelerator [8].

Computation
kernels

RAPIDDSC

We use the existing

deep learning framework TensorFlow [1] as a front
end. Users write their program, e.g. a deep neu-

IR generation functions foreach operation categories- ElementWiseActFn- Pooling- Conv- …

IR classes- Loop- Kernel block- Reg update- …

ral network, in TensorFlow. TensorFlow then automatically generates a computational graph thatis passed to a scheduler. The scheduler takes thecomputational graph generated by TensorFlow and

Loop
IRs

KernelBlock

Optimizations- Pre-loading- Double buffering- Dead-code
elimination- …

the hardware parameters (e.g. the number of cores)
as its input, and computes a mapping of the neuralnetwork onto the hardware architecture. In particular, it partitions the computations among thecompute units and splits the data into multiple

Assemblycode

stages to be transferred to each level of the memory hierarchy. As a result, for each operator, there

図3

Compiler Overview

is a mapping, called RAPIDDSC, representing how
data are split and transferred to each level of theunits (PEs) connected via nearest-neighbor FIFO

memory hierarchy. The compiler finally generates

links, an added row of special-function units (SFUs)

optimized assembly code by using the RAPIDDSC

and a 2-level scratchpad memory as shown in Fig. 1.

and an annotated computation kernel for each op-

The 8KB level-0 (L0) scratchpad is attached toerator (Sec. 2. 2). The assembly code can be run

both array dimensions, and connects to the 2MB

on an actual acceleration core or on a simulator.

next-level (Lx) scratpad. Each scratchpad has apair of control units, i.e. a load unit (LU) and2. 2 Compiler

a store unit (SU). Data enters and leaves compute

Figure 3 shows the overview of our compiler. The

units (PEs and SFUs) through connections between

compiler takes a RAPIDDSC and a computation

the L0s and Lx scratchpads. All data transfers are

kernel as inputs, and produces an assembly code

software controlled, and the compiler must deter-

for the accelerator.

mine the load/store address for each data transfer

Each operator, e.g.

convolutional or fully-

instruction. All units have a carefully curated in-connected layer, is associated with a RAPIDDSC

struction set, a capacity-limited instruction buﬀer

and a computation kernel template.

and a program counter, which is to achieve high-

RAPIDDSC captures the spatial partitioning of theperformance and energy-eﬃcient deep learning pro-

operator across the cores, loop ordering to com-cessing. At a higher level, one processor chip con-plete the operator and data transfers through eachsists of many cores that share an external device

unit [7].

Thememory. The device memory controller (DMC) in

In a RAPIDDSC, computation of an operator

a core is used to transfer data between the core’s

is described by using a 5-tuple N(in,out,ij,mb,kij)

Lx scratchpad and the device memory.

(Fig. 4), where 1) Nin is the number of input fea-

2. 1. 2 DEEPTOOLS Software Stacktures, 2) Nout is the number of output features,

Figure 2 shows a simplified view of the3) Nij is the dimensions of each feature, 4) Nmb is

DEEPTOOLS software stack developed for thethe number of mini-batch inputs, and 5) Nkij is the

Nin
Nin

Nout

Ni
Nj

Ni

Nout
Ni

..
.
Nj

Nj

図4

Data Layout for Input (left), Kernel (middle), and Output (right)

Workload
Input: N(in, out, ij, mb, kij)
Core: D(in, out, ij, mb, kij)
Lx: B(in, out, ij, mb, kij)
L0: T(in, out, ij, mb, kij)
Main loop: ["tpij", "tpmb", "tpkij", "tpin", "tpout", "btij", "btmb", "btkij","btout", "btin", "dbmb", "dbkij", "dbout", "dbin", "dbij"]
Data transfer locations:
Data size

Source starting address

Destination starting address

dInp dbkij

Location

384

128

0

dKer btin

9

512

1024

Dimension layout order:
Inp: [“ij”, “mb”, “in”]
Ker: [“ij”, “in”, “out”]
図5

Example of a RAPIDDSC for an operator

dimensions of each kernel. The parameter Nij isis [”ij”, ”mb”, ”in”], where the first item in the list

actually the product of two dimensions Ni and Nj .

indicates the innermost partition that is stored in

So is Nkij . From these parameters we can infer size

memory.

of input, output or kernel data structure, in which,

The scheduler partitions the computation to each

input feature size, Inp, is Nin ∗ Nij ∗ Nmb output

core, i.e. D(in,out,ij,kij,mb) work allocated to eachfeature size, Out, is Nout ∗ Nij ∗ Nmb , and kernel

core, B(in,out,ij,kij,mb) data blocks reused from Lx,

size, Ker, is Nin ∗ Nout ∗ Nkij . Each data structure

T(in,out,ij,kij,mb) data tiles reused from L0, and coreis associated with a layout dimension order that

P(in,out,ij,kij,mb) quantum of work fed to processing

indicates how the data are stored in memory. A

elements (PEs). It needs to explore a huge space ofdimension layout order is represented by a list ofpartitioning in order to find the best data partition

dimensions, e.g. a layout dimension order for input

strategy.

loop of data transfer and computation.
for _ in 1 to Din/Binfor _ in 1 to Dout/BoutdInp
for _ in 1 to Dij/Bij
for _ in 1 to Dkij/Bkij
dKer
for _ in 1 to Dmb/Bmb
bKer
for _ in 1 to Bin/Tin
for _ in 1 to Bout/Tout
dOut, bOut
for _ in 1 to Bkij/Tkij
for _ in 1 to Bij/TijbInp
for _ in 1 to Bmb/TmbtKer, pKer, tOut
for _ in 1 to Tout/Pout
for _ in 1 to Tin/Pin
tInp
for _ in 1 to Tkij/Pkij
for _ in 1 to Tmb/Pmbfor _ in 1 to Tij/Pij
pInp, pOut
computation

Note that, for each partition, we may send thewhole partition at once, or divide the partition
again into chunks and send chunks one-by-one,
depending on the data transfer location for thedata structure. For example, let’s consider a datatransfer location, dOut in Fig. 6 that is for output
Dij ∗ Dmb ∗ Dout , from device memory to Lx, andconsider the dimension out of the output. SincedOut is inside the loops dbout and btout , we donot send the whole partition of the output in device memory but we will divide the partition into
chunks in which the dimension out of a chunk will
be Dout /dbout /btout . So do the other dimensions.

図6

Main loop of data transfer andcomputation

Figure 5 shows an example of RAPIDDSC for
an operator. We have information about workload
such as input data, data for each core, Lx, and L0.

To complete work for a computation, each core

We have a main loop that is executed at each core,needs to execute a main loop consisting of 15 nested

and data transfer locations. For example, the lo-loop iterations clustered in 3 stages, i.e. (T /B),

cation to transfer input from the external memory(B/T ) and (D/B). The main loop is represented as

device to the core’s Lx scatchpad, dInp , is “btout”

a list of dimensions, e.g. [“tpij”, “tpmb”, “tpkij”,

in the main loop, the size of input data is 384, and“tpin”, “tpout”, “btij”, “btmb”, “btkij”, “btout”,

the input is stored at the address 128 in the external“btin”, “dbmb”, “dbkij”, “dbout”, “dbin”, “dbij”],

memory device and is sent to the address 0 in thewhere their first two characters denote memory

Lx scratchpad. Finally, we have information aboutlevels, e.g.

dimension layout order for each data structure.

“db” means data between the ex-

ternal memory device to Lx scratchpad. In the

The annotated computation kernel of an opera-

main loop list, the first item is the innermost loop

tor represents an operation template for the oper-

while the last item is the outermost loop. Valueator, including the operation category and kernel

for, say, “dbmb” is computed by taking Dmb di-computation instructions for each hardware unit,

vided by Bmb . So are other dimensions’ values.

hand-crafted by top-notch library developers.

It is the number of partitions obtained by split-

Using the kernel instructions and the operationting data along dimension “ij”, also denoting thecategory from the kernel, as well as the RAPIDDSC

number of iterations needed to transfer all of thefrom the scheduler, the compiler automatically gen-partitions. To transfer data of input, output anderates outer loops for the kernel for each computa-

kernel data structures between the diﬀerent mem-tion and data-transfer unit. For the DMC, the com-ory levels, there are 12 parameters indicating lo-

piler generates its code to transfer data between

cations in the main loop to trigger the transfers,

the device memory and the Lx scratchpad. The li-

i.e p(Inp,Out,Ker) , t(Inp,Out,Ker) , b(Inp,Out,Ker) , andbrary developers need to write instructions for alld(Inp,Out,Ker) . Fig. 6 shows an example of a main

computation and data-transfer units except for thedescription in the scheduler’s output. The simulaScheduler

RAPIDDSC

information about each instruction. For verifying

RAPIDDSC
Computation
kernels

tor can execute the whole assembly code and log

data transfer, we extract only traces about data
Compiler

Verification

The most important part in our verification

Assembly code

Simulatortransfer from the simulator’s output.

Data transfer
tracesframework is finding an intermediate representation (IR) that captures important information from

図7

Verification

both a RAPIDDSC and data transfer traces. In
deep learning, it is common to use tensors (multi-

DMC only on one core. The compiler then auto-ple dimension arrays) to represent data. Hence, we

matically generates data transfer code for multiple

also use tensors as an IR. However, in our verifi-

cores by determining the actual address of data forcation framework, values in a tensor are memory

each core.

addresses instead of real values for input, output

3 Verification of Memory Accessand kernel. We call such tensors address tensor

Since the compiler needs to process a huge

(See Sec. 3. 2).

amount of work, e.g. generating code for every unit,transferring chunks of data to every compute and3. 1 Verification Method

memory unit, and optimizing the generated code,

Our purpose is to verify data transfers traced by

it is non-trivial to ensure that the final generated

the simulator, whether chunks of data are trans-

assembly code is correct. A verification tool would

ferred to a memory level in a correct order and tobe helpful for compiler developers to quickly verify

correct address or not. To do so, we utilize ad-

the generated code [3] [5]. On the other hand, thedress tensors to correctly generate a sequence oftool should be flexible enough so that the develop-

data transfers from a RAPIDDSC (output of theers can easily express their intention.

scheduler) (See Sec. 3. 3). Then, we verify the data

In this paper, we propose a method to help verify

transfers traced by the simulator against this se-data transfers generated by the compiler. In par-quence. Since data are split into chunks, it is mean-

ticular, we verify whether data (input, output andingless to verify data transfers one by one. Hence,kernel) are transferred between correct addresses orfor each chunks of data, we generate a set of data

not. One data transfer means sending one datum

transfers.

(e.g. a number) from a memory address to anotherA sequence of data transfers traced by the sim-

memory address. This paper only focuses on verify

ulator is represented by a list of tuples where eachdata transfers from the external memory device totuple represents a data transfer from a source to aeach core, in particular, to the Lx scrathpad of adestination. Let S be the sequence of data transferscore. Verification of data transfers from Lx to L0

traced by the simulator, its type is:or to compute units is left for future work.
Fig. 7 shows how our verification is positioned in
the software stack. It takes the output from thescheduler and the output from the simulator as inputs, and verifies the simulator’s output against the

S :: [(src, dest)]

grouping data transfers in S into sets so that the

where
src

::

(Mem Level, Addr)

dest

::

(Mem Level, Addr)

Mem Level::

Stringsize of one set in S ′ is equal to the size of the corresponding set in T . Grouping is done from the firstto the last element in S, so the size of the last set

Addr :: Integer
where [] denotes a list and () denotes a tuple.
A sequence of data transfers generated from a
RAPIDDSC is represented by a list of sets of tuples,
where each tuple represents a data transfer froma source to a destination. Let T be the sequenceof data transfers generated from a RAPIDDSC, its
type is:(or several last sets) in S ′ might be diﬀerent fromthe corresponding one in T . After that we verify
S ′ against T by comparing sets in S ′ and T one
by one from the first to the last element. For eachcomparison, we use set equality, reporting 1) two
sets are equal or not (data transfers exist in bothsets), and 2) which data transfers in S ′ are missing
in T and vice versa,

T :: [{(src, dest)}]3. 1. 2 Verifying Chunk Order for Each

where {} denotes a set.

Data Structure

We propose two verifications: one is to verify thewhole data transfers chunk by chunk, the other is toverify data transfers for each data structure. The

S :: [(src, dest)]

verifyTI/O/K :: [{(src, dest)}]reason to have the latter verification is that theextract

compiler is able to do optimization for data transfers by doing overlap of data transfers and com-

T :: [{(src, dest)}]putation, in which each chunk is divided into subchunks and a sub-chunk is a triple of sub-chunks for

図9

Verifying chunk order for a data structure

input, output and kernel. Hence, if the former verification reports invalid data transfers, we need thelatter verification to know for which data structure

Figure 9 shows how we verify chunk order for adata structure. We first extract sequences of data

the invalid transfers happened.

transfers for each data structure, i.e. TI for input,

3. 1. 1 Verifying Chunk Order

TO for output, and TK for kernel. Then, we verify
S :: [(src, dest)]

group

S ′ :: [{(src, dest)}]S against each of the sequences.
However, S contains data transfers for all data
structures. Hence, we need an algorithm to verify

verifyonly data transfers of interest. Alg. 1 shows our algorithm to verify S again TI/O/K . The key idea is

T :: [{(src, dest)}]to keep the maximum index in S after each chunkcomparison. We start from the first element in S

図8

Verifying chunk order(Lines 1 and 5). For each chunk i TI/O/K (Lines
2–3), we find the existence of all elements of the

Figure 8 shows how we verify a sequence of datatransfers, S, traced by the simulator against the sequence T . We first create a new list, S ′ , from S bychunk in S starting from max idx (Lines 4–12). If
a data transfer exists, we update max idx to move
forward in S. Otherwise, we report an invalid datatransfer.

5:

if dt ∈ S[max id :] then6:idx ← S.index(dt)7:

if idx > max idx thenmax idx ← idx

8:

end if

9:

0

1

2

3

0

1

2

3

22

23

24

25

1

3

21

0
2

20

1

19

0

18

3

17

2

16

for all dt ∈ chunki do

1

1

15

4:

0
0

14

chunki ← TI/O/K [i]dimension mb
dimension ij

1

13

3:

0

12

2: for i ← 0, |TI/O/K | − 1 dodimension in

11

1: max idx ← 0

10Input: S, TI/O/K

Memory address

図 10

An example of an address tensor withlayout [(“ij”, 4), (“mb”, 2), (“in”, 2)] andstarting memory address 10

else

10:

Invalid11:

representing memory addresses for an input data

12:

end ifstructure that is stored in memory at address 10.

13:

end forTo get the address of an item, say in = 0, mb =14: end for

Algorithm 1: Verify data transfers for a data
structure

1, ij = 2, calling where(2, 1, 0) returns 16.
Actually, we use two diﬀerent dimensions “i” and“j” (or “ki” and “kj”) for “ij” (or “kij”) to precisely
capture the data structures. However, for brevity,

3. 2 Address Tensor
This section describes address tensors and basic

we sometimes use “ij” or “kij” instead in this paper.
3. 2. 1 Basic Operations

operations to work with them. We implemented

Since data are partitioned and passed to computeour verification framework in Python. Hence, we

and memory units, we provides operations for split-

will use Python code to describe our address ten-ting an address tensor into multiple address tensors.

sors.

A simple operation is splitting an address tensor

Address tensor is a wrapper of a normal tensor

along a specific dimension. Given a dimension andin which we change its interface and add some ad-

the number of partitions, the operation will split

ditional operations so that it is more suitable tothe tensor along such dimension into multiple ad-express RAPIDDSC.

dress tensors. Its interface is

To create an address tensor, we pass a layout anda starting memory address to its constructor,
class Tensor () :def __init__ ( self , layout , mem_loc = None ) :...

def split ( self , dim , n_partitions =2)

To split a tensor along multiple dimensions, we
provide operation split n. Its interface isdef split_n ( self , dims , flatten = False )where layout is a list of tuples of dimension andwhere dims is a list of tuples of dimension anditem count, e.g. [(“ij”, 4), (“mb”, 2), (“in”, 2)].

number of partitions, e.g. [(“ij”, 1), (“mb”, 2),

The order of elements in the list follows the layout(“in”, 2)]. This operation will recursively call op-

dimension order in a RAPIDDSC generated by theeration split to split the tensor, starting from thescheduler. An element in a tensor can be accessed

last item in the dimension list dims. It will returnby using operation where(x, y, z, ...), where x, y, z

a nested dictionary of address tensors or a list of

etc. are dimension indices.

address tensors, depending on the value of the ar-

Figure 10 shows an example of an address tensor

gument flatten. The nested dictionary is indexedin the reversed order of dims for convenient use. In

the dimension list loop dims. It will return a nested

most cases, we would like to have a nested dictio-

dictionary of address tensors. The nested dictio-

nary. In cases of biasadd operation and convolution

nary is indexed in the reversed order of loop dims

operation with padding, we will flatten the dictio-

for convenient use in the main loop.

nary and return a list of address tensors instead.
The last basic operation is padding an address
tensor, which is used to present zero-padding for

Let us give an example about split tensor by loop.
Assume that we have an address tensor as the one
in Fig. 10. If we split the tensor by using a list

multiple dimension arrays. However, values used[(“btij”, 2), (“dbmb”, 1), (“dbij”, 1), (“dbin”, 2)],

to pad the address tensor are not zeros but mem-

we will have a nested dictionary of address tensors

ory address. For this operation, we allow users toin which each tensor has layout of

set a value as memory address for padding area[(“ij”, 2), (“mb”, 2), (“in”, 1)].

in the address tensor, depending configurations in

We access these tensors by the indices in the nested

a RAPIDDSC. We will explain this design in de-dictionary, e.g. by using index (0, 0, 0, 1), we gettail when discussing verification of data transfers

the tensor at the first position of “dbin”, first posi-in Sec. 3. 1. The interface of this operation istion of “dbmb”, first position of “dbij” and second

def pad ( self , pad_width , value = -1)

where pad width is a tuple of ((r before, r after),position of “btij”.
Finally,

we provide an operation to split(c before, c after)) containing values to pad to thean address tensor with overlapping,

top/bottom row and leftmost/rightmost column,

split tensor by slicing. This is used in convolutional

value is the value used to pad. This operation sup-operator with padding. The idea is to split a tensor

ports padding along only the two innermost dimen-along one of its dimension into multiple partitions

sions. Hence, values “r” (row) and “c” (column)

by slicing a window along that dimension with aindicates “i” and “j” respectively, or “ki” and “kj”

stride. Its interface isrespectively, depending on whether data is input orkernel.
3. 2. 2 Utility Operations

that isdef s p l i t _ t e n s o r _ b y _ s l i c i n g ( ts , n_slices ,stride =1 , axis = ’r ’ , flatten = False )where ts is the tensor we would like to split,

As is often the case with RAPIDDSC, data aren slices is the number of slices we would like to get,partitioned along multiple dimensions through mul-

stride is the stride to move the window, axis is thetiple loops. Hence, we provide a special split opera-

dimension to split, flatten has the same meaningtion that uses the loop information to partition anas the one in operation split n. This operation sup-address tensor. Its interface isports splitting along only the two innermost dimen-

def s p l i t _ t e n s o r _ b y _ l o o p ( ts , loop_dims )sions. Hence, axis has only two values “r” (row) andwhere ts is the tensor we would like to split,“c” (column). If data is input, “r” and “c” corre-loop dims is a list of tuples of loop dimension andspond to “i” and “j”, respectively. If data is kernel,

number of partitions, e.g.

[(“btij”, 2), (“dbij”,“r” and “c” correspond to “ki” and “kj”, respec-1), (“dbmb”, 2), (“dbin”, 2)]. Note that, dimen-

tively. Actually, slicing over the other dimensions

sions here are loop stages in the main loop in thedoes not make sense.

RAPIDDSC. This operation will recursively call itself to split the input tensor along dimensions suchas “ij”, “mb” or “in”, starting from the last item in

3. 3 Generatinga

SequenceofDataTransfers
This section presents how to generate a sequenceof data transfers from a RAPIDDSC by using address tensors. We take data structure input as example. The other data structures, output and kernel, follows the same method.
Assume that input’s dimension layout order is[“ij”, “mb”, “in”], firstly, we create an address tensor, TSN , for input with layout [(“ij”, Nij ), (“mb”,Nmb ), (“in”, Nin )] and memory location 0.
TSD = TSN = Tensor ([( " ij " , Nij ) ,( " mb " , Nmb ) ,( " in " , Nin ) ] , 0)

TSN is stored in the external memory device andit must be partitioned into multiple tensors for multiple cores. To do so, we just call operation split n
for TSN .

Input: TSiD (address tensor for core i)
Output: T :: [{(src, dest)}]
1: T ← []2: chunk loop ← [(”dbout”, x), (”dbin”, y), (”dbij”, z)]
3: chunk map ←split tensor by chunk(TSiD , chunk loop)// Main loop
4: for dbij ← 0, x − 1 do
5:
for dbin ← 0, y − 1 do
6:
for dbout ← 0, z − 1 do
7:
src c ← chunk map(dbij, dbin, dbout)
8:
dest c ←T ensor(src chunk.layout, dest address)9:seq ← do transf er(src c, dest c)
10:
T ←T+
+ [seq]11:
for dbkij ← 0, w do
12:
...
13:
end for14:
end for15:
end for
16: end for

Algorithm 2: Generating data transfers for input

TSD = TSN . split_n ( dims =[( " ij " , Nij /Dij ) ,( " mb " , Nmb /Dmb ) ,( " in " , Nin /Din ) ])for a core

As a result, we have TSD is a list of address ten-iteration as a source chunk, create a destinationsors for each core. These tensors will be transferredchunk with the same layout at the lower memory

to lower levels in a core such as Lx, L0, PE, whichlevel, transfer the source chunk to the destination

is done by the main loop.

chunk to obtain a set of data transfers, seq, andLet us take the RAPIDDSC in Fig. 5 as exam-

append the set seq to the return list T (Lines 7–9).

ple. Alg. 2 shows how to generate a sequence ofOperation do transf er just takes pairs of elements

data transfers, T , for input from an external mem-of the same index in src c and dest c and createsory device to Lx scratchpath. Before starting thetuples of them, representing a data transfer frommain loop, we need to prepare tensors for trans-

one memory address in the source memory device

ferring. For each location, we know the outer loop

to one memory address in the destination memory(the chunk loop) by looking at the location in thedevice.

main loop. In this example, location is “dbkij”, so

The algorithm 2 can be extended naturally

the chunk loop according to the main loop mustto support pre-loading, double-buﬀering and sub-be [(“dbout”, x), (“dbin”, y), (“dbij”, z)] (Linechunk transfers, which are optimization techniques2), where x, y, z are the number of iterations forin the compiler, by splitting a chunk (Line 7) again

each loop calculated by taking Dout/in/ij divided

into sub-chunks and transferring the sub-chunks at

by Bout/in/ij , respectively. Using the chunk loop

a sub-chunk location that should be calculated in

we split the address tensor for this core i,

TSiD ,

advance.

into multiple tensors to transfer them to the lower
memory level (Line 3). After that, we do the main

3. 4 Preliminary Resultsloop. At the transfer location, e.g. “dbkij”, we

The verification method in this paper has beentake the corresponding chunk based on the current

using during the development of our compiler forcally verify data transfers generated by a compiler,
which helps compiler developers detect and fix bugs
quickly. Our key idea is proposing a data structure, address tensor, that can capture both multidimension information at a high level and address
information at a low level. As shown in the paper,
address tensor with a few operations helped us express the input of the compiler in a succinct way.
It is also flexible enough for us to express diﬀerent
strategies implemented in the compiler.
In this paper, we borrowed a simulator to generate data transfers from a generated assembly code,
where we assumed that the simulator behavior iscorrect. In the future, we would like to directly
generate data transfers from the assembly code ina systematic way such as using an execution graph.
Also, we will extend our method to verify datatransfers at all memory levels in the accelerator.
図 11

Example of verifying BiasAdd operator
in the VGG16 neural modelthe deep learning accelerator core. It can automatically verify all operators in a neural network.
During the development of deep learning operatorsin the compiler, the verification has been helping
us identify bugs such as missing buﬀer switching indouble-buﬀer transfers in BiasAdd operators in the
VGG16 neural model, which is non-trivial to know
if we look at an output from the simulator only
(Fig. 11). Since address tensors used in the verification can capture both information of input data
and addresses, they are very useful for compiler developers to check whether their address calculation
for an operator is correct or not without manuallycalculating them by hand.

4 Conclusion
Developing a compiler for deep-learning-specialized
accelerators is time-consuming and error-prone. In
this paper, we propose a method to automati-

参 考 文 献[1] Abadi, M., Barham, P., Chen, J., Chen, Z., Davis,
A., Dean, J., Devin, M., Ghemawat, S., Irving,G., Isard, M., Kudlur, M., Levenberg, J., Monga,
R., Moore, S., Murray, D. G., Steiner, B., Tucker,
P., Vasudevan, V., Warden, P., Wicke, M., Yu, Y.,
and Zheng, X.: TensorFlow: A System for Largescale Machine Learning, Proceedings of the 12th
USENIX Conference on Operating Systems Design
and Implementation, OSDI’16, Berkeley, CA, USA,USENIX Association, 2016, pp. 265–283.
[2] Fleischer, B., Shukla, S., Ziegler, M., Silberman,
J., Oh, J., Srinivasan, V., Choi, J., Mueller, S.,
Agrawal, A., Babinsky, T., Cao, N., Chen, C.,
Chuang, P., Fox, T., Gristede, G., Guillorn, M.,
Haynie, H., Klaiber, M., Lee, D., Lo, S., Maier,G., Scheuermann, M., Venkataramani, S., Vezyrtzis,C., Wang, N., Yee, F., Zhou, C., Lu, P., Curran,B., Chang, L., and Gopalakrishnan, K.: A Scalable
Multi-TeraOPS Deep Learning Processor Core for
AI Training and Inference, 2018 IEEE Symposium
on VLSI Circuits, June 2018, pp. 35–36.
[3] Fox, A., Myreen, M. O., Tan, Y. K., and Kumar, R.: Verified compilation of CakeML to multiple machine-code targets, Proceedings of the 6th
ACM SIGPLAN Conference on Certified Programs
and Proofs, ACM, 2017, pp. 125–137.
[4] Jouppi, N. P., Young, C., Patil, N., Patterson, D.,
Agrawal, G., Bajwa, R., Bates, S., Bhatia, S., Boden, N., Borchers, A., Boyle, R., Cantin, P.-l., Chao,

C., Clark, C., Coriell, J., Daley, M., Dau, M., Dean,
J., Gelb, B., Ghaemmaghami, T. V., Gottipati, R.,
Gulland, W., Hagmann, R., Ho, C. R., Hogberg, D.,
Hu, J., Hundt, R., Hurt, D., Ibarz, J., Jaﬀey, A., Jaworski, A., Kaplan, A., Khaitan, H., Killebrew, D.,
Koch, A., Kumar, N., Lacy, S., Laudon, J., Law, J.,
Le, D., Leary, C., Liu, Z., Lucke, K., Lundin, A.,
MacKean, G., Maggiore, A., Mahony, M., Miller,
K., Nagarajan, R., Narayanaswami, R., Ni, R.,
Nix, K., Norrie, T., Omernick, M., Penukonda, N.,
Phelps, A., Ross, J., Ross, M., Salek, A., Samadiani,
E., Severn, C., Sizikov, G., Snelham, M., Souter,J., Steinberg, D., Swing, A., Tan, M., Thorson, G.,
Tian, B., Toma, H., Tuttle, E., Vasudevan, V., Walter, R., Wang, W., Wilcox, E., and Yoon, D. H.: InDatacenter Performance Analysis of a Tensor Processing Unit, Proceedings of the 44th Annual International Symposium on Computer Architecture,
ISCA ’17, New York, NY, USA, ACM, 2017, pp. 1–
12.
[5] Myreen, Magnus O and Gordon, Michael JC andSlind, Konrad: Machine-code verification for multiple architectures-an application of decompilation

into logic, 2008 Formal Methods in Computer-Aided
Design, IEEE, 2008, pp. 1–8.
[6] Ogawa, E., Ishizaki, K., Inoue, H., Venkataramani, S., Choi, J., Wang, W., Srinivasan, V.,
Ohara, M., and Gopalakrishnan, K.: A Compiler
for Deep Neural Network Accelerators to Generate
Optimized Code for a Wide Range of Data Parameters from a Hand-crafted Computation Kernel, 2019
IEEE Symposium in Low-Power and High-Speed
Chips (COOL CHIPS), April 2019, pp. 1–3.
[7] Venkataramani, S., Choi, J., Srinivasan, V.,
Gopalakrishnan, K., and Chang, L.: POSTER: Design Space Exploration for Performance Optimization of Deep Neural Networks on Shared Memory
Accelerators, 2017 26th International Conference
on Parallel Architectures and Compilation Techniques (PACT), Sep. 2017, pp. 146–147.
[8] Venkataramani, S., Choi, J., Srinivasan, V.,
Wang, W., Zhang, J., Schaal, M., Serrano, M.,
Ishizaki, K., Inoue, H., Ogawa, E., Ohara, M.,
Chang, L., and k. gopalkrishnan: DeepTools: Compiler and Execution Runtime Extensions for RaPiD
AI Accelerator, IEEE Micro, (2019), pp. 1–1.