From: Peizhao Ou <peizhaoo@uci.edu>
Date: Thu, 16 Jan 2014 01:47:54 +0000 (-0800)
Subject: minor fix
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=62d76554c8b9c023653f29487b796edf54511b57;p=cdsspec-compiler.git

minor fix
---

diff --git a/benchmark/mcs-lock/mcs-lock.h b/benchmark/mcs-lock/mcs-lock.h
index 6dc66ed..8ff58a2 100644
--- a/benchmark/mcs-lock/mcs-lock.h
+++ b/benchmark/mcs-lock/mcs-lock.h
@@ -4,31 +4,7 @@
 #include <unrelacy.h>
 
 
-/**
-	Properties to check:
-	1. At any point, only one thread can acquire the mutex; when any thread
-		nlock the mutex, he must have it in his hand.
-	2. The sequence of the lock is guaranteed, which means there is a queue for
-		all the lock operations.
-	####
-	3. Should establish the happens-before relationship between unlock and lock
-*/
 
-/**
-	@Begin
-	@Global_define:
-		# The invariant is that the thread that has a guard at the head of the
-		# queue should be the one who currently has the lock.
-	
-		int __lock_acquired = 0;
-		queue<guard*> __lock_waiting_queue;
-	
-	@Happens-before:
-		# Without any specifying, this means the beginning of a successful Unlock()
-		# happens before the end of the next successful Lock().
-		Unlock -> Lock
-	@End
-*/
 
 struct mcs_node {
 	std::atomic<mcs_node *> next;
@@ -40,12 +16,18 @@ struct mcs_node {
 	}
 };
 
