From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 4 Feb 2016 00:24:13 +0000 (-0800)
Subject: edits
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=c46d1e2c3835a9c637375a79b82fb36bf96116c7

edits
---

diff --git a/notes/definition.cc b/notes/definition.cc
index fda4eba..99d5a93 100644
--- a/notes/definition.cc
+++ b/notes/definition.cc
@@ -12,24 +12,43 @@
 
 using namespace std;
 
-typedef struct MethodCall {
+struct MethodCall;
+
+typedef MethodCall *Method;
+typedef set<Method> *MethodSet;
+
+struct MethodCall {
 	string interfaceName; // The interface label name
 	void *value; // The pointer that points to the struct that have the return
 				 // value and the arguments
 	void *state; // The pointer that points to the struct that represents
 					  // the state
-	set<MethodCall*> *prev; // Method calls that are hb right before me
-	set<MethodCall*> *next; // Method calls that are hb right after me
-	set<MethodCall*> *concurrent; // Method calls that are concurrent with me
-} MethodCall;
+	MethodSet prev; // Method calls that are hb right before me
+	MethodSet next; // Method calls that are hb right after me
+	MethodSet concurrent; // Method calls that are concurrent with me
+
+	MethodCall(string name) : MethodCall() { interfaceName = name; }
+	
+	MethodCall() : interfaceName(""), prev(new set<Method>),
+		next(new set<Method>), concurrent(new set<Method>) { }
+
+	void addPrev(Method m) { prev->insert(m); }
+
+	void addNext(Method m) { next->insert(m); }
+	
+	void addConcurrent(Method m) { concurrent->insert(m); }
+
+};
 
-typedef MethodCall *Method;
-typedef set<Method> *MethodSet;
 
 typedef vector<int> IntVector;
 typedef list<int> IntList;
 typedef set<int> IntSet;
 
+typedef vector<double> DoubleVector;
+typedef list<double> DoubleList;
+typedef set<double> DoubleSet;
+
 /********** More general specification-related types and operations **********/
 
 #define NewMethodSet new set<Method>
@@ -97,19 +116,19 @@ typedef set<int> IntSet;
 /**
 	We provide a more general subset operation that takes a plain boolean
 	expression on each item (access by the name "ITEM") of the set, and put it
-	into a new set if the boolean expression (Guard) on that item holds. This is
-	used as the second arguments of the Subset operation. An example to extract
-	a subset of positive elements on an IntSet "s" would be "Subset(s,
+	into a new set if the boolean expression (Guard) on that item holds.  This
+	is used as the second arguments of the Subset operation. An example to
+	extract a subset of positive elements on an IntSet "s" would be "Subset(s,
 	GeneralGuard(int, ITEM > 0))"
 */
 #define GeneralGuard(type, expression)  std::function<bool(type)> ( \
-	[](type ITEM) -> bool { return (expression);}) \
+	[&](type ITEM) -> bool { return (expression);}) \
 
 /**
 	This is a more specific guard designed for the Method (MethodCall*). It
 	basically wrap around the GeneralGuard with the type Method. An example to
-	extract the subset of method calls in the PREV set whose state "x" is
-	equal to "val" would be "Subset(PREV, Guard(STATE(x) == val))"
+	extract the subset of method calls in the PREV set whose state "x" is equal
+	to "val" would be "Subset(PREV, Guard(STATE(x) == val))"
 */
 #define Guard(expression) GeneralGuard(Method, expression)
 
@@ -117,9 +136,8 @@ typedef set<int> IntSet;
 	A general subset operation that takes a condition and returns all the item
 	for which the boolean guard holds.
 */
