Continuity Analysis of Programs
CAUCHY
Continuity analysis of
programs
Uncertainty and robustness
•
Trends:
cyber-physical systems, integration
of computation and science, …
•
Uncertainty:
stale satellite data, erroneous
sensor measurements, …
•
Does your program handle uncertainty
robustly?
–
Correctness in settings without
uncertainty does not imply correctness
in uncertain environments.
Robustness analysis of programs
•
Robustness:
small perturbations to a
program’s operating conditions do not
change its behavior significantly.
–
Continuity:
Infinitesimal changes to inputs only
cause infinitesimal changes to outputs.
–
Discrete continuity:
Similar, except for non-infinitesimal
changes to discrete numbers.
–
Derivative has low complexity.
–
Asymptotic stability
•
Verify these!
P
First step: Continuity analysis of programs
•
Continuity of mathematical functions:
–
definition.
–
Equivalently, infinitesimal changes in
inputs only cause infinitesimal
changes in outputs.
•
Continuity of programs
–
Associate metric spaces with types,
lift it into a metric over states.
–
Same question. Do infinitesimal
changes in program inputs only cause
infinitesimal changes to outputs?
This paper:
structural analysis of
continuity.
P
Example: an implementation of Dijkstra’s algorithm
•
Small change to real array: each element changes at most by a
small amount.
•
Small change to graph with real edge weight: each edge
weight changes at most by a small amount.
•
Is this program continuous?
p
r
o
c
e
d
u
r
e
D
i
j
k
s
t
r
a
(
G
:
g
r
a
p
h
,
s
r
c
:
n
o
d
e
)
:
f
o
r
e
a
c
h
n
o
d
e
v
i
n
G
:
{d
[
v
]
:
=
I
n
f
i
n
i
t
y
}
d[src] := 0; Worklist := set of all nodes in G;
w
h
i
l
e
W
o
r
k
l
i
s
t
i
s
n
o
t
e
m
p
t
y
{Remove node w from Worklist s.t. d[w] is minimal;
f
o
r
e
a
c
h
n
e
i
g
h
b
o
r
v
o
f
w
:
{z := d[w] + G[w,v];
if (z < d[v]) { d[v] := z; prev[v] := w; } } }Example: Dijkstra’s algorithm
•
Small change to real array: each element changes at most by a
small amount.
•
Small change to graph with real edge weight: each edge
weight changes at most by a small amount.
•
Is this program continuous?
p
r
o
c
e
d
u
r
e
D
i
j
k
s
t
r
a
(
G
:
g
r
a
p
h
,
s
r
c
:
n
o
d
e
)
:
f
o
r
e
a
c
h
n
o
d
e
v
i
n
G
:
{d
[
v
]
:
=
I
n
f
i
n
i
t
y
}
d[src] := 0; Worklist := set of all nodes in G;
w
h
i
l
e
W
o
r
k
l
i
s
t
i
s
n
o
t
e
m
p
t
y
{Remove node w from Worklist s.t. d[w] is minimal;
f
o
r
e
a
c
h
n
e
i
g
h
b
o
r
v
o
f
w
:
{z := d[w] + G[w,v];
if (z < d[v]) { d[v] := z; prev[v] := w; } } }•
Depends on what is observable.
•
At point of output, d is a continuous
function of G, but prev is not.
•
Sorting algorithms
are continuous
… but only if output = array of keys.
•
Minimum spanning tree algorithms
are continuous
… but only if the output is the weight of the tree.
•
Integer knapsack
is continuous in values of items but not
in their weights.
•
Fractional knapsack
is continuous in values
and
weights.
Continuity at work!
2.0
3.0
4.0
3.0
2.0
3.0
3.0
4.0
2.0
3.0
4.0
2.99
2.0
2.99
3.0
4.0
•
Key Idea: Prove branch-equivalence at the
zeroes
of b—i.e.,
conditions under which guard can flip on small changes.
•
Example: d[v] is continuous after
if
(d[v] < z) d[v] := z.
The guard (d[v] < z) flips (under small changes) only when
d[v]
=
z. Then, d[v] has similar values on both branches.
•
Automate using an SMT-solver. (cf. Translation validation)
Challenge #1: Control flow
if
b
P
1
P
2
1.
2.
P
1
and P
2
are continuous.
P is continuous
P
Challenge #2: Noninductiveness
w
h
i
l
e
W
o
r
k
l
i
s
t
i
s
n
o
t
e
m
p
t
y
{Remove node w from Worklist s.t. d[w] is minimal;
f
o
r
e
a
c
h
n
e
i
g
h
b
o
r
v
o
f
w
:
{z := d[w] + G[w,v];
if (z < d[v]) { d[v] := z; prev[v] := w; } } }•
Small change to d at iteration-entry can completely change
the value of d at the end.
•
Thus, continuity is not inductive.
u
1
d[u
1
] = 2.00
u
2
d[u
2
] = 2.00
u
3
d[u
2
] = 4.00
u
2
d[u
2
] = 2.00
u
1
d[u
1
] = 2.00
Key idea: Induction over epochs
w
h
i
l
e
W
o
r
k
l
i
s
t
i
s
n
o
t
e
m
p
t
y
{Remove node w from Worklist s.t. d[w] is minimal;
•
To be reordered, iterations must be approximately tied on
selection criterion. Epoch = cluster of such iterations.
•
Prove that iterations within epochs are
commutative.
•
Proof can be discharged using an SMT-solver.
u
3
d[u
2
] = 4.00
u
1
d[u
2
] = 2.01
u
2
d[u
1
] = 2.00
u
3
d[u
2
] = 4.02
u
2
d[u
2
] = 2.00
u
1
d[u
1
] = 2.00
Key idea: Induction over epochs
w
h
i
l
e
W
o
r
k
l
i
s
t
i
s
n
o
t
e
m
p
t
y
{Remove node w from Worklist s.t. d[w] is minimal;
Now do induction over epochs.
u
3
d[u
2
] = 4.00
u
1
d[u
2
] = 2.01
u
2
d[u
1
] = 2.00
u
3
d[u
2
] = 4.02
Original
Perturbed
But often, simple induction is enough
f
o
r
k
:
=
1
t
o
N
f
o
r
i
,
j
:
=
1
t
o
N
:
i
f
G
[
i
,
j
]
>
G
[
i
,
k
]
+
G
[
k
,
j
]
G[i, j] := G[i, k] + G[k. j];
Floyd-Warshall shortest path algorithm
Challenge #3: Early or late termination
•
Key Idea: Prove idempotence under conditions when
guard can flip.
•
Example:
while
(z > 0) { x := x + z; z := z * w; }If z = 0, then loop body is idempotent.
while
b
P
Original
Perturbed
•
Soundness with respect to definition. (Tricky!)
•
Proof rules discharged using Z3 SMT solver.
•
Able to prove 11 of the 13 continuous algorithms
targeted:
–
Sorting (Merge sort, Bubble sort, Insertion sort, Selection sort).
–
Minimum Spanning Tree (Prim’s and Kruskal’s)
–
Shortest Paths (Floyd-Warshall, Bellman-Ford, Dijkstra)
–
Knapsack (Fractional and integer)
•
Epoch induction needed in 5/13 cases.
•
Early termination check needed in 3/13 cases.
•
Current work exploring “real” applications (embedded
medical devices and GPS apps).
Results
Ongoing work: discrete derivatives of
programs
•
Instead of infinitesimal changes to real
variables, consider unit changes to finite-
precision variables.
•
More natural in the quantitative setting.
•
Changes the game somewhat:
–
E.g., Addition is not continuous.
•
But most of the rules/insights still apply.
•
Goal:
Mechanically generate
discrete
derivatives
of programs:
–
E.g., Discrete derivative of Dijkstra’s
algorithm in O(n).
P
The Cauchy challenge
Cauchy
Develop an analytical calculus of computation
Limits of programs
Hybrid
representations
Continuity
analysis
Analytic
approximations of
programs
(Discrete)
d
erivatives
of programs
Applications in cyber-physical systems, approximate
computation. Also, pedagogical value.
Fourier analysis of
programs
Conclusion
•
Robustness is an important correctness property
for programs operating under uncertainty.
•
Continuity is one, but by no means the only,
robustness property.
•
This paper offers one, but by no means the only,
continuity analysis.
•
First step towards an analytical calculus of
computation.
This content delves into the concept of continuity analysis in programs, focusing on aspects like uncertainty, robustness, and infinitesimal changes in inputs and outputs. It explores the implications of handling uncertainty robustly, the significance of correctness in uncertain environments, and the relationship between small perturbations in program conditions and behavior. Theoretical explanations and examples, such as Dijkstra's algorithm, are used to illustrate the principles of continuity analysis in programs.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
CAUCHY Continuity analysis of programs Swarat Chaudhuri Roberto Lublinerman Sumit Gulwani Microsoft Research Pennsylvania State University
Uncertainty and robustness Trends: cyber-physical systems, integration of computation and science, Uncertainty: stale satellite data, erroneous sensor measurements, Does your program handle uncertainty robustly? Correctness in settings without uncertainty does not imply correctness in uncertain environments.
Robustness analysis of programs Robustness: small perturbations to a program s operating conditions do not change its behavior significantly. Continuity: Infinitesimal changes to inputs only cause infinitesimal changes to outputs. Discrete continuity: Similar, except for non-infinitesimal changes to discrete numbers. Derivative has low complexity. Asymptotic stability Verify these! P
First step: Continuity analysis of programs Continuity of mathematical functions: definition. Equivalently, infinitesimal changes in inputs only cause infinitesimal changes in outputs. Continuity of programs Associate metric spaces with types, lift it into a metric over states. Same question. Do infinitesimal changes in program inputs only cause infinitesimal changes to outputs? P This paper: structural analysis of continuity.
Example: an implementation of Dijkstras algorithm procedure Dijkstra (G: graph, src: node): for each node v in G: { d[v] := Infinity } d[src] := 0; Worklist := set of all nodes in G; while Worklist is not empty { Remove node w from Worklist s.t. d[w] is minimal; for each neighbor v of w: { z := d[w] + G[w,v]; if (z < d[v]) { d[v] := z; prev[v] := w; } } } Small change to real array: each element changes at most by a small amount. Small change to graph with real edge weight: each edge weight changes at most by a small amount. Is this program continuous?
Example: Dijkstras algorithm procedure Dijkstra (G: graph, src: node): for each node v in G: { d[v] := Infinity } d[src] := 0; Worklist := set of all nodes in G; while Worklist is not empty { Remove node w from Worklist s.t. d[w] is minimal; for each neighbor v of w: { z := d[w] + G[w,v]; if (z < d[v]) { d[v] := z; prev[v] := w; } } } Small change to real array: each element changes at most by a small amount. Small change to graph with real edge weight: each edge weight changes at most by a small amount. Is this program continuous? function of G, but prev is not. Depends on what is observable. At point of output, d is a continuous
Continuity at work! Sorting algorithms are continuous 2.0 3.0 4.0 3.0 2.0 3.0 4.0 2.99 2.0 3.0 3.0 4.0 2.0 2.99 3.0 4.0 but only if output = array of keys. Minimum spanning tree algorithms are continuous but only if the output is the weight of the tree. Integer knapsack is continuous in values of items but not in their weights. Fractional knapsack is continuous in values and weights.
Challenge #1: Control flow P if b 1. 2. P1 and P2 are continuous. P is continuous P2 P1 Key Idea: Prove branch-equivalence at the zeroes of b i.e., conditions under which guard can flip on small changes. Example: d[v] is continuous after if (d[v] < z) d[v] := z. The guard (d[v] < z) flips (under small changes) only when d[v] = z. Then, d[v] has similar values on both branches. Automate using an SMT-solver. (cf. Translation validation)
Challenge #2: Noninductiveness while Worklist is not empty { Remove node w from Worklist s.t. d[w] is minimal; for each neighbor v of w: { z := d[w] + G[w,v]; if (z < d[v]) { d[v] := z; prev[v] := w; } } } u1 u2 u3 d[u1] = 2.00 d[u2] = 2.00 d[u2] = 4.00 Small change to d at iteration-entry can completely change the value of d at the end. Thus, continuity is not inductive.
Key idea: Induction over epochs while Worklist is not empty { Remove node w from Worklist s.t. d[w] is minimal; u1 u2 u3 d[u1] = 2.00 d[u2] = 2.00 d[u2] = 4.00 u3 u2 u1 d[u2] = 4.02 d[u1] = 2.00 d[u2] = 2.01 To be reordered, iterations must be approximately tied on selection criterion. Epoch = cluster of such iterations. Prove that iterations within epochs are commutative. Proof can be discharged using an SMT-solver.
Key idea: Induction over epochs while Worklist is not empty { Remove node w from Worklist s.t. d[w] is minimal; Perturbed u3 u1 u2 d[u2] = 4.00 d[u1] = 2.00 d[u2] = 2.00 Original u2 u3 u1 d[u1] = 2.00 d[u2] = 4.02 d[u2] = 2.01 Now do induction over epochs.
But often, simple induction is enough for k := 1 to N for i, j := 1 to N: if G[i, j] > G[i, k] + G [k, j] G[i, j] := G[i, k] + G[k. j]; Floyd-Warshall shortest path algorithm
Challenge #3: Early or late termination while b P Perturbed Original Key Idea: Prove idempotence under conditions when guard can flip. Example: while (z > 0) { x := x + z; z := z * w; } If z = 0, then loop body is idempotent.
Results Soundness with respect to definition. (Tricky!) Proof rules discharged using Z3 SMT solver. Able to prove 11 of the 13 continuous algorithms targeted: Sorting (Merge sort, Bubble sort, Insertion sort, Selection sort). Minimum Spanning Tree (Prim s and Kruskal s) Shortest Paths (Floyd-Warshall, Bellman-Ford, Dijkstra) Knapsack (Fractional and integer) Epoch induction needed in 5/13 cases. Early termination check needed in 3/13 cases. Current work exploring real applications (embedded medical devices and GPS apps).
Ongoing work: discrete derivatives of programs Instead of infinitesimal changes to real variables, consider unit changes to finite- precision variables. More natural in the quantitative setting. Changes the game somewhat: E.g., Addition is not continuous. But most of the rules/insights still apply. Goal: Mechanically generate discrete derivatives of programs: E.g., Discrete derivative of Dijkstra s algorithm in O(n). P
The Cauchy challenge Develop an analytical calculus of computation (Discrete) derivatives of programs Continuity analysis Cauchy Analytic approximations of programs Limits of programs Hybrid Fourier analysis of programs representations Applications in cyber-physical systems, approximate computation. Also, pedagogical value.
Conclusion Robustness is an important correctness property for programs operating under uncertainty. Continuity is one, but by no means the only, robustness property. This paper offers one, but by no means the only, continuity analysis. First step towards an analytical calculus of computation.
