Divide-and-Conquer Checkpointing for Arbitrary
Programs with No User Annotation
Jeffrey Mark Siskind, qobi@purdue.edu

NIPS 2017 Workshop on
The Future of Gradient-Based Machine Learning Software & Techniques
Saturday 9 December 2017

Joint work with Barak Avrum Pearlmutter
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

1 / 48

Barak and my WorkSiskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

2 / 48

Barak and my WorkAD in functional programs.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

2 / 48

Barak and my WorkAD in functional programs.
AD is easier in functional programs.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

2 / 48

A Neural Networkx0 ∂∂ xx08
layer0 θ0 w0
x1 ∂∂ xx18
layer1 θ1 w1
x2 ∂∂ xx28
layer2 θ2 w2
x3 ∂∂ xx38
layer3 θ3 w3
x4 ∂∂ xx48
layer4 θ4 w4
x5 ∂∂ xx58
layer5 θ5 w5
x6 ∂∂ xx68
layer6 θ6 w6
x7 ∂∂ xx78
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

3 / 48

A Neural Network is a (Functional) Programx0 ∂∂ xx08
layer0 θ0 w0
x1 ∂∂ xx18
layer1 θ1 w1
x2 ∂∂ xx28
layer2 θ2 w2
x3 ∂∂ xx38
layer3 θ3 w3
x4 ∂∂ xx48
layer4 θ4 w4
x5 ∂∂ xx58
layer5 θ5 w5
x6 ∂∂ xx68
layer6 θ6 w6
x7 ∂∂ xx78
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)△

net [θ0 , . . . , θ7 ] [w0 , . . . , w7 ] x0 =let x1 = layer0 θ0 w0 x0
x2 = layer1 θ1 w1 x1
x3 = layer2 θ2 w2 x2
x4 = layer3 θ3 w3 x3
x5 = layer4 θ4 w4 x4
x6 = layer5 θ5 w5 x5x7 = layer6 θ6 w6 x6
x8 = layer7 θ7 w7 x7
in x8

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

3 / 48A (Functional) Program△

f [w0 , w1 ] [x0 , x1 ] =let t0 = w0 × x0
t1 = w1 × x1
y = t0 + t1
in y

w0

x0

w1

×

x1
×

t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

4 / 48A (Functional) Program is a (Neural) Network△

f [w0 , w1 ] [x0 , x1 ] =let t0 = w0 × x0
t1 = w1 × x1
y = t0 + t1
in y

w0

x0

w1

×

x1
×

t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

4 / 48A (Functional) Program is a (Neural) Network△

f [w0 , w1 ] [x0 , x1 ] =let t0 = w0 × x0
t1 = w1 × x1
y = t0 + t1
in y

w0

w1

x0

x1
×

×
t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

4 / 48A (Functional) Program is a (Neural) Network△

f [w0 , w1 ] [x0 , x1 ] =let t0 = w0 × x0
t1 = w1 × x1
y = t0 + t1
in y

w0

x0

w1

×

x1
×

t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

4 / 48A (Functional) Program is a (Neural) Network△

f [w0 , w1 ] [x0 , x1 ] =let t0 = w0 × x0
t1 = w1 × x1
y = t0 + t1
in y

w0

x0

x1

w1

×

×
t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

4 / 48A (Functional) Program is a (Neural) Network△

f [w0 , w1 ] [x0 , x1 ] =let t0 = w0 × x0
t1 = w1 × x1
y = t0 + t1
in y

w0

x0

x1

w1

×

×
t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

4 / 48

Some Observations

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

5 / 48

Some Observations▸ Deep learning network ‘frameworks’ are domain specific (functional)

programming languages.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

5 / 48

Some Observations▸ Deep learning network ‘frameworks’ are domain specific (functional)

programming languages.
▸ A deep neural network is a long running (functional) program.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

5 / 48

Some Observations▸ Deep learning network ‘frameworks’ are domain specific (functional)

programming languages.
▸ A deep neural network is a long running (functional) program.
▸ Can perform backpropagation on (functional) programs

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

5 / 48

Some Observations▸ Deep learning network ‘frameworks’ are domain specific (functional)

programming languages.
▸ A deep neural network is a long running (functional) program.
▸ Can perform backpropagation on (functional) programsby having an execution of the program generate a network.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

5 / 48

Some Observations▸ Deep learning network ‘frameworks’ are domain specific (functional)

programming languages.
▸ A deep neural network is a long running (functional) program.
▸ Can perform backpropagation on (functional) programsby having an execution of the program generate a network.
This is called reverse-mode automatic differentiation (AD).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

5 / 48A (Brief) History of Backpropagation aka Reverse-Mode AD

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

6 / 48A (Brief) History of Backpropagation aka Reverse-Mode AD
D.E. Rumelhart, G.E. Hinton, and R.J. Williams, Learning representations byback-propagating errors, Nature, 323:533–536, 1986.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

6 / 48A (Brief) History of Backpropagation aka Reverse-Mode AD
D.E. Rumelhart, G.E. Hinton, and R.J. Williams, Learning representations byback-propagating errors, Nature, 323:533–536, 1986.
B. Speelpenning, Compiling Fast Partial Derivatives of Functions Given by
Algorithms, Department of Computer Science, University of Illinois at
Urbana-Champaign, 1980.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

