-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathcuda.why
124 lines (114 loc) · 4.33 KB
/
cuda.why
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
theory Cuda
use import int.Int
use import bool.Bool
use import map.Map
type dim3 = { x : int; y : int; z : int }
type block = dim3
type thread = (block, dim3)
function bid_of (t : thread) : block = let (bid, _) = t in bid
function tid_of (t : thread) : dim3 = let (_, tid) = t in tid
(* type local 'a = map thread 'a *)
(* type shared 'a = map block 'a *)
(* type global 'a = 'a *)
(* constant threadIdx : local dim3 *)
(* constant blockIdx : shared dim3 *)
constant blockDim : dim3
constant gridDim : dim3
axiom blockDim_x_pos : 0 < blockDim.x
axiom blockDim_y_pos : 0 < blockDim.y
axiom blockDim_z_pos : 0 < blockDim.z
axiom gridDim_x_pos : 0 < gridDim.x
axiom gridDim_y_pos : 0 < gridDim.y
axiom gridDim_z_pos : 0 < gridDim.z
predicate is_valid_bid (i : dim3) =
0 <= i.x < gridDim.x /\ 0 <= i.y < gridDim.y /\ 0 <= i.z < gridDim.z
predicate is_valid_tid (i : dim3) =
0 <= i.x < blockDim.x /\ 0 <= i.y < blockDim.y /\ 0 <= i.z < blockDim.z
predicate is_valid_thread (t : thread) =
let (bid, tid) = t in is_valid_bid bid /\ is_valid_tid tid
end
(* standard library does not seem to support sums of real values *)
theory Sum
use import int.Int
use import HighOrd
use import real.RealInfix
function sum_i (f : int -> int) (a b : int) : int
function sum_r (f : int -> real) (a b : int) : real
axiom sum_i_base : forall f a b. a > b -> sum_i f a b = 0
axiom sum_r_base : forall f a b. a > b -> sum_r f a b = 0.
axiom sum_i_down : forall f a b. a <= b -> sum_i f a b = f b + sum_i f a (b - 1)
axiom sum_r_down : forall f a b. a <= b -> sum_r f a b = f b +. sum_r f a (b - 1)
axiom sum_r_ext :
forall f g. (forall k. f k = g k) ->
forall a b. sum_r f a b = sum_r g a b
axiom sum_i_ext :
forall f g. (forall k. f k = g k) ->
forall a b. sum_i f a b = sum_i g a b
end
(* hints for automation *)
(* theory SimtHints
* use import int.Int
* use import bool.Bool
* use import map.Map
* use import int.ComputerDivision
* use import Simt
*
* predicate is_accessed (int)
* predicate is_loop_count (int)
* predicate is_loop_var (map thread int)
* predicate is_index_x (int)
* predicate is_index_y (int)
*
* lemma divide_into_block_1' :
* forall i : int. 0 <= i < gridDim.x * blockDim.x ->
* let t = ({x = div i blockDim.x; y = 0; z = 0},
* {x = mod i blockDim.x; y = 0; z = 0}) in
* is_valid_thread t /\ i = blockDim.x * (bid_of t).x + (tid_of t).x
*
* lemma divide_into_block_1 :
* forall i : int. 0 <= i < gridDim.x * blockDim.x ->
* exists t : thread.
* is_valid_thread t /\
* i = blockDim.x * (bid_of t).x + (tid_of t).x
*
* lemma divide_into_block_2' :
* forall i j.
* 0 <= i < x gridDim * x blockDim ->
* 0 <= j < y gridDim * y blockDim ->
* let t = ({x = div i blockDim.x; y = div j blockDim.y; z = 0},
* {x = mod i blockDim.x; y = mod j blockDim.y; z = 0}) in
* is_valid_thread t /\
* i = x blockDim * x (bid_of t) + x (tid_of t) /\
* j = y blockDim * y (bid_of t) + y (tid_of t)
*
* lemma divide_into_block_2 :
* forall i j [is_index_x i, is_index_y j].
* 0 <= i < x gridDim * x blockDim ->
* 0 <= j < y gridDim * y blockDim ->
* exists t.
* is_valid_thread t /\
* i = x blockDim * x (bid_of t) + x (tid_of t) /\
* j = y blockDim * y (bid_of t) + y (tid_of t)
*
* lemma thread_exists_xy :
* forall i j [is_index_x i, is_index_y j].
* 0 <= i < x blockDim ->
* 0 <= j < y blockDim ->
* exists t. is_valid_tid t /\ i = x t /\ j = y t
*
* lemma find_thread_from_index :
* forall k0 k. k0 <= k < k0 + x gridDim * x blockDim ->
* forall i. (forall t. is_valid_thread t ->
* i[t] = x blockDim * x (bid_of t) + x (tid_of t) + k0) ->
* exists t. is_valid_thread t /\ i[t] = k
*
* lemma find_thread_from_index' :
* forall m [is_loop_count m]. forall k.
* x gridDim * x blockDim * m <= k < x gridDim * x blockDim * (m + 1) ->
* forall i [is_loop_var i].
* (forall t. is_valid_thread t ->
* i[t] = x blockDim * x (bid_of t) + x (tid_of t) +
* x gridDim * x blockDim * m) ->
* exists t. is_valid_thread t /\ i[t] = k
*
* end *)