# correctness. The key thing is to identify all the commit point.
@Begin
+ @Options:
+ LANG = C;
@Global_define:
@DeclareVar:
spec_hashtable<TypeK, TypeV*> map;
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 */
/**
@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)
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)
} 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();
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.
--- /dev/null
+package edu.uci.eecs.specCompiler.specExtraction;
+
+public class EntryPointConstruct extends Construct {
+ public String toString() {
+ return "@Entry_point";
+ }
+}
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>());
--- /dev/null
+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;
+ }
+}
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,
}
_constructs.add(specConstruct);
specText = new StringBuilder();
-// System.out.println(specConstruct);
+ // System.out.println(specConstruct);
}
}
} else {
}
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);
}
}
}
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;
else
return line.substring(i, j + 1);
}
-
+
public ArrayList<SpecConstruct> getConstructs() {
return this._constructs;
}
--- /dev/null
+#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;
+}
--- /dev/null
+struct Test {
+ int x;
+
+ Test() {
+ x = 2;
+ }
+};
projects / cdsspec-compiler.git / commitdiff