6 / 48A (Brief) History of Backpropagation aka Reverse-Mode AD
D.E. Rumelhart, G.E. Hinton, and R.J. Williams, Learning representations byback-propagating errors, Nature, 323:533–536, 1986.
B. Speelpenning, Compiling Fast Partial Derivatives of Functions Given by
Algorithms, Department of Computer Science, University of Illinois at
Urbana-Champaign, 1980.
P.J. Werbos, Beyond Regression: New Tools for Prediction and Analysis in the
Behavioral Sciences, Harvard University, 1974.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

6 / 48A (Brief) History of Backpropagation aka Reverse-Mode AD
D.E. Rumelhart, G.E. Hinton, and R.J. Williams, Learning representations byback-propagating errors, Nature, 323:533–536, 1986.
B. Speelpenning, Compiling Fast Partial Derivatives of Functions Given by
Algorithms, Department of Computer Science, University of Illinois at
Urbana-Champaign, 1980.
P.J. Werbos, Beyond Regression: New Tools for Prediction and Analysis in the
Behavioral Sciences, Harvard University, 1974.
G.M. Ostrovskii, Y.M. Volin, and W.W. Borisov, Über die Berechnung vonAbleitungen, Wissenschaftliche Zeitschrift der Technischen Hochschule für
Chemie, Leuna-Merseburg, 13(4):382–384, 1971.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

6 / 48A (Brief) History of Backpropagation aka Reverse-Mode AD
D.E. Rumelhart, G.E. Hinton, and R.J. Williams, Learning representations byback-propagating errors, Nature, 323:533–536, 1986.
B. Speelpenning, Compiling Fast Partial Derivatives of Functions Given by
Algorithms, Department of Computer Science, University of Illinois at
Urbana-Champaign, 1980.
P.J. Werbos, Beyond Regression: New Tools for Prediction and Analysis in the
Behavioral Sciences, Harvard University, 1974.
G.M. Ostrovskii, Y.M. Volin, and W.W. Borisov, Über die Berechnung vonAbleitungen, Wissenschaftliche Zeitschrift der Technischen Hochschule für
Chemie, Leuna-Merseburg, 13(4):382–384, 1971.
S. Linnainmaa, The representation of the cumulative rounding error of analgorithm as a Taylor expansion of the local rounding errors (in Finnish),Department of Computer Science, University of Helsinki, 1970.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

6 / 48A (Brief) History of Backpropagation aka Reverse-Mode AD
D.E. Rumelhart, G.E. Hinton, and R.J. Williams, Learning representations byback-propagating errors, Nature, 323:533–536, 1986.
B. Speelpenning, Compiling Fast Partial Derivatives of Functions Given by
Algorithms, Department of Computer Science, University of Illinois at
Urbana-Champaign, 1980.
P.J. Werbos, Beyond Regression: New Tools for Prediction and Analysis in the
Behavioral Sciences, Harvard University, 1974.
G.M. Ostrovskii, Y.M. Volin, and W.W. Borisov, Über die Berechnung vonAbleitungen, Wissenschaftliche Zeitschrift der Technischen Hochschule für
Chemie, Leuna-Merseburg, 13(4):382–384, 1971.
S. Linnainmaa, The representation of the cumulative rounding error of analgorithm as a Taylor expansion of the local rounding errors (in Finnish),Department of Computer Science, University of Helsinki, 1970.
A.E. Bryson, Jr. and Y.-C. Ho, Applied optimal control, Blaisdell, 1969.
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

6 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Neural Networkx0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

7 / 48

Evaluating a Network

w0

x0

w1

×

x1
×

t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

8 / 48

Evaluating a Network

w0

x0

w1

×

x1
×

t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

8 / 48

Evaluating a Network

w0

x0

w1

×

x1
×

t1

t0
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

8 / 48

Evaluating a Network

w0

x0

w1

×

x1
×

t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

8 / 48

Evaluating a Network

w0

x0

x1

w1

×

×
t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

8 / 48

Evaluating a Network

w0

x0

x1

w1

×

×
t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

8 / 48

Evaluating a Network

w0

x0

x1

w1

×

×
t0

t1
+

y

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

8 / 48

Some Observations

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

9 / 48

Some Observations▸ Only need to store live variables.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

9 / 48

Some Observations▸ Only need to store live variables.
▸ Most deep learning frameworks store all intermediate variables to allow

subsequent backpropagation.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

9 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Evaluating a Neural Network to Allow Subsequent Backpropagation
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201610 / 48

Some Observations

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201611 / 48

Some Observations▸ Only need to store live variables from forward pass until they are used inreverse pass.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201611 / 48

Some Observations▸ Only need to store live variables from forward pass until they are used inreverse pass.
▸ Only need to store live variables during reverse pass.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201611 / 48

Some Observations▸ Only need to store live variables from forward pass until they are used inreverse pass.
▸ Only need to store live variables during reverse pass.
▸ Most deep learning frameworks store all intermediate forward andreverse pass variables for simplicity of implementation.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201611 / 48

Some Observations▸ Only need to store live variables from forward pass until they are used inreverse pass.
▸ Only need to store live variables during reverse pass.
▸ Most deep learning frameworks store all intermediate forward andreverse pass variables for simplicity of implementation.
▸ It doesn’t matter because storage use is dominated by maximal use.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201611 / 48

