| 1 | $tass compare csr_add_spec.c csr_add_impl.c
|
|---|
| 2 |
|
|---|
| 3 | To compare the two different approaches of adding two matrices.
|
|---|
| 4 | The 'csr_add_spec' uses the traditional method on two dense matrices:
|
|---|
| 5 | In this piece of code, it directly adds each element in the two matrices;
|
|---|
| 6 | and then assigns the sum back to each position in the result matrix.
|
|---|
| 7 | The 'csr_add_impl' uses the CSR matrix addition method on two CSR matrices.
|
|---|
| 8 | In this piece of code, it firstly constructs two CSR matrices from two given
|
|---|
| 9 | array of doubles; and then using a CSR matrices addition method to calculate
|
|---|
| 10 | the result matrix in CSR form; finally, it will expands the result CSR matrix
|
|---|
| 11 | into the dense form and outputs the array containing each element (including 0).
|
|---|
| 12 |
|
|---|
| 13 | # The Input:
|
|---|
| 14 | 'A0': an array of doubles, representing each element in the first DENSE matrix.
|
|---|
| 15 | 'B0': an array of doubles, representing each element in the second DENSE matrix.
|
|---|
| 16 |
|
|---|
| 17 | # The Output:
|
|---|
| 18 | 'OUT': an array of doubles, representing the result DENSE matrix.
|
|---|
| 19 |
|
|---|
| 20 | # Performance:
|
|---|
| 21 | Number Of Row Number Of Col Time Cost (sec) States
|
|---|
| 22 | 1 1 00.294 909
|
|---|
| 23 | 1 2 00.953 4181
|
|---|
| 24 | 1 3 04.031 19481
|
|---|
| 25 | 1 4 53.978 92369
|
|---|
| 26 | 1 5
|
|---|
| 27 | 2 1 00.829 4533
|
|---|
| 28 | 2 2 44.91
|
|---|
| 29 | 2 3
|
|---|
| 30 | 3 1 03.876 22129
|
|---|
| 31 | 3 2
|
|---|
| 32 | 4 1 50.896 105049
|
|---|
| 33 |
|
|---|
| 34 |
|
|---|
| 35 | # loop invariant:
|
|---|
| 36 |
|
|---|
| 37 | correctEle(i,j):
|
|---|
| 38 | exists k.(
|
|---|
| 39 | (impl.A_i[i] <= k && k < impl.A_i[i+1]) &&
|
|---|
| 40 | (j == impl.A_j[k] && spec.C[i][j] == impl.C->data[k])) ||
|
|---|
| 41 | !exists k.(
|
|---|
| 42 | (impl.A_i[i] <= k && k < impl.A_i[i+1]) &&
|
|---|
| 43 | (j == impl.A_j[k] && spec.C[i][j] == 0.0))
|
|---|
| 44 |
|
|---|
| 45 | correctRow(i):
|
|---|
| 46 | forall j.(0 <= j && j < spec.nc && correctEle(i,j))
|
|---|
| 47 |
|
|---|
| 48 | correctMat:
|
|---|
| 49 | forall i.(0 <= i && i < spec.nr && correctRow(i))
|
|---|
| 50 |
|
|---|
| 51 |
|
|---|
| 52 |
|
|---|
| 53 |
|
|---|
| 54 |
|
|---|
| 55 | #pragma TASS joint invariant LoopCorrect // Correct Mat
|
|---|
| 56 | (forall {int r | 0 <= r && r < spec.nr} // Correct Row
|
|---|
| 57 | (forall {int c | 0 <= c && c < spec.nc}(( // Correct Element
|
|---|
| 58 | (forall {int nz1 | C_i[r] <= nz1 && nz1 < C_i[r+1]} // Exist nz1 {nz1 | C_i[r] <= nz1 < C_i[r+1]} (c == C_j[nz1] && spec.C_data[r][c] != C_data[nz1]):
|
|---|
| 59 | (c != C_j[nz1] || spec.C_data[r*spec.nc + c] != C_data[nz1])) // == !( Forall nz1 {..} !(c == C_j[nz1] && spec.C_data[r][c] == C_data[nz1]))
|
|---|
| 60 | != true) // == (( Forall nz1 {..} (c != C_j[nz1] || spec.C_data[r][c] != C_data[nz1])) != true)
|
|---|
| 61 | || // Or
|
|---|
| 62 | (forall {int nz2 | C_i[r] <= nz2 && nz2 < C_i[r+1]} // ! Exist nz2 {nz2 | C_i[r] <= nz2 && nz2 < C_i[r+1]} (c == C_j[nz1] && spec.C_data[r*spec.nc + c] == 0.0)
|
|---|
| 63 | (c != C_j[nz1] || spec.C_data[r*spec.nc + c] != 0.0))) // == Forall nz2 {..} !(c == C_j[nz1] && spec.C_data[r*spec.nc + c] == 0.0)
|
|---|
| 64 | )); // == Forall nz2 {..} (c != C_j[nz1] || spec.C_data[r*spec.nc + c] != 0.0)
|
|---|
| 65 | |
|---|
