Prune taskparallel dir #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

erickoskinen wants to merge 284 commits into veracity-lang:main from veracity-lang:prune-taskparallel-dir

.gitmodules

-Original file line number
+Diff line change
@@ Expand Up / @@ -5,4 +5,4 @@ @@
     [submodule "src/servois2"]
     	path = src/servois2
     	url = https://github.com/veracity-lang/servois2.git
-    	ignore = dirty
+    	ignore = dirty

.vscode/settings.json

-Original file line number
+Diff line change
@@ Expand Up / @@ -3,6 +3,8 @@ @@
             "*.smtlib2": "smt-lib",
             "*.vcy": "c",
             "random": "c",
+            "stdlib.h": "c",
+            "string": "c"
             "fetchandadd": "c"
         }
-    }
+    }

README.md

-Original file line number
+Diff line change
@@ Expand Up / @@ -17,16 +17,19 @@ add-apt-repository ppa:avsm/ppa @@
     apt update
     apt install opam
     apt install cvc4
+    apt install graphviz # optional, for PDG output
     opam init
     eval $(opam env)
     opam update
-    opam switch create 4.12.0mc 4.12.0+domains+effects --repositories=multicore=git+https://github.com/ocaml-multicore/multicore-opam.git,default
-    opam switch 4.12.0mc
+    #opam switch create 4.12.0mc 4.12.0+domains+effects --repositories=multicore=git+https://github.com/ocaml-multicore/multicore-opam.git,default
+    #opam switch 4.12.0mc
+    opam switch create 5.2.0
     eval $(opam env)
