lots of change and add notes
authorPeizhao Ou <peizhaoo@uci.edu>
Fri, 18 Oct 2013 01:14:58 +0000 (18:14 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Fri, 18 Oct 2013 01:14:58 +0000 (18:14 -0700)
benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h
benchmark/ms-queue/my_queue.c
benchmark/ms-queue/my_queue.h
notes/impl.txt
src/edu/uci/eecs/specCompiler/specExtraction/EntryPointConstruct.java [new file with mode: 0644]
src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java
src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java [new file with mode: 0644]
src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java
test.c [new file with mode: 0644]
test.h [new file with mode: 0644]

index 89efb8f..3af3a78 100644 (file)
@@ -83,6 +83,8 @@ class cliffc_hashtable {
                # correctness. The key thing is to identify all the commit point.
        
                @Begin
+               @Options:
+                       LANG = C;
                @Global_define:
                        @DeclareVar:
                        spec_hashtable<TypeK, TypeV*> map;
index 6a2737f..634a051 100644 (file)
@@ -58,6 +58,12 @@ static void reclaim(unsigned int node)
 
 void init_queue(queue_t *q, int num_threads)
 {
+       /**
+               @Begin
+               @Entry_point
+               @End
+       */
+
        int i, j;
 
        /* Initialize each thread's free list with INITIAL_FREE pointers */
@@ -78,41 +84,7 @@ void init_queue(queue_t *q, int num_threads)
 
 /**
        @Begin
-       @Global_define:
-               @DeclareVar:
-               typedef struct tag_elem {
-                       Tag id;
-                       unsigned int data;
-                       
-                       tag_elem(Tag _id, unsigned int _data) {
-                               id = _id;
-                               data = _data;
-                       }
-               } tag_elem_t;
-
-               spec_queue<tag_elem_t> queue;
-               Tag tag;
-               @InitVar:
-                       queue = spec_queue<tag_elem_t>();
-                       tag = Tag();
-       @Happens_before:
-               # Only check the happens-before relationship according to the id of the
-               # commit_point_set. For commit_point_set that has same ID, A -> B means
-               # B happens after the previous A.
-               Enqueue -> Dequeue
-       @End
-*/
-
-/**
-       @Begin
-       @Interface: Enqueue
-       @Commit_point_set: Enqueue_Success_Point
-       @ID: __sequential.tag.getCurAndInc()
-       @Action:
-               # __ID__ is an internal macro that refers to the id of the current
-               # interface call
-               @Code:
-               __sequential.queue.enqueue(tag_elem_t(__ID__, val));
+       @Interface_define: Enqueue
        @End
 */
 void enqueue(queue_t *q, unsigned int val)
@@ -165,16 +137,10 @@ void enqueue(queue_t *q, unsigned int val)
                        release, release);
 }
 
+
 /**
        @Begin
-       @Interface: Dequeue
-       @Commit_point_set: Dequeue_Success_Point
-       @ID: __sequential.queue.peak().tag
-       @Action:
-               @Code:
-               unsigned int _Old_Val = __sequential.queue.dequeue().data;
-       @Post_check:
-               _Old_Val == __RET__
+       @Interface_define: Dequeue
        @End
 */
 unsigned int dequeue(queue_t *q)
index c92e420..3a344d6 100644 (file)
@@ -26,6 +26,61 @@ typedef struct {
 } queue_t;
 
 void init_queue(queue_t *q, int num_threads);
+
+/**
+       @Begin
+       @Global_define:
+               @DeclareVar:
+               typedef struct tag_elem {
+                       Tag id;
+                       unsigned int data;
+                       
+                       tag_elem(Tag _id, unsigned int _data) {
+                               id = _id;
+                               data = _data;
+                       }
+               } tag_elem_t;
+
+               spec_queue<tag_elem_t> queue;
+               Tag tag;
+               @InitVar:
+                       queue = spec_queue<tag_elem_t>();
+                       tag = Tag();
+       @Happens_before:
+               # Only check the happens-before relationship according to the id of the
+               # commit_point_set. For commit_point_set that has same ID, A -> B means
+               # B happens after the previous A.
+               Enqueue -> Dequeue
+       @End
+*/
+
+
+
+/**
+       @Begin
+       @Interface: Enqueue
+       @Commit_point_set: Enqueue_Success_Point
+       @ID: __sequential.tag.getCurAndInc()
+       @Action:
+               # __ID__ is an internal macro that refers to the id of the current
+               # interface call
+               @Code:
+               __sequential.queue.enqueue(tag_elem_t(__ID__, val));
+       @End
+*/
 void enqueue(queue_t *q, unsigned int val);
+
+/**
+       @Begin
+       @Interface: Dequeue
+       @Commit_point_set: Dequeue_Success_Point
+       @ID: __sequential.queue.peak().tag
+       @Action:
+               @Code:
+               unsigned int _Old_Val = __sequential.queue.dequeue().data;
+       @Post_check:
+               _Old_Val == __RET__
+       @End
+*/
 unsigned int dequeue(queue_t *q);
 int get_thread_num();
index 67eeb67..12e364b 100644 (file)
 3. Happens-before initialization
   This concerns the place where we pass to the specanalysis the happens-before
   rules????
+
+4. To make implementation easier and the spec cleaner, we make a difference C
+  and C++ programs. Since C does not support template and class, we require
+  users to provide an entry point where we can initialize the sequential
+  variables. By default, it's a C++ program, and everything is wrapped in an
+  inner class because it can have easy initialization and template support.
+
+5. We add @Interface_define construct in the specification. Basically,
+  @Interface construct can be used in both interface declaration and interface
+  definition, if they are not separated. However, if they are, then @Interface
+  is used for the interface declaration and @Interface_define is for the
+  interface definition. This is redundant information, but it makes the
+  implementation much easier because we don't need to parse the C/C++ program.
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/EntryPointConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/EntryPointConstruct.java
new file mode 100644 (file)
index 0000000..df9d4d6
--- /dev/null
@@ -0,0 +1,7 @@
+package edu.uci.eecs.specCompiler.specExtraction;
+
+public class EntryPointConstruct extends Construct {
+       public String toString() {
+               return "@Entry_point";
+       }
+}
index 094361a..c2f0efb 100644 (file)
@@ -8,14 +8,16 @@ public class GlobalConstruct extends Construct {
        private final HashMap<String, HashSet<ConditionalInterface>> interfaceCluster;
        private final HashMap<ConditionalInterface, HashSet<ConditionalInterface>> originalHBRelations;
        public final HashMap<ConditionalInterface, HashSet<ConditionalInterface>> hbRelations;
+       public final HashMap<String, String> options;
        
-       public GlobalConstruct(SequentialDefineSubConstruct code) {
+       public GlobalConstruct(SequentialDefineSubConstruct code, HashMap<String, String> options) {
                this.code = code;
                this.interfaceCluster = new HashMap<String, HashSet<ConditionalInterface>>();
                this.originalHBRelations = new HashMap<ConditionalInterface, HashSet<ConditionalInterface>>();
                this.hbRelations = new HashMap<ConditionalInterface, HashSet<ConditionalInterface>>();
+               this.options = options;
        }
-       
+               
        public void addInterface2Cluster(String clusterName, ConditionalInterface condInterface) {
                if (!interfaceCluster.containsKey(clusterName)) {
                        interfaceCluster.put(clusterName, new HashSet<ConditionalInterface>());
diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java
new file mode 100644 (file)
index 0000000..920e301
--- /dev/null
@@ -0,0 +1,14 @@
+package edu.uci.eecs.specCompiler.specExtraction;
+
+public class InterfaceDefineConstruct extends Construct {
+       public final String name;
+       private String funcDecl;
+       
+       public InterfaceDefineConstruct(String name) {
+               this.name = name;
+       }
+       
+       public String toString() {
+               return "@Interface_define: " + name;
+       }
+}
index 3c462c1..1d34199 100644 (file)
@@ -71,11 +71,13 @@ public class SpecExtractor {
                                                                continue;
                                                        Construct inst = SpecParser.parseSpec(specText
                                                                        .toString());
-                                                       if (inst instanceof InterfaceConstruct) {
+                                                       if (inst instanceof InterfaceConstruct
+                                                                       || inst instanceof InterfaceDefineConstruct) {
                                                                funcDecl = readFunctionDecl(reader);
                                                                specConstruct = new SpecConstruct(
                                                                                specText.toString(), file,
-                                                                               _beginLineNum, _endLineNum, inst, funcDecl);
+                                                                               _beginLineNum, _endLineNum, inst,
+                                                                               funcDecl);
                                                        } else {
                                                                specConstruct = new SpecConstruct(
                                                                                specText.toString(), file,
@@ -83,7 +85,7 @@ public class SpecExtractor {
                                                        }
                                                        _constructs.add(specConstruct);
                                                        specText = new StringBuilder();
-//                                                     System.out.println(specConstruct);
+                                                       // System.out.println(specConstruct);
                                                }
                                        }
                                } else {
@@ -98,19 +100,20 @@ public class SpecExtractor {
                                                }
                                                Construct inst = SpecParser.parseSpec(specText
                                                                .toString());
-                                               if (inst instanceof InterfaceConstruct) {
+                                               if (inst instanceof InterfaceConstruct
+                                                               || inst instanceof InterfaceDefineConstruct) {
                                                        funcDecl = readFunctionDecl(reader);
                                                        specConstruct = new SpecConstruct(
-                                                                       specText.toString(), file,
-                                                                       _beginLineNum, _endLineNum, inst, funcDecl);
+                                                                       specText.toString(), file, _beginLineNum,
+                                                                       _endLineNum, inst, funcDecl);
                                                } else {
                                                        specConstruct = new SpecConstruct(
-                                                                       specText.toString(), file,
-                                                                       _beginLineNum, _endLineNum, inst);
+                                                                       specText.toString(), file, _beginLineNum,
+                                                                       _endLineNum, inst);
                                                }
                                                _constructs.add(specConstruct);
                                                specText = new StringBuilder();
-//                                             System.out.println(specConstruct);
+                                               // System.out.println(specConstruct);
                                        }
                                }
                        }
@@ -133,15 +136,14 @@ public class SpecExtractor {
                        e.printStackTrace();
                }
        }
-       
+
        private void printSpecInfo(File file, String text) {
                System.out.println("Error in spec!");
                System.out.println("File: " + file.getAbsolutePath());
-               System.out.println("Begin: "
-                               + _beginLineNum + "  End: " + _endLineNum);
+               System.out.println("Begin: " + _beginLineNum + "  End: " + _endLineNum);
                System.out.println(text);
        }
-       
+
        private boolean isComment(String specText) {
                if (specText.indexOf("@Begin") != -1)
                        return false;
@@ -181,7 +183,7 @@ public class SpecExtractor {
                else
                        return line.substring(i, j + 1);
        }
-       
+
        public ArrayList<SpecConstruct> getConstructs() {
                return this._constructs;
        }
diff --git a/test.c b/test.c
new file mode 100644 (file)
index 0000000..2dec27e
--- /dev/null
+++ b/test.c
@@ -0,0 +1,14 @@
+#include <stdio.h>
+#include "test.h"
+
+void _foo(struct Test t) {
+       printf("%d\n", t.x);
+}
+
+void foo(struct Test t) {
+       _foo(t);
+}
+
+int main() {
+       return 0;
+}
diff --git a/test.h b/test.h
new file mode 100644 (file)
index 0000000..fb016e4
--- /dev/null
+++ b/test.h
@@ -0,0 +1,7 @@
+struct Test {
+       int x;
+
+       Test() {
+               x = 2;
+       }
+};