Some Observations▸ Only need to store live variables from forward pass until they are used inreverse pass.
▸ Only need to store live variables during reverse pass.
▸ Most deep learning frameworks store all intermediate forward andreverse pass variables for simplicity of implementation.
▸ It doesn’t matter because storage use is dominated by maximal use.
▸ Maximal use is proportional to the depth of the network i.e., the running

time of the program.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201611 / 48

Complexity of Reverse-Mode AD

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201612 / 48

Complexity of Reverse-Mode AD▸ If running time of primal is O(t)Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201612 / 48

Complexity of Reverse-Mode AD▸ If running time of primal is O(t)and primal has maximal live storage O(w)Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201612 / 48

Complexity of Reverse-Mode AD▸ If running time of primal is O(t)and primal has maximal live storage O(w)▸ then reverse mode takes O(wt) space

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201612 / 48

Complexity of Reverse-Mode AD▸ If running time of primal is O(t)and primal has maximal live storage O(w)▸ then reverse mode takes O(wt) spaceand O(t) time.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201612 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Backpropagation in a Neural Network with Checkpointing
x0 ∂∂ xx80
layer0 θ0 w0
x1 ∂∂ xx81
layer1 θ1 w1
x2 ∂∂ xx82
layer2 θ2 w2
x3 ∂∂ xx83
layer3 θ3 w3
x4 ∂∂ xx84
layer4 θ4 w4
x5 ∂∂ xx85
layer5 θ5 w5
x6 ∂∂ xx86
layer6 θ6 w6
x7 ∂∂ xx87
layer7 θ7 w7
x8 ∂∂ xx88
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201613 / 48

Checkpointing

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Checkpointing▸ Trades off extra running time for reduction in space.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Checkpointing▸ Trades off extra running time for reduction in space.
▸ Forward pass of first half performed twice.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Checkpointing▸ Trades off extra running time for reduction in space.
▸ Forward pass of first half performed twice.

Once without saving intermediate variables.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Checkpointing▸ Trades off extra running time for reduction in space.
▸ Forward pass of first half performed twice.

Once without saving intermediate variables.
Once with saving intermediate variables.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Checkpointing▸ Trades off extra running time for reduction in space.
▸ Forward pass of first half performed twice.

Once without saving intermediate variables.
Once with saving intermediate variables.
▸ Backpropagation done in stages.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Checkpointing▸ Trades off extra running time for reduction in space.
▸ Forward pass of first half performed twice.

Once without saving intermediate variables.
Once with saving intermediate variables.
▸ Backpropagation done in stages.

Interleaved with (re)running forward pass.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Checkpointing▸ Trades off extra running time for reduction in space.
▸ Forward pass of first half performed twice.

Once without saving intermediate variables.
Once with saving intermediate variables.
▸ Backpropagation done in stages.

Interleaved with (re)running forward pass.
Only need saved intermediate variables from forward pass for current
stage.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Checkpointing▸ Trades off extra running time for reduction in space.
▸ Forward pass of first half performed twice.

Once without saving intermediate variables.
Once with saving intermediate variables.
▸ Backpropagation done in stages.

Interleaved with (re)running forward pass.
Only need saved intermediate variables from forward pass for current
stage.
▸ Can perform divide-and-conquer.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201614 / 48

Divide-and-Conquer CheckpointinguSiskind (Purdue)

p0

p1

p2

Checkpointing for Arbitrary Programs

p3

v

NIPS 2017 WS 9 December 201615 / 48

Divide-and-Conquer CheckpointinguSiskind (Purdue)

p0

p1

p2

Checkpointing for Arbitrary Programs

p3

v

NIPS 2017 WS 9 December 201615 / 48

Divide-and-Conquer CheckpointinguSiskind (Purdue)p

Checkpointing for Arbitrary Programsv

NIPS 2017 WS 9 December 201615 / 48

Divide-and-Conquer CheckpointinguSiskind (Purdue)

p0

p1

p2

Checkpointing for Arbitrary Programsv

NIPS 2017 WS 9 December 201615 / 48

Divide-and-Conquer CheckpointinguSiskind (Purdue)

p0

p1

p2

p3

p4

p5

p6

Checkpointing for Arbitrary Programsv

NIPS 2017 WS 9 December 201615 / 48

Complexity of Divide-and-Conquer Checkpointing

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201616 / 48

Complexity of Divide-and-Conquer Checkpointing▸ If running time of primal is O(t)Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201616 / 48

Complexity of Divide-and-Conquer Checkpointing▸ If running time of primal is O(t)and primal has maximal live storage O(w)Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201616 / 48

Complexity of Divide-and-Conquer Checkpointing▸ If running time of primal is O(t)and primal has maximal live storage O(w)▸ then reverse mode takes O(w log t) space

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201616 / 48

Complexity of Divide-and-Conquer Checkpointing▸ If running time of primal is O(t)and primal has maximal live storage O(w)▸ then reverse mode takes O(w log t) spaceand O(t log t) time.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201616 / 48

A (Brief) History of Divide-and-Conquer Checkpointing

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201617 / 48

A (Brief) History of Divide-and-Conquer Checkpointing

T. Chen, B. Xu, Z. Zhang, and C. Guestrin, Training deep nets with sublinear
memory cost, arXiv 1604.06174, 2016.
A. Gruslys, R. Munos, I. Danihelka, M. Lanctot, and A. Graves,
Memory-Efficient Backpropagation Through Time, NIPS, 2016.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201617 / 48