-    opam install sexplib ppxlib.0.22.0+effect-syntax ppx_deriving_yaml ounit2 menhir
+    #opam install sexplib ppxlib.0.22.0+effect-syntax ppx_deriving_yaml
+    opam install ounit2 menhir zarith yaml domainslib
     eval $(opam env)
     ```
@@ Expand Down @@

benchmarks/global_commutativity/2d-array.vcy

-Original file line number
+Diff line change
@@ -0,0 +1,49 @@
+    int main(int argc, string[] argv) {
+        int[] pIds = new int[100];
+        bool[] visited = new bool[100];
+        int pSize = 100;
+        /* Each row is a fixed p, variable q */
+        int[] pValue = new int[100];
+        bool[][] pqFlag = new bool[][100];
+        int sum =0;
+        /* initialize pqFlag */
+        int i = 0;
+        int p = 0;
+        int id = 0;
+        int row = 0;
+        int q = 0;
+        int scalingfactor = 1000;
+        scalingfactor = int_of_string(argv[1]);
+        /* mutex_init(0); */
+        while(i < 100) {
+            pqFlag[i] = new bool[100];
+            pIds[i] = i;
+            pValue[i] = i;
+            /* if (pIds[i] < 0) { pIds[i] = i; } */
+            i = i + 1;
+        }
+        while(p < pSize){
+            id = pIds[p];
+            if(!visited[id % 100]){
+                visited[id % 100] = true;
+                row = p; /* "row" should be the dep */
+                q = 0;
+                while (q < 99 && !pqFlag[row][q%100]){
+                    busy_wait(scalingfactor);
+                    q = q+1;
+                }
+                if(q < 100){
+                    mutex_lock(0);
+                    sum = (sum + pValue[row]) % 256;
+                    mutex_unlock(0);
+                }
+            }
+            p = p + 1;
+        }
+        return sum;
+    }

benchmarks/global_commutativity/commset-verify.vcy

-Original file line number
+Diff line change
@@ -0,0 +1,40 @@
+    commutativity {
+       {f1(i_left)}, {f1(i_right)} : (i_left != i_right)
+    }
+    int main(int argc, string[] argv) {
+        int i = 1;
+        int i_left = 1;
+        int i_right = 1;
+        string[] digest = new string[16];
+        while (i < argc){
+            f1(i):{
+                string temp = "";
+                string filename = "";
+                string s = "";
+                int m = md5_lower(s);
+                filename = argv[i];
+                in_channel c = open_read(filename);
+                s = read_line(c);
+                temp = string_of_int(m);
+                close(c);
+                digest[i] = temp;
+                print(digest[i]);
+                print("\n");
+                temp = "";
+                filename = "";
+                s = "";
+                m = 0;
+                c = open_read(temp);
+                close(c);
+            }
+            i = i + 1;
+        }
+        return 0;
+    }

benchmarks/global_commutativity/commset.vcy

-Original file line number
+Diff line change
@@ -0,0 +1,38 @@
+    commutativity {
+       {f1(i_1)}, {f1(i_2)} : (i_1 != i_2)
+    }
+    int main(int argc, string[] argv) {
+        int i = 1;
+        string[] digest = new string[16];
+        string s = "";
+        int i_1 = 0;
+        int i_2 = 0;
+        string filename = "";
+        while (i < argc){
+            f1(i):{
+                int j = 0;
+                string temp = "";
+                filename = argv[i];
+                while (j < 10) { /* Artificially increase workload by 10x */
+                    j = j+1;
+                    in_channel c = open_read(filename);
+                    s = read_line(c);
+                    int j = 0;
+                    temp = string_of_int(md5_lower(s));
+                    close(c);
+                }
+                digest[i] = temp;
+                print(digest[i]);
+                print("\n");
+            }
+            i = i + 1;
+        }
+        return 0;
+    }

benchmarks/global_commutativity/commset_infer.vcy

-Original file line number
+Diff line change
@@ -0,0 +1,34 @@
+    commutativity {
+       {f1(i_1, digest)}, {f1(i_2, digest)} : _
+    }
+    int i = 1;
+    string[] digest = new string[16];
+    int main(int argc, string[] argv) {
+        int i_1 = 0;
+        int i_2 = 0;
+        while (i < argc){
+            f1(i, digest):{
+                string filename = argv[i];
+                in_channel c = open_read(filename);
+                string s = read_line(c);
+                int md5 = md5_lower(s);
+                string temp = string_of_int(md5);
+                digest[i] = temp;
+                close(c);
+                filename = "";
+                s = "";
+                temp = "";
+                md5 = 0;
+                c = open_read(filename);
+            }
+            i = i + 1;
+        }
+        return 0;
+    }

benchmarks/global_commutativity/motivation.vcy

-Original file line number
+Diff line change
@@ -0,0 +1,45 @@
+    commutativity {
+        {f1(i_1, x, arr)}, {f2(i_2, arr)}: ((i_1 != i_2) || (i_1 == i_2 && arr[i_1] > 0))
+    }
+    int main(int argc, string[] argv) {
+        int scalingfactor = int_of_string(argv[1]);
+        int x = 10;
+        int[] arr = new int[1000];
+        int size = int_of_string(argv[2]);
+        int[] out = new int[size];
+        int i = 0;
+        int j = 0;
+        int i_1 = 0;
+        int i_2 = 2;
+        int res = 0;
+        int t = 0;
+        while (j < 1000) {
+            arr[j] = random(1, 1000);
+            j = j + 1;
+        }
+        while (i < size) {
+            f1(i, x, arr):{ /* will only increase arr[i] */
+                busy_wait(scalingfactor);
+                x = i;
+                arr[i] = arr[i] + (x*x);
+            }
+            f2(i, arr):{ /* only observes if arr[i]>0 */
+                t = /*compute*/(i);
+                busy_wait(scalingfactor);
+                if (arr[i] > 0 && t < 0) {
+                    arr[i] = arr[i] - 1;
+                    out[i] = /*calc2*/(t);
+                } else {
+                    out[i] = /*calc3*/(t);
+                }
+            }
+            i = i + 1;
+        }
+        return arr[0];
+    }

benchmarks/global_commutativity/multi-blocks.vcy

-Original file line number
+Diff line change
@@ -0,0 +1,71 @@
+    commutativity {
+        {f1(tbl,x,y)}, {f2(tbl,z,y)}: (tbl[z] == tbl[x] && !(z == x) || z == x);
+        {f2(tbl,z,y)}, {f3(tbl,z,y)}: (!(ht_size(tbl) > 0) && !(0 == z) || 0 == z);
+        {f4(files,i_1)}, {f4(files,i_2)}: (files[i_2] == files[i_1]);
+        {f4(files,i_1)}, {f6(files,i_3)}: (!(i_3 == i_1));
+        {f1(tbl,x,y)}, {f3(tbl,z,y)}: (!(ht_size(tbl) > 0) && !(0 == ht_size(tbl)) && !(0 == z) || 0 == ht_size(tbl) && !(0 == z) || 0 == z);
+        {f1(tbl,x,y)}, {f4(files,i_1)}: (true);
+        {f1(tbl,x,y)}, {f6(files,i_3)}: (true);
+        {f2(tbl,z,y)}, {f4(files,i_1)}: (true);
+        {f2(tbl,z,y)}, {f6(files,i_3)}: (true);
+        {f3(tbl,z,y)}, {f4(files,i_1)}: (true);
+        {f3(tbl,z,y)}, {f6(files,i_3)}: (true)
+    }
+    int main(int argc, string[] argv) {
+    	hashtable[int,int] tbl = new hashtable[int,int];
+    	int n = 1000 * int_of_string(argv[1]);
+    	int x = 2;
+    	int y = 5;
+    	int z = 0;
+        int f = 1;
+        int g = 0;
+        int i = 0;
+        int i_1 = 3;
+        int i_2 = 3;
+        int i_3 = 4;
+        int j = 0;
+        int[] files = new int[10];
+        tbl[x] = 12;
+    	tbl[z] = 12;
+        while(j < 10) {
+            files[j] = j;
+            j = j + 1;
+        }
+        f1(tbl,x,y):{
+            busy_wait(n);
+            if(ht_mem(tbl, x)) {
+                y = ht_get(tbl, x);
+            }
+        }
+        f2(tbl,z,y): {
+            y = ht_get(tbl, z);
+            busy_wait(n);
+        }
+    	f3(tbl,z,y): {
+            busy_wait(n);
+            if(ht_size(tbl) > 0) {
+                y = y + z;
+            }
+    	}
+        f4(files,i):{
+            busy_wait(n);
+            f = files[i];
+            f = f + 5;
+            files[i] = f;
+        }
+        f6(files,i):{
+            busy_wait(n);
+            g = files[i];
+            g = g + 5;
+            files[i] = g;
+        }
+    	return 0;
+    }

benchmarks/global_commutativity/nested_if.vcy

-Original file line number
+Diff line change
@@ -0,0 +1,20 @@
+    commutativity {
+    }
+    int main(int argc, string[] argv) {
+        int x = 1;
+        x = x + 2;
+        if(x > 2) {
+            if (x == 3){
+                x = x - 1;
+            }
+        }
+        else{
+            x = x + 1;
+        }
+        return x;
+    }

benchmarks/global_commutativity/nested_if_loop.vcy

-Original file line number
+Diff line change
@@ -0,0 +1,32 @@
+    commutativity {
+    }
+    int main(int argc, string[] argv) {
+        int x = 0;
+        x = 1;
+        x = x + 2;
+        if(x > 2) {
+            if (x == 3){
+                x = x * 10;
+                while(x > 4) {
+                    x = x - 1;
+                }
+            }
+            else{
+                x = x * 2;
+            }
+        }
+        else{
+            if(x == 0){
+                x = x + 2;
+            }
+            else{
+                x = x + 1;
+            }
+        }
+        return x;
+    }

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Prune taskparallel dir #4

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Prune taskparallel dir #4

Are you sure you want to change the base?

Uh oh!

Prune taskparallel dir #4

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!