add destructors

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
index 41a5bddfe32eefba8c061e6455fc99f152dc8fd6..22e39084f2d696ca773c15566319696942a6c030 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGenerator.java
@@ -326,14 +326,9 @@ public class CodeGenerator {
        }
 
        static public void main(String[] args) {
-//             String[] dirNames = { 
-//                             Environment.REGISTER, 
-//                             Environment.MS_QUEUE,
-//                             Environment.LINUXRWLOCKS,
-//                             Environment.MCS_LOCK,
-//                             Environment.DEQUE, 
-//                             Environment.TREIBER_STACK };
+       
                String[] dirNames = args;
+//             String[] dirNames = Environment.Benchmarks;
 
                for (int i = 0; i < dirNames.length; i++) {
                        String dirName = dirNames[i];

diff --git a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
index 73176b9566d82152f36f4000db198718aa1d108e..694695cf48ca9db30cae73666101a9ccb75ef066 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
+++ b/src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java
@@ -140,8 +140,12 @@ public class CodeGeneratorUtils {
                code.addLine("*/");
                code.addLine("");
 
-               code.addLine("#ifndef _" + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-', '_') + "_H");
-               code.addLine("#define _" + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-', '_') + "_H");
+               code.addLine("#ifndef _"
+                               + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
+                                               '_') + "_H");
+               code.addLine("#define _"
+                               + SpecNaming.CDSSpecGeneratedName.toUpperCase().replace('-',
+                                               '_') + "_H");
                code.addLine("");
 
                // FIXME: We have included ad-hoc header files here
@@ -166,9 +170,6 @@ public class CodeGeneratorUtils {
                code.addLine("");
 
                code.addLine(ShortComment("Declaration of some c-strings (CSTR)"));
-               code.addLine(ShortComment("A special empty string"));
-               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.EmptyCString));
-               code.addLine("");
 
                // Interface name strings
                code.addLine(ShortComment("Interface name strings"));
@@ -176,70 +177,34 @@ public class CodeGeneratorUtils {
                        ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
                        for (InterfaceConstruct construct : list) {
                                String name = construct.getName();
-                               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(name)));
+                               code.addLine(Declare("extern " + SpecNaming.CString,
+                                               SpecNaming.AppendStr(name)));
                        }
                }
                code.addLine("");
 
-               // Commutativity rule strings
-               code.addLine(ShortComment("Commutativity rule strings"));
-               for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-                       code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.Commutativity + i)));
-               }
-               code.addLine("");
-
                // Ordering points label strings
                code.addLine(ShortComment("Ordering points label strings"));
                for (String label : OPLabelSet) {
-                       code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(label)));
+                       code.addLine(Declare("extern " + SpecNaming.CString,
+                                       SpecNaming.AppendStr(label)));
                }
                code.addLine("");
 
-               // Special function name strings
-               code.addLine(ShortComment("Special function name strings"));
-               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.InitalState)));
-               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.CopyState)));
-               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.FinalState)));
-               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.PrintState)));
-               code.addLine("");
-
-               // Interface name strings
-               for (File file : interfaceListMap.keySet()) {
-                       ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
-                       for (InterfaceConstruct construct : list) {
-                               String name = construct.getName();
-                               code.addLine(ShortComment(name + " function strings"));
-                               // Transition
-                               String tmpFunc = name + "_" + SpecNaming.Transition;
-                               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-                               // PreCondition
-                               tmpFunc = name + "_" + SpecNaming.PreCondition;
-                               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-                               // SideEffect
-                               tmpFunc = name + "_" + SpecNaming.SideEffect;
-                               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-                               // PostCondition
-                               tmpFunc = name + "_" + SpecNaming.PostCondition;
-                               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-                               // Print
-                               tmpFunc = name + "_" + SpecNaming.PrintValue;
-                               code.addLine(Declare("extern " + SpecNaming.CString, SpecNaming.AppendStr(tmpFunc)));
-                               code.addLine("");
-                       }
-               }
-
                // Declare customized value struct
                for (File file : interfaceListMap.keySet()) {
                        ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
                        for (InterfaceConstruct construct : list) {
                                // Declare custom value struct for the interface
                                String name = construct.getName();
-                               code.addLine(ShortComment("Declare custom value struct for " + name));
+                               code.addLine(ShortComment("Declare custom value struct for "
+                                               + name));
                                code.addLine("typedef struct " + name + " {");
                                FunctionHeader funcHeader = construct.getFunctionHeader();
                                // RET
                                if (!funcHeader.returnType.equals("void"))
-                                       code.addLine(TabbedLine(Declare(funcHeader.returnType, SpecNaming.RET)));
+                                       code.addLine(TabbedLine(Declare(funcHeader.returnType,
+                                                       SpecNaming.RET)));
                                // Arguments
                                for (VariableDeclaration decl : funcHeader.args) {
                                        code.addLine(TabbedLine(Declare(decl)));
@@ -249,75 +214,6 @@ public class CodeGeneratorUtils {
                        }
                }
 
-               // Declare @Initial
-               code.addLine(ShortComment("Declare @" + SpecNaming.InitalState));
-               code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "(" + SpecNaming.Method + " "
-                               + SpecNaming.Method1 + ");");
-               code.addLine("");
-               // Declare @Copy
-               code.addLine(ShortComment("Declare @" + SpecNaming.CopyState));
-               code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "(" + SpecNaming.Method + " " + "dest, "
-                               + SpecNaming.Method + " src);");
-               code.addLine("");
-               // Declare @Print
-               code.addLine(ShortComment("Declare @" + SpecNaming.PrintState));
-               if (!globalConstruct.printState.isEmpty()) {
-                       code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "(" + SpecNaming.Method + " "
-                                       + SpecNaming.Method1 + ");");
-                       code.addLine("");
-               }
-
-               // Declare @Commutativity
-               code.addLine(ShortComment("Declare commutativity checking functions"));
-               for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-                       code.addLine("bool _check" + SpecNaming.Commutativity + i + "(" + SpecNaming.Method + " m1, "
-                                       + SpecNaming.Method + " m2);");
-               }
-               code.addLine("");
-
-               // Declare customized interface functions
-               for (File file : interfaceListMap.keySet()) {
-                       ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
-                       for (InterfaceConstruct construct : list) {
-                               // Declare interface functions
-                               String name = construct.getName();
-                               code.addLine("/**********    " + name + " functions    **********/");
-                               // Declare @Transition for INTERFACE
-                               code.addLine(ShortComment("Declare @" + SpecNaming.Transition + " for " + name));
-                               code.addLine("void _" + name + "_" + SpecNaming.Transition + "(" + SpecNaming.Method + " "
-                                               + SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ");");
-                               code.addLine("");
-                               // Declare @PreCondition
-                               if (!construct.preCondition.isEmpty()) {
-                                       code.addLine(ShortComment("Declare @" + SpecNaming.PreCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_" + SpecNaming.PreCondition + "(" + SpecNaming.Method + " "
-                                                       + SpecNaming.Method1 + ");");
-                                       code.addLine("");
-                               }
-                               // Declare @SideEffect
-                               if (!construct.sideEffect.isEmpty()) {
-                                       code.addLine(ShortComment("Declare @" + SpecNaming.SideEffect + " for " + name));
-                                       code.addLine("void _" + name + "_" + SpecNaming.SideEffect + "(" + SpecNaming.Method + " "
-                                                       + SpecNaming.Method1 + ");");
-                                       code.addLine("");
-                               }
-                               // Declare @PostCondition
-                               if (!construct.postCondition.isEmpty()) {
-                                       code.addLine(ShortComment("Declare @" + SpecNaming.PostCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_" + SpecNaming.PostCondition + "(" + SpecNaming.Method + " "
-                                                       + SpecNaming.Method1 + ");");
-                                       code.addLine("");
-                               }
-                               // Declare @Print
-                               if (!construct.print.isEmpty()) {
-                                       code.addLine(ShortComment("Declare @" + SpecNaming.PrintValue + " for " + name));
-                                       code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
-                                                       + SpecNaming.Method1 + ");");
-                                       code.addLine("");
-                               }
-                       }
-               }
-
                // Declare INIT annotation instrumentation function
                code.addLine(ShortComment("Declare INIT annotation instrumentation function"));
                code.addLine("void _createInitAnnotation();");
@@ -377,14 +273,31 @@ public class CodeGeneratorUtils {
                        code.addLine(TabbedLine(Declare(decl)));
                }
                code.addLine("");
+               // Define state destructor
+               code.addLine(TabbedLine(ShortComment("Define state destructor")));
+               code.addLine(TabbedLine("~" + SpecNaming.StateStruct + "() {"));
+               if (!globalConstruct.autoGenClear) {
+                       code.addLine(TabbedLine(
+                                       ShortComment("Execute user-defined state clear code"), 2));
+               } else {
+                       code.addLine(TabbedLine(
+                                       ShortComment("Execute auto-generated state clear code"), 2));
+               }
+               globalConstruct.clearState.align(2);
+               code.addLines(globalConstruct.clearState);
+               code.addLine(TabbedLine("}"));
+               code.addLine("");
+
                code.addLine(TabbedLine("SNAPSHOTALLOC"));
+               code.addLine("");
                code.addLine("} " + SpecNaming.StateStruct + ";");
                code.addLine("");
                code.addLine("");
 
                code.addLine(ShortComment("Definition of some c-strings (CSTR)"));
                code.addLine(ShortComment("A special empty string"));
-               code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString, "\"\""));
+               code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.EmptyCString,
+                               "\"\""));
                code.addLine("");
 
                // Interface name strings