A (Brief) History of Divide-and-Conquer Checkpointing

T. Chen, B. Xu, Z. Zhang, and C. Guestrin, Training deep nets with sublinear
memory cost, arXiv 1604.06174, 2016.
A. Gruslys, R. Munos, I. Danihelka, M. Lanctot, and A. Graves,
Memory-Efficient Backpropagation Through Time, NIPS, 2016.
A. Griewank, Achieving Logarithmic Growth of Temporal and Spatial
Complexity in Reverse Automatic Differentiation, Optimization Methods andSoftware, 1:35-54, 1992.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201617 / 48

Implemented for DO Loops

L. Hascoët and V. Pascual, TAPENADE 2.1 User’s Guide, Rapport technique
300, INRIA, 2004.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201618 / 48

Implemented for DO Loops

L. Hascoët and V. Pascual, TAPENADE 2.1 User’s Guide, Rapport technique
300, INRIA, 2004.

10

do 10 i=1, n...
continue

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201618 / 48

Implemented for DO Loops

L. Hascoët and V. Pascual, TAPENADE 2.1 User’s Guide, Rapport technique
300, INRIA, 2004.

10

⎫
⎧
⎪
⎪
c$ad binomial-ckp n+1 30 1
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
do 10 i=1, n⎬ ↝ ⎨do 10 i=1, n
⎪
⎪
...
...
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
continue
10
continue⎭ ⎩Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201618 / 48

Implemented for DO Loops

L. Hascoët and V. Pascual, TAPENADE 2.1 User’s Guide, Rapport technique
300, INRIA, 2004.

10

⎫
⎧
⎪
⎪
c$ad binomial-ckp n+1 30 1
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
do 10 i=1, n⎬ ↝ ⎨do 10 i=1, n
⎪
⎪
...
...
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
continue
10
continue⎭ ⎩https://www-sop.inria.fr/tropics/tapenade/faq.html
Assuming that the final number of iterations N is known, andassuming that each iteration has the same runtime cost,

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201618 / 48

Desiderata

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201619 / 48

Desiderata

A (deep) neural network has no loops (except inside primitives).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201619 / 48

Desiderata

A (deep) neural network has no loops (except inside primitives).
Want to implement for arbitrary code (not just a single DO loop).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201619 / 48

program point

Execution Trace of Loop

0

6

12

18

24

30

36

42

47

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Loop

program point

Easy to make regular and uniform checkpoints

24
time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Loop

program point

Easy to make regular and uniform checkpoints

24

36

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Loop

program point

Easy to make regular and uniform checkpoints

24

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Loop

program point

Easy to make regular and uniform checkpoints

24

30

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Loop

program point

Easy to make regular and uniform checkpoints

12

24

30

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Loop

program point

Easy to make regular and uniform checkpoints

12

18

24

30

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Loop

program point

Easy to make regular and uniform checkpoints

6

12

18

24

30

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

program point

Execution Trace of Arbitrary Code

0

6

12

18

24

30

36

42

47

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Arbitrary Codeprogram point

Difficult to make regular and uniform checkpoints

24
time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Arbitrary Codeprogram point

Difficult to make regular and uniform checkpoints

24

36

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Arbitrary Codeprogram point

Difficult to make regular and uniform checkpoints

24

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Arbitrary Codeprogram point

Difficult to make regular and uniform checkpoints

24

30

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Arbitrary Codeprogram point

Difficult to make regular and uniform checkpoints

12

24

30

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Arbitrary Codeprogram point

Difficult to make regular and uniform checkpoints

12

18

24

30

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Execution Trace of Arbitrary Codeprogram point

Difficult to make regular and uniform checkpoints

6

12

18

24

30

36

42

time

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

20 / 48

Key Challenges

Need to interleave generation of the network with forward and backward
passes through the network.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

21 / 48

Key Challenges

Need to interleave generation of the network with forward and backward
passes through the network.
Portions of the network need to be (re)generated, and (re)evaluated withforward and backward passes, multiple times and out of order.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

21 / 48

Key Idea

function main(w)local x = f(w)local y = h(g(x))
local z = p(y)return z
end

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201622 / 48

Key Idea⎧⎪
function main(w)
⎪
⎪
⎪
⎪
⎪
for i = 1, 5
⎪
⎪
⎪
⎪
⎪
if i==1 then
⎪
⎪
⎪
⎪
⎪
local x = f(w)
⎪
⎪
⎪
⎫
⎪
⎪
⎪
function main(w)elseifi==2 then
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
local x = f(w)local
t = g(x)
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
local y = h(g(x))⎬ ↝ ⎨elseif i==3 then⎪⎪local z = p(y)local y = h(t)
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
return z
elseif i==4 then
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
⎪
end
local z = p(y)
⎪
⎭ ⎪
⎪
⎪
⎪
⎪
elseifi==5 then⎪⎪⎪⎪⎪return z
⎪
⎪
⎪
⎪
⎪
end
⎪
⎪
⎪
⎪
⎪
⎩end
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201622 / 48

Core Languagee ∶∶= c ∣ x ∣ λx.e ∣ e1 e2 ∣ if e1 then e2 else e3 ∣ ◇e ∣ e1 ● e2

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201623 / 48