-template <class T>
-inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
-	set<T> *res = new set<T>;
+inline MethodSet Subset(MethodSet original, std::function<bool(Method)> condition) {
+	MethodSet res = new SnapSet<Method>;
 	ForEach (_M, original) {
 		if (condition(_M))
 			res->insert(_M);
@@ -327,12 +345,16 @@ int main() {
 	m->value = ld;
 	ms->insert(m);
 
-	MakeSet(int, ms, newis, STATE(x));
+	//MakeSet(int, ms, newis, STATE(x));
 	//cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
-	cout << "HasItem=" << HasItem(ms, Guard(STATE(x) == 2)) << endl;
-	ForEach (i, newis) {
+	
+	int x = 2;
+	int y = 2;
+	cout << "HasItem=" << HasItem(ms, Guard(STATE(x) == x && y == 0)) << endl;
+	
+	//ForEach (i, newis) {
 		//cout << "elem: " << i << endl;
-	}
+	//}
 
 
 	//Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
diff --git a/notes/register-example/Makefile b/notes/register-example/Makefile
new file mode 100644
index 0000000..618b173
--- /dev/null
+++ b/notes/register-example/Makefile
@@ -0,0 +1,12 @@
+include ../benchmarks.mk
+
+TESTNAME = register
+all: $(TESTNAME)
+
+CFLAGS := $(CFLAGS) --std=c++11
+
+$(TESTNAME): $(TESTNAME).cc $(TESTNAME).h
+	$(CXX) -o $@ $< $(CFLAGS) $(LDFLAGS)
+
+clean:
+	rm -f $(TESTNAME) *.o 
diff --git a/notes/register-example/cdsspec-generated.h b/notes/register-example/cdsspec-generated.h
new file mode 100644
index 0000000..dab50eb
--- /dev/null
+++ b/notes/register-example/cdsspec-generated.h
@@ -0,0 +1,152 @@
+#include <cdsannotate.h>
+#include <modeltypes.h>
+#include <atomic>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "mymemory.h"
+#include "specannotation.h"
+#include "cdsspec.h"
+#include "methodcall.h"
+
+using namespace std;
+
+typedef struct StateStruct {
+	int val;
+
+	SNAPSHOTALLOC
+} StateStruct;
+
+typedef struct LOAD {
+	int RET;
+	atomic_int *loc;
+} LOAD;
+
+typedef struct STORE {
+	atomic_int *loc;
+	int val;
+} STORE;
+
+inline void _initial(Method m) {
+	StateStruct *state = new StateStruct;
+	state->val = 0;
+	m->state = state;
+}
+
+inline void _copyState(Method dest, Method src) {
+	StateStruct *stateSrc = (StateStruct*) src;
+	StateStruct *stateDest = (StateStruct*) dest;
+	stateDest->val = stateSrc->val;
+}
+
+inline bool _checkCommutativity1(Method m1, Method m2) {
+	if (m1->interfaceName == "LOAD" && m2->interfaceName == "LOAD") {
+		if (true)
+			return true;
+		else
+			return false;
+	}
+	return false;
+}
+
+inline bool _checkCommutativity2(Method m1, Method m2) {
+	if (m1->interfaceName == "STORE" && m2->interfaceName == "LOAD") {
+		if (true)
+			return true;
+		else
+			return false;
+	}
+	return false;
+}
+
+inline bool _checkCommutativity3(Method m1, Method m2) {
+	if (m1->interfaceName == "STORE" && m2->interfaceName == "STORE") {
+		if (true)
+			return true;
+		else
+			return false;
+	}
+	return false;
+}
+
+inline void _LOAD_Transition(Method _M, Method _exec) {
+	return;
+}
+
+inline bool _LOAD_PreCondition(Method _M) {
+	int RET = ((LOAD*) _M->value)->RET;
+	atomic_int *loc = ((LOAD*) _M->value)->loc;
+	return HasItem(PREV, Guard(STATE(val) == RET && loc));
+}
+
+inline void _LOAD_SideEffect(Method _M) {
+	int RET = ((LOAD*) _M->value)->RET;
+	atomic_int *loc = ((LOAD*) _M->value)->loc;
+	STATE(val) = RET;
+}
+
+inline void _STORE_Transition(Method _M, Method _exec) {
+	return;
+}
+
+inline void _STORE_SideEffect(Method _M) {
+	atomic_int *loc = ((STORE*) _M->value)->loc;
+	int val = ((STORE*) _M->value)->val;
+	STATE(val) = val;
+}
+
+inline void _createInitAnnotation() {
+	int CommuteRuleSize = 3;
+	void *raw = CommutativityRule::operator new[](sizeof(CommutativityRule) * CommuteRuleSize);
+	CommutativityRule *commuteRules = static_cast<CommutativityRule*>(raw);
+
+	// Initialize commutativity rule 1
+	new( &commuteRules[0] )CommutativityRule("LOAD", "LOAD", "LOAD <-> LOAD (true)", _checkCommutativity1);
+	// Initialize commutativity rule 2
+	new( &commuteRules[1] )CommutativityRule("Store", "LOAD", "STORE <-> LOAD (true)", _checkCommutativity2);
+	// Initialize commutativity rule 3
+	new( &commuteRules[2] )CommutativityRule("STORE", "STORE", "STORE <-> STORE (true)", _checkCommutativity3);
+
+	// Initialize AnnoInit
+	AnnoInit *anno = new AnnoInit(_initial, _copyState, commuteRules, CommuteRuleSize);
+
+	// Initialize StateFunctions map
+	StateFunctions *stateFuncs;
+
+	// StateFunction for LOAD
+	stateFuncs = new StateFunctions("LOAD", _LOAD_Transition, NULL, _LOAD_PreCondition, _LOAD_SideEffect, NULL);
+	anno->addInterfaceFunctions("LOAD", stateFuncs);
+	// StateFunction for STORE 
+	stateFuncs = new StateFunctions("STORE", _STORE_Transition, NULL, NULL, _STORE_SideEffect, NULL);
+	anno->addInterfaceFunctions("STORE", stateFuncs);
+
+	// Create and instrument with the INIT annotation
+	cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, anno));
+}
+
+inline Method _createInterfaceBeginAnnotation(string name) {
+	Method cur = new MethodCall(name);
+	// Create and instrument with the INTERFACE_BEGIN annotation
+	cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INTERFACE_BEGIN, cur));
+	return cur;
+}
+
+inline void _createOPDefineAnnotation() {
+	cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_DEFINE, NULL));
+}
+
+inline void _createPotentialOPAnnotation(string label) {
+	cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(POTENTIAL_OP, new AnnoPotentialOP(label)));
+}
+
+inline void _createOPCheckAnnotation(string label) {
+	cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CHECK, new AnnoOPCheck(label)));
+}
+
+inline void _createOPClearAnnotation() {
+	cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR, NULL));
+}
+
+inline void _createOPClearDefineAnnotation() {
+	cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR_DEFINE, NULL));
+}
diff --git a/notes/register-example/register.cc b/notes/register-example/register.cc
new file mode 100644
index 0000000..7f62bb7
--- /dev/null
+++ b/notes/register-example/register.cc
@@ -0,0 +1,99 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "librace.h"
+#include "register.h"
+
+/**	@DeclareState: int val;
+	@Initial: val = 0;
+	@Commutativity: LOAD <-> LOAD (true)
+	@Commutativity: STORE <-> LOAD (true)
+	@Commutativity: STORE <-> STORE (true)
+*/
+
+/** @Interface: LOAD
+	@PreCondition:
+	return HasItem(PREV, STATE(val) == RET);
+	@SideEffect: STATE(val) = RET;
+
+*/
+int Load_WRAPPER__(atomic_int *loc) {
+	return loc->load(memory_order_acquire);
+}
+
+int Load(atomic_int *loc) {
+	// Instrument with the INTERFACE_BEGIN annotation
+	Method cur = _createInterfaceBeginAnnotation("LOAD");
+	// Call the actual function
+	int RET = Load_WRAPPER__(loc);
+	
+	// Initialize the value struct
+	LOAD *value = new LOAD;
+	value->RET = RET;
+	value->loc = loc;
+
+	// Store the value info into the current MethodCall
+	cur->value = value;
+
+	// Return if there exists a return value
+	return RET;
+}
+
+/** @Interface: STORE 
+	@SideEffect: STATE(val) = val;
+
+*/
+void Store_WRAPPER__(atomic_int *loc, int val) {
+	loc->store(val, memory_order_release);
+}
+
+void Store(atomic_int *loc, int val) {
+	// Instrument with the INTERFACE_BEGIN annotation
+	Method cur = _createInterfaceBeginAnnotation("STORE");
+	// Call the actual function
+	Store_WRAPPER__(loc, val);
+	
+	// Initialize the value struct
+	STORE *value = new STORE;
+	value->loc = loc;
+	value->val = val;
+
+	// Store the value info into the current MethodCall
+	cur->value = value;
+}
+
+static void a(void *obj)
+{
+	Store(&x, 1);
+	Store(&x, 2);
+}
+
+static void b(void *obj)
+{
+	Store(&x, 3);
+}
+
+static void c(void *obj)
+{
+	int r1 = Load(&x);
+	int r2 = Load(&x);
+}
+
+int user_main(int argc, char **argv)
+{
+	thrd_t t1, t2, t3;
+
+	/** @Entry */
+	_createInitAnnotation();
+
+	thrd_create(&t1, (thrd_start_t)&a, NULL);
+	thrd_create(&t2, (thrd_start_t)&b, NULL);
+	thrd_create(&t3, (thrd_start_t)&c, NULL);
+
+	thrd_join(t1);
+	thrd_join(t2);
+	thrd_join(t3);
+
+	return 0;
+}
diff --git a/notes/register-example/register.cc.original b/notes/register-example/register.cc.original
new file mode 100644
index 0000000..bd8d032
--- /dev/null
+++ b/notes/register-example/register.cc.original
@@ -0,0 +1,65 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "librace.h"
+#include "register.h"
+
+/**	@DeclareState: int val;
+	@Initial: val = 0;
+	@Commutativity: LOAD <-> LOAD (true)
+	@Commutativity: STORE <-> LOAD (true)
+	@Commutativity: STORE <-> STORE (true)
+*/
+
+/** @Interface: LOAD
+	@PreCondition:
+	return HasItem(PREV, STATE(val) == RET);
+	@SideEffect: STATE(val) = RET;
+
+*/
+int Load(atomic_int *loc) {
+	return loc->load(memory_order_acquire);
+}
+
+/** @Interface: STORE 
+	@SideEffect: STATE(val) = val;
+
+*/
+void Store(atomic_int *loc, int val) {
+	loc->store(val, memory_order_release);
+}
+
+static void a(void *obj)
+{
+	Store(&x, 1);
+	Store(&x, 2);
+}
+
+static void b(void *obj)
+{
+	Store(&x, 3);
+}
+
+static void c(void *obj)
+{
+	int r1 = Load(&x);
+	int r2 = Load(&x);
+}
+
+int user_main(int argc, char **argv)
+{
+	thrd_t t1, t2, t3;
+
+	/** @Entry */
+
+	thrd_create(&t1, (thrd_start_t)&a, NULL);
+	thrd_create(&t2, (thrd_start_t)&b, NULL);
+	thrd_create(&t3, (thrd_start_t)&c, NULL);
+
+	thrd_join(t1);
+	thrd_join(t2);
+	thrd_join(t3);
+
+	return 0;
+}
diff --git a/notes/register-example/register.h b/notes/register-example/register.h
new file mode 100644
index 0000000..51c350a
--- /dev/null
+++ b/notes/register-example/register.h
@@ -0,0 +1,11 @@
+#include <stdio.h>
+#include <stdatomic.h>
+
+#include "librace.h"
+#include "cdsspec-generated.h"
+
+atomic_int x;
+
+int Load(atomic_int *loc);
+
+void Store(atomic_int *loc, int val);