@@ -393,7 +306,8 @@ public class CodeGeneratorUtils {
                        ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
                        for (InterfaceConstruct construct : list) {
                                String name = construct.getName();
-                               code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(name), Quote(name)));
+                               code.addLine(DeclareDefine(SpecNaming.CString,
+                                               SpecNaming.AppendStr(name), Quote(name)));
                        }
                }
                code.addLine("");
@@ -401,8 +315,10 @@ public class CodeGeneratorUtils {
                // Commutativity rule strings
                code.addLine(ShortComment("Commutativity rule strings"));
                for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-                       CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
-                       code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.Commutativity + i),
+                       CommutativityRule rule = globalConstruct.commutativityRules
+                                       .get(i - 1);
+                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                       SpecNaming.AppendStr(SpecNaming.Commutativity + i),
                                        Quote(rule.toString())));
                }
                code.addLine("");
@@ -410,20 +326,28 @@ public class CodeGeneratorUtils {
                // Ordering points label strings
                code.addLine(ShortComment("Ordering points label strings"));
                for (String label : OPLabelSet) {
-                       code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(label), Quote(label)));
+                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                       SpecNaming.AppendStr(label), Quote(label)));
                }
                code.addLine("");
 
                // Special function name strings
                code.addLine(ShortComment("Special function name strings"));
-               code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.InitalState),
-                               Quote("_" + SpecNaming.InitalState.toLowerCase())));
-               code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.CopyState),
-                               Quote("_" + SpecNaming.CopyState.toLowerCase())));
-               code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.FinalState),
-                               Quote("_" + SpecNaming.FinalState.toLowerCase())));
-               code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(SpecNaming.PrintState),
-                               Quote("_" + SpecNaming.PrintState.toLowerCase())));
+               code.addLine(DeclareDefine(SpecNaming.CString,
+                               SpecNaming.AppendStr(SpecNaming.InitalState), Quote("_"
+                                               + SpecNaming.InitalState.toLowerCase())));
+               code.addLine(DeclareDefine(SpecNaming.CString,
+                               SpecNaming.AppendStr(SpecNaming.CopyState), Quote("_"
+                                               + SpecNaming.CopyState.toLowerCase())));
+               code.addLine(DeclareDefine(SpecNaming.CString,
+                               SpecNaming.AppendStr(SpecNaming.ClearState), Quote("_"
+                                               + SpecNaming.ClearState.toLowerCase())));
+               code.addLine(DeclareDefine(SpecNaming.CString,
+                               SpecNaming.AppendStr(SpecNaming.FinalState), Quote("_"
+                                               + SpecNaming.FinalState.toLowerCase())));
+               code.addLine(DeclareDefine(SpecNaming.CString,
+                               SpecNaming.AppendStr(SpecNaming.PrintState), Quote("_"
+                                               + SpecNaming.PrintState.toLowerCase())));
                code.addLine("");
 
                // Interface name strings
@@ -434,52 +358,49 @@ public class CodeGeneratorUtils {
                                code.addLine(ShortComment(name + " function strings"));
                                // Transition
                                String tmpFunc = name + "_" + SpecNaming.Transition;
-                               code.addLine(DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+                               code.addLine(DeclareDefine(SpecNaming.CString,
+                                               SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
                                // PreCondition
                                tmpFunc = name + "_" + SpecNaming.PreCondition;
                                if (!construct.preCondition.isEmpty())
-                                       code.addLine(
-                                                       DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
                                else
-                                       code.addLine(
-                                                       DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
-                               // SideEffect
-                               tmpFunc = name + "_" + SpecNaming.SideEffect;
-                               if (!construct.sideEffect.isEmpty())
-                                       code.addLine(
-                                                       DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
-                               else
-                                       code.addLine(
-                                                       DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc),
+                                                       SpecNaming.EmptyCString));
                                // PostCondition
                                tmpFunc = name + "_" + SpecNaming.PostCondition;
                                if (!construct.postCondition.isEmpty())
-                                       code.addLine(
-                                                       DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
                                else
-                                       code.addLine(
-                                                       DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc),
+                                                       SpecNaming.EmptyCString));
                                // Print
                                tmpFunc = name + "_" + SpecNaming.PrintValue;
                                if (!construct.print.isEmpty())
-                                       code.addLine(
-                                                       DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc), Quote("_" + tmpFunc)));
                                else
-                                       code.addLine(
-                                                       DeclareDefine(SpecNaming.CString, SpecNaming.AppendStr(tmpFunc), SpecNaming.EmptyCString));
+                                       code.addLine(DeclareDefine(SpecNaming.CString,
+                                                       SpecNaming.AppendStr(tmpFunc),
+                                                       SpecNaming.EmptyCString));
                                code.addLine("");
                        }
                }
 
                // Define @Initial
                code.addLine(ShortComment("Define @" + SpecNaming.InitalState));