Adding AD Operators to the Core Language←ÐJ ∶ f x ỳ ↦ (y, x̀)Siskind (Purdue)✓

J ∶ f x ỳ ↦ (y, x̀)Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201624 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:

h○g=f
z=gx
✓

(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 0)(step 1)(step 2)(step 3)(step 4)NIPS 2017 WS 9 December 201625 / 48

What is Needed to Implement the Algorithm?

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

26 / 48

What is Needed to Implement the Algorithm?

1

measure the length of the primal computation

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

26 / 48

What is Needed to Implement the Algorithm?

1

measure the length of the primal computation

2

interrupt the primal computation at a portion of the measured length

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

26 / 48

What is Needed to Implement the Algorithm?

1

measure the length of the primal computation

2

interrupt the primal computation at a portion of the measured length3

save the state of the interrupted computation as a capsule

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

26 / 48

What is Needed to Implement the Algorithm?

1

measure the length of the primal computation

2

interrupt the primal computation at a portion of the measured length3

save the state of the interrupted computation as a capsule4

resume an interrupted computation from a capsule

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

26 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

General-Purpose Interruption and Resumption Interface

PRIMOPS f x ↦ lReturn the number l of evaluation steps needed tocompute y = f (x).

INTERRUPT f x l ↦ z

Run the first l steps of the computation of f (x) andreturn a capsule z.

RESUME z ↦ y

If z = (INTERRUPT f x l), return y = f (x).

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201627 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:h○g = fz=gx

