From: Peizhao Ou Date: Fri, 18 Oct 2013 01:14:58 +0000 (-0700) Subject: lots of change and add notes X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=efe3f6d7242a505f593c8535c7c1339ccc1bd11a lots of change and add notes --- diff --git a/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h b/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h index 89efb8f..3af3a78 100644 --- a/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h +++ b/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h @@ -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 map; diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c index 6a2737f..634a051 100644 --- a/benchmark/ms-queue/my_queue.c +++ b/benchmark/ms-queue/my_queue.c @@ -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 queue; - Tag tag; - @InitVar: - queue = spec_queue(); - 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) diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h index c92e420..3a344d6 100644 --- a/benchmark/ms-queue/my_queue.h +++ b/benchmark/ms-queue/my_queue.h @@ -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 queue; + Tag tag; + @InitVar: + queue = spec_queue(); + 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(); diff --git a/notes/impl.txt b/notes/impl.txt index 67eeb67..12e364b 100644 --- a/notes/impl.txt +++ b/notes/impl.txt @@ -18,3 +18,16 @@ 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 index 0000000..df9d4d6 --- /dev/null +++ b/src/edu/uci/eecs/specCompiler/specExtraction/EntryPointConstruct.java @@ -0,0 +1,7 @@ +package edu.uci.eecs.specCompiler.specExtraction; + +public class EntryPointConstruct extends Construct { + public String toString() { + return "@Entry_point"; + } +} diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java index 094361a..c2f0efb 100644 --- a/src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java +++ b/src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java @@ -8,14 +8,16 @@ public class GlobalConstruct extends Construct { private final HashMap> interfaceCluster; private final HashMap> originalHBRelations; public final HashMap> hbRelations; + public final HashMap options; - public GlobalConstruct(SequentialDefineSubConstruct code) { + public GlobalConstruct(SequentialDefineSubConstruct code, HashMap options) { this.code = code; this.interfaceCluster = new HashMap>(); this.originalHBRelations = new HashMap>(); this.hbRelations = new HashMap>(); + this.options = options; } - + public void addInterface2Cluster(String clusterName, ConditionalInterface condInterface) { if (!interfaceCluster.containsKey(clusterName)) { interfaceCluster.put(clusterName, new HashSet()); diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java b/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java new file mode 100644 index 0000000..920e301 --- /dev/null +++ b/src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java @@ -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; + } +} diff --git a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java index 3c462c1..1d34199 100644 --- a/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java +++ b/src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java @@ -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 getConstructs() { return this._constructs; } diff --git a/test.c b/test.c new file mode 100644 index 0000000..2dec27e --- /dev/null +++ b/test.c @@ -0,0 +1,14 @@ +#include +#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 index 0000000..fb016e4 --- /dev/null +++ b/test.h @@ -0,0 +1,7 @@ +struct Test { + int x; + + Test() { + x = 2; + } +};