-               code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "(" + SpecNaming.Method + " "
-                               + SpecNaming.Method1 + ") {");
-               code.addLine(TabbedLine(
-                               DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
+               code.addLine("void _" + SpecNaming.InitalState.toLowerCase() + "("
+                               + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+               code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+                               + SpecNaming.StateInst, "new " + SpecNaming.StateStruct)));
                // Define macros
                for (VariableDeclaration decl : globalConstruct.declState) {
-                       code.addLine(TabbedLine("#define " + decl.name + " " + SpecNaming.StateInst + "->" + decl.name));
+                       code.addLine(TabbedLine("#define " + decl.name + " "
+                                       + SpecNaming.StateInst + "->" + decl.name));
                }
                if (!globalConstruct.autoGenInitial)
                        code.addLine(TabbedLine(ShortComment("User-defined state intialization code")));
@@ -494,20 +415,23 @@ public class CodeGeneratorUtils {
                        code.addLine(TabbedLine("#undef " + decl.name));
                }
                code.addLine("");
-               code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1, SpecNaming.StateInst, SpecNaming.StateInst)));
+               code.addLine(TabbedLine(AssignToPtr(SpecNaming.Method1,
+                               SpecNaming.StateInst, SpecNaming.StateInst)));
                code.addLine("}");
                code.addLine("");
 
                // Define @Copy
                code.addLine(ShortComment("Define @" + SpecNaming.CopyState));
-               code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "(" + SpecNaming.Method + " " + "dest, "
-                               + SpecNaming.Method + " src) {");
+               code.addLine("void _" + SpecNaming.CopyState.toLowerCase() + "("
+                               + SpecNaming.Method + " " + "dest, " + SpecNaming.Method
+                               + " src) {");
                // StateStruct *OLD = (StateStruct*) src->state;
-               code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.OldStateInst,
-                               Brace(SpecNaming.StateStruct + "*") + " src->" + SpecNaming.StateInst)));
+               code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+                               + SpecNaming.OldStateInst, Brace(SpecNaming.StateStruct + "*")
+                               + " src->" + SpecNaming.StateInst)));
                // StateStruct *NEW = new StateStruct;
-               code.addLine(TabbedLine(
-                               DeclareDefine(SpecNaming.StateStruct, "*" + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
+               code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+                               + SpecNaming.NewStateInst, "new " + SpecNaming.StateStruct)));
                if (!globalConstruct.autoGenCopy)
                        code.addLine(TabbedLine(ShortComment("User-defined state copy statements")));
                else