(step 1)(step 2)✓(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 3)(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:h○g = fz=gx

(step 1)(step 2)✓(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 3)(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:h○g = fz=gx

(step 1)(step 2)✓(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 3)(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ

(step 0)l = PRIMOPS f x
z=gx(step 1)(step 2)

inductive case:✓(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 3)(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ

(step 0)l = PRIMOPS f x
z=gx(step 1)(step 2)

inductive case:✓(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 3)(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ

(step 0)l = PRIMOPS f x
z=gx(step 1)(step 2)

inductive case:✓(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 3)(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:l = PRIMOPS f x
z = INTERRUPT f x ⌊ 2l ⌋(step 1)(step 2)(y,z̀) = J h z ỳ

(step 3)✓✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:l = PRIMOPS f x
z = INTERRUPT f x ⌊ 2l ⌋(step 1)(step 2)(y,z̀) = J h z ỳ

(step 3)✓✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:l = PRIMOPS f x
z = INTERRUPT f x ⌊ 2l ⌋(step 1)(step 2)(y,z̀) = J h z ỳ

(step 3)✓✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:l = PRIMOPS f x
z = INTERRUPT f x ⌊ 2l ⌋(step 1)(step 2)(y,z̀) = J (λz.RESUME z) z ỳ

(step 3)✓✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:l = PRIMOPS f x
z = INTERRUPT f x ⌊ 2l ⌋(step 1)(step 2)(y,z̀) = J (λz.RESUME z) z ỳ

(step 3)✓✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:l = PRIMOPS f x
z = INTERRUPT f x ⌊ 2l ⌋(step 1)(step 2)(y,z̀) = J (λz.RESUME z) z ỳ

(step 3)✓✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 4)NIPS 2017 WS 9 December 201628 / 48

Algorithm for Divide-and-Conquer Checkpointing
via General-Purpose Interruption and Resumption Interface✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:(step 0)l = PRIMOPS f x
z = INTERRUPT f x ⌊ 2l ⌋(step 1)(step 2)(y,z̀) = J (λz.RESUME z) z ỳ

(step 3)✓✓(z, x̀) = J (λx.INTERRUPT f x ⌊ 2l ⌋) x z̀Siskind (Purdue)

Checkpointing for Arbitrary Programs(step 4)NIPS 2017 WS 9 December 201628 / 48

Example of CPS Conversion⎧⎪⎪
function f(c, x)
⎪
⎪
⎪
⎪
⎪
return g(function(t1)
⎪
⎪
⎪
⎪
⎪
return h(function(t2)
⎪
⎪
⎪
⎫
⎪
⎪
⎪
return p(function(t3)⎪function f(x)
⎪
⎪
⎪ ⎪
⎪
return q(c, t3)↝⎨
return q(p(g(x), h(x)))⎬
⎪
⎪
⎪
⎪
⎪
⎪
end, t1, t2)
⎪
⎪
end
⎭ ⎪
⎪
⎪
⎪
end, x)⎪⎪⎪⎪⎪end, x)
⎪
⎪
⎪
⎪
⎪
end
⎪
⎪
⎩

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201629 / 48

Implementation

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201630 / 48

Implementation

1

Convert source program to CPS.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201630 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201630 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

3

Translate CPS to C.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201630 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

3

Translate CPS to C.

4

Combine with general-purpose interruption and resumption interface and✓J written in C.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201630 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

3

Translate CPS to C.

4

Combine with general-purpose interruption and resumption interface and✓J written in C.

5

Compile to machine code.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201630 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

3

Translate CPS to C.

4

Combine with general-purpose interruption and resumption interface and✓J written in C.

5

Compile to machine code.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201631 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

CPS Conversion as a Program Transformation

2x∣k7 ↝ k x
2(λx.e)∣k7 ↝ k (λk′ x.2e∣k′7)
2(e1 e2)∣k7 ↝ 2e1∣(λx1.2e2∣(λx2.(x1 k x2))7)7e0 ↝ 2e0∣(λx.x)7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201632 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

3

Translate CPS to C.

4

Combine with general-purpose interruption and resumption interface and✓J written in C.

5

Compile to machine code.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201633 / 48

Treading Step Counts and Limits in CPS Conversion

2x∣k

7↝ k

x

2(λx.e)∣k

7↝ k

(λk

2(e1 e2 )∣k

7 ↝ 2e1 ∣(λSiskind (Purdue)x1 .
2e2 ∣(λx.2e∣k

x2 .
(x1 k
7),
7

Checkpointing for Arbitrary Programs7)x2 )),NIPS 2017 WS 9 December 201634 / 48

Treading Step Counts and Limits in CPS Conversion

2x∣k

7↝ k

x

2(λx.e)∣k

7↝ k

(λk

2(e1 e2 )∣k

7 ↝ 2e1 ∣(λSiskind (Purdue)x1 .
2e2 ∣(λx.2e∣k

x2 .
(x1 k
7),
7

Checkpointing for Arbitrary Programs7)x2 )),NIPS 2017 WS 9 December 201634 / 48

Treading Step Counts and Limits in CPS Conversion

2x∣k, n 7 ↝ k (n + 1) x2(λx.e)∣k, n 7 ↝ k (n + 1) (λk n x.2e∣k, n 7)2(e1 e2 )∣k, n 7 ↝ 2e1 ∣(λn x1 .
2e2 ∣(λn x2 .
(x1 k n x2 )),n 7),(n + 1) 7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201634 / 48

Treading Step Counts and Limits in CPS Conversion

2x∣k, n, l7 ↝ k (n + 1) l x2(λx.e)∣k, n, l7 ↝ k (n + 1) l (λk n l x.2e∣k, n, l7)2(e1 e2 )∣k, n, l7 ↝ 2e1 ∣(λn l x1 .
2e2 ∣(λn l x2 .
(x1 k n l x2 )),n, l7),(n + 1), l7

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201634 / 48

Treading Step Counts and Limits in CPS Conversion

2x∣k, n, l7 ↝ k (n + 1) l x2(λx.e)∣k, n, l7 ↝ k (n + 1) l (λk n l x.2e∣k, n, l7)2(e1 e2 )∣k, n, l7 ↝ 2e1 ∣(λn l x1 .
2e2 ∣(λn l x2 .
(x1 k n l x2 )),n, l7),(n + 1), l7⟪e⟫k,n,l ↝ if n = l then ⟦k, λk n l .e⟧ else e

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201634 / 48

Treading Step Counts and Limits in CPS Conversion

2x∣k, n, l7 ↝ ⟪k (n + 1) l x⟫k,n,l2(λx.e)∣k, n, l7 ↝ ⟪k (n + 1) l (λk n l x.2e∣k, n, l7)⟫k,n,l2(e1 e2 )∣k, n, l7 ↝ ⟪2e1 ∣(λn l x1 .
2e2 ∣(λn l x2 .
(x1 k n l x2 )),n, l7),(n + 1), l7⟫k,n,l⟪e⟫k,n,l ↝ if n = l then ⟦k, λk n l .e⟧ else e

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201634 / 48

Treading Step Counts and Limits in CPS Conversion

2x∣k, n, l7 ↝ ⟪k (n + 1) l x⟫k,n,l2(λx.e)∣k, n, l7 ↝ ⟪k (n + 1) l (λk n l x.2e∣k, n, l7)⟫k,n,l2(e1 e2 )∣k, n, l7 ↝ ⟪2e1 ∣(λn l x1 .
2e2 ∣(λn l x2 .
(x1 k n l x2 )),n, l7),(n + 1), l7⟫k,n,l⋮⟪e⟫k,n,l ↝ if n = l then ⟦k, λk n l .e⟧ else e

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201634 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201635 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

3

Translate CPS to C.

4

Combine with general-purpose interruption and resumption interface and✓J written in C.

5

Compile to machine code.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201636 / 48

Code Generation

S π () = null constant
S π true = true constantS π false = false constantS π (c1 , c2 ) = cons((S π c1 ), (S π c1 ))SπnS π ‘k’ = continuation
S π ‘n’ = countS π ‘l’ = limit
S π ‘x’ = argument
S π x = as closure(target)->environment[π x]Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201637 / 48

Code Generation
S π (λ3 n l x.e) = ({thing function(thing target,
thing count,thing limit,
thing argument) {return (S (φ e) e);}
thing lambda = (thing)GC malloc(sizeof(struct {enum tag tag;struct {thing (*function)();unsigned n;thing environment[∣φ e∣];}))}set closure(lambda);
as closure(lambda)->function = &function;
as closure(lambda)->n = ∣φ e∣;
as closure(lambda)->environment[0] = S π (φ e)0⋮
as closure(lambda)->environment[∣φ e∣ − 1] = S π (φ e)∣φ e∣−1lambda;})Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201637 / 48

Code Generation
S π (λ4 k n l x.e) = ({thing function(thing target,
thing continuation,
thing count,thing limit,
thing argument) {return (S (φ e) e);}
thing lambda = (thing)GC malloc(sizeof(struct {enum tag tag;struct {thing (*function)();unsigned n;thing environment[∣φ e∣];}))}set closure(lambda);
as closure(lambda)->function = &function;
as closure(lambda)->n = ∣φ e∣;
as closure(lambda)->environment[0] = S π (φ e)0⋮
as closure(lambda)->environment[∣φ e∣ − 1] = S π (φ e)∣φ e∣−1lambda;})Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201637 / 48

Code Generation

S π (e1 e2 e3 e4 ) = continuation apply((S π e1 ),(S π e2 ),(S π e3 ),(S π e4 ))S π (e1 e2 e3 e4 e5 ) = converted apply((S π e1 ),(S π e2 ),(S π e3 ),(S π e4 ),(S π e5 ))S π (if e1 then e2 else e3 ) = (!is false((S π e1 ))?(S π e2 ):(S π e3 ))S π (◇e) = (N ◇)((S π e))
S π (e1 ● e2 ) = (N ●)((S π e1 ), (S π e2 ))Ð→Ð→S π ( J e1 e2 e3 ) = (N J )((S π e1 ), (S π e2 ), (S π e3 ))←Ð←ÐS π ( J e1 e2 e3 ) = (N J )((S π e1 ), (S π e2 ), (S π e3 ))✓✓S π (J e1 e2 e3 ) = (N J )((S π e1 ), (S π e2 ), (S π e3 ))Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201637 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

3

Translate CPS to C.

4

Combine with general-purpose interruption and resumption interface and✓J written in C.

5

Compile to machine code.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201638 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPSPRIMOPS f x = A (λn l v.n) 0 ∞ f x
INTERRUPT f x l = A (λn l v.v) 0 l f x
RESUME ⟦k, f ⟧ = A k 0 ∞ f Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

39 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPS
written in C
static thing lambda_expression_that_returns_x(thing f, thing n, thing l, thing x) {return x;}
static thing lambda_expression_that_returns_n(thing f, thing n, thing l, thing x) {return n;}static thing lambda_expression_that_resumes(thing f, thing continuation, thing n, thing l, thing x) {if (!is_interrupt(x)) internal_error();return converted_apply(as_interrupt(x)->closure,as_interrupt(x)->continuation,
make_real(0.0),l,null_constant);}
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

39 / 48

Implementation of the General-Purpose Interruption andResumption Interface with Threaded CPS

static unsigned long primops(thing f, thing x) {thing result = converted_apply(f,continuation_that_returns_n,
make_real(0.0),
make_real(HUGE_VAL),x);else if (is_real(result)) return (unsigned long)as_real(result);}
static thing interrupt(thing f, thing x, thing l) {thing result = converted_apply(f,continuation_that_returns_x,
make_real(0.0),l,x);
if (!is_interrupt(result)) internal_error();return result;}

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

39 / 48

Algorithm for Divide-and-Conquer Checkpointing✓

To compute (y, x̀) = J f x ỳ:←Ðbase case (f x fast): (y, x̀) = J f x ỳ
inductive case:h○g = fz=gx

(step 1)(step 2)✓(y,z̀) = J h z ỳ✓(z, x̀) = J g x z̀Siskind (Purdue)(step 0)

Checkpointing for Arbitrary Programs(step 3)(step 4)NIPS 2017 WS 9 December 2016

40 / 48

Algorithm for Divide-and-Conquer Checkpointing
written in C

static thing checkpoint_starj(thing f, thing x, thing y_cotangent){
thing loop(thing f, thing x, thing y_cotangent, unsigned long l) {if (l<=base_case_duration) return ternary_starj(f, x, y_cotangent);
else {
thing u = interrupt(f, x, make_real(l/2));
thing y_u_cotangent = loop(closure_that_resumes, u, y_cotangent, l-l/2);
if (!is_pair(y_u_cotangent)) internal_error();thing u_x_cotangent =loop(make_closure_for_interrupt(f, l/2),x,as_pair(y_u_cotangent)->cdr,
l/2);
if (!is_pair(u_x_cotangent)) internal_error();return cons(as_pair(y_u_cotangent)->car,as_pair(u_x_cotangent)->cdr);}}
return loop(f, x, y_cotangent, primops(f, x));}Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

40 / 48

Implementation

1

Convert source program to CPS.

2

Thread step count and limit.

3

Translate CPS to C.

4

Combine with general-purpose interruption and resumption interface and✓J written in C.

5

Compile to machine code.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201641 / 48

Determinant Example(define (car (cons car cdr)) car)(define (cdr (cons car cdr)) cdr)
(define (matrix-rows a)(if (null? a) 0 (+ (matrix-rows (cdr a)) 1)))
(define (list-ref l i)(if (zero? i) (car l) (list-ref (cdr l) (- i 1))))(define (matrix-ref a i j) (list-ref (list-ref a i) j))(define (list-set l i x)
(if (zero? i)(cons x (cdr l))(cons (car l) (list-set (cdr l) (- i 1) x))))(define (matrix-set a i j x)(list-set a i (list-set (list-ref a i) j x)))(define (map-n f n)
(if (zero? n) ’() (cons (f (- n 1)) (map-n f (- n 1)))))(define (identity-matrix n)(map-n (lambda (i) (map-n (lambda (j) (if (= i j) 1 0)) n)) n))

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201642 / 48

Determinant Example(define (determinant a)(let ((n (matrix-rows a)))(let loop ((i 0) (b a) (d 1))(if (= i n)d(let* ((c (matrix-ref b i i))(b (let loop ((j i) (b b))(if (= j n)b(loop (+ j 1) (matrix-set b i j (/ (matrix-ref b i j) c)))))))(loop (+ i 1)
(let loop ((j (+ i 1)) (b b))(if (= j n)b(loop (+ j 1)
(let ((e (matrix-ref b j i)))(let loop ((k (+ i 1)) (b b))(if (= k n)b(loop (+ k 1)
(matrix-set b j k(- (matrix-ref b j k)(* e (matrix-ref b i k)))))))))))(* d c)))))))(write-real (determinant (cdr (checkpoint-*j determinant (identity-matrix (read-real)) 1))))
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201642 / 48

Complexity Analysis

primalno checkpointing
divide-and-conquer checkpointing

Siskind (Purdue)

space
O(n2 )O(n3 )O(n2 log n)

Checkpointing for Arbitrary Programstime
O(n4 )O(n4 )O(n4 log n)

NIPS 2017 WS 9 December 201643 / 48

Space Usage of the Determinant Example
space
Maximum resident set size (kbytes)

350000no checkpointing
divide-and-conquer checkpointing
O(n3)O(n2 log n)

300000250000200000150000100000
50000
0

10

20

30

40

50

60

70

80

90

100

n
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201644 / 48

Time Usage of the Determinant Example
time
45000

no checkpointing
divide-and-conquer checkpointing
O(n4)O(n4 log n)

40000
User time (seconds)

35000
30000
25000
20000
15000
10000
5000
0
-5000

10

20

30

40

50

60

70

80

90

100

n
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201645 / 48

Three Reference Implementations

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201646 / 48

Three Reference Implementations
1

Interpreter using CPS evaluator

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201646 / 48

Three Reference Implementations
1

Interpreter using CPS evaluator

2

Hybrid compiler/interpreter using CPS conversion followed bydirect-style evaluator

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201646 / 48

Three Reference Implementations
1

Interpreter using CPS evaluator

2

Hybrid compiler/interpreter using CPS conversion followed bydirect-style evaluator

3

Compiler using CPS conversion followed by translation to C

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201646 / 48

Three Reference Implementations
1

Interpreter using CPS evaluator

2

Hybrid compiler/interpreter using CPS conversion followed bydirect-style evaluator

3

Compiler using CPS conversion followed by translation to C

All three support exact same source language. No exceptions.
Same space and time complexity. Differ only in constant factors.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201646 / 48

Three Reference Implementations
1

Interpreter using CPS evaluator

2

Hybrid compiler/interpreter using CPS conversion followed bydirect-style evaluator

3

Compiler using CPS conversion followed by translation to C

All three support exact same source language. No exceptions.
Same space and time complexity. Differ only in constant factors.
Could add FFI bindings to GPU Tensor library.
Could serve as reference for rewrite to P YTHON,. . . .

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201646 / 48

Three Reference Implementations
1

Interpreter using CPS evaluator

2

Hybrid compiler/interpreter using CPS conversion followed bydirect-style evaluator

3

Compiler using CPS conversion followed by translation to C

All three support exact same source language. No exceptions.
Same space and time complexity. Differ only in constant factors.
Could add FFI bindings to GPU Tensor library.
Could serve as reference for rewrite to P YTHON,. . . .
All three documented in detail in manuscript.
http://arxiv.org/abs/1708.06799

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201646 / 48

Three Reference Implementations
1

Interpreter using CPS evaluator

2

Hybrid compiler/interpreter using CPS conversion followed bydirect-style evaluator

3

Compiler using CPS conversion followed by translation to C

All three support exact same source language. No exceptions.
Same space and time complexity. Differ only in constant factors.
Could add FFI bindings to GPU Tensor library.
Could serve as reference for rewrite to P YTHON,. . . .
All three documented in detail in manuscript.
http://arxiv.org/abs/1708.06799
Will release when manuscript is accepted.
Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 201646 / 48

Take-Home Message

Divide-and-Conquer checkpointing

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

47 / 48

Take-Home Message

Divide-and-Conquer checkpointing▸

is traditionally formulated around loop iterations

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

47 / 48

Take-Home Message

Divide-and-Conquer checkpointing▸

is traditionally formulated around loop iterations▸

but can be extended to arbitrary code

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

47 / 48

Take-Home Message

Divide-and-Conquer checkpointing▸

is traditionally formulated around loop iterations▸

but can be extended to arbitrary code▸that doesn’t have same-size iterations of a single loop

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

47 / 48

Take-Home Message

Divide-and-Conquer checkpointing▸

is traditionally formulated around loop iterations▸

but can be extended to arbitrary code▸that doesn’t have same-size iterations of a single loop▸

using CPS to make arbitrary code look like it does.

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

47 / 48

Take-Home Message

Divide-and-Conquer checkpointing▸

is traditionally formulated around loop iterations▸

but can be extended to arbitrary code▸that doesn’t have same-size iterations of a single loop▸

using CPS to make arbitrary code look like it does.

metaphor: a CPU is an instruction-execution loop

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

47 / 48

Thank You

Siskind (Purdue)

Checkpointing for Arbitrary Programs

NIPS 2017 WS 9 December 2016

48 / 48