 Забыли?

?

Programming by Sketching

код для вставкиСкачать
```Programming by Sketching
Armando Solar-Lezama, Liviu Tancau, Gilad Arnold,
Rastislav Bodik, Sanjit Seshia UC Berkeley, Rodric Rabbah
MIT,
Kemal Ebcioglu, Vijay Saraswat, Vivek Sarkar IBM
Merge sort
int[] mergeSort (int[] input, int n) {
return merge(
mergeSort (input[0::n/2]),
mergeSort (input[n/2+1::n]) , n);
}
int[] merge (int[] a, int b[], int n) {
int j=0, k=0;
for (int i = 0; i < n; i++)
if ( a[j] < b[k] ) {
result[i] = a[j++];
} else {
result[i] = b[k++];
looks simple to code,
}
but there is a bug
}
return result;
}
2
Merge sort
int[] mergeSort (int[] input, int n) {
return merge(
mergeSort (input[0::n/2]),
mergeSort (input[n/2+1::n]) , n);
}
int[] merge (int[] a, int b[], int n) {
int j, k;
for (int i = 0; i < n; i++)
if ( j<n && ( !(k<n) || a[j] < b[k]) ) {
result[i] = a[j++];
} else {
result[i] = b[k++];
}
}
return result;
}
3
The sketching experience
spec
+
specification
sketch
implementation
(completed sketch)
4
The spec: bubble sort
int[] sort (int[] input, int n) {
for (int i=0; i<n; ++i)
for (int j=i+1; j<n; ++j)
if (input[j] < input[i])
swap(input, j, i);
}
5
Merge sort: sketched
int[] mergeSort (int[] input, int n) {
return merge(
mergeSort (input[0::n/2]),
mergeSort (input[n/2+1::n]) , n);
}
int[] merge (int[] a, int b[], int n) {
int j, k;
for (int i = 0; i < n; i++)
if ( expression(
||, &&, <, !, [] ) ) {
hole
result[i] = a[j++];
} else {
result[i] = b[k++];
}
}
return result;
}
6
Merge sort: synthesized
int[] mergeSort (int[] input, int n) {
return merge(
mergeSort (input[0::n/2]),
mergeSort (input[n/2::n])
}
int[] merge (int[] a, int b[], int n) {
int j, k;
for (int i = 0; i < n; i++)
if ( j<n && ( !(k<n) || a[j] < b[k]) ) {
result[i] = a[j++];
} else {
result[i] = b[k++];
}
}
return result;
}
);
7
Sketching: spec vs. sketch
вЂў Specification
вЂ“ executable: easy to debug, serves as a prototype
вЂ“ a reference implementation: simple and sequential
вЂ“ written by domain experts: crypto, bio, MPEG
committee
вЂў Sketched implementation
вЂ“ program with holes: filled in by synthesizer
вЂ“ programmer sketches strategy: machine provides
details
вЂ“ written by performance experts: vector wizard;
cache guru
8
How sketching fits into autotuning
вЂў Autotuning: two methods for obtaining code
variants
1. optimizing compiler: transform a вЂњspecвЂќ in various
ways
2. custom generator: for a specific algorithm
вЂў We seek to simplify the second approach
вЂў Scenario 1: library of variants stores resolved
sketches
вЂ“ as if written by hand
вЂў Scenario 2: library has unresolved, flexible
sketches
9
SKETCH
вЂў A language with support for sketching-based
synthesis
вЂ“ like C without pointers
вЂ“ two simple synthesis constructs
вЂў restricted to finite programs:
вЂ“ input size known at compile time, terminates on all inputs
вЂў most high-performance kernels are finite:
вЂ“ matrix multiply: yes
вЂ“ binary search tree: no
вЂў weвЂ™re already working on relaxing the fineteness
restriction
вЂ“ later in this talk
10
Ex1: Isolate rightmost 0-bit. 1010 0111 пѓ 0000 1000
bit[W] isolate0 (bit[W] x) {
// W: word size
bit[W] ret = 0;
for (int i = 0; i < W; i++)
if (!x[i]) { ret[i] = 1; break; }
return ret;
}
bit[W] isolate0Fast (bit[W] x) implements isolate0 {
return ~x & (x+1);
}
bit[W] isolate0Sketched (bit[W] x) implements isolate0 {
return ~(x + ??) & (x + ??);
}
11
ProgrammerвЂ™s view of sketches
вЂў the ?? operator replaced with a suitable constant
вЂў as directed by the implements clause.
вЂў the ?? operator introduces non-determinism
вЂў the implements clause constrains it.
12
Beyond synthesis of literals
вЂў Synthesizing values of ?? already very useful
вЂ“ parallelization machinery: bitmasks, tables in crypto
codes
вЂ“ array indices: A[i+??,j+??]
вЂў We can synthesize more than constants
вЂ“ semi-permutations: functions that select and shuffle
bits
вЂ“ polynomials: over one or more variables
вЂ“ actually, arbitrary expressions, programs
14
Synthesizing polynomials
int spec (int x) {
return 2*x*x*x*x + 3*x*x*x + 7*x*x + 10;
}
int p (int x) implements spec {
return (x+1)*(x+2)*poly(3,x);
}
int poly(int n, int x) {
if (n==0) return ??;
else return x * poly(n-1, x) + ??;
}
17
KaratsubaвЂ™s multiplication
x = x1*b + x0
y = y1*b + y0
b=2k
x*y = b2*x1*y1 + b*(x1*y0 + x0*y1) + x0*y0
x*y = poly(??,b) * x1*y1 +
+ poly(??,b) * poly(1,x1,x0,y1,y0)*poly(1,x1, x0, y1, y0)
+ poly(??,b) * x0*y0
x*y = (b2 +b) * x1*y1
+
b * (x1 - x0)*(y1 - y0)
+ (b+1) * x0*y0
18
Sketch of Karatsuba
bit[N*2] k<int N>(bit[N] x, bit[N] y) implements mult {
if (N<=1) return x*y;
bit[N/2] x1 = x[0:N/2-1];
bit[N/2] y1 = y[0:N/2-1];
bit[N/2+1] x2 = x[N/2:N-1];
bit[N/2+1] y2 = y[N/2:N-1];
bit[2*N] t11 = x1 * y1;
bit[2*N] t12 = poly(1, x1, x2, y1, y2) * poly(1, x1, x2, y1, y2);
bit[2*N] t22 = x2 * y2;
return multPolySparse<2*N>(2, N/2, t11)
+ multPolySparse<2*N>(2, N/2, t12)
+ multPolySparse<2*N>(2, N/2, t22);
// log b = N/2
}
bit[2*N] poly<int N>(int n, bit[N] x0, x1, x2, x3) {
if (n<=0) return ??;
else return (??*x0 + ??*x1 + ??*x2 + ??*x3) * poly<N>(n-1, x0, x1, x2, x3);
}
bit[2*N] multPolySparse<int N>(int n, int x, bit[N] y) {
if (n<=0) return 0;
else return y << x*?? + multPolySparse<N>(n-1, x, y);
}
19
Semantic view of sketches
вЂў a sketch represents a set of functions:
вЂ“ the ?? operator modeled as reading from an oracle
int f (int y) {
x = ??;
loop (x) {
y = y + ??;
}
return y;
}
int f (int y, bit[][K] oracle) {
x = oracle;
loop (x) {
y = y + oracle;
}
return y;
}
Synthesizer must find oracle satisfying f
implements g
20
Synthesis algorithm: overview
1. translation: represent spec and sketch as
circuits
2. synthesis: find suitable oracle
3. code generation: specialize sketch wrt oracle
21
Ex : Population count.
пѓ 3
x
int pop (bit[W] x)
{
int count = 0;
for (int i = 0; i < W; i++) {
if (x[i]) count++;
}
return count;
}
0010 0110
count
0 0 0 0
one
0 0 0 1
+
mux
count
+
mux
count
+
mux
count
mux
+
F(x) =count
22
Synthesis as generalized SAT
вЂў The sketch synthesis problem is an instance of 2QBF:
п‚Ѕ o . п‚ј x . P(x) = S(x,o)
вЂў Counter-example driven solver:
I = {}
S(x1, c)=P(x1) пЂ® вЂ¦ пЂ®
x = random()
c)=P(xk)
do
I ={ x1, x2, вЂ¦, xk }
I = I U {x}
c = synthesizeForSomeInputs(I)
if c = nil then exit(вЂњbuggy sketch'')
x = verifyForAllInputs(c)
// x: counter-example
while x != nil
return c
S(xk,
S(x, c) пЂЎ
P(x)
23
Case study
вЂў Implemented AES
вЂ“ the modern block-cipher standard
вЂ“ 14 rounds: each has table lookup, permutation, GFmultiply
вЂ“ a good implementation collapses each round into table
lookups
вЂў Our results
вЂ“
вЂ“
вЂ“
вЂ“
we synthesized 32Kbit oracle!
counterexample-driven synthesizer iterated 655 times
performance of synthesized code within 10% of handtuned
24
Finite programs
вЂў In theory, SKETCH is complete for all finite
programs:
вЂ“ specification can specify any finite program
вЂ“ sketch can describe any implementation over given
instructions
вЂ“ synthesizer can resolve any sketch
вЂў In practice, SKETCH scales for small finite
programs
вЂ“ small finite programs: block ciphers, small kernels
вЂ“ large finite: big-integer multiplication, matrix
multiplication
вЂў Solution:
25
Lossless abstraction
вЂў Problem
вЂ“ does result of synthesis for a small matrix work for all
matrices?
вЂў Approach
вЂ“ spec, sketch have unbounded-input/output
вЂ“ abstract them into finite functions, with the same
abstraction
вЂ“ synthesize
вЂ“ obtained oracle works for original sketch
вЂў Stencil kernels
вЂ“ concrete:
вЂ“ abstract:
matrix A[N] пЃґ matrix B[N]
A[e(i)], i, N пЃґ B[i]
28
Example: divide and conquer
parallelization
вЂў Parallel algorithm:
вЂ“ Data rearrangement + parallel computation
вЂў spec:
вЂ“ sequential version of the program
вЂў sketch:
вЂ“ parallel computation
вЂў automatically synthesized:
вЂ“ Rearranging the data (dividing the data structure)
29
```
Документ
Категория
Без категории
Просмотров
11
Размер файла
454 Кб
Теги
1/--страниц
Пожаловаться на содержимое документа