@@ -516,19 +440,35 @@ public class CodeGeneratorUtils {
                globalConstruct.copyState.align(1);
                code.addLines(globalConstruct.copyState);
                code.addLine("");
-               code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst, SpecNaming.NewStateInst)));
+               code.addLine(TabbedLine(AssignToPtr("dest", SpecNaming.StateInst,
+                               SpecNaming.NewStateInst)));
+               code.addLine("}");
+               code.addLine("");
+
+               // Define @Clear
+               code.addLine(ShortComment("Define @" + SpecNaming.ClearState));
+               code.addLine("void _" + SpecNaming.ClearState.toLowerCase() + "("
+                               + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
+               // Retrieve the state
+               code.addLine(TabbedLine(ShortComment("Retrieve the state")));
+               code.addLine(TabbedLine(DeclareDefine(SpecNaming.StateStruct, "*"
+                               + SpecNaming.StateInst, "(" + SpecNaming.StateStruct + "*) "
+                               + SpecNaming.Method1 + "->state")));
+               // Explicitly call the state destructor
+               code.addLine(TabbedLine(ShortComment("Explicitly call the state destructor")));
+               code.addLine(TabbedLine("delete " + SpecNaming.StateInst + ";"));
                code.addLine("}");
                code.addLine("");
 
                // Define @Print
                if (!globalConstruct.printState.isEmpty()) {
                        code.addLine(ShortComment("Define @" + SpecNaming.PrintState));
-                       code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "(" + SpecNaming.Method + " "
-                                       + SpecNaming.Method1 + ") {");
+                       code.addLine("void _" + SpecNaming.PrintState.toLowerCase() + "("
+                                       + SpecNaming.Method + " " + SpecNaming.Method1 + ") {");
 
                        // Initialize state struct fields
-                       Code fieldsInit = GenerateStateFieldsInitialization(SpecNaming.Method1, SpecNaming.StateInst,
-                                       globalConstruct);
+                       Code fieldsInit = GenerateStateFieldsInitialization(
+                                       SpecNaming.Method1, SpecNaming.StateInst, globalConstruct);
                        fieldsInit.align(1);
                        code.addLines(fieldsInit);
                        code.addLine("");
@@ -548,16 +488,23 @@ public class CodeGeneratorUtils {
                // Define @Commutativity
                code.addLine(ShortComment("Define commutativity checking functions"));
                for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-                       CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
-                       code.addLine("bool _check" + SpecNaming.Commutativity + i + "(" + SpecNaming.Method + " m1, "
-                                       + SpecNaming.Method + " m2) {");
+                       CommutativityRule rule = globalConstruct.commutativityRules
+                                       .get(i - 1);
+                       code.addLine("bool _check" + SpecNaming.Commutativity + i + "("
+                                       + SpecNaming.Method + " m1, " + SpecNaming.Method
+                                       + " m2) {");
                        // if (m1->name == _ENQ_str && m2->name == _DEQ_str) {
-                       code.addLine(TabbedLine("if (m1->name == " + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
+                       code.addLine(TabbedLine("if (m1->name == "
+                                       + SpecNaming.AppendStr(rule.method1) + " && m2->name == "
                                        + SpecNaming.AppendStr(rule.method2) + ") {"));
                        // Initialize M1 & M2 in commutativity rule
                        // e.g. ENQ *M1 = (ENQ*) m1->value;
-                       code.addLine(TabbedLine(DeclareDefine(rule.method1, "*M1", "(" + rule.method1 + "*) m1->value"), 2));
-                       code.addLine(TabbedLine(DeclareDefine(rule.method2, "*M2", "(" + rule.method2 + "*) m2->value"), 2));
+                       code.addLine(TabbedLine(
+                                       DeclareDefine(rule.method1, "*M1", "(" + rule.method1
+                                                       + "*) m1->value"), 2));
+                       code.addLine(TabbedLine(
+                                       DeclareDefine(rule.method2, "*M2", "(" + rule.method2
+                                                       + "*) m2->value"), 2));
                        code.addLine(TabbedLine("return " + rule.condition + ";", 2));
                        code.addLine(TabbedLine("}"));
                        code.addLine(TabbedLine("return false;"));
@@ -574,14 +521,20 @@ public class CodeGeneratorUtils {
 
                                // Define interface functions
                                String name = construct.getName();
-                               code.addLine("/**********    " + name + " functions    **********/");
+                               code.addLine("/**********    " + name
+                                               + " functions    **********/");
                                // Define @Transition for INTERFACE
-                               code.addLine(ShortComment("Define @" + SpecNaming.Transition + " for " + name));
-                               code.addLine("void _" + name + "_" + SpecNaming.Transition + "(" + SpecNaming.Method + " "
-                                               + SpecNaming.Method1 + ", " + SpecNaming.Method + " " + SpecNaming.Method2 + ") {");
+                               code.addLine(ShortComment("Define @" + SpecNaming.Transition
+                                               + " for " + name));
+                               code.addLine("void _" + name + "_" + SpecNaming.Transition
+                                               + "(" + SpecNaming.Method + " " + SpecNaming.Method1
+                                               + ", " + SpecNaming.Method + " " + SpecNaming.Method2
+                                               + ") {");
 
                                // Initialize value struct fields
-                               fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method2, SpecNaming.InterfaceValueInst, construct);
+                               fieldsInit = GenerateInterfaceFieldsInitialization(
+                                               SpecNaming.Method2, SpecNaming.InterfaceValueInst,
+                                               construct);
                                fieldsInit.align(1);
                                code.addLines(fieldsInit);
 
@@ -594,12 +547,16 @@ public class CodeGeneratorUtils {
 
                                // Define @PreCondition
                                if (!construct.preCondition.isEmpty()) {
-                                       code.addLine(ShortComment("Define @" + SpecNaming.PreCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_" + SpecNaming.PreCondition + "(" + SpecNaming.Method + " "
-                                                       + SpecNaming.Method1 + ") {");
+                                       code.addLine(ShortComment("Define @"
+                                                       + SpecNaming.PreCondition + " for " + name));
+                                       code.addLine("bool _" + name + "_"
+                                                       + SpecNaming.PreCondition + "(" + SpecNaming.Method
+                                                       + " " + SpecNaming.Method1 + ") {");
 
                                        // Initialize value struct fields
-                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(
+                                                       SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+                                                       construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
 
@@ -611,32 +568,19 @@ public class CodeGeneratorUtils {
                                        code.addLine("");
 
                                }
-                               // Define @SideEffect
-                               if (!construct.sideEffect.isEmpty()) {
-                                       code.addLine(ShortComment("Define @" + SpecNaming.SideEffect + " for " + name));
-                                       code.addLine("void _" + name + "_" + SpecNaming.SideEffect + "(" + SpecNaming.Method + " "
-                                                       + SpecNaming.Method1 + ") {");
-
-                                       // Initialize value struct fields
-                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
-                                       fieldsInit.align(1);
-                                       code.addLines(fieldsInit);
-
-                                       construct.sideEffect.align(1);
-                                       code.addLine(TabbedLine(ShortComment("Execute SideEffect")));
-                                       code.addLines(construct.sideEffect);
-
-                                       code.addLine("}");
-                                       code.addLine("");
-                               }
                                // Define @PostCondition
                                if (!construct.postCondition.isEmpty()) {
-                                       code.addLine(ShortComment("Define @" + SpecNaming.PostCondition + " for " + name));
-                                       code.addLine("bool _" + name + "_" + SpecNaming.PostCondition + "(" + SpecNaming.Method + " "
-                                                       + SpecNaming.Method1 + ") {");
+                                       code.addLine(ShortComment("Define @"
+                                                       + SpecNaming.PostCondition + " for " + name));
+                                       code.addLine("bool _" + name + "_"
+                                                       + SpecNaming.PostCondition + "("
+                                                       + SpecNaming.Method + " " + SpecNaming.Method1
+                                                       + ") {");
 
                                        // Initialize value struct fields
-                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(
+                                                       SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+                                                       construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
 
@@ -649,11 +593,15 @@ public class CodeGeneratorUtils {
                                }
                                // Define @Print
                                if (!construct.print.isEmpty()) {
-                                       code.addLine(ShortComment("Define @" + SpecNaming.PrintValue + " for " + name));
-                                       code.addLine("void _" + name + "_" + SpecNaming.PrintValue + "(" + SpecNaming.Method + " "
+                                       code.addLine(ShortComment("Define @"
+                                                       + SpecNaming.PrintValue + " for " + name));
+                                       code.addLine("void _" + name + "_" + SpecNaming.PrintValue
+                                                       + "(" + SpecNaming.Method + " "
                                                        + SpecNaming.Method1 + ") {");
                                        // Initialize value struct fields
-                                       fieldsInit = GenerateInterfaceFieldsInitialization(SpecNaming.Method1, SpecNaming.InterfaceValueInst, construct);
+                                       fieldsInit = GenerateInterfaceFieldsInitialization(
+                                                       SpecNaming.Method1, SpecNaming.InterfaceValueInst,
+                                                       construct);
                                        fieldsInit.align(1);
                                        code.addLines(fieldsInit);
 
@@ -677,35 +625,46 @@ public class CodeGeneratorUtils {
 
                // Init commutativity rules
                code.addLine(TabbedLine(ShortComment("Init commutativity rules")));
-               code.addLine(TabbedLine(DeclareDefine("int", SpecNaming.CommutativityRuleSizeInst,
+               code.addLine(TabbedLine(DeclareDefine("int",
+                               SpecNaming.CommutativityRuleSizeInst,
                                Integer.toString(globalConstruct.commutativityRules.size()))));
-               String tmp = SpecNaming.NewSize + Brace(SpecNaming.CommutativityRule + ", sizeof"
-                               + Brace(SpecNaming.CommutativityRule) + " * " + SpecNaming.CommutativityRuleSizeInst);
-               code.addLine(
-                               TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*" + SpecNaming.CommutativityRuleInst, tmp)));
+               String tmp = SpecNaming.NewSize
+                               + Brace(SpecNaming.CommutativityRule + ", sizeof"
+                                               + Brace(SpecNaming.CommutativityRule) + " * "
+                                               + SpecNaming.CommutativityRuleSizeInst);
+               code.addLine(TabbedLine(DeclareDefine(SpecNaming.CommutativityRule, "*"
+                               + SpecNaming.CommutativityRuleInst, tmp)));
                for (int i = 1; i <= globalConstruct.commutativityRules.size(); i++) {
-                       CommutativityRule rule = globalConstruct.commutativityRules.get(i - 1);
-                       code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ") + i));
+                       CommutativityRule rule = globalConstruct.commutativityRules
+                                       .get(i - 1);
+                       code.addLine(TabbedLine(ShortComment("Initialize commutativity rule ")
+                                       + i));
                        // new( &commuteRules[0] )CommutativityRule(_ENQ_str, _DEQ_str,
                        // _Commutativity1_str, _checkCommutativity1)
-                       line = "new" + Brace(" &" + SpecNaming.CommutativityRuleInst + "[" + (i - 1) + "] ")
-                                       + SpecNaming.CommutativityRule + "(" + SpecNaming.AppendStr(rule.method1) + ", "
-                                       + SpecNaming.AppendStr(rule.method2) + ", " + SpecNaming.AppendStr(SpecNaming.Commutativity + i)
-                                       + ", " + "_check" + SpecNaming.Commutativity + i + ");";
+                       line = "new"
+                                       + Brace(" &" + SpecNaming.CommutativityRuleInst + "["
+                                                       + (i - 1) + "] ") + SpecNaming.CommutativityRule
+                                       + "(" + SpecNaming.AppendStr(rule.method1) + ", "
+                                       + SpecNaming.AppendStr(rule.method2) + ", "
+                                       + SpecNaming.AppendStr(SpecNaming.Commutativity + i) + ", "
+                                       + "_check" + SpecNaming.Commutativity + i + ");";
                        code.addLine(TabbedLine(line));
                }
 
                // Initialize AnnoInit
                code.addLine(TabbedLine(ShortComment("Initialize AnnoInit")));
                // AnnoInit *init = new AnnoInit(
-               code.addLine(TabbedLine(
-                               SpecNaming.AnnoInit + " *" + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit + "("));
+               code.addLine(TabbedLine(SpecNaming.AnnoInit + " *"
+                               + SpecNaming.AnnoInitInst + " = new " + SpecNaming.AnnoInit
+                               + "("));
                // new NamedFunction(_Initial_str, INITIAL, (void*) _initial),
-               code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.InitalState)
-                               + ", " + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
+               code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+                               + SpecNaming.AppendStr(SpecNaming.InitalState) + ", "
+                               + SpecNaming.InitalState.toUpperCase() + ", " + "(void*) _"
                                + SpecNaming.InitalState.toLowerCase() + "),", 2));
                // new NamedFunction(_Final_str, FINAL, (void*) NULL_FUNC),
-               line = "new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
+               line = "new " + SpecNaming.NamedFunction + "("
+                               + SpecNaming.AppendStr(SpecNaming.FinalState) + ", "
                                + SpecNaming.FinalState.toUpperCase() + ", " + "(void*) ";
                if (globalConstruct.finalState.isEmpty()) {
                        line = line + SpecNaming.NullFunc + "),";
@@ -714,26 +673,29 @@ public class CodeGeneratorUtils {
                }
                code.addLine(TabbedLine(line, 2));
                // new NamedFunction(_Copy_str, COPY, (void*) _copy),
-               code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.CopyState)
-                               + ", " + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _" + SpecNaming.CopyState.toLowerCase()
-                               + "),", 2));
+               code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+                               + SpecNaming.AppendStr(SpecNaming.CopyState) + ", "
+                               + SpecNaming.CopyState.toUpperCase() + ", " + "(void*) _"
+                               + SpecNaming.CopyState.toLowerCase() + "),", 2));
+               // new NamedFunction(_Clear_str, CLEAR, (void*) _clear),
+               code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+                               + SpecNaming.AppendStr(SpecNaming.ClearState) + ", "
+                               + SpecNaming.ClearState.toUpperCase() + ", " + "(void*) _"
+                               + SpecNaming.ClearState.toLowerCase() + "),", 2));
                // new NamedFunction(_Print_str, PRINT_STATE, (void*) _print),
-               line = "new " + SpecNaming.NamedFunction + "(" + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
-                               + SpecNaming.PrintStateType + ", " + "(void*)";
-               if (globalConstruct.printState.isEmpty()) {
-                       line = line + SpecNaming.NullFunc + "),";
-               } else {
-                       line = line + "_" + SpecNaming.PrintState.toLowerCase() + "),";
-               }
-               code.addLine(TabbedLine(line, 2));
+               code.addLine(TabbedLine("new " + SpecNaming.NamedFunction + "("
+                               + SpecNaming.AppendStr(SpecNaming.PrintState) + ", "
+                               + SpecNaming.PrintStateType + ", " + "(void*) _"
+                               + SpecNaming.PrintState.toLowerCase() + "),", 2));
                // commuteRules, CommuteRuleSize);
-               code.addLine(
-                               TabbedLine(SpecNaming.CommutativityRuleInst + ", " + SpecNaming.CommutativityRuleSizeInst + ");", 2));
+               code.addLine(TabbedLine(SpecNaming.CommutativityRuleInst + ", "
+                               + SpecNaming.CommutativityRuleSizeInst + ");", 2));
                code.addLine("");
 
                // Declare StateFunctions map
                code.addLine(TabbedLine(ShortComment("Declare StateFunctions map")));
-               code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*" + SpecNaming.StateFunctionsInst)));
+               code.addLine(TabbedLine(Declare(SpecNaming.StateFunctions, "*"
+                               + SpecNaming.StateFunctionsInst)));
                code.addLine("");
 
                // StateFunction for interface
@@ -741,62 +703,72 @@ public class CodeGeneratorUtils {
                        ArrayList<InterfaceConstruct> list = interfaceListMap.get(file);
                        for (InterfaceConstruct construct : list) {
                                String name = construct.getName();
-                               code.addLine(TabbedLine(ShortComment("StateFunction for " + name)));
+                               code.addLine(TabbedLine(ShortComment("StateFunction for "
+                                               + name)));
                                // stateFuncs = new StateFunctions(
-                               code.addLine(TabbedLine(SpecNaming.StateFunctionsInst + " = new " + SpecNaming.StateFunctions + "("));
+                               code.addLine(TabbedLine(SpecNaming.StateFunctionsInst
+                                               + " = new " + SpecNaming.StateFunctions + "("));
                                // new NamedFunction(_ENQ_Transition_str, TRANSITION, (void*)
                                // _ENQ_Transition),
                                // Transition
                                code.addLine(TabbedLine(
-                                               "new " + SpecNaming.NamedFunction + "("
-                                                               + SpecNaming.AppendStr(name + "_" + SpecNaming.Transition) + ", "
-                                                               + SpecNaming.TransitionType + ", (void*) _" + name + "_" + SpecNaming.Transition + "),",
-                                               2));
+                                               "new "
+                                                               + SpecNaming.NamedFunction
+                                                               + "("
+                                                               + SpecNaming.AppendStr(name + "_"
+                                                                               + SpecNaming.Transition) + ", "
+                                                               + SpecNaming.TransitionType + ", (void*) _"
+                                                               + name + "_" + SpecNaming.Transition + "),", 2));
                                // PreCondition
-                               line = "new " + SpecNaming.NamedFunction + "("
-                                               + SpecNaming.AppendStr(name + "_" + SpecNaming.PreCondition) + ", "
+                               line = "new "
+                                               + SpecNaming.NamedFunction
+                                               + "("
+                                               + SpecNaming.AppendStr(name + "_"
+                                                               + SpecNaming.PreCondition) + ", "
                                                + SpecNaming.PreConditionType + ", (void*) ";
                                if (construct.preCondition.isEmpty()) {
                                        line = line + SpecNaming.NullFunc + "),";
                                } else {
-                                       line = line + "_" + name + "_" + SpecNaming.PreCondition + "),";
-                               }
-                               code.addLine(TabbedLine(line, 2));
-                               // SideEffect
-                               line = "new " + SpecNaming.NamedFunction + "("
-                                               + SpecNaming.AppendStr(name + "_" + SpecNaming.SideEffect) + ", " + SpecNaming.SideEffectType
-                                               + ", (void*) ";
-                               if (construct.sideEffect.isEmpty()) {
-                                       line = line + SpecNaming.NullFunc + "),";
-                               } else {
-                                       line = line + "_" + name + "_" + SpecNaming.SideEffect + "),";
+                                       line = line + "_" + name + "_" + SpecNaming.PreCondition
+                                                       + "),";
                                }
                                code.addLine(TabbedLine(line, 2));
                                // PostCondition
-                               line = "new " + SpecNaming.NamedFunction + "("
-                                               + SpecNaming.AppendStr(name + "_" + SpecNaming.PostCondition) + ", "
+                               line = "new "
+                                               + SpecNaming.NamedFunction
+                                               + "("
+                                               + SpecNaming.AppendStr(name + "_"
+                                                               + SpecNaming.PostCondition) + ", "
                                                + SpecNaming.PostConditionType + ", (void*) ";
                                if (construct.postCondition.isEmpty()) {
                                        line = line + SpecNaming.NullFunc + "),";
                                } else {
-                                       line = line + "_" + name + "_" + SpecNaming.PostCondition + "),";
+                                       line = line + "_" + name + "_" + SpecNaming.PostCondition
+                                                       + "),";
                                }
                                code.addLine(TabbedLine(line, 2));
                                // Print (PrintValue
-                               line = "new " + SpecNaming.NamedFunction + "("
-                                               + SpecNaming.AppendStr(name + "_" + SpecNaming.PrintValue) + ", " + SpecNaming.PrintValueType
-                                               + ", (void*) ";
+                               line = "new "
+                                               + SpecNaming.NamedFunction
+                                               + "("
+                                               + SpecNaming.AppendStr(name + "_"
+                                                               + SpecNaming.PrintValue) + ", "
+                                               + SpecNaming.PrintValueType + ", (void*) ";
                                if (construct.print.isEmpty()) {
                                        line = line + SpecNaming.NullFunc + ")";
                                } else {
-                                       line = line + "_" + name + "_" + SpecNaming.PrintValue + ")";
+                                       line = line + "_" + name + "_" + SpecNaming.PrintValue
+                                                       + ")";
                                }
                                code.addLine(TabbedLine(line, 2));
                                code.addLine(TabbedLine(");"));
 
                                // init->addInterfaceFunctions(_ENQ_str, stateFuncs);
-                               code.addLine(TabbedLine(SpecNaming.AnnoInitInst + "->" + SpecNaming.AddInterfaceFunctions
-                                               + Brace(SpecNaming.AppendStr(name) + ", " + SpecNaming.StateFunctionsInst) + ";"));
+                               code.addLine(TabbedLine(SpecNaming.AnnoInitInst
+                                               + "->"
+                                               + SpecNaming.AddInterfaceFunctions
+                                               + Brace(SpecNaming.AppendStr(name) + ", "
+                                                               + SpecNaming.StateFunctionsInst) + ";"));
                                code.addLine("");
                        }
                }
@@ -804,8 +776,12 @@ public class CodeGeneratorUtils {
                // Create and instrument with the INIT annotation
                code.addLine(TabbedLine(ShortComment("Create and instrument with the INIT annotation")));
                // cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, init));
-               code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc + Brace(SpecNaming.SPEC_ANALYSIS + ", new "
-                               + SpecNaming.SpecAnnotation + Brace(SpecNaming.AnnoTypeInit + ", " + SpecNaming.AnnoInitInst)) + ";"));
+               code.addLine(TabbedLine(SpecNaming.CDSAnnotateFunc
+                               + Brace(SpecNaming.SPEC_ANALYSIS
+                                               + ", new "
+                                               + SpecNaming.SpecAnnotation
+                                               + Brace(SpecNaming.AnnoTypeInit + ", "
+                                                               + SpecNaming.AnnoInitInst)) + ";"));
 
                code.addLine("}");
                code.addLine("");
@@ -839,13 +815,16 @@ public class CodeGeneratorUtils {
         *            The global state construct
         * @return The generated code
         */
-       public static Code GenerateStateFieldsInitialization(String methodInst, String inst, GlobalConstruct construct) {
+       public static Code GenerateStateFieldsInitialization(String methodInst,
+                       String inst, GlobalConstruct construct) {
                Code res = new Code();
-               res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct + " fields"));
-               res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst,
-                               "(" + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
+               res.addLine(ShortComment("Initialize " + SpecNaming.StateStruct
+                               + " fields"));
+               res.addLine(DeclareDefine(SpecNaming.StateStruct, "*" + inst, "("
+                               + SpecNaming.StateStruct + "*) " + methodInst + "->state"));
                for (VariableDeclaration decl : construct.declState) {
-                       res.addLine(DeclareDefine(decl.type, decl.name, inst + "->" + decl.name));
+                       res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
+                                       + decl.name));
                }
                return res;
        }
@@ -876,21 +855,23 @@ public class CodeGeneratorUtils {
         *            The corresponding interface construct
         * @return The generated code
         */
-       public static Code GenerateInterfaceFieldsInitialization(String methodInst, String inst,
-                       InterfaceConstruct construct) {
+       public static Code GenerateInterfaceFieldsInitialization(String methodInst,
+                       String inst, InterfaceConstruct construct) {
                Code res = new Code();
                String name = construct.getName();
                res.addLine(ShortComment("Initialize fields for " + name));
                // The very first assignment "
-               res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) " + methodInst + "->" + SpecNaming.MethodValueField));
+               res.addLine(DeclareDefine(name, "*" + inst, "(" + name + "*) "
+                               + methodInst + "->" + SpecNaming.MethodValueField));
                // Don't leave out the RET field
                if (!construct.getFunctionHeader().isReturnVoid()) {
-                       res.addLine(DeclareDefine(construct.getFunctionHeader().returnType, SpecNaming.RET,
-                                       inst + "->" + SpecNaming.RET));
+                       res.addLine(DeclareDefine(construct.getFunctionHeader().returnType,
+                                       SpecNaming.RET, inst + "->" + SpecNaming.RET));
                }
                // For arguments
                for (VariableDeclaration decl : construct.getFunctionHeader().args) {
-                       res.addLine(DeclareDefine(decl.type, decl.name, inst + "->" + decl.name));
+                       res.addLine(DeclareDefine(decl.type, decl.name, inst + "->"
+                                       + decl.name));
                }
                return res;
        }
@@ -920,16 +901,19 @@ public class CodeGeneratorUtils {
                        code.addLine(prefixTabs + SpecNaming.CreateOPDefineAnnoFunc + "();");
                        break;
                case PotentialOP:
-                       code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc + "(" + SpecNaming.AppendStr(label) + ");");
+                       code.addLine(prefixTabs + SpecNaming.CreatePotentialOPAnnoFunc
+                                       + "(" + SpecNaming.AppendStr(label) + ");");
                        break;
                case OPCheck:
-                       code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "(" + SpecNaming.AppendStr(label) + ");");
+                       code.addLine(prefixTabs + SpecNaming.CreateOPCheckAnnoFunc + "("
+                                       + SpecNaming.AppendStr(label) + ");");
                        break;
                case OPClear:
                        code.addLine(prefixTabs + SpecNaming.CreateOPClearAnnoFunc + "();");
                        break;
                case OPClearDefine:
-                       code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc + "();");
+                       code.addLine(prefixTabs + SpecNaming.CreateOPClearDefineAnnoFunc
+                                       + "();");
                        break;
                default:
                        break;
@@ -998,7 +982,8 @@ public class CodeGeneratorUtils {
 
                // Add one line to separate
                code.addLine("");
-               code.addLine(prefixTabs + ShortComment("Generated wrapper interface for " + name));
+               code.addLine(prefixTabs
+                               + ShortComment("Generated wrapper interface for " + name));
                if (beginLine.indexOf('{') == -1) { // We need to add the '{' to the end
                                                                                        // of the line
                        code.addLine(beginLine + " {");
@@ -1006,34 +991,56 @@ public class CodeGeneratorUtils {
                        code.addLine(beginLine);
                }
                // Instrument with the INTERFACE_BEGIN annotations
-               code.addLine(prefixTabs + "\t" + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
+               code.addLine(prefixTabs
+                               + "\t"
+                               + ShortComment("Instrument with the INTERFACE_BEGIN annotation"));
                // CAnnoInterfaceInfo info = _createInterfaceBeginAnnotation(_DEQ_str);
-               code.addLine(
-                               prefixTabs + "\t" + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*" + SpecNaming.AnnoInterfaceInfoInst,
-                                               SpecNaming.CreateInterfaceBeginAnnoFunc + Brace(SpecNaming.AppendStr(name))));
+               code.addLine(prefixTabs
+                               + "\t"
+                               + DeclareDefine(SpecNaming.AnnoInterfaceInfo, "*"
+                                               + SpecNaming.AnnoInterfaceInfoInst,
+                                               SpecNaming.CreateInterfaceBeginAnnoFunc
+                                                               + Brace(SpecNaming.AppendStr(name))));
                // Call the actual function
-               code.addLine(prefixTabs + "\t" + ShortComment("Call the actual function"));
+               code.addLine(prefixTabs + "\t"
+                               + ShortComment("Call the actual function"));
                // bool RET = dequeue_ORIGINAL__(q, retVal, reclaimNode);
-               code.addLine(prefixTabs + "\t" + construct.getFunctionHeader().getRenamedCall() + ";");
+               code.addLine(prefixTabs + "\t"
+                               + construct.getFunctionHeader().getRenamedCall() + ";");
                code.addLine("");
 
                // Initialize the value struct
-               code.addLine(prefixTabs + "\t" + ShortComment("Initialize the value struct"));
+               code.addLine(prefixTabs + "\t"
+                               + ShortComment("Initialize the value struct"));
                // The very first assignment "
-               code.addLine(prefixTabs + "\t" + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst, SpecNaming.New + Brace(name)));
+               code.addLine(prefixTabs
+                               + "\t"
+                               + DeclareDefine(name, "*" + SpecNaming.InterfaceValueInst,
+                                               SpecNaming.New + Brace(name)));
                // Don't leave out the RET field
                if (!construct.getFunctionHeader().isReturnVoid())
-                       code.addLine(prefixTabs + "\t" + AssignToPtr(SpecNaming.InterfaceValueInst, SpecNaming.RET, SpecNaming.RET));
+                       code.addLine(prefixTabs
+                                       + "\t"
+                                       + AssignToPtr(SpecNaming.InterfaceValueInst,
+                                                       SpecNaming.RET, SpecNaming.RET));
                // For arguments
                for (VariableDeclaration decl : construct.getFunctionHeader().args)
-                       code.addLine(prefixTabs + "\t" + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name, decl.name));
+                       code.addLine(prefixTabs
+                                       + "\t"
+                                       + AssignToPtr(SpecNaming.InterfaceValueInst, decl.name,
+                                                       decl.name));
                code.addLine("");
 
                // Store the value info into the current MethodCall
                // _setInterfaceBeginAnnotationValue(info, value);
-               code.addLine(prefixTabs + "\t" + ShortComment("Store the value info into the current MethodCall"));
-               code.addLine(prefixTabs + "\t" + SpecNaming.SetInterfaceBeginAnnoValueFunc
-                               + Brace(SpecNaming.AnnoInterfaceInfoInst + ", " + SpecNaming.InterfaceValueInst) + ";");
+               code.addLine(prefixTabs
+                               + "\t"
+                               + ShortComment("Store the value info into the current MethodCall"));
+               code.addLine(prefixTabs
+                               + "\t"
+                               + SpecNaming.SetInterfaceBeginAnnoValueFunc
+                               + Brace(SpecNaming.AnnoInterfaceInfoInst + ", "
+                                               + SpecNaming.InterfaceValueInst) + ";");
                code.addLine("");
 
                // Return if necessary

diff --git a/src/edu/uci/eecs/codeGenerator/Environment.java b/src/edu/uci/eecs/codeGenerator/Environment.java
index 84fc4ee57ed842d9005d602898429217304f1d3a..563babbbd15d518706dda3b8cb77ec11fbf1789a 100644 (file)
--- a/src/edu/uci/eecs/codeGenerator/Environment.java
+++ b/src/edu/uci/eecs/codeGenerator/Environment.java
@@ -1,5 +1,7 @@
 package edu.uci.eecs.codeGenerator;
 
+import java.util.ArrayList;
+
 /**
  * <p>
  * This class contains some constant strings related to the code generation
@@ -26,5 +28,26 @@ public class Environment {
        public final static String MCS_LOCK = "mcs-lock";
        public final static String DEQUE = "chase-lev-deque-bugfix";
        public final static String TREIBER_STACK = "treiber-stack";
+       public final static String TICKET_LOCK = "ticket-lock";
+       public final static String SEQLOCK = "seqlock";
+       public final static String READ_COPY_UPDATE = "read-copy-update";
+       public final static String CONCURRENT_MAP = "concurrent-hashmap";
+       public final static String SPSC = "spsc-bugfix";
+       public final static String MPMC = "mpmc-queue";
+       
+       public final static String[] Benchmarks = {
+               REGISTER,
+               MS_QUEUE,
+               LINUXRWLOCKS,
+               MCS_LOCK,
+               DEQUE,
+               TREIBER_STACK,
+               TICKET_LOCK,
+               SEQLOCK,
+               READ_COPY_UPDATE,
+               CONCURRENT_MAP,
+               SPSC,
+               MPMC
+       }; 
 
 }

diff --git a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
index b2e52a03d5b333626b5b014a8e433a91d4c22184..d8f6dd42491bfaaa62b17b9e3c06efd8840a4e6e 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/GlobalConstruct.java
@@ -21,6 +21,7 @@ public class GlobalConstruct extends Construct {
        public final ArrayList<VariableDeclaration> declState;
        public final Code initState;
        public final Code copyState;
+       public final Code clearState;
        public final Code finalState;
        public final Code printState;
        public final ArrayList<CommutativityRule> commutativityRules;
@@ -31,6 +32,8 @@ public class GlobalConstruct extends Construct {
        public final boolean autoGenInitial;
        // Whether we have auto-gen the state copying code
        public final boolean autoGenCopy;
+       // Whether we have auto-gen the state clearing code
+       public final boolean autoGenClear;
        // Whether we have auto-gen the state printing code
        public final boolean autoGenPrint;
 
@@ -40,6 +43,7 @@ public class GlobalConstruct extends Construct {
                declState = new ArrayList<VariableDeclaration>();
                initState = new Code();
                copyState = new Code();
+               clearState = new Code();
                finalState = new Code();
                printState = new Code();
                commutativityRules = new ArrayList<CommutativityRule>();
@@ -64,6 +68,12 @@ public class GlobalConstruct extends Construct {
                        copyState.addLines(code);
                }
 
+               autoGenClear = clearState.isEmpty();
+               if (autoGenClear) {
+                       Code code = generateAutoClearFunction();
+                       clearState.addLines(code);
+               }
+
                autoGenPrint = printState.isEmpty();
                if (autoGenPrint) {
                        Code code = generateAutoPrintFunction();
@@ -167,6 +177,35 @@ public class GlobalConstruct extends Construct {
 
                return code;
        }
+       
+       /**
+        * <p>
+        * This function will automatically generate the clear statements for
+        * supported types if the user has not defined the "@Clear" primitive
+        * </p>
+        * 
+        * @return The auto-generated state copy statements
+        * @throws WrongAnnotationException
+        */
+       private Code generateAutoClearFunction() throws WrongAnnotationException {
+               Code code = new Code();
+               if (emptyState) // Empty state should have empty copy function
+                       return code;
+               
+               // FIXME: Just try our best to generate recycling statements
+               for (VariableDeclaration decl : declState) {
+                       String type = decl.type;
+                       String name = decl.name;
+                       if (type.equals("IntList *") || type.equals("IntSet *")
+                                       || type.equals("IntMap *")) {
+                               // Supported pointer types
+                               // if (stack) delete stack;
+                               code.addLine("if (" + name + ") delete " + name + ";");
+                       }
+               }
+
+               return code;
+       }
 
        /**
         * <p>
@@ -209,6 +248,7 @@ public class GlobalConstruct extends Construct {
                if (!name.equals(SpecNaming.DeclareState)
                                && !name.equals(SpecNaming.InitalState)
                                && !name.equals(SpecNaming.CopyState)
+                               && !name.equals(SpecNaming.ClearState)
                                && !name.equals(SpecNaming.FinalState)
                                && !name.equals(SpecNaming.Commutativity)
                                && !name.equals(SpecNaming.PrintState)) {
@@ -292,6 +332,8 @@ public class GlobalConstruct extends Construct {
                                initState.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.CopyState)) {
                                copyState.addLines(primitive.contents);
+                       } else if (name.equals(SpecNaming.ClearState)) {
+                               clearState.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.FinalState)) {
                                finalState.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PrintState)) {

diff --git a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
index 6afd5f127abd4261ec94b0285d23d56718209ae7..232acaf2b34bc5529db9d64bb10af8547059f1ca 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
+++ b/src/edu/uci/eecs/specExtraction/InterfaceConstruct.java
@@ -24,7 +24,6 @@ public class InterfaceConstruct extends Construct {
        private String name;
        public final Code transition;
        public final Code preCondition;
-       public final Code sideEffect;
        public final Code postCondition;
        public final Code print;
 
@@ -47,7 +46,6 @@ public class InterfaceConstruct extends Construct {
                this.name = null;
                this.transition = new Code();
                this.preCondition = new Code();
-               this.sideEffect = new Code();
                this.postCondition = new Code();
                this.print = new Code();
 
@@ -171,8 +169,6 @@ public class InterfaceConstruct extends Construct {
                                this.transition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PreCondition)) {
                                this.preCondition.addLines(primitive.contents);
-                       } else if (name.equals(SpecNaming.SideEffect)) {
-                               this.sideEffect.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PostCondition)) {
                                this.postCondition.addLines(primitive.contents);
                        } else if (name.equals(SpecNaming.PrintValue)) {
@@ -214,8 +210,6 @@ public class InterfaceConstruct extends Construct {
                        sb.append("@Transition:\n" + transition);
                if (!preCondition.isEmpty())
                        sb.append("@PreCondition:\n" + preCondition);
-               if (!sideEffect.isEmpty())
-                       sb.append("@SideEffect:\n" + sideEffect);
                if (!postCondition.isEmpty())
                        sb.append("@PostCondition:\n" + postCondition);
                if (!print.isEmpty())

diff --git a/src/edu/uci/eecs/specExtraction/SpecNaming.java b/src/edu/uci/eecs/specExtraction/SpecNaming.java
index 463d2c93e59a25387e5acd5aabb9ea4a17c12bdf..f1f97ffd11f7011f0602501e1e683f6b3dc20116 100644 (file)
--- a/src/edu/uci/eecs/specExtraction/SpecNaming.java
+++ b/src/edu/uci/eecs/specExtraction/SpecNaming.java
@@ -21,6 +21,7 @@ public class SpecNaming {
        public static final String DeclareState = "DeclareState";
        public static final String InitalState = "Initial";
        public static final String CopyState = "Copy";
+       public static final String ClearState = "Clear";
        public static final String FinalState = "Final";
        public static final String PrintState = "Print";
        public static final String Commutativity = "Commutativity";