+
 struct mcs_mutex {
 public:
 	// tail is null when lock is not held
 	std::atomic<mcs_node *> m_tail;
 
 	mcs_mutex() {
+		/**
+			@Begin
+	        @Entry_point
+			@End
+		*/
 		m_tail.store( NULL );
 	}
 	~mcs_mutex() {
@@ -62,22 +44,29 @@ public:
 		~guard() { m_t->unlock(this); }
 	};
 
+	/**
+		@Begin
+		@Options:
+			LANG = CPP;
+			CLASS = mcs_mutex;
+		@Global_define:
+			@DeclareVar:
+				bool _lock_acquired;
+			@InitVar:
+				_lock_acquired = false;
+		@Happens_before:
+			Unlock -> Lock
+		@End
+	*/
 
 	/**
 		@Begin
-		# This function will soon enqueue the current guard to the queue to make
-		# sure it will get fair lock successfully.
 		@Interface: Lock
-		@Commit_point_set: Lock_Enqueue_Point
+		@Commit_point_set: Lock_Enqueue_Point1 | Lock_Enqueue_Point2
+		@Check:
+			_lock_acquired == false;
 		@Action:
-			@Code:
-			__lock_waiting_queue.enqueue(I);
-		@Post_action:
-			__lock_acquired++;
-		@Post_check:
-			# Make sure when it successfully locks, the lock is not acquired yet
-			# and the locking is in a FIFO order
-			__lock_acquired == 1 && I == __lock_waiting_queue.peak()
+			_lock_acquired = true;
 		@End
 	*/
 	void lock(guard * I) {
@@ -91,11 +80,9 @@ public:
 		// publish my node as the new tail :
 		mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
 		/**
-			# Once the exchange completes, the thread already claimed the next
-			# available slot for the lock
 			@Begin
-			@Commit_point_check_define: true
-			@Label: Lock_Enqueue_Point
+			@Commit_point_define_check: pred == NULL
+			@Label: Lock_Enqueue_Point1
 			@End
 		*/
 		if ( pred != NULL ) {
@@ -111,7 +98,14 @@ public:
 			// wait on predecessor setting my flag -
 			rl::linear_backoff bo;
 			int my_gate = 1;
-			while ( (my_gate = me->gate.load(std::mo_acquire)) ) {
+			while (my_gate ) {
+				my_gate = me->gate.load(std::mo_acquire);
+				/**
+					@Begin
+					@Commit_point_define_check: my_gate == 0
+					@Label: Lock_Enqueue_Point2
+					@End
+				*/
 				thrd_yield();
 			}
 		}
@@ -121,13 +115,11 @@ public:
 		@Begin
 		@Interface: Unlock
 		@Commit_point_set:
-			Unlock = Unlock_Point_Success_1 | Unlock_Point_Success_2
+			Unlock_Point_Success_1 | Unlock_Point_Success_2
 		@Check:
-			lock_acquired == 1 && I == lock_waiting_queue.peak()
+			_lock_acquired == true
 		@Action:
-			@Code:
-			lock_acquired--;
-			lock_waiting_queue.dequeue();
+			_lock_acquired = false;
 		@End
 	*/
 	void unlock(guard * I) {
@@ -138,14 +130,16 @@ public:
 		{
 			mcs_node * tail_was_me = me;
 			bool success;
-			if ( (success = m_tail.compare_exchange_strong(
-				tail_was_me,NULL,std::mo_acq_rel)) ) {
-				/**
-					@Begin
-					@Commit_point_check_define: __ATOMIC_RET__ == true
-					@Label: Unlock_Point_Success_1
-					@End
-				*/
+			success = m_tail.compare_exchange_strong(
+				tail_was_me,NULL,std::mo_acq_rel);
+			/**
+				@Begin
+				@Commit_point_define_check: success == true
+				@Label: Unlock_Point_Success_1
+				@End
+			*/
+			if (success) {
+				
 				// got null in tail, mutex is unlocked
 				return;
 			}
@@ -167,9 +161,14 @@ public:
 		next->gate.store( 0, std::mo_release );
 		/**
 			@Begin
-			@Commit_point_check_define: true
+			@Commit_point_define_check: true
 			@Label: Unlock_Point_Success_2
 			@End
 		*/
 	}
 };
+/**
+	@Begin
+	@Class_end
+	@End
+*/
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
index 1e22706..802dd3e 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java
@@ -122,10 +122,15 @@ public class CodeGenerator {
 						new ArrayList<CodeAddition>());
 			}
 			codeAdditions.get(defineConstruct.file).add(addition);
-		} else { // No declaration needed but should add forward declaration
+		} else { // No declaration needed but should add forward declaration in
+					// Class
 			// Last generate the definition
 			newCode = new ArrayList<String>();
-			newCode.addAll(CodeVariables.generateInterfaceWrapperDeclaration(_semantics, construct));
+			if (_semantics.getOption("CLASS") == null) {
+				newCode.addAll(CodeVariables
+						.generateInterfaceWrapperDeclaration(_semantics,
+								construct));
+			}
 			newCode.addAll(CodeVariables.generateInterfaceWrapperDefinition(
 					_semantics, construct));
 			lineNum = construct.beginLineNum;
@@ -178,6 +183,20 @@ public class CodeGenerator {
 		codeAdditions.get(construct.file).add(addition);
 	}
 
+	/**
+	private void ClassEnd2Code(ClassEndConstruct construct) {
+		int lineNum = construct.beginLineNum;
+		ArrayList<String> newCode = CodeVariables.generateStaticVarDefine(_semantics,
+				_semantics.getGlobalConstruct());
+
+		CodeAddition addition = new CodeAddition(lineNum, newCode);
+		if (!codeAdditions.containsKey(construct.file)) {
+			codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
+		}
+		codeAdditions.get(construct.file).add(addition);
+	}
+	*/
+	
 	private void EntryPoint2Code(EntryPointConstruct construct) {
 		int lineNum = construct.beginLineNum;
 		ArrayList<String> newCode = new ArrayList<String>();
@@ -229,6 +248,12 @@ public class CodeGenerator {
 				EntryPoint2Code((EntryPointConstruct) construct);
 			}
 		}
+
+//		ClassEndConstruct endConstruct = _semantics.getClassEndConstruct();
+//		if (endConstruct != null) {
+//			ClassEnd2Code(endConstruct);
+//		}
+
 		// Sort code additions
 		HashSet<String> headers = CodeVariables.getAllHeaders(_semantics);
 		ArrayList<String> headerCode = new ArrayList<String>(headers.size());
@@ -257,22 +282,28 @@ public class CodeGenerator {
 	public static void main(String[] argvs) {
 		String homeDir = Environment.HOME_DIRECTORY;
 		File[] srcFiles = {
-//				new File(homeDir
-//				+ "/benchmark/linuxrwlocks/linuxrwlocks.c") };
-		// new File(homeDir
-		// +
-		// "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
-		// };
-		 new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
-		 new File(homeDir + "/benchmark/ms-queue/main.c"),
-		 new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
-
-//		 new File(homeDir + "/benchmark/read-copy-update/rcu.cc") };
-		 
-//		new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.c"),
-//		 new File(homeDir + "/benchmark/chase-lev-deque-bugfix/main.c"),
-//		 new File(homeDir + "/benchmark/chase-lev-deque-bugfix/deque.h") };
-		
+				// new File(homeDir
+				// + "/benchmark/linuxrwlocks/linuxrwlocks.c") };
+				// new File(homeDir
+				// +
+				// "/benchmark/cliffc-hashtable/simplified_cliffc_hashtable.h"),
+				// };
+				// new File(homeDir + "/benchmark/ms-queue/my_queue.c"),
+				// new File(homeDir + "/benchmark/ms-queue/main.c"),
+				// new File(homeDir + "/benchmark/ms-queue/my_queue.h") };
+
+				// new File(homeDir + "/benchmark/read-copy-update/rcu.cc") };
+
+				// new File(homeDir +
+				// "/benchmark/chase-lev-deque-bugfix/deque.c"),
+				// new File(homeDir +
+				// "/benchmark/chase-lev-deque-bugfix/main.c"),
+				// new File(homeDir +
+				// "/benchmark/chase-lev-deque-bugfix/deque.h") };
+
+				new File(homeDir + "/benchmark/mcs-lock/mcs-lock.cc"),
+				new File(homeDir + "/benchmark/mcs-lock/mcs-lock.h") };
+
 		CodeGenerator gen = new CodeGenerator(srcFiles);
 		gen.generateCode();
 	}
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
index aeace48..0953eef 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java
@@ -374,9 +374,11 @@ public class CodeVariables {
 		String interfaceSize = Integer
 				.toString(semantics.interfaceName2Construct.size());
 		newCode.add(DEFINE("INTERFACE_SIZE", interfaceSize));
-		newCode.add(DECLARE("void**", "func_ptr_table"));
+		// Make it static
+		newCode.add("static " + DECLARE("void**", "func_ptr_table"));
 		// Happens-before initialization rules
-		newCode.add(DECLARE(ANNO_HB_INIT + "**", "hb_init_table"));
+		// Should make it static
+		newCode.add("static " + DECLARE(ANNO_HB_INIT + "**", "hb_init_table"));
 
 		newCode.add("");
 		newCode.add(COMMENT("Define function for sequential code initialization"));
@@ -438,7 +440,7 @@ public class CodeVariables {
 		String templateDecl = semantics.getTemplateFullStr();
 		if (templateList == null) {
 			newCode.add(DECLARE("void**", varPrefix + "func_ptr_table"));
-			newCode.add(DECLARE("void**", varPrefix + "hb_init_table"));
+			newCode.add(DECLARE("anno_hb_init**", varPrefix + "hb_init_table"));
 			for (int i = 0; i < construct.code.declareVar.size(); i++) {
 				VariableDeclaration varDecl = construct.code.declareVar.get(i);
 				newCode.add(DECLARE(varDecl.type, varPrefix + varDecl.name));
diff --git a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
index 6073230..580120b 100644
--- a/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
+++ b/src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java
@@ -40,6 +40,7 @@ public class SemanticsChecker {
 	private ArrayList<EntryPointConstruct> entryPointConstructs;
 	private ClassBeginConstruct classBeginConstruct;
 	private ClassEndConstruct classEndConstruct;
+	private GlobalConstruct globalConstruct;
 	
 	private String templateStr;
 	private String templateFullStr;
@@ -96,6 +97,10 @@ public class SemanticsChecker {
 	public String getClassName() {
 		return this.className;
 	}
+	
+	public GlobalConstruct getGlobalConstruct() {
+		return this.globalConstruct;
+	}
 
 	public HashMap<ConditionalInterface, HashSet<ConditionalInterface>> getHBConditions() {
 		return this.hbConditions;
@@ -210,6 +215,7 @@ public class SemanticsChecker {
 			Construct construct = constructs.get(i);
 			if (construct instanceof GlobalConstruct) {
 				GlobalConstruct theConstruct = (GlobalConstruct) construct;
+				globalConstruct = theConstruct;
 				if (!hasGlobalConstruct)
 					hasGlobalConstruct = true;
 				else {
@@ -279,6 +285,7 @@ public class SemanticsChecker {
 				
 			} else if (construct instanceof ClassEndConstruct) {
 				classEndConstruct = (ClassEndConstruct) construct;
+				className = getOption("CLASS");
 			}
 		}
 	}