From 62d76554c8b9c023653f29487b796edf54511b57 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Wed, 15 Jan 2014 17:47:54 -0800 Subject: [PATCH] minor fix --- benchmark/mcs-lock/mcs-lock.h | 107 +++++++++--------- .../codeGenerator/CodeGenerator.java | 67 ++++++++--- .../codeGenerator/CodeVariables.java | 8 +- .../codeGenerator/SemanticsChecker.java | 7 ++ 4 files changed, 114 insertions(+), 75 deletions(-) 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 -/** - 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 __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 next; @@ -40,12 +16,18 @@ struct mcs_node { } }; + struct mcs_mutex { public: // tail is null when lock is not held std::atomic 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()); } 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(); - 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 newCode = CodeVariables.generateStaticVarDefine(_semantics, + _semantics.getGlobalConstruct()); + + CodeAddition addition = new CodeAddition(lineNum, newCode); + if (!codeAdditions.containsKey(construct.file)) { + codeAdditions.put(construct.file, new ArrayList()); + } + codeAdditions.get(construct.file).add(addition); + } + */ + private void EntryPoint2Code(EntryPointConstruct construct) { int lineNum = construct.beginLineNum; ArrayList newCode = new ArrayList(); @@ -229,6 +248,12 @@ public class CodeGenerator { EntryPoint2Code((EntryPointConstruct) construct); } } + +// ClassEndConstruct endConstruct = _semantics.getClassEndConstruct(); +// if (endConstruct != null) { +// ClassEnd2Code(endConstruct); +// } + // Sort code additions HashSet headers = CodeVariables.getAllHeaders(_semantics); ArrayList headerCode = new ArrayList(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 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> 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"); } } } -- 2.34.1