clean code
authorPeizhao Ou <peizhaoo@uci.edu>
Thu, 18 Feb 2016 00:43:11 +0000 (16:43 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Thu, 18 Feb 2016 00:43:11 +0000 (16:43 -0800)
133 files changed:
benchmark/chase-lev-deque-bugfix/deque.c
benchmark/chase-lev-deque-bugfix/deque.h
grammer/README.txt [deleted file]
grammer/backup-spec-compiler.jj [deleted file]
grammer/pre_scanner.jj [deleted file]
grammer/spec.txt [deleted file]
grammer/spec_compiler.jj [deleted file]
grammer/util.jj
notes/nondeterm-spec.txt
output/Makefile [deleted file]
output/benchmarks.mk [deleted file]
output/chase-lev-deque-bugfix/Makefile [deleted file]
output/chase-lev-deque-bugfix/deque.c [deleted file]
output/chase-lev-deque-bugfix/deque.h [deleted file]
output/chase-lev-deque-bugfix/deque.o [deleted file]
output/chase-lev-deque-bugfix/main [deleted file]
output/chase-lev-deque-bugfix/main.c [deleted file]
output/chase-lev-deque-bugfix/testcase.c [deleted file]
output/chase-lev-deque-bugfix/testcase1 [deleted file]
output/chase-lev-deque-bugfix/testcase1.c [deleted file]
output/chase-lev-deque-bugfix/testcase2 [deleted file]
output/chase-lev-deque-bugfix/testcase2.c [deleted file]
output/cliffc-hashtable/cliffc_hashtable.h [deleted file]
output/cliffc-hashtable/main.cc [deleted file]
output/concurrent-hashmap/ConcurrentHashMap.java [deleted file]
output/concurrent-hashmap/Makefile [deleted file]
output/concurrent-hashmap/hashmap.h [deleted file]
output/concurrent-hashmap/hashmap.o [deleted file]
output/concurrent-hashmap/main [deleted file]
output/concurrent-hashmap/main.cc [deleted file]
output/concurrent-hashmap/note.txt [deleted file]
output/concurrent-hashmap/testcase1 [deleted file]
output/concurrent-hashmap/testcase1.cc [deleted file]
output/include/unrelacy.h [deleted file]
output/linuxrwlocks/Makefile [deleted file]
output/linuxrwlocks/linuxrwlocks [deleted file]
output/linuxrwlocks/linuxrwlocks.c [deleted file]
output/linuxrwlocks/testcase1 [deleted file]
output/linuxrwlocks/testcase1.c [deleted file]
output/linuxrwlocks/testcase2 [deleted file]
output/linuxrwlocks/testcase2.c [deleted file]
output/mcs-lock/Makefile [deleted file]
output/mcs-lock/mcs-lock [deleted file]
output/mcs-lock/mcs-lock.cc [deleted file]
output/mcs-lock/mcs-lock.h [deleted file]
output/mpmc-queue/Makefile [deleted file]
output/mpmc-queue/mpmc-queue.cc [deleted file]
output/mpmc-queue/mpmc-queue.h [deleted file]
output/mpmc-queue/testcase [deleted file]
output/mpmc-queue/testcase.cc [deleted file]
output/mpmc-queue/testcase1 [deleted file]
output/mpmc-queue/testcase1.cc [deleted file]
output/mpmc-queue/testcase2 [deleted file]
output/mpmc-queue/testcase2.cc [deleted file]
output/mpmc-queue/testcase3 [deleted file]
output/mpmc-queue/testcase3.cc [deleted file]
output/ms-queue/Makefile [deleted file]
output/ms-queue/main [deleted file]
output/ms-queue/main.c [deleted file]
output/ms-queue/main.o [deleted file]
output/ms-queue/my_queue.c [deleted file]
output/ms-queue/my_queue.h [deleted file]
output/ms-queue/my_queue.o [deleted file]
output/ms-queue/testcase1 [deleted file]
output/ms-queue/testcase1.c [deleted file]
output/ms-queue/testcase1.o [deleted file]
output/ms-queue/testcase2 [deleted file]
output/ms-queue/testcase2.c [deleted file]
output/ms-queue/testcase2.o [deleted file]
output/ms-queue/testcase3 [deleted file]
output/ms-queue/testcase3.c [deleted file]
output/ms-queue/testcase3.o [deleted file]
output/read-copy-update/Makefile [deleted file]
output/read-copy-update/rcu [deleted file]
output/read-copy-update/rcu.cc [deleted file]
output/run.sh [deleted file]
output/seqlock/Makefile [deleted file]
output/spsc-bugfix/Makefile [deleted file]
output/spsc-bugfix/eventcount.h [deleted file]
output/spsc-bugfix/queue.h [deleted file]
output/spsc-bugfix/spsc-queue [deleted file]
output/spsc-bugfix/spsc-queue.cc [deleted file]
run-javacc.sh
setup-env.sh [deleted file]
src/edu/uci/eecs/codeGenerator/CodeAdditions.java [new file with mode: 0644]
src/edu/uci/eecs/codeGenerator/CodeGenerator.java [new file with mode: 0644]
src/edu/uci/eecs/codeGenerator/CodeGeneratorUtils.java [new file with mode: 0644]
src/edu/uci/eecs/codeGenerator/Environment.java [new file with mode: 0644]
src/edu/uci/eecs/specCompiler/codeGenerator/CodeAddition.java [deleted file]
src/edu/uci/eecs/specCompiler/codeGenerator/CodeGenerator.java [deleted file]
src/edu/uci/eecs/specCompiler/codeGenerator/CodeVariables.java [deleted file]
src/edu/uci/eecs/specCompiler/codeGenerator/Environment.java [deleted file]
src/edu/uci/eecs/specCompiler/codeGenerator/InterfaceWrongFormatException.java [deleted file]
src/edu/uci/eecs/specCompiler/codeGenerator/ProgramUnit.java [deleted file]
src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsChecker.java [deleted file]
src/edu/uci/eecs/specCompiler/codeGenerator/SemanticsCheckerException.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/CPClearConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/CPDefineCheckConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/CPDefineConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/ClassBeginConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/ClassEndConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/CommutativityRule.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/ConditionalInterface.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/Construct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/EntryPointConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/FunctionHeader.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/GlobalConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/IDExtractor.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/InterfaceConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/InterfaceDefineConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/ParserUtils.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/PotentialCPDefineConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/QualifiedName.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/SequentialDefineSubConstruct.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/SourceFileInfo.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/SpecExtractor.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/SpecInfoScanner.java [deleted file]
src/edu/uci/eecs/specCompiler/specExtraction/VariableDeclaration.java [deleted file]
src/edu/uci/eecs/specExtraction/Code.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/CommutativityRule.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/Construct.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/EntryConstruct.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/FunctionHeader.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/GlobalConstruct.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/InterfaceConstruct.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/OPConstruct.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/OPType.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/QualifiedName.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/SpecExtractor.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/SpecNaming.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/SpecUtils.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/VariableDeclaration.java [new file with mode: 0644]
src/edu/uci/eecs/specExtraction/WrongAnnotationException.java [new file with mode: 0644]

index bb12be0..9c6625e 100644 (file)
@@ -4,6 +4,10 @@
 #include <stdlib.h>
 #include <stdio.h>
 
+inline bool fail(int ret) {
+       return ret == ABORT || ret == EMPTY;
+}
+
 Deque * create() {
        Deque * q = (Deque *) calloc(1, sizeof(Deque));
        Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
index 9292e16..4d1f34e 100644 (file)
@@ -21,6 +21,7 @@ typedef struct {
 #define EMPTY 0xffffffff
 #define ABORT 0xfffffffe
 
+inline bool fail(int ret);
 /**
     @Begin
     @Options:
@@ -42,7 +43,7 @@ typedef struct {
         Push -> Steal
        @Commutativity: Push <-> Steal: true
        @Commutativity: Take <-> Steal: true
-       @Commutativity: Steal <-> Steal: _Method1.__RET__ == ABORT || _Method2.__RET__ == ABORT
+       @Commutativity: Steal <-> Steal: fail(_Method1.__RET__) || fail(_Method2.__RET__)
 
     @End
 */
diff --git a/grammer/README.txt b/grammer/README.txt
deleted file mode 100644 (file)
index 0d25b20..0000000
+++ /dev/null
@@ -1,7 +0,0 @@
-"preScanner.jj" is used to process the backslash sign at the end of a line
-(basically splice broken lines before really processing the specifications).
-
-"util.jj" is used to process some specific strings, such as the declaration of a
-function with templated types. It is designed to be used as a library funcions.
-
-"spec_compiler.jj" is the file to parse the extracted specifications.
diff --git a/grammer/backup-spec-compiler.jj b/grammer/backup-spec-compiler.jj
deleted file mode 100644 (file)
index e65f339..0000000
+++ /dev/null
@@ -1,800 +0,0 @@
-/* spec-compiler.jj Grammer definition for the specification */
-
-
-/*
-       SPEC constructs:
-       Each construct should be embraced by /DOUBLE_STAR ... STAR/ annotation.
-       Within there, any line beginning with a "#" is a comment of the annotation.
-       Each constrcut should begin with @Begin and end with @End. Otherwise, the
-       annotation would be considered as normal comments of the source.
-       
-       a) Global construct
-       @Begin
-       @Options:
-               # If LANG is not define, it's C++ by default. C does not support class
-               # and template, so if it's defined as C, we should also have a explicit
-               # entry point.
-               LANG = C;
-       @Global_define:
-               @DeclareVar:
-               @InitVar:
-               @DefineFunc:
-               ...
-       @Interface_cluster:
-               ...
-       @Happens-before:
-               ...
-       @End
-       
-       b) Interface construct
-       @Begin
-       @Interface: ...
-       @Commit_point_set:
-               IDENTIFIER | IDENTIFIER ...
-       @Condition: ... (Optional)
-       @HB_Condition:
-               IDENTIFIER :: <C_CPP_Condition>
-       @HB_Condition: ...
-       @ID: ... (Optional, use default ID)
-       @Check: (Optional)
-               ...
-       @Action: (Optional)
-               # Type here must be a pointer
-               @DefineVar: Type var1 = SomeExpression (Optional)
-               @Code (Optional)
-               ...
-       @Post_action: (Optional)
-       @Post_check: (Optional)
-       @End
-
-       c) Potential commit construct
-       @Begin
-       @Potential_commit_point_define: ...
-       @Label: ...
-       @End
-
-       d) Commit point define construct
-       @Begin
-       @Commit_point_define_check: ...
-       @Label: ...
-       @End
-       
-               OR
-
-       @Begin
-       @Commit_point_define: ...
-       @Potential_commit_point_label: ...
-       @Label: ...
-       @End
-
-       e) Entry point construct
-       @Begin
-       @Entry_point
-       @End
-
-       f) Interface define construct
-       @Begin
-       @Interface_define: <Interface_Name>
-       @End
-*/
-
-
-
-options {
-       STATIC = false;
-       JAVA_UNICODE_ESCAPE = true;
-}
-
-PARSER_BEGIN(SpecParser)
-package edu.uci.eecs.specCompiler.grammerParser;
-
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.InputStream;
-import java.io.ByteArrayInputStream;
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.HashSet;
-
-import edu.uci.eecs.specCompiler.specExtraction.Construct;
-import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
-import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.ActionSubConstruct.DefineVar;
-import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
-
-       public class SpecParser {
-               public static void main(String[] argvs)
-               throws ParseException, TokenMgrError {
-                       try {
-                               FileInputStream fis = new FileInputStream("./grammer/spec.txt");
-                               SpecParser parser = new SpecParser(fis);
-                               //parser.Parse();
-                               System.out.println("Parsing finished!");
-                               ArrayList<String> typeParams = parser.FormalParamList();
-                       } catch (FileNotFoundException e) {
-                               e.printStackTrace();
-                       }
-               }
-       
-               public static Construct parseSpec(String text)
-               throws ParseException, TokenMgrError {
-                       InputStream input = new ByteArrayInputStream(text.getBytes());
-                       SpecParser parser = new SpecParser(input);
-                       return parser.Parse();
-               }
-
-
-       }
-PARSER_END(SpecParser)
-
-       "/*"}
-
-< IN_COMMENT > SKIP : { <  ~[] > }
-
-< IN_COMMENT > SKIP : {
-       "*/": DEFAULT
-}
-
-<IN_COMMENT> TOKEN : {
-       <A: "@A"> |
-       <B: "@B">
-}
-
-SKIP :
-{
-       " "
-|
-       "\n"
-|
-       "\r"
-|
-       "\r\n"
-|
-       "\t"
-|
-       // "#" comment for the specification
-       <"#" (~["\n", "\r"])* (["\n", "\r"])>
-|
-       // "//" comment for the specification
-       <"//" (~["\n", "\r"])* (["\n", "\r"])>
-}
-
-<IN_COMMENT, DEFAULT> TOKEN :
-{
-/*   Above are specification-only tokens   */
-       <HEAD: "/**" : IN_COMMENT>
-|
-       <TAIL: "*/" : DEFAULT>
-|
-       <BEGIN: "@Begin">
-|
-       <END: "@End">
-|
-       <OPTIONS: "@Options:">
-|
-       <GLOBAL_DEFINE: "@Global_define:">
-|
-       <DECLARE_VAR: "@DeclareVar:">
-|
-       <INIT_VAR: "@InitVar:">
-|
-       <DEFINE_FUNC: "@DefineFunc:">
-|
-       <INTERFACE_CLUSTER: "@Interface_cluster:">
-|
-       <HAPPENS_BEFORE: "@Happens_before:">
-|
-       <INTERFACE: "@Interface:">
-|
-       <COMMIT_POINT_SET: "@Commit_point_set:">
-|
-       <ENTRY_POINT: "@Entry_point">
-|
-       <INTERFACE_DEFINE: "@Interface_define:">
-|
-       <CONDITION: "@Condition:">
-|
-       <HB_CONDITION: "@HB_condition:">
-|
-       <ID: "@ID:">
-|
-       <CHECK: "@Check:">
-|
-       <ACTION: "@Action:">
-|
-       <DEFINEVAR: "@DefineVar:">
-|
-       <CODE: "@Code:">
-|
-       <POST_ACTION: "@Post_action:">
-|
-       <POST_CHECK: "@Post_check:">
-|
-       <POTENTIAL_COMMIT_POINT_DEFINE: "@Potential_commit_point_define:">
-|
-       <LABEL: "@Label:">
-|
-       <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
-|
-       <COMMIT_POINT_DEFINE: "@Commit_point_define:">
-|
-       <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
-
-
-/*   Specification & C/C++ shared tokens   */
-
-// Reserved keywords
-|
-       <CONST: "const">
-|
-       <STRUCT: "struct">
-|
-       <TYPENAME: "typename">
-
-
-|
-       <#DIGIT: ["0"-"9"]>
-|
-       <#LETTER: ["a"-"z", "A"-"Z"]>
-|
-       <IDENTIFIER: (<LETTER> | "_") (<LETTER> | <DIGIT> | "_")*>
-|
-       <EQUALS: "=">
-|
-       <OPEN_PAREN: "{">
-|
-       <CLOSE_PAREN: "}">
-|
-       <OPEN_BRACKET: "(">
-|
-       <CLOSE_BRACKET: ")">
-|
-       <HB_SYMBOL: "->">
-|
-       <COMMA: ",">
-
-|
-/*   C/C++ only token*/
-       <DOT: ".">
-|
-       <STAR: "*">
-|
-       <NEGATE: "~">
-|
-       <EXCLAMATION: "!">
-|
-       <AND: "&">
-|
-       <OR: "|">
-|
-       <MOD: "%">
-|
-       <PLUS: "+">
-|
-       <PLUSPLUS: "++">
-|
-       <MINUS: "-">
-|
-       <MINUSMINUS: "--">
-|
-       <DIVIDE: "/">
-|
-       <BACKSLASH: "\\">
-|
-       <LESS_THAN: "<">
-|
-       <GREATER_THAN: ">">
-|
-       <GREATER_EQUALS: ">=">
-|
-       <LESS_EQUALS: "<=">
-|
-       <LOGICAL_EQUALS: "==">
-|
-       <NOT_EQUALS: "!=">
-|
-       <LOGICAL_AND: "&&">
-|
-       <LOGICAL_OR: "||">
-|
-       <XOR: "^">
-|
-       <QUESTION_MARK: "?">
-|
-       <COLON: ":">
-|
-       <DOUBLECOLON: "::">
-|
-       <SEMI_COLON: ";">
-|
-       <STRING_LITERAL:
-       "\""
-       ((~["\"","\\","\n","\r"])
-       | ("\\"
-               ( ["n","t","b","r","f","\\","'","\""]
-               | ["0"-"7"] ( ["0"-"7"] )?
-               | ["0"-"3"] ["0"-"7"]
-                       ["0"-"7"]
-               )
-               )
-       )*
-       "\"">
-|
-       <CHARACTER_LITERAL:
-       "'"
-       ((~["'","\\","\n","\r"])
-       | ("\\"
-               (["n","t","b","r","f","\\","'","\""]
-               | ["0"-"7"] ( ["0"-"7"] )?
-               | ["0"-"3"] ["0"-"7"]
-               ["0"-"7"]
-               )
-               )
-       )
-       "'">
-|
-       < INTEGER_LITERAL:
-        <DECIMAL_LITERAL> (["l","L"])?
-      | <HEX_LITERAL> (["l","L"])?
-      | <OCTAL_LITERAL> (["l","L"])?>
-|
-       < #DECIMAL_LITERAL: ["1"-"9"] (["0"-"9"])* >
-|
-       < #HEX_LITERAL: "0" ["x","X"] (["0"-"9","a"-"f","A"-"F"])+ >
-|
-       < #OCTAL_LITERAL: "0" (["0"-"7"])* >
-|
-       < FLOATING_POINT_LITERAL:
-        <DECIMAL_FLOATING_POINT_LITERAL>
-      | <HEXADECIMAL_FLOATING_POINT_LITERAL> >
-|
-       < #DECIMAL_FLOATING_POINT_LITERAL:
-        (["0"-"9"])+ "." (["0"-"9"])* (<DECIMAL_EXPONENT>)? (["f","F","d","D"])?
-      | "." (["0"-"9"])+ (<DECIMAL_EXPONENT>)? (["f","F","d","D"])?
-      | (["0"-"9"])+ <DECIMAL_EXPONENT> (["f","F","d","D"])?
-      | (["0"-"9"])+ (<DECIMAL_EXPONENT>)? ["f","F","d","D"]>
-|
-       < #DECIMAL_EXPONENT: ["e","E"] (["+","-"])? (["0"-"9"])+ >
-|
-       < #HEXADECIMAL_FLOATING_POINT_LITERAL:
-        "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])+ (".")? <HEXADECIMAL_EXPONENT> (["f","F","d","D"])?
-      | "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])* "." (["0"-"9","a"-"f","A"-"F"])+ <HEXADECIMAL_EXPONENT> (["f","F","d","D"])?>
-|
-       < #HEXADECIMAL_EXPONENT: ["p","P"] (["+","-"])? (["0"-"9"])+ >
-}
-
-String Type() :
-{
-       String type;
-       String str;
-}
-{
-       { type = ""; }
-       ("const"
-       { type = "const"; }
-       )?
-       (("struct" { type = type + " struct"; })? 
-       (str = <IDENTIFIER>.image {
-               if (!type.equals(""))
-                       type = type + " " + str;
-               else
-                       type = str;
-       }))
-       ((str = "const".image {
-               if (!type.equals(""))
-                       type = type + " " + str;
-               else
-                       type = str;
-       }) |
-       (str = <STAR>.image {
-               if (!type.equals(""))
-                       type = type + " " + str;
-               else
-                       type = str;
-       }) |
-       (str = <AND>.image {
-               if (!type.equals(""))
-                       type = type + " " + str;
-               else
-                       type = str;
-       })
-       )*
-       {
-               return type;
-       }
-}
-
-ArrayList<String> FormalParamList() :
-{
-       ArrayList<String> typeParams;
-}
-{
-       {
-               typeParams = new ArrayList<String>();
-       }
-       (TypeParam(typeParams) (<COMMA> TypeParam(typeParams))*)?
-       {
-               System.out.println(typeParams);
-               return typeParams;
-       }
-}
-
-void TypeParam(ArrayList<String> typeParams) :
-{
-       String type, param;
-}
-{
-       (type = Type()) (param = <IDENTIFIER>.image)
-       {
-               typeParams.add(type);
-               typeParams.add(param);
-       }
-}
-
-Construct Parse() :
-{
-       Construct res;  
-}
-{
-       (
-       LOOKAHEAD(3) res = Global_construct() |
-       LOOKAHEAD(3) res = Interface() |
-       LOOKAHEAD(3) res = Potential_commit_point_define() |
-       LOOKAHEAD(3) res = Commit_point_define() |
-       LOOKAHEAD(3) res = Commit_point_define_check() |
-       LOOKAHEAD(3) res = Entry_point() |
-       LOOKAHEAD(3) res = Interface_define()
-       )
-       <EOF>
-       {
-               //System.out.println(res);
-               return res;
-       }
-}
-
-GlobalConstruct Global_construct() :
-{
-       GlobalConstruct res;
-       SequentialDefineSubConstruct code;
-       HashMap<String, String> options;
-       String key, value;
-}
-{
-       {
-               res = null;
-               options = new HashMap<String, String>();
-       }
-       <HEAD>
-               <BEGIN> 
-                       (<OPTIONS>
-                               ((key = <IDENTIFIER>.image)
-                               <EQUALS>
-                               (value = <IDENTIFIER>.image)
-                               {
-                                       if (options.containsKey(key)) {
-                                               throw new ParseException("Duplicate options!");
-                                       }
-                                       options.put(key, value);
-                               }
-                               <SEMI_COLON>
-                               )*
-                       )?
-                       (code = Global_define())
-                       { res = new GlobalConstruct(code, options); }
-                       (Interface_clusters(res))?
-                       (Happens_before(res))?
-               <END>
-       <TAIL>
-       {
-               res.unfoldInterfaceCluster();
-               return res;
-       }
-}
-
-String C_CPP_CODE() :
-{
-       StringBuilder text;
-       Token t;
-}
-{
-       {
-               text = new StringBuilder();
-               t = new Token();
-       }
-       (
-       //LOOKAHEAD(2)
-       (
-       t = <CONST> | t = <STRUCT> |
-       t = <IDENTIFIER> | t = <EQUALS> | t = <OPEN_PAREN> | t = <CLOSE_PAREN> |
-       t = <OPEN_BRACKET> | t = <CLOSE_BRACKET> | t = <HB_SYMBOL> | t = <COMMA> |
-       t = <DOT> | t = <STAR> | t = <NEGATE> | t = <EXCLAMATION> | t = <AND> | t = <OR> | t = <MOD> | t = <PLUS> |
-       t = <PLUSPLUS> | t = <MINUS> | t = <MINUSMINUS> | t = <DIVIDE> | t = <BACKSLASH> |
-       t = <LESS_THAN> | t = <GREATER_THAN> | t = <GREATER_EQUALS>     | t = <LESS_EQUALS> |
-       t = <LOGICAL_EQUALS> | t = <NOT_EQUALS> | t = <LOGICAL_AND> | t = <LOGICAL_OR> | t = <XOR> |
-       t = <QUESTION_MARK> | t = <COLON> | t = <DOUBLECOLON> |
-       t = <SEMI_COLON> | t = <STRING_LITERAL> | t = <CHARACTER_LITERAL> |
-       t = <INTEGER_LITERAL> | t = <FLOATING_POINT_LITERAL>
-       )
-       {
-               text.append(t.image);
-               if (t.image.equals(";") || t.image.equals("\\")
-                       || t.image.equals("{") || t.image.equals("}"))
-                       text.append("\n");
-               else
-                       text.append(" ");
-       }
-       )+
-       {
-               //System.out.println(text);
-               return text.toString();
-       }
-}
-
-SequentialDefineSubConstruct Global_define() :
-{
-       String declareVar, initVar, defineFunc;
-}
-{
-       {
-               declareVar = "";
-               initVar = "";
-               defineFunc = "";
-       }
-       <GLOBAL_DEFINE>
-               (<DECLARE_VAR> (declareVar = C_CPP_CODE()))?
-       (<INIT_VAR> (initVar = C_CPP_CODE()))?
-       (<DEFINE_FUNC> (defineFunc = C_CPP_CODE()))?
-       {
-               SequentialDefineSubConstruct res = new SequentialDefineSubConstruct(declareVar, initVar, defineFunc);
-               //System.out.println(res);
-               return res;
-       }
-}
-
-ConditionalInterface Conditional_interface() :
-{
-       String interfaceName, hbConditionLabel;
-}
-{
-       {
-               hbConditionLabel = "";
-       }
-       interfaceName = <IDENTIFIER>.image (<OPEN_BRACKET> hbConditionLabel =
-       <IDENTIFIER>.image <CLOSE_BRACKET>)?
-       {
-               return new ConditionalInterface(interfaceName, hbConditionLabel);
-       }
-}
-
-void Interface_cluster(GlobalConstruct inst) :
-{
-       String clusterName;
-       ConditionalInterface condInterface;
-}
-{
-       (clusterName= <IDENTIFIER>.image)
-       <EQUALS> <OPEN_PAREN>
-               (condInterface = Conditional_interface()
-               { inst.addInterface2Cluster(clusterName, condInterface); } 
-               )
-               (<COMMA> condInterface = Conditional_interface()
-               { inst.addInterface2Cluster(clusterName, condInterface); } 
-               )*
-       <CLOSE_PAREN>
-}
-
-void Interface_clusters(GlobalConstruct inst) :
-{}
-{
-       <INTERFACE_CLUSTER> (Interface_cluster(inst))+
-}
-
-void Happens_before(GlobalConstruct inst) :
-{
-       ConditionalInterface left, right;       
-}
-{
-       <HAPPENS_BEFORE> 
-       (
-       left = Conditional_interface() <HB_SYMBOL> right = Conditional_interface()
-       { inst.addHBCondition(left, right); }
-       )+
-}
-
-InterfaceConstruct Interface() :
-{
-       InterfaceConstruct res;
-       String interfaceName, condition, idCode, check, postAction,
-               postCheck, commitPoint, hbLabel, hbCondition;
-       ActionSubConstruct action;
-       ArrayList<String> commitPointSet;
-       HashMap<String, String> hbConditions;
-}
-{
-       {
-               res = null;
-               action = null;
-               condition = "";
-               idCode = "";
-               check = "";
-               postAction = "";
-               postCheck = "";
-               commitPointSet = new ArrayList<String>();
-               hbConditions = new HashMap<String, String>();
-       }
-       <HEAD> 
-               <BEGIN>
-                       <INTERFACE> (interfaceName = <IDENTIFIER>.image)
-                       <COMMIT_POINT_SET>
-                               (commitPoint = <IDENTIFIER>.image
-                               { commitPointSet.add(commitPoint); }
-                               )
-                               (<OR>
-                                       (commitPoint = <IDENTIFIER>.image)
-                                       {
-                                               if (commitPointSet.contains(commitPoint)) {
-                                                       throw new ParseException(interfaceName + " has" +
-                                                               "duplicate commit point labels");
-                                               }
-                                               commitPointSet.add(commitPoint);
-                                       }
-                               )*
-
-                       (<CONDITION> (condition = C_CPP_CODE()))?
-                       (
-                               <HB_CONDITION>
-                               (hbLabel = <IDENTIFIER>.image)
-                               (hbCondition = C_CPP_CODE())
-                               {
-                                       if (hbConditions.containsKey(hbLabel)) {
-                                               throw new ParseException(interfaceName + " has" +
-                                                       "duplicate happens-before condtion labels");
-                                       }
-                                       hbConditions.put(hbLabel, hbCondition);
-                               }
-                       )*
-                       (<ID> (idCode = C_CPP_CODE()))?
-                       (<CHECK> (check = C_CPP_CODE()))?
-                       (action = Action())?
-                       (<POST_ACTION> (postAction = C_CPP_CODE()))?
-                       (<POST_CHECK> (postCheck = C_CPP_CODE()))?
-               <END>
-       <TAIL>
-       {
-               res = new InterfaceConstruct(interfaceName, commitPointSet, condition,
-                       hbConditions, idCode, check, action, postAction, postCheck);
-               return res;
-       }
-}
-
-ActionSubConstruct Action() :
-{
-       String type, name, expr, defineVarStr, code;
-       ArrayList<DefineVar> defineVars;
-}
-{
-       {
-               defineVars = new ArrayList<DefineVar>();
-               code = "";
-       }
-       <ACTION>
-       (
-               (
-               (<DEFINEVAR> (defineVarStr = C_CPP_CODE()) 
-               {
-                       int eqIdx = defineVarStr.indexOf('=');
-                       int typeEnd = defineVarStr.lastIndexOf(' ', eqIdx - 2);
-                       type = defineVarStr.substring(0, typeEnd);
-                       name = defineVarStr.substring(typeEnd + 1, eqIdx - 1);
-                       expr = defineVarStr.substring(eqIdx + 2);
-                       DefineVar defineVar = new DefineVar(type, name, expr);
-                       defineVars.add(defineVar);
-               })*  (<CODE> (code = C_CPP_CODE()))? ) 
-       )
-       
-       {
-               ActionSubConstruct res = new ActionSubConstruct(defineVars, code);
-               return res;
-       }
-}
-
-PotentialCPDefineConstruct Potential_commit_point_define() :
-{
-       PotentialCPDefineConstruct res;
-       String label, condition;
-}
-{
-
-       { res = null; }
-       <HEAD> 
-               <BEGIN>
-                       <POTENTIAL_COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       <TAIL>
-       {
-               res = new PotentialCPDefineConstruct(label, condition); 
-               return res;
-       }
-}
-
-
-CPDefineConstruct Commit_point_define() :
-{
-       CPDefineConstruct res;
-       String label, potentialCPLabel, condition;
-}
-{
-
-       { res = null; }
-       <HEAD> 
-               <BEGIN>
-                       <COMMIT_POINT_DEFINE> (condition = C_CPP_CODE())
-                       <POTENTIAL_COMMIT_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       <TAIL>
-       {
-               res = new CPDefineConstruct(label, potentialCPLabel, condition);
-               return res;
-       }
-}
-
-
-CPDefineCheckConstruct Commit_point_define_check() :
-{
-       CPDefineCheckConstruct res;     
-       String label, condition;
-}
-{
-
-       { res = null; }
-       <HEAD> 
-               <BEGIN> 
-                       <COMMIT_POINT_DEFINE_CHECK> (condition = C_CPP_CODE())
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       <TAIL>
-       {
-               res = new CPDefineCheckConstruct(label, condition);
-               return res;
-       }
-}
-
-EntryPointConstruct Entry_point() :
-{}
-{
-
-       <HEAD> 
-               <BEGIN> 
-                       <ENTRY_POINT>
-               <END>
-       <TAIL>
-       {
-               return new EntryPointConstruct();
-       }
-}
-
-InterfaceDefineConstruct Interface_define() :
-{
-       String name;    
-}
-{
-       <HEAD>
-               <BEGIN>
-                       <INTERFACE_DEFINE> (name = <IDENTIFIER>.image)
-               <END>
-       <TAIL>
-       {
-               return new InterfaceDefineConstruct(name);
-       }
-}
-
-
diff --git a/grammer/pre_scanner.jj b/grammer/pre_scanner.jj
deleted file mode 100644 (file)
index 301ae88..0000000
+++ /dev/null
@@ -1,52 +0,0 @@
-/* pre_scan.jj Process the backslash at the end of line */
-
-options {
-       STATIC = false;
-       JAVA_UNICODE_ESCAPE = true;
-}
-
-PARSER_BEGIN(PreScanner)
-package edu.uci.eecs.specCompiler.grammerParser.preScanner;
-
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.InputStream;
-import java.io.ByteArrayInputStream;
-import java.util.ArrayList;
-
-       public class PreScanner {
-               public static void main(String[] argvs)
-               throws ParseException, TokenMgrError {
-                       try {
-                               FileInputStream fis = new FileInputStream("./grammer/spec.txt");
-                               PreScanner preScanner = new PreScanner(fis);
-                               String code = preScanner.ProcessEndBackslash();
-                               System.out.println(code);
-                               System.out.println("Finished!");
-                       } catch (FileNotFoundException e) {
-                               e.printStackTrace();
-                       }
-               }
-       }
-PARSER_END(PreScanner)
-
-SKIP : {
-       <"\\\n">
-}
-
-TOKEN : {
-       <ANY: ~[]>
-}
-
-String ProcessEndBackslash() :
-{
-       StringBuilder sb;
-       String str;
-}
-{
-       { sb = new StringBuilder(); }
-       (str = <ANY>.image { sb.append(str); } )* <EOF>
-       {
-               return sb.toString();
-       }
-}
diff --git a/grammer/spec.txt b/grammer/spec.txt
deleted file mode 100644 (file)
index 1ac8dc1..0000000
+++ /dev/null
@@ -1,55 +0,0 @@
-/**
-@Begin
-               @Options:
-                       LANG = C;
-                       CLASS = cliffc_hashtable;
-               @Global_define:
-                       @DeclareVar:
-                       spec_hashtable<TypeK, TypeV*> map;
-                       spec_hashtable<TypeK, Tag> id_map;
-                       Tag tag;
-                       @InitVar:
-                               map = spec_hashtable<TypeK, TypeV*>();
-                               id_map = spec_hashtable<TypeK, TypeV*>();
-                               tag = Tag();
-                       @DefineFunc:
-                       static bool equals_val(TypeV *ptr1, TypeV *ptr2) {
-                               // ...
-                       }
-                       
-                       # Update the tag for the current key slot if the corresponding tag
-                       # is NULL, otherwise just return that tag. It will update the next
-                       # available tag too if it requires a new tag for that key slot.
-                       static Tag getKeyTag(TypeK &key) {
-                               if (id_map.get(key) == NULL) {
-                                       Tag cur_tag = tag.current();
-                                       id_map.put(key, cur_tag);
-                                       tag.next();
-                                       return cur_tag;
-                               } else {
-                                       return id_map.get(key);
-                               }
-                       }
-               
-               @Interface_cluster:
-                       Read_interface = {
-                               Get,
-                               PutIfAbsent,
-                               RemoveAny,
-                               RemoveIfMatch,
-                               ReplaceAny,
-                               ReplaceIfMatch
-                       }
-                       
-                       Write_interface = {
-                               Put,
-                               PutIfAbsent(COND_PutIfAbsentSucc),
-                               RemoveAny,
-                               RemoveIfMatch(COND_RemoveIfMatchSucc),
-                               ReplaceAny,
-                               ReplaceIfMatch(COND_ReplaceIfMatchSucc)
-                       }
-               @Happens_before:
-                       Write_interface -> Read_interface
-               @End
-       */
diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj
deleted file mode 100644 (file)
index 2a8c779..0000000
+++ /dev/null
@@ -1,1280 +0,0 @@
-/* spec-compiler.jj Grammer definition for the specification */
-
-
-/*
-       SPEC constructs:
-       Each construct should be embraced by /DOUBLE_STAR ... STAR/ annotation.
-       Within there, any line beginning with a "#" is a comment of the annotation.
-       Each constrcut should begin with @Begin and end with @End. Otherwise, the
-       annotation would be considered as normal comments of the source.
-       
-       a) Global construct
-       @DeclareState: C/C++ variable declaration; // Declare the state structure
-       @InitState: C/C++ statements; // Specify how to initialize the state
-       @CopyState: // A function on how to copy an existing state (Not sure if we
-                               // need this because we might be able to auto this
-       @Commutativity: Method1 <-> Method2 (Guard) // Admissibility condition.
-                                                                                               // Allow specify 0-many rules
-       
-       b) Interface construct
-       @Interface: InterfaceName // Required; a label to represent the interface
-       @LocalState: // Optional; to calculate the accumulative local state before this
-                                // method call in a customized fashion. If not specified here, the
-                                // local state would be default, which is the result of the
-                                // execution on the subset of method calls in the sequential order
-       @PreCondition: // Optional; checking code
-       @LocalSideEffect: // Optional; to calculate the side effect this method call
-                                         // have on the local state in a customized fashion. If this
-                                         // field is not stated, it means we don't care about it.
-       @SideEffect: // Optional; to calculate the side effect on the global state. When
-                       // the "@LocalSideEffect" specification is ommitted, we also impose the
-                       // same side effect on the set of method calls that happen before this
-                       // method call in the sequential order.
-       @PostCondition: // Optional; checking code
-
-
-       c) Ordering point construct
-       @OPDefine: condition    // If the specified condition satisfied, the atomic
-                                                       // operation right before is an ordering point
-
-       @PotentialOP(Label): condition  // If the specified condition satisfied, the
-                                                                       // atomic operation right before is a potential
-                                                                       // ordering point, and we label it with a tag
-
-       @OPCheck(Label): condition      // If the specified condition satisfied, the
-                                                               // potential ordering point defined earlier with the
-                                                               // same tag becomes an ordering point
-
-       @OPClear: condition             // If the specified condition satisfied, all the
-                                                       // ordering points and potential ordering points will be
-                                                       // cleared
-
-       @OPClearDefine: condition       // If the specified condition satisfied, all the
-                                                               // ordering points and potential ordering points will
-                                                               // be cleared, and the atomic operation right before
-                                                               // becomes an ordering point. This is a syntax sugar
-                                                               // as the combination of an "OPClear" and "OPDefine"
-                                                               // statement
-
-*/
-
-
-
-options {
-       STATIC = false;
-       JAVA_UNICODE_ESCAPE = true;
-}
-
-PARSER_BEGIN(SpecParser)
-package edu.uci.eecs.specCompiler.grammerParser;
-
-import java.io.FileInputStream;
-import java.io.FileNotFoundException;
-import java.io.InputStream;
-import java.io.ByteArrayInputStream;
-import java.io.File;
-import java.util.ArrayList;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.Arrays;
-
-import edu.uci.eecs.specCompiler.specExtraction.Construct;
-import edu.uci.eecs.specCompiler.specExtraction.GlobalConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.InterfaceConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.PotentialCPDefineConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.CommutativityRule;
-import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
-import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.EntryPointConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.ClassBeginConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
-import edu.uci.eecs.specCompiler.specExtraction.FunctionHeader;
-import edu.uci.eecs.specCompiler.specExtraction.QualifiedName;
-import edu.uci.eecs.specCompiler.specExtraction.SourceFileInfo;
-import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
-
-       public class SpecParser {
-               private static ArrayList<String> _content;
-               private static File _file;
-               private static ArrayList<Construct> _constructs;
-
-
-               public static void main(String[] argvs)
-               throws ParseException, TokenMgrError {
-                       try {
-                               File f = new File("./grammer/spec1.txt");
-                               FileInputStream fis = new FileInputStream(f);
-                               SpecParser parser = new SpecParser(fis);
-                               
-                               ArrayList<String> content = new ArrayList<String>();
-                               ArrayList<Construct> constructs = new ArrayList<Construct>();
-                               ArrayList<String> headers = new ArrayList<String>();
-                               parser.Parse(f, content, constructs, headers);
-                               for (int i = 0; i < content.size(); i++) {
-                                       System.out.println(content.get(i));
-                               }
-                               
-                               for (int i = 0; i < constructs.size(); i++) {
-                                       System.out.println(constructs.get(i));
-                               }
-                               
-                               
-                               //parser.Test();
-                               System.out.println("Parsing finished!");
-                       } catch (FileNotFoundException e) {
-                               e.printStackTrace();
-                       }
-               }
-
-               public static SourceFileInfo ParseFile(File f)
-               throws ParseException, TokenMgrError {
-                       try {
-                               InputStream input = new FileInputStream(f);
-                               SpecParser parser = new SpecParser(input);
-                               ArrayList<String> content = new ArrayList<String>(),
-                                       headers = new ArrayList<String>();
-                               ArrayList<Construct> constructs = new ArrayList<Construct>();
-                               parser.Parse(f, content, constructs, headers);
-                               return new SourceFileInfo(f, content, headers, constructs);
-                       } catch (FileNotFoundException e) {
-                               e.printStackTrace();
-                       }
-                       return null;
-               }
-
-
-               private static ArrayList<String> breakLines(String all) {
-                       String lines[] = all.split("[\\r\\n]+");
-                       return new ArrayList<String>(Arrays.asList(lines));
-               }
-
-
-               public static ArrayList<VariableDeclaration> getTemplateArg(String line)
-               throws ParseException {
-                       InputStream input = new ByteArrayInputStream(line.getBytes());
-                       SpecParser parser = new SpecParser(input);
-                       return parser.TemplateParamList();
-               }
-
-               public static FunctionHeader parseFuncHeader(String line)
-               throws ParseException {
-                       InputStream input = new ByteArrayInputStream(line.getBytes());
-                       SpecParser parser = new SpecParser(input);
-                       return parser.FuncDecl();
-               }
-
-
-               public static String stringArray2String(ArrayList<String> content) {
-                       StringBuilder sb = new StringBuilder();
-                       if (content.size() == 1)
-                               return content.get(0);
-                       for (int i = 0; i < content.size(); i++) {
-                               sb.append(content.get(i) + "\n");
-                       }
-                       return sb.toString();
-               }
-
-               /**
-               boolean spaceSeparator(Token t) {
-                       switch (t.image) {
-                               case "[":
-                               case "]":
-                               case "=":
-                               case "(":
-                               case ")":
-                               case ",":
-                               case ".":
-                               case "*":
-                               case "~":
-                               case "!":
-                               case "&":
-                               case "|":
-                               case "%":
-                               case "+":
-                               case "-":
-                               case "/":
-                               case "<":
-                               case ">":
-                               case "<=":
-                               case ">=":
-                               case "==":
-                               case "!=":
-                               case "&&":
-                               case "||":
-                               case "^":
-                               case "?":
-                               case ":":
-                               case "::":
-                               case "<<":
-                               case ">>":
-                               case ">>>":
-                               case "+=":
-                               case "-=":
-                               case "*=":
-                               case "/=":
-                               case "%=":
-                               case "^=":
-                               case "&=":
-                               case ";":
-                                       return false;
-                               default:
-                                       return true;
-                       }
-               }
-               */
-
-       }
-PARSER_END(SpecParser)
-
-
-
-<IN_POTENTIAL_SPEC, IN_SPEC> SKIP :
-{
-       " "
-|
-       "\n"
-|
-       "\r"
-|
-       "\r\n"
-|
-       "\t"
-}
-
-SKIP : {
-       "/**" : IN_POTENTIAL_SPEC
-}
-
-<IN_POTENTIAL_SPEC> TOKEN : {
-       <BEGIN: "@Begin"> : IN_SPEC
-}
-
-<IN_SPEC> SKIP : {
-       "*/" : DEFAULT
-}
-
-SKIP : {
-       "/*": IN_COMMENT
-}
-
-<DEFAULT> TOKEN: {
-       <ANY: ~[]>
-}
-
-<*> SKIP : {
-       // "//" comment for the specification
-       <"//" (~["\n", "\r"])* (["\n", "\r"])>
-}
-
-<IN_COMMENT, IN_POTENTIAL_SPEC> SKIP : {
-       "*/": DEFAULT
-}
-
-<IN_COMMENT, IN_POTENTIAL_SPEC> SKIP : { <  ~[] > }
-
-<IN_SPEC> SKIP :
-{
-       // "#" comment for the specification
-       <"#" (~["\n", "\r"])* (["\n", "\r"])>
-}
-
-
-<IN_SPEC> TOKEN : {
-       <END: "@End">
-|
-       <OPTIONS: "@Options:">
-|
-       <GLOBAL_DEFINE: "@Global_define:">
-|
-       <DECLARE_STRUCT: "@DeclareStruct:">
-|
-       <DECLARE_VAR: "@DeclareVar:">
-|
-       <INIT_VAR: "@InitVar:">
-|
-       <CLEANUP: "@Finalize:">
-|
-       <DEFINE_FUNC: "@DefineFunc:">
-|
-       <INTERFACE_CLUSTER: "@Interface_cluster:">
-|
-       <HAPPENS_BEFORE: "@Happens_before:">
-|
-       <COMMUTATIVITY: "@Commutativity:">
-|
-       <INTERFACE: "@Interface:">
-|
-       <COMMIT_POINT_SET: "@Commit_point_set:">
-|
-       <ENTRY_POINT: "@Entry_point">
-|
-       <CLASS_BEGIN: "@Class_begin">
-|
-       <CLASS_END: "@Class_end">
-|
-       <INTERFACE_DEFINE: "@Interface_define:">
-|
-       <CONDITION: "@Condition:">
-|
-       <HB_CONDITION: "@HB_condition:">
-|
-       <ID: "@ID:">
-|
-       <CHECK: "@Check:">
-|
-       <ACTION: "@Action:">
-|
-       <CODE: "@Code:">
-|
-       <POST_ACTION: "@Post_action:">
-|
-       <POST_CHECK: "@Post_check:">
-|
-       <POTENTIAL_COMMIT_POINT_DEFINE: "@Potential_commit_point_define:">
-|
-       <POTENTIAL_ADDITIONAL_ORDERING_POINT_DEFINE: "@Potential_additional_ordering_point_define:">
-|
-       <LABEL: "@Label:">
-|
-       <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
-|
-       <ADDITIONAL_ORDERING_POINT_DEFINE_CHECK: "@Additional_ordering_point_define_check:">
-|
-       <COMMIT_POINT_DEFINE: "@Commit_point_define:">
-|
-       <ADDITIONAL_ORDERING_POINT_DEFINE: "@Additional_ordering_point_define:">
-|
-       <COMMIT_POINT_CLEAR: "@Commit_point_clear:">
-|
-       <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
-|
-       <POTENTIAL_ADDITIONAL_ORDERING_POINT_LABEL: "@Potential_additional_ordering_point_label:">
-}
-
-
-<IN_SPEC> TOKEN :
-{
-/*   Specification & C/C++ shared tokens   */
-// Reserved keywords
-       <CONST: "const">
-|
-       <STRUCT: "struct">
-|
-       <CLASS: "class">
-|
-       <UNSIGNED: "unsigned">
-|
-       <TEMPLATE: "template">
-|
-       <INLINE: "inline">
-|
-       <STATIC: "static">
-|
-       <FOR: "for">
-|
-       <#DIGIT: ["0"-"9"]>
-|
-       <#LETTER: ["a"-"z", "A"-"Z"]>
-|
-       <IDENTIFIER: (<LETTER> | "_") (<LETTER> | <DIGIT> | "_")*>
-|
-       <POUND: "#">
-|
-       <OPEN_BRACKET: "[">
-|
-       <CLOSE_BRACKET: "]">
-|
-       <EQUALS: "=">
-|
-       <OPEN_PAREN: "(">
-|
-       <CLOSE_PAREN: ")">
-|
-       <OPEN_BRACE: "{">
-|
-       <CLOSE_BRACE: "}">
-|
-       <HB_SYMBOL: "->">
-|
-       <COMMUTATIVITY_SYMBOL: "<->">
-|
-       <COMMA: ",">
-|
-/*   C/C++ only token*/
-       <DOT: ".">
-|
-       <DOLLAR: "$">
-|
-       <STAR: "*">
-|
-       <NEGATE: "~">
-|
-       <EXCLAMATION: "!">
-|
-       <AND: "&">
-|
-       <OR: "|">
-|
-       <MOD: "%">
-|
-       <PLUS: "+">
-|
-       <PLUSPLUS: "++">
-|
-       <MINUS: "-">
-|
-       <MINUSMINUS: "--">
-|
-       <DIVIDE: "/">
-|
-       <BACKSLASH: "\\">
-|
-       <LESS_THAN: "<">
-|
-       <GREATER_THAN: ">">
-|
-       <GREATER_EQUALS: ">=">
-|
-       <LESS_EQUALS: "<=">
-|
-       <LOGICAL_EQUALS: "==">
-|
-       <NOT_EQUALS: "!=">
-|
-       <LOGICAL_AND: "&&">
-|
-       <LOGICAL_OR: "||">
-|
-       <XOR: "^">
-|
-       <QUESTION_MARK: "?">
-|
-       <COLON: ":">
-|
-       <DOUBLECOLON: "::">
-|
-       <DOUBLELESSTHAN: "<<">
-|
-       <DOUBLEGREATERTHAN: ">>">
-|
-       <TRIPLEGREATERTHAN: ">>>">
-|
-       <PLUS_EQUALS: "+=">
-|
-       <MINUS_EQUALS: "-=">
-|
-       <TIMES_EQUALS: "*=">
-|
-       <DIVIDE_EQUALS: "/=">
-|
-       <MOD_EQUALS: "%=">
-|
-       <XOR_EQUALS: "^=">
-|
-       <OR_EQUALS: "|=">
-|
-       <AND_EQUALS: "&=">
-|
-       <SEMI_COLON: ";">
-|
-       <STRING_LITERAL:
-       "\""
-       ((~["\"","\\","\n","\r"])
-       | ("\\"
-               ( ["n","t","b","r","f","\\","'","\""]
-               | ["0"-"7"] ( ["0"-"7"] )?
-               | ["0"-"3"] ["0"-"7"]
-                       ["0"-"7"]
-               )
-               )
-       )*
-       "\"">
-|
-       <CHARACTER_LITERAL:
-       "'"
-       ((~["'","\\","\n","\r"])
-       | ("\\"
-               (["n","t","b","r","f","\\","'","\""]
-               | ["0"-"7"] ( ["0"-"7"] )?
-               | ["0"-"3"] ["0"-"7"]
-               ["0"-"7"]
-               )
-               )
-       )
-       "'">
-|
-       < INTEGER_LITERAL:
-        <DECIMAL_LITERAL> (["l","L"])?
-      | <HEX_LITERAL> (["l","L"])?
-      | <OCTAL_LITERAL> (["l","L"])?>
-|
-       < #DECIMAL_LITERAL: ["1"-"9"] (["0"-"9"])* >
-|
-       < #HEX_LITERAL: "0" ["x","X"] (["0"-"9","a"-"f","A"-"F"])+ >
-|
-       < #OCTAL_LITERAL: "0" (["0"-"7"])* >
-|
-       < FLOATING_POINT_LITERAL:
-        <DECIMAL_FLOATING_POINT_LITERAL>
-      | <HEXADECIMAL_FLOATING_POINT_LITERAL> >
-|
-       < #DECIMAL_FLOATING_POINT_LITERAL:
-        (["0"-"9"])+ "." (["0"-"9"])* (<DECIMAL_EXPONENT>)? (["f","F","d","D"])?
-      | "." (["0"-"9"])+ (<DECIMAL_EXPONENT>)? (["f","F","d","D"])?
-      | (["0"-"9"])+ <DECIMAL_EXPONENT> (["f","F","d","D"])?
-      | (["0"-"9"])+ (<DECIMAL_EXPONENT>)? ["f","F","d","D"]>
-|
-       < #DECIMAL_EXPONENT: ["e","E"] (["+","-"])? (["0"-"9"])+ >
-|
-       < #HEXADECIMAL_FLOATING_POINT_LITERAL:
-        "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])+ (".")? <HEXADECIMAL_EXPONENT> (["f","F","d","D"])?
-      | "0" ["x", "X"] (["0"-"9","a"-"f","A"-"F"])* "." (["0"-"9","a"-"f","A"-"F"])+ <HEXADECIMAL_EXPONENT> (["f","F","d","D"])?>
-|
-       < #HEXADECIMAL_EXPONENT: ["p","P"] (["+","-"])? (["0"-"9"])+ >
-|
-       < #SPACE: (" " | "\t")+>
-|
-       < #TO_END_OF_LINE: (~["\n"])+>
-|
-       /* Macro token */
-       <INCLUDE: "#" (<SPACE>)? "include" <SPACE> (<STRING_LITERAL> | "<" (<LETTER> | <DOT>)+ ">")>
-|
-       <DEFINE: "#" (<SPACE>)? <TO_END_OF_LINE>>
-}
-
-String Type() :
-{
-       String type;
-       String str;
-       QualifiedName name;
-}
-{
-       { type = ""; }
-       (<CONST>
-       { type = "const"; }
-       )?
-       (((str = <STRUCT>.image | str = <CLASS>.image | str = <UNSIGNED>.image) { type = type + " " + str; })? 
-       (
-       name = ParseQualifiedName() {
-               if (!type.equals(""))
-                       type = type + " " + name.fullName;
-               else
-                       type = name.fullName;
-       })
-       )
-       ((str = <CONST>.image {
-               if (!type.equals(""))
-                       type = type + " " + str;
-               else
-                       type = str;
-       }) |
-       (str = <STAR>.image {
-               if (!type.equals(""))
-                       type = type + " " + str;
-               else
-                       type = str;
-       }) |
-       (str = <AND>.image {
-               if (!type.equals(""))
-                       type = type + " " + str;
-               else
-                       type = str;
-       })
-       )*
-       {
-               return type;
-       }
-}
-
-
-String ParameterizedName() :
-{
-       String res = "";
-       String str;
-}
-{
-       (str = <IDENTIFIER>.image {res = str;})
-       (<OPEN_BRACKET> str = Type() { res = res + "<" + str; }
-       (<COMMA> str = Type() { res = res + ", " + str; })* <CLOSE_BRACKET>
-       { res = res + ">"; }
-       )?
-       {
-               return res;
-       }
-}
-
-FunctionHeader FuncDecl() :
-{
-       String ret;
-       QualifiedName funcName;
-       ArrayList<VariableDeclaration> args;
-}
-{
-       (<STATIC> | <INLINE>)*
-       ret = Type() 
-       funcName = ParseQualifiedName() 
-       args = FormalParamList() 
-       {
-               FunctionHeader res = new FunctionHeader(ret, funcName, args);
-               //System.out.println(res);
-               return res;
-       }
-}
-
-QualifiedName ParseQualifiedName() :
-{
-       String qualifiedName, str;
-}
-{
-       { qualifiedName = ""; }
-       (str = ParameterizedName() { qualifiedName = qualifiedName + str; } )
-       ( <DOUBLECOLON> (str = ParameterizedName() { qualifiedName = qualifiedName +
-       "::" + str; }  ))*
-       {
-               QualifiedName res = new QualifiedName(qualifiedName);
-               //System.out.println(res);
-               return res;
-       }
-}
-
-ArrayList<VariableDeclaration> TemplateParamList() :
-{
-       ArrayList<VariableDeclaration> params;
-       String type;
-       String name;
-}
-{
-       {
-               params = new ArrayList<VariableDeclaration>();
-       }
-       <TEMPLATE>
-       <OPEN_BRACKET>
-       (type = <IDENTIFIER>.image 
-       name = <IDENTIFIER>.image
-       {
-               params.add(new VariableDeclaration(type, name));
-       }
-       )
-
-       (<COMMA> type = <IDENTIFIER>.image 
-       name = <IDENTIFIER>.image
-       {
-               params.add(new VariableDeclaration(type, name));
-       }
-       )*
-       <CLOSE_BRACKET>
-       {
-               //System.out.println(params);
-               return params;
-       }
-}
-
-ArrayList<VariableDeclaration > FormalParamList() :
-{
-       ArrayList<VariableDeclaration > typeParams;
-       VariableDeclaration varDecl;
-}
-{
-       {
-               typeParams = new ArrayList<VariableDeclaration >();
-       }
-       <OPEN_PAREN>
-       ((varDecl = TypeParam() {typeParams.add(varDecl);})
-       ((<COMMA> varDecl = TypeParam() {typeParams.add(varDecl);}))*)?
-       <CLOSE_PAREN>
-       {
-               return typeParams;
-       }
-}
-
-VariableDeclaration TypeParam() :
-{
-       String type, param;
-}
-{
-       (type = Type()) (param = <IDENTIFIER>.image)
-       {
-               return new VariableDeclaration(type, param);
-       }
-}
-
-
-
-ArrayList<String> C_CPP_CODE(ArrayList<String> headers) :
-{
-       String text;
-       Token t;
-       boolean newLine = false;
-       boolean newSpace = true;
-       boolean inTemplate = false;
-       boolean inForLoop = false;
-       ArrayList<String> content;
-       String header;
-}
-{
-       {
-               text = "";
-               t = new Token();
-               content = new ArrayList<String>();
-       }
-       (
-       LOOKAHEAD(2)
-       (
-       t = <CONST> | t = <STRUCT> | t = <CLASS> | t = <UNSIGNED> |
-       (t = <TEMPLATE> { inTemplate = true;  })|
-       t = <STATIC> | t = <INLINE> |
-       (t = <FOR> { inForLoop = true; })|
-       (t = <INCLUDE>
-       {
-               header = t.image;
-               newLine = true;
-               if (headers != null) {
-                       headers.add(header.substring(header.lastIndexOf(' ') + 1));
-               }
-       })
-       | t = <IDENTIFIER> | t = <POUND> |
-       (t = <OPEN_BRACE>  { newLine = true; } ) |
-       (t = <CLOSE_BRACE>  { newLine = true; inForLoop = false;} ) | 
-       t = <EQUALS> | t = <OPEN_PAREN> | t = <CLOSE_PAREN> | 
-       t = <OPEN_BRACKET> | t = <CLOSE_BRACKET>
-       | t = <HB_SYMBOL> | t = <COMMA> |
-       t = <DOT> | t = <STAR> | t = <DOLLAR> | t = <NEGATE> | t = <EXCLAMATION> | t = <AND> | t = <OR> | t = <MOD> | t = <PLUS> |
-       t = <PLUSPLUS> | t = <MINUS> | t = <MINUSMINUS> | t = <DIVIDE> | t = <BACKSLASH> |
-       t = <LESS_THAN> |
-       (t = <GREATER_THAN> { if (inTemplate) newLine = true; }) |
-       t = <GREATER_EQUALS>    | t = <LESS_EQUALS> |
-       t = <LOGICAL_EQUALS> | t = <NOT_EQUALS> | t = <LOGICAL_AND> | t = <LOGICAL_OR> | t = <XOR> |
-       t = <QUESTION_MARK> | t = <COLON> | t = <DOUBLECOLON> |
-       t = <DOUBLELESSTHAN> | 
-       t = <DOUBLEGREATERTHAN> |
-       t = <TRIPLEGREATERTHAN> | 
-
-       t = <PLUS_EQUALS> |
-       t = <MINUS_EQUALS> |
-       t = <TIMES_EQUALS> |
-       t = <DIVIDE_EQUALS> |
-       t = <MOD_EQUALS> |
-       t = <XOR_EQUALS> |
-       t = <OR_EQUALS> |
-       t = <AND_EQUALS> |
-
-       (t = <SEMI_COLON> { if (!inForLoop) newLine = true; } )
-       | t = <STRING_LITERAL> | t = <CHARACTER_LITERAL> |
-       t = <INTEGER_LITERAL> | t = <FLOATING_POINT_LITERAL> |
-       (t = <DEFINE> { newLine = true; } )
-       )
-       {
-               if (text.equals("")) {
-                       text = t.image;
-                       newSpace = true;
-               } else {
-                       text = text + " " + t.image;
-                       /*
-                       if (newSpace && spaceSeparator(t)) {
-                               text = text + " " + t.image;
-                       } else {
-                               text = text + t.image;
-                               if (spaceSeparator(t))
-                                       newSpace = true;
-                       }*/
-               }
-               if (newLine) {
-                       content.add(text);
-                       text = "";
-                       newLine = false;
-                       inTemplate = false;
-               }
-       }
-       )+
-
-       {
-               if (content.size() == 0) {
-                       content.add(text);
-               }
-               return content;
-       }
-}
-
-
-void Parse(File f, ArrayList<String> content, ArrayList<Construct> constructs, ArrayList<String> headers) :
-{
-       Construct inst;
-       StringBuilder sb;
-       boolean flushSB;
-}
-{
-       {
-               _file = f;
-               _content = content;
-               _constructs = constructs;
-               sb = new StringBuilder();
-       }
-       (
-       (inst = ParseSpec()
-       {
-               _constructs.add(inst);
-       }
-       ) |
-       //((code = C_CPP_CODE(headers)) { _content.addAll(code); })
-       (
-       flushSB = OriginalCode(sb)
-       {
-               if (flushSB) {
-                       sb = new StringBuilder();
-               }
-       }
-       )
-       )* 
-       // For the last piece of code
-       {
-               _content.add(sb.toString());
-       }
-       <EOF>
-}
-
-// If true, there's a new line and sb should be flushed
-boolean OriginalCode(StringBuilder sb) :
-{
-       String str;
-}
-{
-       str = <ANY>.image
-       {
-               if (!str.equals("\n")) {
-                       sb.append(str);
-                       return false;
-               } else {
-                       _content.add(sb.toString());
-                       return true;
-               }
-       }
-}
-
-Construct ParseSpec() :
-{
-       Construct res;  
-}
-{
-       (
-       LOOKAHEAD(2) res = Global_construct() |
-       LOOKAHEAD(2) res = Interface() |
-       LOOKAHEAD(2) res = Potential_commit_point_define() |
-       LOOKAHEAD(2) res = Commit_point_define() |
-       LOOKAHEAD(2) res = Commit_point_define_check() |
-       LOOKAHEAD(2) res = Potential_additional_ordering_point_define() |
-       LOOKAHEAD(2) res = Additional_ordering_point_define() |
-       LOOKAHEAD(2) res = Additional_ordering_point_define_check() |
-       LOOKAHEAD(2) res = Commit_point_clear() |
-       LOOKAHEAD(2) res = Entry_point() |
-       LOOKAHEAD(2) res = Class_begin() |
-       LOOKAHEAD(2) res = Class_end() |
-       LOOKAHEAD(2) res = Interface_define()
-       )
-       {
-               //System.out.println(res);
-               return res;
-       }
-}
-
-GlobalConstruct Global_construct() :
-{
-       GlobalConstruct res;
-       SequentialDefineSubConstruct code;
-       HashMap<String, String> options;
-       String key, value;
-}
-{
-       {
-               res = null;
-               options = new HashMap<String, String>();
-       }
-               <BEGIN> 
-                       (<OPTIONS>
-                               ((key = <IDENTIFIER>.image)
-                               <EQUALS>
-                               (value = <IDENTIFIER>.image)
-                               {
-                                       if (options.containsKey(key)) {
-                                               throw new ParseException("Duplicate options!");
-                                       }
-                                       options.put(key, value);
-                               }
-                               <SEMI_COLON>
-                               )*
-                       )?
-                       (code = Global_define())
-                       { res = new GlobalConstruct(_file, _content.size(), code, options); }
-                       (Interface_clusters(res))?
-                       (Happens_before(res))?
-                       (Commutativity(res))?
-               <END>
-       {
-               res.unfoldInterfaceCluster();
-               return res;
-       }
-}
-
-SequentialDefineSubConstruct Global_define() :
-{
-       ArrayList<String> initVar, cleanup, defineFunc, code, declareStruct;
-       ArrayList<ArrayList<String>> defineFuncs;
-       ArrayList<VariableDeclaration> declareVars;
-       ArrayList<ArrayList<String>> declareStructs;
-       VariableDeclaration declareVar;
-
-}
-{
-       {
-               declareVars = new ArrayList<VariableDeclaration>();
-               initVar = new ArrayList<String>();
-               cleanup = new ArrayList<String>();
-               defineFuncs = new ArrayList<ArrayList<String>>();
-               declareStructs = new ArrayList<ArrayList<String>>();
-       }
-       <GLOBAL_DEFINE>
-       (<DECLARE_STRUCT> (declareStruct = C_CPP_CODE(null) {
-               declareStructs.add(declareStruct); }))*
-               (<DECLARE_VAR> ((declareVar = TypeParam() <SEMI_COLON> {
-                       declareVars.add(declareVar); } )*))?
-       (<INIT_VAR> (code = C_CPP_CODE(null) { initVar = code; } ))?
-       (<CLEANUP> (code = C_CPP_CODE(null) { cleanup = code; } ))?
-       (<DEFINE_FUNC> (defineFunc = C_CPP_CODE(null) { defineFuncs.add(defineFunc); }))*
-       {
-               SequentialDefineSubConstruct res = new
-                       SequentialDefineSubConstruct(declareStructs, declareVars, initVar, cleanup, defineFuncs);
-               //System.out.println(res);
-               return res;
-       }
-}
-
-ConditionalInterface Conditional_interface() :
-{
-       String interfaceName, hbConditionLabel;
-}
-{
-       {
-               hbConditionLabel = "";
-       }
-       interfaceName = <IDENTIFIER>.image (<OPEN_PAREN> hbConditionLabel =
-       <IDENTIFIER>.image <CLOSE_PAREN>)?
-       {
-               return new ConditionalInterface(interfaceName, hbConditionLabel);
-       }
-}
-
-void Interface_cluster(GlobalConstruct inst) :
-{
-       String clusterName;
-       ConditionalInterface condInterface;
-}
-{
-       (clusterName= <IDENTIFIER>.image)
-       <EQUALS> <OPEN_BRACE>
-               (condInterface = Conditional_interface()
-               { inst.addInterface2Cluster(clusterName, condInterface); } 
-               )
-               (<COMMA> condInterface = Conditional_interface()
-               { inst.addInterface2Cluster(clusterName, condInterface); } 
-               )*
-       <CLOSE_BRACE>
-}
-
-void Interface_clusters(GlobalConstruct inst) :
-{}
-{
-       <INTERFACE_CLUSTER> (Interface_cluster(inst))+
-}
-
-void Happens_before(GlobalConstruct inst) :
-{
-       ConditionalInterface left, right;       
-}
-{
-       <HAPPENS_BEFORE> 
-       (
-       left = Conditional_interface() <HB_SYMBOL> right = Conditional_interface()
-       { inst.addHBCondition(left, right); }
-       )+
-}
-
-void Commutativity(GlobalConstruct inst) :
-{
-       String method1, method2, condition;
-       ArrayList<String> content;
-}
-{
-       {
-               content = new ArrayList<String>();
-       }
-
-       (
-       <COMMUTATIVITY>
-       method1 = <IDENTIFIER>.image  <COMMUTATIVITY_SYMBOL>
-       method2 = <IDENTIFIER>.image
-       <COLON>
-       content = C_CPP_CODE(null)
-       { condition = stringArray2String(content); }
-       {
-               inst.addCommutativityRule(method1, method2, condition);
-       }
-       )+
-}
-
-InterfaceConstruct Interface() :
-{
-       InterfaceConstruct res;
-       String interfaceName, condition, idCode, check,
-               postCheck, commitPoint, hbLabel, hbCondition;
-       ArrayList<String> commitPointSet;
-       ArrayList<String> action, postAction;
-       HashMap<String, String> hbConditions;
-       ArrayList<String> content;
-}
-{
-       {
-               res = null;
-               action = new ArrayList<String>();
-               condition = "";
-               idCode = "";
-               check = "";
-               postCheck = "";
-               commitPointSet = new ArrayList<String>();
-               hbConditions = new HashMap<String, String>();
-               postAction = new ArrayList<String>();
-       }
-               <BEGIN>
-                       <INTERFACE> (interfaceName = <IDENTIFIER>.image)
-                       <COMMIT_POINT_SET>
-                               (commitPoint = <IDENTIFIER>.image
-                               { commitPointSet.add(commitPoint); }
-                               )
-                               (<OR>
-                                       (commitPoint = <IDENTIFIER>.image)
-                                       {
-                                               if (commitPointSet.contains(commitPoint)) {
-                                                       throw new ParseException(interfaceName + " has" +
-                                                               "duplicate commit point labels");
-                                               }
-                                               commitPointSet.add(commitPoint);
-                                       }
-                               )*
-
-                       (<CONDITION> (content = C_CPP_CODE(null) { condition = stringArray2String(content); }))?
-                       (
-                               <HB_CONDITION>
-                               (hbLabel = <IDENTIFIER>.image) <DOUBLECOLON>
-                               (content = C_CPP_CODE(null) { hbCondition = stringArray2String(content); })
-                               {
-                                       if (hbConditions.containsKey(hbLabel)) {
-                                               throw new ParseException(interfaceName + " has" +
-                                                       "duplicate happens-before condtion labels");
-                                       }
-                                       hbConditions.put(hbLabel, hbCondition);
-                               }
-                       )*
-                       (<ID> (content = C_CPP_CODE(null) { idCode = stringArray2String(content); }))?
-                       (<CHECK> (content = C_CPP_CODE(null) { check = stringArray2String(content); }))?
-                       (<ACTION> action = C_CPP_CODE(null))?
-                       (<POST_ACTION> (postAction = C_CPP_CODE(null) ))?
-                       (<POST_CHECK> (content = C_CPP_CODE(null) { postCheck = stringArray2String(content); }))?
-               <END>
-       {
-               res = new InterfaceConstruct(_file, _content.size(), interfaceName, commitPointSet, condition,
-                       hbConditions, idCode, check, action, postAction, postCheck);
-               return res;
-       }
-}
-
-
-PotentialCPDefineConstruct Potential_commit_point_define() :
-{
-       PotentialCPDefineConstruct res;
-       String label, condition;
-       ArrayList<String> content;
-}
-{
-
-       { res = null; }
-               <BEGIN>
-                       <POTENTIAL_COMMIT_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       {
-               res = new PotentialCPDefineConstruct(_file, _content.size(), label, condition); 
-               return res;
-       }
-}
-
-PotentialCPDefineConstruct Potential_additional_ordering_point_define() :
-{
-       PotentialCPDefineConstruct res;
-       String label, condition;
-       ArrayList<String> content;
-}
-{
-
-       { res = null; }
-               <BEGIN>
-                       <POTENTIAL_ADDITIONAL_ORDERING_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       {
-               // Set the boolean flag isAdditionalOrderingPoint to be true
-               res = new PotentialCPDefineConstruct(_file, _content.size(), true, label, condition); 
-               return res;
-       }
-}
-
-
-CPDefineConstruct Commit_point_define() :
-{
-       CPDefineConstruct res;
-       String label, potentialCPLabel, condition;
-       ArrayList<String> content;
-}
-{
-
-       { res = null; }
-               <BEGIN>
-                       <COMMIT_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
-                       <POTENTIAL_COMMIT_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       {
-               res = new CPDefineConstruct(_file, _content.size(), false, label, potentialCPLabel, condition);
-               return res;
-       }
-}
-
-CPDefineConstruct Additional_ordering_point_define() :
-{
-       CPDefineConstruct res;
-       String label, potentialCPLabel, condition;
-       ArrayList<String> content;
-}
-{
-
-       { res = null; }
-               <BEGIN>
-                       <ADDITIONAL_ORDERING_POINT_DEFINE> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
-                       <POTENTIAL_ADDITIONAL_ORDERING_POINT_LABEL> (potentialCPLabel = <IDENTIFIER>.image)
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       {
-               // Set the boolean flag isAdditionalOrderingPoint to be true
-               res = new CPDefineConstruct(_file, _content.size(), true, label, potentialCPLabel, condition);
-               return res;
-       }
-}
-
-CPClearConstruct Commit_point_clear() :
-{
-       CPClearConstruct res;   
-       String label, condition;
-       ArrayList<String> content;
-}
-{
-
-       { res = null; }
-               <BEGIN> 
-                       <COMMIT_POINT_CLEAR> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       {
-               res = new CPClearConstruct(_file, _content.size(), label, condition);
-               return res;
-       }
-}
-
-
-CPDefineCheckConstruct Commit_point_define_check() :
-{
-       CPDefineCheckConstruct res;     
-       String label, condition;
-       ArrayList<String> content;
-}
-{
-
-       { res = null; }
-               <BEGIN> 
-                       <COMMIT_POINT_DEFINE_CHECK> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       {
-               res = new CPDefineCheckConstruct(_file, _content.size(), false, label, condition);
-               return res;
-       }
-}
-
-CPDefineCheckConstruct Additional_ordering_point_define_check() :
-{
-       CPDefineCheckConstruct res;     
-       String label, condition;
-       ArrayList<String> content;
-}
-{
-
-       { res = null; }
-               <BEGIN> 
-                       <ADDITIONAL_ORDERING_POINT_DEFINE_CHECK> (content = C_CPP_CODE(null) { condition = stringArray2String(content); })
-                       <LABEL> (label = <IDENTIFIER>.image)
-               <END>
-       {
-               // Set the boolean flag isAdditionalOrderingPoint to be true
-               res = new CPDefineCheckConstruct(_file, _content.size(), true, label, condition);
-               return res;
-       }
-}
-
-EntryPointConstruct Entry_point() :
-{}
-{
-
-               <BEGIN> 
-                       <ENTRY_POINT>
-               <END>
-       {
-               return new EntryPointConstruct(_file, _content.size());
-       }
-}
-
-ClassBeginConstruct Class_begin() :
-{}
-{
-
-               <BEGIN> 
-                       <CLASS_BEGIN>
-               <END>
-       {
-               return new ClassBeginConstruct(_file, _content.size());
-       }
-}
-
-ClassEndConstruct Class_end() :
-{}
-{
-
-               <BEGIN> 
-                       <CLASS_END>
-               <END>
-       {
-               return new ClassEndConstruct(_file, _content.size());
-       }
-}
-
-InterfaceDefineConstruct Interface_define() :
-{
-       String name;    
-}
-{
-               <BEGIN>
-                       <INTERFACE_DEFINE> (name = <IDENTIFIER>.image)
-               <END>
-       {
-               return new InterfaceDefineConstruct(_file, _content.size(), name);
-       }
-}
index 5194e64..7e8b0c3 100644 (file)
@@ -6,10 +6,11 @@ options {
 }
 
 PARSER_BEGIN(UtilParser)
-package edu.uci.eecs.specCompiler.grammerParser.utilParser;
-import edu.uci.eecs.specCompiler.specExtraction.FunctionHeader;
-import edu.uci.eecs.specCompiler.specExtraction.QualifiedName;
-import edu.uci.eecs.specCompiler.specExtraction.VariableDeclaration;
+package edu.uci.eecs.utilParser;
+import edu.uci.eecs.specExtraction.FunctionHeader;
+import edu.uci.eecs.specExtraction.QualifiedName;
+import edu.uci.eecs.specExtraction.VariableDeclaration;
+//import edu.uci.eecs.specExtraction.WrongAnnotationException;
 
 import java.io.FileInputStream;
 import java.io.FileNotFoundException;
@@ -17,47 +18,48 @@ import java.io.InputStream;
 import java.io.ByteArrayInputStream;
 import java.io.File;
 import java.util.ArrayList;
+
        
-       public class UtilParser {
-               public static void main(String[] argvs)
-               throws ParseException, TokenMgrError {
-                       try {
-                               File f = new File("./grammer/spec1.txt");
-                               FileInputStream fis = new FileInputStream(f);
-                               UtilParser parser = new UtilParser(fis);
-                               
-                               //parser.Test();
-                               System.out.println("Parsing finished!");
-                       } catch (FileNotFoundException e) {
-                               e.printStackTrace();
-                       }
+public class UtilParser {
+       public static void main(String[] argvs)
+       throws ParseException, TokenMgrError {
+               try {
+                       File f = new File("./grammer/spec1.txt");
+                       FileInputStream fis = new FileInputStream(f);
+                       UtilParser parser = new UtilParser(fis);
+                       
+                       //parser.Test();
+                       System.out.println("Parsing finished!");
+               } catch (FileNotFoundException e) {
+                       e.printStackTrace();
                }
+       }
 
-               public static ArrayList<VariableDeclaration> getTemplateArg(String line)
-               throws ParseException {
-                       InputStream input = new ByteArrayInputStream(line.getBytes());
-                       UtilParser parser = new UtilParser(input);
-                       return parser.TemplateParamList();
-               }
+       public static ArrayList<VariableDeclaration> getTemplateArg(String line)
+       throws ParseException {
+               InputStream input = new ByteArrayInputStream(line.getBytes());
+               UtilParser parser = new UtilParser(input);
+               return parser.TemplateParamList();
+       }
 
-               public static FunctionHeader parseFuncHeader(String line)
-               throws ParseException {
-                       InputStream input = new ByteArrayInputStream(line.getBytes());
-                       UtilParser parser = new UtilParser(input);
-                       return parser.FuncDecl();
-               }
+       public static FunctionHeader parseFuncHeader(String line)
+       throws ParseException {
+               InputStream input = new ByteArrayInputStream(line.getBytes());
+               UtilParser parser = new UtilParser(input);
+               return parser.FuncDecl();
+       }
 
 
-               public static String stringArray2String(ArrayList<String> content) {
-                       StringBuilder sb = new StringBuilder();
-                       if (content.size() == 1)
-                               return content.get(0);
-                       for (int i = 0; i < content.size(); i++) {
-                               sb.append(content.get(i) + "\n");
-                       }
-                       return sb.toString();
+       public static String stringArray2String(ArrayList<String> content) {
+               StringBuilder sb = new StringBuilder();
+               if (content.size() == 1)
+                       return content.get(0);
+               for (int i = 0; i < content.size(); i++) {
+                       sb.append(content.get(i) + "\n");
                }
+               return sb.toString();
        }
+}
 PARSER_END(UtilParser)
 
 SKIP :
index 70383b3..9898a22 100644 (file)
@@ -315,6 +315,13 @@ using our specification checker.
 
 
 V. Examples
+
+!!!!!!! The register example should be extended to commute if we think of their
+transitional effects as set operations --- a set operation that will only mask
+out side the effects of its own previous behavior (things that are hb/SC before
+it)  ---- VERY IMPORTANT note here!!
+
+
 1. The register examples: Basically, we can think of registers as the cache on a
 memory system. The effect of a load or store basically tells us what the current
 value in the cache line is, and a load can read from values that can be
diff --git a/output/Makefile b/output/Makefile
deleted file mode 100644 (file)
index fc54440..0000000
+++ /dev/null
@@ -1,19 +0,0 @@
-#DIRS := barrier mcs-lock mpmc-queue spsc-queue spsc-bugfix linuxrwlocks \
-       dekker-fences chase-lev-deque ms-queue chase-lev-deque-bugfix \
-       concurrent-hashmap seqlock spsc-example spsc-queue-scfence \
-       treiber-stack
-
-DIRS := ms-queue concurrent-hashmap linuxrwlocks mcs-lock read-copy-update \
-       chase-lev-deque-bugfix spsc-bugfix mpmc-queue seqlock
-
-.PHONY: $(DIRS)
-
-all: $(DIRS)
-
-clean: $(DIRS:%=clean-%)
-
-$(DIRS):
-       $(MAKE) -C $@
-
-clean-%:
-       -$(MAKE) -C $* clean
diff --git a/output/benchmarks.mk b/output/benchmarks.mk
deleted file mode 100644 (file)
index e7a8736..0000000
+++ /dev/null
@@ -1,33 +0,0 @@
-# A few common Makefile items
-
-CC = gcc
-CXX = g++
-
-UNAME = $(shell uname)
-
-LIB_NAME = model
-LIB_SO = lib$(LIB_NAME).so
-
-BASE = $(HOME)/model-checker-priv/model-checker-priv
-INCLUDE = -I$(BASE)/include -I../include -I$(BASE)/spec-analysis -I$(BASE)
-
-# C preprocessor flags
-CPPFLAGS += $(INCLUDE) -O3
-
-# C++ compiler flags
-CXXFLAGS += $(CPPFLAGS)
-
-# C compiler flags
-CFLAGS += $(CPPFLAGS)
-
-# Linker flags
-LDFLAGS += -L$(BASE) -l$(LIB_NAME) -rdynamic
-
-# Mac OSX options
-ifeq ($(UNAME), Darwin)
-MACFLAGS = -D_XOPEN_SOURCE -DMAC
-CPPFLAGS += $(MACFLAGS)
-CXXFLAGS += $(MACFLAGS)
-CFLAGS += $(MACFLAGS)
-LDFLAGS += $(MACFLAGS)
-endif
diff --git a/output/chase-lev-deque-bugfix/Makefile b/output/chase-lev-deque-bugfix/Makefile
deleted file mode 100644 (file)
index 3980f68..0000000
+++ /dev/null
@@ -1,17 +0,0 @@
-include ../benchmarks.mk
-
-TESTNAME = main testcase1 testcase2
-
-HEADERS = deque.h
-OBJECTS = deque.o
-
-all: $(TESTNAME)
-
-$(TESTNAME): % : %.c $(OBJECTS)
-       $(CC) -o $@ $^ $(CPPFLAGS) $(LDFLAGS)
-
-%.o: %.c
-       $(CC) -c -o $@ $< $(CPPFLAGS)
-
-clean:
-       rm -f $(TESTNAME) *.o
diff --git a/output/chase-lev-deque-bugfix/deque.c b/output/chase-lev-deque-bugfix/deque.c
deleted file mode 100644 (file)
index 68eab07..0000000
+++ /dev/null
@@ -1,271 +0,0 @@
-#include <stdatomic.h>
-#include <inttypes.h>
-#include "deque.h"
-#include <stdlib.h>
-#include <stdio.h>
-
-Deque * create() {
-       Deque * q = (Deque *) calloc(1, sizeof(Deque));
-       Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
-       atomic_store_explicit(&q->array, a, memory_order_relaxed);
-       atomic_store_explicit(&q->top, 0, memory_order_relaxed);
-       atomic_store_explicit(&q->bottom, 0, memory_order_relaxed);
-       atomic_store_explicit(&a->size, 2, memory_order_relaxed);
-       return q;
-}
-
-
-
-int take(Deque * q) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 0; // Take
-               interface_begin->interface_name = "Take";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       int __RET__ = __wrapper__take(q);
-       Take_info* info = (Take_info*) malloc(sizeof(Take_info));
-       info->__RET__ = __RET__;
-       info->q = q;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 0; // Take
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-       return __RET__;
-}
-
-int __wrapper__take(Deque * q) {
-       size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
-       /* Automatically generated code for commit point define check: Take_Read_Bottom */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 0;
-               cp_define_check->label_name = "Take_Read_Bottom";
-               cp_define_check->interface_num = 0;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-       
-       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
-       
-       atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
-       
-       atomic_thread_fence(memory_order_seq_cst);
-       size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
-       
-       int x;
-       if (t <= b) {
-               
-               int size = atomic_load_explicit(&a->size,memory_order_relaxed);
-               x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
-               
-               if (t == b) {
-                       
-                                               bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
-                               1, memory_order_seq_cst, memory_order_relaxed);
-                       
-
-       /* Automatically generated code for commit point define check: Take_Additional_Point */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 1;
-               cp_define_check->label_name = "Take_Additional_Point";
-               cp_define_check->interface_num = 0;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-                       
-                       if (!succ) {
-                               
-                               x = EMPTY;
-                       }
-                       atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
-               }
-       } else { 
-               x = EMPTY;
-               atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
-       }
-       return x;
-}
-
-void resize(Deque *q) {
-       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
-       size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
-       size_t new_size=size << 1;
-       Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
-       size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
-       size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
-       atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
-       size_t i;
-       for(i=top; i < bottom; i++) {
-               atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
-       }
-       
-       atomic_store_explicit(&q->array, new_a, memory_order_release);
-       }
-
-
-void push(Deque * q, int x) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 1; // Push
-               interface_begin->interface_name = "Push";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       __wrapper__push(q, x);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 1; // Push
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Push_info* info = (Push_info*) malloc(sizeof(Push_info));
-       info->q = q;
-       info->x = x;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 1; // Push
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-}
-
-void __wrapper__push(Deque * q, int x) {
-       size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
-       
-       size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
-       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
-       if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1)  {
-               resize(q);
-                                               a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
-               
-       }
-       int size = atomic_load_explicit(&a->size, memory_order_relaxed);
-
-       atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
-       
-       
-       atomic_thread_fence(memory_order_release);
-       /* Automatically generated code for commit point define check: Push_Update_Bottom */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 2;
-               cp_define_check->label_name = "Push_Update_Bottom";
-               cp_define_check->interface_num = 1;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-                       
-       atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
-       
-}
-
-
-int steal(Deque * q) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 2; // Steal
-               interface_begin->interface_name = "Steal";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       int __RET__ = __wrapper__steal(q);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 2; // Steal
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Steal_info* info = (Steal_info*) malloc(sizeof(Steal_info));
-       info->__RET__ = __RET__;
-       info->q = q;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 2; // Steal
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-       return __RET__;
-}
-
-int __wrapper__steal(Deque * q) {
-                       size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
-       
-               atomic_thread_fence(memory_order_seq_cst);
-       
-       size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
-       /* Automatically generated code for commit point define check: Steal_Read_Bottom */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 3;
-               cp_define_check->label_name = "Steal_Read_Bottom";
-               cp_define_check->interface_num = 2;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-       
-
-       
-       int x = EMPTY;
-       if (t < b) {
-               
-               
-               Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
-               
-               int size = atomic_load_explicit(&a->size, memory_order_relaxed);
-               x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
-               
-                
-               bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
-                       memory_order_seq_cst, memory_order_relaxed);
-               
-
-       /* Automatically generated code for commit point define check: Steal_Additional_Point */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 4;
-               cp_define_check->label_name = "Steal_Additional_Point";
-               cp_define_check->interface_num = 2;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-               
-
-               
-               if (!succ) {
-                       
-                       return ABORT;
-               }
-       }
-       return x;
-}
-
diff --git a/output/chase-lev-deque-bugfix/deque.h b/output/chase-lev-deque-bugfix/deque.h
deleted file mode 100644 (file)
index 3a3a869..0000000
+++ /dev/null
@@ -1,233 +0,0 @@
-#ifndef DEQUE_H
-#define DEQUE_H
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h"
-
-typedef struct {
-       atomic_size_t size;
-       atomic_int buffer[];
-} Array;
-
-typedef struct {
-       atomic_size_t top, bottom;
-       atomic_uintptr_t array; 
-} Deque;
-
-#define EMPTY 0xffffffff
-#define ABORT 0xfffffffe
-
-/* All other user-defined structs */
-static IntegerList * __deque;
-/* All other user-defined functions */
-inline static bool succ ( int res ) {
-return res != EMPTY && res != ABORT ;
-}
-
-/* Definition of interface info struct: Steal */
-typedef struct Steal_info {
-int __RET__;
-Deque * q;
-} Steal_info;
-/* End of info struct definition: Steal */
-
-/* ID function of interface: Steal */
-inline static call_id_t Steal_id(void *info, thread_id_t __TID__) {
-       Steal_info* theInfo = (Steal_info*)info;
-       int __RET__ = theInfo->__RET__;
-       Deque * q = theInfo->q;
-
-       call_id_t __ID__ = succ ( __RET__ ) ? __RET__ : DEFAULT_CALL_ID;
-       return __ID__;
-}
-/* End of ID function: Steal */
-
-/* Check action function of interface: Steal */
-inline static bool Steal_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Steal_info* theInfo = (Steal_info*)info;
-       int __RET__ = theInfo->__RET__;
-       Deque * q = theInfo->q;
-
-       int elem = 0 ;
-       if ( succ ( __RET__ ) ) {
-       elem = front ( __deque ) ;
-       pop_front ( __deque ) ;
-       }
-       check_passed = succ ( __RET__ ) ? __RET__ == elem : true;
-       if (!check_passed)
-               return false;
-       return true;
-}
-/* End of check action function: Steal */
-
-/* Definition of interface info struct: Take */
-typedef struct Take_info {
-int __RET__;
-Deque * q;
-} Take_info;
-/* End of info struct definition: Take */
-
-/* ID function of interface: Take */
-inline static call_id_t Take_id(void *info, thread_id_t __TID__) {
-       Take_info* theInfo = (Take_info*)info;
-       int __RET__ = theInfo->__RET__;
-       Deque * q = theInfo->q;
-
-       call_id_t __ID__ = succ ( __RET__ ) ? __RET__ : DEFAULT_CALL_ID;
-       return __ID__;
-}
-/* End of ID function: Take */
-
-/* Check action function of interface: Take */
-inline static bool Take_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Take_info* theInfo = (Take_info*)info;
-       int __RET__ = theInfo->__RET__;
-       Deque * q = theInfo->q;
-
-       int elem = 0 ;
-       if ( succ ( __RET__ ) ) {
-       elem = back ( __deque ) ;
-       pop_back ( __deque ) ;
-       }
-       check_passed = succ ( __RET__ ) ? __RET__ == elem : true;
-       if (!check_passed)
-               return false;
-       return true;
-}
-/* End of check action function: Take */
-
-/* Definition of interface info struct: Push */
-typedef struct Push_info {
-Deque * q;
-int x;
-} Push_info;
-/* End of info struct definition: Push */
-
-/* ID function of interface: Push */
-inline static call_id_t Push_id(void *info, thread_id_t __TID__) {
-       Push_info* theInfo = (Push_info*)info;
-       Deque * q = theInfo->q;
-       int x = theInfo->x;
-
-       call_id_t __ID__ = x;
-       return __ID__;
-}
-/* End of ID function: Push */
-
-/* Check action function of interface: Push */
-inline static bool Push_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Push_info* theInfo = (Push_info*)info;
-       Deque * q = theInfo->q;
-       int x = theInfo->x;
-
-       push_back ( __deque , x ) ;
-       return true;
-}
-/* End of check action function: Push */
-
-#define INTERFACE_SIZE 3
-static void** func_ptr_table;
-static hb_rule** hb_rule_table;
-static commutativity_rule** commutativity_rule_table;
-inline static bool CommutativityCondition0(void *info1, void *info2) {
-       Push_info *_info1 = (Push_info*) info1;
-       Steal_info *_info2 = (Steal_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition1(void *info1, void *info2) {
-       Take_info *_info1 = (Take_info*) info1;
-       Steal_info *_info2 = (Steal_info*) info2;
-       return true;
-}
-
-/* Initialization of sequential varialbes */
-static void __SPEC_INIT__() {
-       __deque = createIntegerList ( ) ;
-}
-
-/* Cleanup routine of sequential variables */
-static bool __SPEC_CLEANUP__() {
-       if ( __deque ) destroyIntegerList ( __deque ) ;
-       return true ;
-}
-
-/* Define function for sequential code initialization */
-inline static void __sequential_init() {
-       /* Init func_ptr_table */
-       func_ptr_table = (void**) malloc(sizeof(void*) * 3 * 2);
-       func_ptr_table[2 * 2] = (void*) &Steal_id;
-       func_ptr_table[2 * 2 + 1] = (void*) &Steal_check_action;
-       func_ptr_table[2 * 0] = (void*) &Take_id;
-       func_ptr_table[2 * 0 + 1] = (void*) &Take_check_action;
-       func_ptr_table[2 * 1] = (void*) &Push_id;
-       func_ptr_table[2 * 1 + 1] = (void*) &Push_check_action;
-       /* Push(true) -> Steal(true) */
-       struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit0->interface_num_before = 1; // Push
-       hbConditionInit0->hb_condition_num_before = 0; // 
-       hbConditionInit0->interface_num_after = 2; // Steal
-       hbConditionInit0->hb_condition_num_after = 0; // 
-       /* Init hb_rule_table */
-       hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
-       #define HB_RULE_TABLE_SIZE 1
-       hb_rule_table[0] = hbConditionInit0;
-       /* Init commutativity_rule_table */
-       commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 2);
-       commutativity_rule* rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 1;
-       rule->interface_num_after = 2;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition0;
-       commutativity_rule_table[0] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 2;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition1;
-       commutativity_rule_table[1] = rule;
-       /* Pass init info, including function table info & HB rules & Commutativity Rules */
-       struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
-       anno_init->init_func = (void_func_t) __SPEC_INIT__;
-       anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
-       anno_init->func_table = func_ptr_table;
-       anno_init->func_table_size = INTERFACE_SIZE;
-       anno_init->hb_rule_table = hb_rule_table;
-       anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
-       anno_init->commutativity_rule_table = commutativity_rule_table;
-       anno_init->commutativity_rule_table_size = 2;
-       struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       init->type = INIT;
-       init->annotation = anno_init;
-       cdsannotate(SPEC_ANALYSIS, init);
-
-}
-
-/* End of Global construct generation in class */
-
-
-
-Deque * create();
-void resize(Deque *q);
-
-int __wrapper__take(Deque * q);
-
-int __wrapper__take(Deque * q) ;
-
-void __wrapper__push(Deque * q, int x);
-
-void __wrapper__push(Deque * q, int x) ;
-
-int __wrapper__steal(Deque * q);
-
-int __wrapper__steal(Deque * q) ;
-
-#endif
-
diff --git a/output/chase-lev-deque-bugfix/deque.o b/output/chase-lev-deque-bugfix/deque.o
deleted file mode 100644 (file)
index 9314807..0000000
Binary files a/output/chase-lev-deque-bugfix/deque.o and /dev/null differ
diff --git a/output/chase-lev-deque-bugfix/main b/output/chase-lev-deque-bugfix/main
deleted file mode 100755 (executable)
index a7e3297..0000000
Binary files a/output/chase-lev-deque-bugfix/main and /dev/null differ
diff --git a/output/chase-lev-deque-bugfix/main.c b/output/chase-lev-deque-bugfix/main.c
deleted file mode 100644 (file)
index edd09ba..0000000
+++ /dev/null
@@ -1,55 +0,0 @@
-#include <stdlib.h>
-#include <assert.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "model-assert.h"
-
-#include "deque.h"
-
-Deque *q;
-int a;
-int b;
-int c;
-
-static void task(void * param) {
-       a=steal(q);
-       if (a == ABORT) {
-               printf("Steal NULL\n");
-       } else {
-               printf("Steal %d\n", a);
-       }
-}
-
-int user_main(int argc, char **argv)
-{
-       __sequential_init();
-       
-       thrd_t t;
-       q=create();
-       thrd_create(&t, task, 0);
-       push(q, 1);
-       printf("Push 1\n");
-       push(q, 2);
-       printf("Push 2\n");
-       push(q, 4);
-       printf("Push 4\n");
-       b=take(q);
-       if (b == EMPTY) {
-               printf("Take NULL\n");
-       } else {
-               printf("Take %d\n", b);
-       }
-       c=take(q);
-       if (c == EMPTY) {
-               printf("Take NULL\n");
-       } else {
-               printf("Take %d\n", c);
-       }
-       thrd_join(t);
-
-       
-       return 0;
-}
-
diff --git a/output/chase-lev-deque-bugfix/testcase.c b/output/chase-lev-deque-bugfix/testcase.c
deleted file mode 100644 (file)
index 5723259..0000000
+++ /dev/null
@@ -1,62 +0,0 @@
-#include <stdlib.h>
-#include <assert.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "model-assert.h"
-
-#include "deque.h"
-
-Deque *q;
-int a;
-int b;
-int c;
-int x;
-
-static void task(void * param) {
-       a=steal(q);
-       if (a == ABORT) {
-               printf("Steal NULL\n");
-       } else {
-               printf("Steal %d\n", a);
-       }
-       x=steal(q);
-       if (x == ABORT) {
-               printf("Steal NULL\n");
-       } else {
-               printf("Steal %d\n", x);
-       }
-}
-
-int user_main(int argc, char **argv)
-{
-       __sequential_init();
-       
-       thrd_t t;
-       q=create();
-       thrd_create(&t, task, 0);
-       push(q, 1);
-       printf("Push 1\n");
-       push(q, 2);
-       printf("Push 2\n");
-       push(q, 4);
-       printf("Push 4\n");
-       b=take(q);
-       if (b == EMPTY) {
-               printf("Take NULL\n");
-       } else {
-               printf("Take %d\n", b);
-       }
-       c=take(q);
-       if (c == EMPTY) {
-               printf("Take NULL\n");
-       } else {
-               printf("Take %d\n", c);
-       }
-       thrd_join(t);
-
-       
-       return 0;
-}
-
diff --git a/output/chase-lev-deque-bugfix/testcase1 b/output/chase-lev-deque-bugfix/testcase1
deleted file mode 100755 (executable)
index c419a11..0000000
Binary files a/output/chase-lev-deque-bugfix/testcase1 and /dev/null differ
diff --git a/output/chase-lev-deque-bugfix/testcase1.c b/output/chase-lev-deque-bugfix/testcase1.c
deleted file mode 100644 (file)
index 91550f2..0000000
+++ /dev/null
@@ -1,63 +0,0 @@
-#include <stdlib.h>
-#include <assert.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "model-assert.h"
-
-#include "deque.h"
-
-Deque *q;
-int a;
-int b;
-int c;
-int x;
-
-static void task(void * param) {
-       a=steal(q);
-       if (a == ABORT) {
-               printf("Steal NULL\n");
-       } else {
-               printf("Steal %d\n", a);
-       }
-       
-       x=steal(q);
-       if (x == ABORT) {
-               printf("Steal NULL\n");
-       } else {
-               printf("Steal %d\n", x);
-       }
-}
-
-int user_main(int argc, char **argv)
-{
-       __sequential_init();
-       
-       thrd_t t;
-       q=create();
-       thrd_create(&t, task, 0);
-       push(q, 1);
-       printf("Push 1\n");
-       push(q, 2);
-       printf("Push 2\n");
-       push(q, 4);
-       printf("Push 4\n");
-       b=take(q);
-       if (b == EMPTY) {
-               printf("Take NULL\n");
-       } else {
-               printf("Take %d\n", b);
-       }
-       c=take(q);
-       if (c == EMPTY) {
-               printf("Take NULL\n");
-       } else {
-               printf("Take %d\n", c);
-       }
-       thrd_join(t);
-
-       
-       return 0;
-}
-
diff --git a/output/chase-lev-deque-bugfix/testcase2 b/output/chase-lev-deque-bugfix/testcase2
deleted file mode 100755 (executable)
index 41500c3..0000000
Binary files a/output/chase-lev-deque-bugfix/testcase2 and /dev/null differ
diff --git a/output/chase-lev-deque-bugfix/testcase2.c b/output/chase-lev-deque-bugfix/testcase2.c
deleted file mode 100644 (file)
index dc28d1b..0000000
+++ /dev/null
@@ -1,60 +0,0 @@
-#include <stdlib.h>
-#include <assert.h>
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include "model-assert.h"
-
-#include "deque.h"
-
-Deque *q;
-int a;
-int b;
-int c;
-int x;
-
-static void task(void * param) {
-       a=steal(q);
-       if (a == ABORT) {
-               printf("Steal NULL\n");
-       } else {
-               printf("Steal %d\n", a);
-       }
-       
-}
-
-int user_main(int argc, char **argv)
-{
-       __sequential_init();
-       
-       thrd_t t;
-       q=create();
-       push(q, 1);
-       printf("Push 1\n");
-       push(q, 2);
-       printf("Push 2\n");
-       push(q, 4);
-       printf("Push 4\n");
-       push(q, 5);
-       printf("Push 5\n");
-       thrd_create(&t, task, 0);
-
-       b=take(q);
-       if (b == EMPTY) {
-               printf("Take NULL\n");
-       } else {
-               printf("Take %d\n", b);
-       }
-       c=take(q);
-       if (c == EMPTY) {
-               printf("Take NULL\n");
-       } else {
-               printf("Take %d\n", c);
-       }
-       thrd_join(t);
-
-       
-       return 0;
-}
-
diff --git a/output/cliffc-hashtable/cliffc_hashtable.h b/output/cliffc-hashtable/cliffc_hashtable.h
deleted file mode 100644 (file)
index d102f2f..0000000
+++ /dev/null
@@ -1,911 +0,0 @@
-#ifndef CLIFFC_HASHTABLE_H
-#define CLIFFC_HASHTABLE_H
-
-#include <iostream>
-#include <atomic>
-#include "stdio.h" 
-#ifdef STANDALONE
-#include <assert.h>
-#define MODEL_ASSERT assert 
-#else
-#include <model-assert.h>
-#endif
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h" 
-
-using namespace std;
-
-
-
-template<typename TypeK, typename TypeV>
-class cliffc_hashtable;
-
-
-struct kvs_data {
-       int _size;
-       atomic<void*> *_data;
-       
-       kvs_data(int sz) {
-               _size = sz;
-               int real_size = sz * 2 + 2;
-               _data = new atomic<void*>[real_size];
-                                               int *hashes = new int[_size];
-               int i;
-               for (i = 0; i < _size; i++) {
-                       hashes[i] = 0;
-               }
-                               for (i = 2; i < real_size; i++) {
-                       _data[i].store(NULL, memory_order_relaxed);
-               }
-               _data[1].store(hashes, memory_order_relaxed);
-       }
-
-       ~kvs_data() {
-               int *hashes = (int*) _data[1].load(memory_order_relaxed);
-               delete hashes;
-               delete[] _data;
-       }
-};
-
-struct slot {
-       bool _prime;
-       void *_ptr;
-
-       slot(bool prime, void *ptr) {
-               _prime = prime;
-               _ptr = ptr;
-       }
-};
-
-
-
-
-template<typename TypeK, typename TypeV>
-class cliffc_hashtable {
-/* All other user-defined structs */
-static spec_table * map;
-static spec_table * id_map;
-static id_tag_t * tag;
-/* All other user-defined functions */
-inline static bool equals_key ( void * ptr1 , void * ptr2 ) {
-TypeK * key1 = ( TypeK * ) ptr1 , * key2 = ( TypeK * ) ptr2 ;
-if ( key1 == NULL || key2 == NULL ) return false ;
-return key1 -> equals ( key2 ) ;
-}
-
-inline static bool equals_val ( void * ptr1 , void * ptr2 ) {
-if ( ptr1 == ptr2 ) return true ;
-TypeV * val1 = ( TypeV * ) ptr1 , * val2 = ( TypeV * ) ptr2 ;
-if ( val1 == NULL || val2 == NULL ) return false ;
-return val1 -> equals ( val2 ) ;
-}
-
-inline static bool equals_id ( void * ptr1 , void * ptr2 ) {
-id_tag_t * id1 = ( id_tag_t * ) ptr1 , * id2 = ( id_tag_t * ) ptr2 ;
-if ( id1 == NULL || id2 == NULL ) return false ;
-return ( * id1 ) . tag == ( * id2 ) . tag ;
-}
-
-inline static call_id_t getKeyTag ( TypeK * key ) {
-if ( ! spec_table_contains ( id_map , key ) ) {
-call_id_t cur_id = current ( tag ) ;
-spec_table_put ( id_map , key , ( void * ) cur_id ) ;
-next ( tag ) ;
-return cur_id ;
-}
-else {
-call_id_t res = ( call_id_t ) spec_table_get ( id_map , key ) ;
-return res ;
-}
-}
-
-/* Definition of interface info struct: Put */
-typedef struct Put_info {
-TypeV * __RET__;
-TypeK * key;
-TypeV * val;
-} Put_info;
-/* End of info struct definition: Put */
-
-/* ID function of interface: Put */
-inline static call_id_t Put_id(void *info, thread_id_t __TID__) {
-       Put_info* theInfo = (Put_info*)info;
-       TypeV * __RET__ = theInfo->__RET__;
-       TypeK * key = theInfo->key;
-       TypeV * val = theInfo->val;
-
-       call_id_t __ID__ = getKeyTag ( key );
-       return __ID__;
-}
-/* End of ID function: Put */
-
-/* Check action function of interface: Put */
-inline static bool Put_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Put_info* theInfo = (Put_info*)info;
-       TypeV * __RET__ = theInfo->__RET__;
-       TypeK * key = theInfo->key;
-       TypeV * val = theInfo->val;
-
-       TypeV * _Old_Val = ( TypeV * ) spec_table_get ( map , key ) ;
-       spec_table_put ( map , key , val ) ;
-       bool passed = false ;
-       if ( ! passed ) {
-       int old = _Old_Val == NULL ? 0 : _Old_Val -> _val ;
-       int ret = __RET__ == NULL ? 0 : __RET__ -> _val ;
-       }
-       check_passed = equals_val ( __RET__ , _Old_Val );
-       if (!check_passed)
-               return false;
-       return true;
-}
-/* End of check action function: Put */
-
-/* Definition of interface info struct: Get */
-typedef struct Get_info {
-TypeV * __RET__;
-TypeK * key;
-} Get_info;
-/* End of info struct definition: Get */
-
-/* ID function of interface: Get */
-inline static call_id_t Get_id(void *info, thread_id_t __TID__) {
-       Get_info* theInfo = (Get_info*)info;
-       TypeV * __RET__ = theInfo->__RET__;
-       TypeK * key = theInfo->key;
-
-       call_id_t __ID__ = getKeyTag ( key );
-       return __ID__;
-}
-/* End of ID function: Get */
-
-/* Check action function of interface: Get */
-inline static bool Get_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Get_info* theInfo = (Get_info*)info;
-       TypeV * __RET__ = theInfo->__RET__;
-       TypeK * key = theInfo->key;
-
-       TypeV * _Old_Val = ( TypeV * ) spec_table_get ( map , key ) ;
-       bool passed = false ;
-       if ( ! passed ) {
-       int old = _Old_Val == NULL ? 0 : _Old_Val -> _val ;
-       int ret = __RET__ == NULL ? 0 : __RET__ -> _val ;
-       }
-       check_passed = equals_val ( _Old_Val , __RET__ );
-       if (!check_passed)
-               return false;
-       return true;
-}
-/* End of check action function: Get */
-
-#define INTERFACE_SIZE 2
-static void** func_ptr_table;
-static anno_hb_init** hb_init_table;
-
-/* Initialization of sequential varialbes */
-static void __SPEC_INIT__() {
-       map = new_spec_table_default ( equals_key ) ;
-       id_map = new_spec_table_default ( equals_id ) ;
-       tag = new_id_tag ( ) ;
-}
-
-/* Cleanup routine of sequential variables */
-static void __SPEC_CLEANUP__() {
-}
-
-/* Define function for sequential code initialization */
-inline static void __sequential_init() {
-       /* Init func_ptr_table */
-       func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
-       func_ptr_table[2 * 1] = (void*) &Put_id;
-       func_ptr_table[2 * 1 + 1] = (void*) &Put_check_action;
-       func_ptr_table[2 * 0] = (void*) &Get_id;
-       func_ptr_table[2 * 0 + 1] = (void*) &Get_check_action;
-       /* Put(true) -> Put(true) */
-       struct anno_hb_init *hbConditionInit0 = (struct anno_hb_init*) malloc(sizeof(struct anno_hb_init));
-       hbConditionInit0->interface_num_before = 1; // Put
-       hbConditionInit0->hb_condition_num_before = 0; // 
-       hbConditionInit0->interface_num_after = 1; // Put
-       hbConditionInit0->hb_condition_num_after = 0; // 
-       /* Put(true) -> Get(true) */
-       struct anno_hb_init *hbConditionInit1 = (struct anno_hb_init*) malloc(sizeof(struct anno_hb_init));
-       hbConditionInit1->interface_num_before = 1; // Put
-       hbConditionInit1->hb_condition_num_before = 0; // 
-       hbConditionInit1->interface_num_after = 0; // Get
-       hbConditionInit1->hb_condition_num_after = 0; // 
-       /* Init hb_init_table */
-       hb_init_table = (anno_hb_init**) malloc(sizeof(anno_hb_init*) * 2);
-       #define HB_INIT_TABLE_SIZE 2
-       hb_init_table[0] = hbConditionInit0;
-       hb_init_table[1] = hbConditionInit1;
-       /* Pass init info, including function table info & HB rules */
-       struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
-       anno_init->init_func = (void*) __SPEC_INIT__;
-       anno_init->cleanup_func = (void*) __SPEC_CLEANUP__;
-       anno_init->func_table = func_ptr_table;
-       anno_init->func_table_size = INTERFACE_SIZE;
-       anno_init->hb_init_table = hb_init_table;
-       anno_init->hb_init_table_size = HB_INIT_TABLE_SIZE;
-       struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       init->type = INIT;
-       init->annotation = anno_init;
-       cdsannotate(SPEC_ANALYSIS, init);
-
-}
-
-/* End of Global construct generation in class */
-       
-
-friend class CHM;
-       
-       private:
-       class CHM {
-               friend class cliffc_hashtable;
-               private:
-               atomic<kvs_data*> _newkvs;
-               
-                               atomic_int _size;
-       
-                               atomic_int _slots;
-               
-                               atomic_int _copy_idx;
-               
-                               atomic_int _copy_done;
-       
-               public:
-               CHM(int size) {
-                       _newkvs.store(NULL, memory_order_relaxed);
-                       _size.store(size, memory_order_relaxed);
-                       _slots.store(0, memory_order_relaxed);
-       
-                       _copy_idx.store(0, memory_order_relaxed);
-                       _copy_done.store(0, memory_order_relaxed);
-               }
-       
-               ~CHM() {}
-               
-               private:
-                       
-                               bool table_full(int reprobe_cnt, int len) {
-                       return
-                               reprobe_cnt >= REPROBE_LIMIT &&
-                               _slots.load(memory_order_relaxed) >= reprobe_limit(len);
-               }
-       
-               kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) {
-                                               
-                       kvs_data *newkvs = _newkvs.load(memory_order_acquire);
-                       if (newkvs != NULL)
-                               return newkvs;
-       
-                                               int oldlen = kvs->_size;
-                       int sz = _size.load(memory_order_relaxed);
-                       int newsz = sz;
-                       
-                                               if (sz >= (oldlen >> 2)) {                              newsz = oldlen << 1;                            if (sz >= (oldlen >> 1))
-                                       newsz = oldlen << 2;                    }
-       
-                                               if (newsz <= oldlen) newsz = oldlen << 1;
-                                               if (newsz < oldlen) newsz = oldlen;
-       
-                                               
-                       newkvs = _newkvs.load(memory_order_acquire);
-                                               if (newkvs != NULL) return newkvs;
-       
-                       newkvs = new kvs_data(newsz);
-                       void *chm = (void*) new CHM(sz);
-                                               newkvs->_data[0].store(chm, memory_order_relaxed);
-       
-                       kvs_data *cur_newkvs; 
-                                               
-                       if ((cur_newkvs = _newkvs.load(memory_order_acquire)) != NULL)
-                               return cur_newkvs;
-                                               kvs_data *desired = (kvs_data*) NULL;
-                       kvs_data *expected = (kvs_data*) newkvs; 
-                       
-                                               if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
-                                       memory_order_relaxed)) {
-                                                               delete newkvs;
-                               
-                               newkvs = _newkvs.load(memory_order_acquire);
-                       }
-                       return newkvs;
-               }
-       
-               void help_copy_impl(cliffc_hashtable *topmap, kvs_data *oldkvs,
-                       bool copy_all) {
-                       MODEL_ASSERT (get_chm(oldkvs) == this);
-                       
-                       kvs_data *newkvs = _newkvs.load(memory_order_acquire);
-                       int oldlen = oldkvs->_size;
-                       int min_copy_work = oldlen > 1024 ? 1024 : oldlen;
-               
-                                               int panic_start = -1;
-                       int copyidx;
-                       while (_copy_done.load(memory_order_relaxed) < oldlen) {
-                               copyidx = _copy_idx.load(memory_order_relaxed);
-                               if (panic_start == -1) {                                        copyidx = _copy_idx.load(memory_order_relaxed);
-                                       while (copyidx < (oldlen << 1) &&
-                                               !_copy_idx.compare_exchange_strong(copyidx, copyidx +
-                                                       min_copy_work, memory_order_relaxed, memory_order_relaxed))
-                                               copyidx = _copy_idx.load(memory_order_relaxed);
-                                       if (!(copyidx < (oldlen << 1)))
-                                               panic_start = copyidx;
-                               }
-       
-                                                               int workdone = 0;
-                               for (int i = 0; i < min_copy_work; i++)
-                                       if (copy_slot(topmap, (copyidx + i) & (oldlen - 1), oldkvs,
-                                               newkvs))
-                                               workdone++;
-                               if (workdone > 0)
-                                       copy_check_and_promote(topmap, oldkvs, workdone);
-       
-                               copyidx += min_copy_work;
-                               if (!copy_all && panic_start == -1)
-                                       return;                         }
-                       copy_check_and_promote(topmap, oldkvs, 0);              }
-       
-               kvs_data* copy_slot_and_check(cliffc_hashtable *topmap, kvs_data
-                       *oldkvs, int idx, void *should_help) {
-                       
-                       kvs_data *newkvs = _newkvs.load(memory_order_acquire);
-                                               if (copy_slot(topmap, idx, oldkvs, newkvs))
-                               copy_check_and_promote(topmap, oldkvs, 1);                      return (should_help == NULL) ? newkvs : topmap->help_copy(newkvs);
-               }
-       
-               void copy_check_and_promote(cliffc_hashtable *topmap, kvs_data*
-                       oldkvs, int workdone) {
-                       int oldlen = oldkvs->_size;
-                       int copyDone = _copy_done.load(memory_order_relaxed);
-                       if (workdone > 0) {
-                               while (true) {
-                                       copyDone = _copy_done.load(memory_order_relaxed);
-                                       if (_copy_done.compare_exchange_weak(copyDone, copyDone +
-                                               workdone, memory_order_relaxed, memory_order_relaxed))
-                                               break;
-                               }
-                       }
-       
-                                               if (copyDone + workdone == oldlen &&
-                               topmap->_kvs.load(memory_order_relaxed) == oldkvs) {
-                               
-                               kvs_data *newkvs = _newkvs.load(memory_order_acquire);
-                               
-                               topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
-                                       memory_order_relaxed);
-                       }
-               }
-       
-               bool copy_slot(cliffc_hashtable *topmap, int idx, kvs_data *oldkvs,
-                       kvs_data *newkvs) {
-                       slot *key_slot;
-                       while ((key_slot = key(oldkvs, idx)) == NULL)
-                               CAS_key(oldkvs, idx, NULL, TOMBSTONE);
-       
-                                               slot *oldval = val(oldkvs, idx);
-                       while (!is_prime(oldval)) {
-                               slot *box = (oldval == NULL || oldval == TOMBSTONE)
-                                       ? TOMBPRIME : new slot(true, oldval->_ptr);
-                               if (CAS_val(oldkvs, idx, oldval, box)) {
-                                       if (box == TOMBPRIME)
-                                               return 1;                                                                               oldval = box;                                   break;
-                               }
-                               oldval = val(oldkvs, idx);                      }
-       
-                       if (oldval == TOMBPRIME) return false;  
-                       slot *old_unboxed = new slot(false, oldval->_ptr);
-                       int copied_into_new = (putIfMatch(topmap, newkvs, key_slot, old_unboxed,
-                               NULL) == NULL);
-       
-                                               while (!CAS_val(oldkvs, idx, oldval, TOMBPRIME))
-                               oldval = val(oldkvs, idx);
-       
-                       return copied_into_new;
-               }
-       };
-
-       
-
-       private:
-       static const int Default_Init_Size = 4; 
-       static slot* const MATCH_ANY;
-       static slot* const NO_MATCH_OLD;
-
-       static slot* const TOMBPRIME;
-       static slot* const TOMBSTONE;
-
-       static const int REPROBE_LIMIT = 10; 
-       atomic<kvs_data*> _kvs;
-
-       public:
-       cliffc_hashtable() {
-       __sequential_init();
-                                                               
-               kvs_data *kvs = new kvs_data(Default_Init_Size);
-               void *chm = (void*) new CHM(0);
-               kvs->_data[0].store(chm, memory_order_relaxed);
-               _kvs.store(kvs, memory_order_relaxed);
-       }
-
-       cliffc_hashtable(int init_size) {
-                                               
-       __sequential_init();
-               
-               kvs_data *kvs = new kvs_data(init_size);
-               void *chm = (void*) new CHM(0);
-               kvs->_data[0].store(chm, memory_order_relaxed);
-               _kvs.store(kvs, memory_order_relaxed);
-       }
-
-
-TypeV * get(TypeK * key) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 0; // Get
-               interface_begin->interface_name = "Get";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       TypeV * __RET__ = __wrapper__get(key);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 0; // Get
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Get_info* info = (Get_info*) malloc(sizeof(Get_info));
-       info->__RET__ = __RET__;
-       info->key = key;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 0; // Get
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-       return __RET__;
-}
-       
-TypeV * __wrapper__get(TypeK * key) {
-               slot *key_slot = new slot(false, key);
-               int fullhash = hash(key_slot);
-               
-               kvs_data *kvs = _kvs.load(memory_order_acquire);
-               
-               slot *V = get_impl(this, kvs, key_slot, fullhash);
-               if (V == NULL) return NULL;
-               MODEL_ASSERT (!is_prime(V));
-               return (TypeV*) V->_ptr;
-       }
-
-
-TypeV * put(TypeK * key, TypeV * val) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 1; // Put
-               interface_begin->interface_name = "Put";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       TypeV * __RET__ = __wrapper__put(key, val);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 1; // Put
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Put_info* info = (Put_info*) malloc(sizeof(Put_info));
-       info->__RET__ = __RET__;
-       info->key = key;
-       info->val = val;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 1; // Put
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-       return __RET__;
-}
-       
-TypeV * __wrapper__put(TypeK * key, TypeV * val) {
-               return putIfMatch(key, val, NO_MATCH_OLD);
-       }
-
-       
-       TypeV* putIfAbsent(TypeK *key, TypeV *value) {
-               return putIfMatch(key, val, TOMBSTONE);
-       }
-
-       
-       TypeV* remove(TypeK *key) {
-               return putIfMatch(key, TOMBSTONE, NO_MATCH_OLD);
-       }
-
-       
-       bool remove(TypeK *key, TypeV *val) {
-               slot *val_slot = val == NULL ? NULL : new slot(false, val);
-               return putIfMatch(key, TOMBSTONE, val) == val;
-
-       }
-
-       
-       TypeV* replace(TypeK *key, TypeV *val) {
-               return putIfMatch(key, val, MATCH_ANY);
-       }
-
-       
-       bool replace(TypeK *key, TypeV *oldval, TypeV *newval) {
-               return putIfMatch(key, newval, oldval) == oldval;
-       }
-
-       private:
-       static CHM* get_chm(kvs_data* kvs) {
-               CHM *res = (CHM*) kvs->_data[0].load(memory_order_relaxed);
-               return res;
-       }
-
-       static int* get_hashes(kvs_data *kvs) {
-               return (int *) kvs->_data[1].load(memory_order_relaxed);
-       }
-       
-               static inline slot* key(kvs_data *kvs, int idx) {
-               MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
-                                               slot *res = (slot*) kvs->_data[idx * 2 + 2].load(memory_order_relaxed);
-       /* Automatically generated code for potential commit point: Read_Key_Point */
-
-       if (true) {
-               struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
-               potential_cp_define->label_num = 0;
-               potential_cp_define->label_name = "Read_Key_Point";
-               potential_cp_define->is_additional_point = false;
-               struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
-               annotation_potential_cp_define->annotation = potential_cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
-       }
-               
-               return res;
-       }
-
-       
-               static inline slot* val(kvs_data *kvs, int idx) {
-               MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
-                                               
-               slot *res = (slot*) kvs->_data[idx * 2 + 3].load(memory_order_acquire);
-       /* Automatically generated code for potential commit point: Read_Val_Point */
-
-       if (true) {
-               struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
-               potential_cp_define->label_num = 1;
-               potential_cp_define->label_name = "Read_Val_Point";
-               potential_cp_define->is_additional_point = false;
-               struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
-               annotation_potential_cp_define->annotation = potential_cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
-       }
-               
-               return res;
-
-
-       }
-
-       static int hash(slot *key_slot) {
-               MODEL_ASSERT(key_slot != NULL && key_slot->_ptr != NULL);
-               TypeK* key = (TypeK*) key_slot->_ptr;
-               int h = key->hashCode();
-                               h += (h << 15) ^ 0xffffcd7d;
-               h ^= (h >> 10);
-               h += (h << 3);
-               h ^= (h >> 6);
-               h += (h << 2) + (h << 14);
-               return h ^ (h >> 16);
-       }
-       
-                               static int reprobe_limit(int len) {
-               return REPROBE_LIMIT + (len >> 2);
-       }
-       
-       static inline bool is_prime(slot *val) {
-               return (val != NULL) && val->_prime;
-       }
-
-                       static bool keyeq(slot *K, slot *key_slot, int *hashes, int hash,
-               int fullhash) {
-                               MODEL_ASSERT (K != NULL);
-               TypeK* key_ptr = (TypeK*) key_slot->_ptr;
-               return
-                       K == key_slot ||
-                               ((hashes[hash] == 0 || hashes[hash] == fullhash) &&
-                               K != TOMBSTONE &&
-                               key_ptr->equals(K->_ptr));
-       }
-
-       static bool valeq(slot *val_slot1, slot *val_slot2) {
-               MODEL_ASSERT (val_slot1 != NULL);
-               TypeK* ptr1 = (TypeV*) val_slot1->_ptr;
-               if (val_slot2 == NULL || ptr1 == NULL) return false;
-               return ptr1->equals(val_slot2->_ptr);
-       }
-       
-                       static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
-               bool res = kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
-                       desired, memory_order_relaxed, memory_order_relaxed);
-       /* Automatically generated code for potential commit point: Write_Key_Point */
-
-       if (res) {
-               struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
-               potential_cp_define->label_num = 2;
-               potential_cp_define->label_name = "Write_Key_Point";
-               potential_cp_define->is_additional_point = false;
-               struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
-               annotation_potential_cp_define->annotation = potential_cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
-       }
-               
-               return res;
-       }
-
-       
-                       static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
-               *desired) {
-               
-               bool res =  kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
-                       desired, memory_order_acq_rel, memory_order_relaxed);
-       /* Automatically generated code for potential commit point: Write_Val_Point */
-
-       if (res) {
-               struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
-               potential_cp_define->label_num = 3;
-               potential_cp_define->label_name = "Write_Val_Point";
-               potential_cp_define->is_additional_point = false;
-               struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
-               annotation_potential_cp_define->annotation = potential_cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
-       }
-               
-               return res;
-       }
-
-       slot* get_impl(cliffc_hashtable *topmap, kvs_data *kvs, slot* key_slot, int
-               fullhash) {
-               int len = kvs->_size;
-               CHM *chm = get_chm(kvs);
-               int *hashes = get_hashes(kvs);
-
-               int idx = fullhash & (len - 1);
-               int reprobe_cnt = 0;
-               while (true) {
-                       slot *K = key(kvs, idx);
-       /* Automatically generated code for commit point define: Get_Point1 */
-
-       if (K == NULL) {
-               struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
-               cp_define->label_num = 4;
-               cp_define->label_name = "Get_Point1";
-               cp_define->potential_cp_label_num = 0;
-               cp_define->potential_label_name = "Read_Key_Point";
-               cp_define->interface_num = 0;
-               cp_define->is_additional_point = false;
-               struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define->type = CP_DEFINE;
-               annotation_cp_define->annotation = cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
-       }
-                       
-                       slot *V = val(kvs, idx);
-                       
-                       if (K == NULL) {
-                                                               return NULL;                    }
-                       
-                       if (keyeq(K, key_slot, hashes, idx, fullhash)) {
-                                                               if (!is_prime(V)) {
-       /* Automatically generated code for commit point clear: Get_Clear */
-
-       if (true) {
-               struct anno_cp_clear *cp_clear = (struct anno_cp_clear*) malloc(sizeof(struct anno_cp_clear));
-               struct spec_annotation *annotation_cp_clear = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_clear->type = CP_CLEAR;
-               annotation_cp_clear->annotation = cp_clear;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_clear);
-       }
-                                       
-
-       /* Automatically generated code for commit point define: Get_Point2 */
-
-       if (true) {
-               struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
-               cp_define->label_num = 6;
-               cp_define->label_name = "Get_Point2";
-               cp_define->potential_cp_label_num = 1;
-               cp_define->potential_label_name = "Read_Val_Point";
-               cp_define->interface_num = 0;
-               cp_define->is_additional_point = false;
-               struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define->type = CP_DEFINE;
-               annotation_cp_define->annotation = cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
-       }
-                                       
-                                       return (V == TOMBSTONE) ? NULL : V;                             }
-                                                               return get_impl(topmap, chm->copy_slot_and_check(topmap, kvs,
-                                       idx, key_slot), key_slot, fullhash);
-                       }
-
-                       if (++reprobe_cnt >= REPROBE_LIMIT ||
-                               key_slot == TOMBSTONE) {
-                                                                                               
-                               kvs_data *newkvs = chm->_newkvs.load(memory_order_acquire);
-                               
-                               return newkvs == NULL ? NULL : get_impl(topmap,
-                                       topmap->help_copy(newkvs), key_slot, fullhash);
-                       }
-
-                       idx = (idx + 1) & (len - 1);            }
-       }
-
-               TypeV* putIfMatch(TypeK *key, TypeV *value, slot *old_val) {
-                               if (old_val == NULL) {
-                       return NULL;
-               }
-               slot *key_slot = new slot(false, key);
-
-               slot *value_slot = new slot(false, value);
-               
-               kvs_data *kvs = _kvs.load(memory_order_acquire);
-               
-               slot *res = putIfMatch(this, kvs, key_slot, value_slot, old_val);
-                               MODEL_ASSERT (res != NULL); 
-               MODEL_ASSERT (!is_prime(res));
-               return res == TOMBSTONE ? NULL : (TypeV*) res->_ptr;
-       }
-
-       
-       static slot* putIfMatch(cliffc_hashtable *topmap, kvs_data *kvs, slot
-               *key_slot, slot *val_slot, slot *expVal) {
-               MODEL_ASSERT (val_slot != NULL);
-               MODEL_ASSERT (!is_prime(val_slot));
-               MODEL_ASSERT (!is_prime(expVal));
-
-               int fullhash = hash(key_slot);
-               int len = kvs->_size;
-               CHM *chm = get_chm(kvs);
-               int *hashes = get_hashes(kvs);
-               int idx = fullhash & (len - 1);
-
-                               int reprobe_cnt = 0;
-               slot *K;
-               slot *V;
-               kvs_data *newkvs;
-               
-               while (true) {                  K = key(kvs, idx);
-                       V = val(kvs, idx);
-                       if (K == NULL) {                                if (val_slot == TOMBSTONE) return val_slot;
-                                                               if (CAS_key(kvs, idx, NULL, key_slot)) {
-       /* Automatically generated code for commit point define: Put_WriteKey */
-
-       if (true) {
-               struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
-               cp_define->label_num = 7;
-               cp_define->label_name = "Put_WriteKey";
-               cp_define->potential_cp_label_num = 2;
-               cp_define->potential_label_name = "Write_Key_Point";
-               cp_define->interface_num = 1;
-               cp_define->is_additional_point = false;
-               struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define->type = CP_DEFINE;
-               annotation_cp_define->annotation = cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
-       }
-                                       
-                                       chm->_slots.fetch_add(1, memory_order_relaxed);                                         hashes[idx] = fullhash;                                         break;
-                               }
-                               K = key(kvs, idx);                              MODEL_ASSERT (K != NULL);
-                       }
-
-                                               if (keyeq(K, key_slot, hashes, idx, fullhash))
-                               break;                  
-                                                                                               if (++reprobe_cnt >= reprobe_limit(len) ||
-                               K == TOMBSTONE) {                               newkvs = chm->resize(topmap, kvs);
-                                                                                               if (expVal != NULL) topmap->help_copy(newkvs);
-                               return putIfMatch(topmap, newkvs, key_slot, val_slot, expVal);
-                       }
-
-                       idx = (idx + 1) & (len - 1);            } 
-               if (val_slot == V) return V;    
-                                               
-               newkvs = chm->_newkvs.load(memory_order_acquire);
-               
-               if (newkvs == NULL &&
-                       ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) {
-                                               newkvs = chm->resize(topmap, kvs);              }
-               
-                               if (newkvs != NULL)
-                       return putIfMatch(topmap, chm->copy_slot_and_check(topmap, kvs, idx,
-                               expVal), key_slot, val_slot, expVal);
-               
-                               while (true) {
-                       MODEL_ASSERT (!is_prime(V));
-
-                       if (expVal != NO_MATCH_OLD &&
-                               V != expVal &&
-                               (expVal != MATCH_ANY || V == TOMBSTONE || V == NULL) &&
-                               !(V == NULL && expVal == TOMBSTONE) &&
-                               (expVal == NULL || !valeq(expVal, V))) {
-                               
-                               
-                               
-                               return V;                       }
-
-                       if (CAS_val(kvs, idx, V, val_slot)) {
-       /* Automatically generated code for commit point define: Put_Point */
-
-       if (true) {
-               struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
-               cp_define->label_num = 8;
-               cp_define->label_name = "Put_Point";
-               cp_define->potential_cp_label_num = 3;
-               cp_define->potential_label_name = "Write_Val_Point";
-               cp_define->interface_num = 1;
-               cp_define->is_additional_point = false;
-               struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define->type = CP_DEFINE;
-               annotation_cp_define->annotation = cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
-       }
-                               
-                               if (expVal != NULL) {                                                                                                                                                           if ((V == NULL || V == TOMBSTONE) &&
-                                               val_slot != TOMBSTONE)
-                                               chm->_size.fetch_add(1, memory_order_relaxed);
-                                       if (!(V == NULL || V == TOMBSTONE) &&
-                                               val_slot == TOMBSTONE)
-                                               chm->_size.fetch_add(-1, memory_order_relaxed);
-                               }
-                               return (V == NULL && expVal != NULL) ? TOMBSTONE : V;
-                       }
-                                               V = val(kvs, idx);
-                       if (is_prime(V))
-                               return putIfMatch(topmap, chm->copy_slot_and_check(topmap, kvs,
-                                       idx, expVal), key_slot, val_slot, expVal);
-               }
-       }
-
-               kvs_data* help_copy(kvs_data *helper) {
-               
-               kvs_data *topkvs = _kvs.load(memory_order_acquire);
-               CHM *topchm = get_chm(topkvs);
-                               if (topchm->_newkvs.load(memory_order_relaxed) == NULL) return helper;
-               topchm->help_copy_impl(this, topkvs, false);
-               return helper;
-       }
-};
-template<typename TypeK, typename TypeV>
-void** cliffc_hashtable<TypeK, TypeV>::func_ptr_table;
-template<typename TypeK, typename TypeV>
-anno_hb_init** cliffc_hashtable<TypeK, TypeV>::hb_init_table;
-template<typename TypeK, typename TypeV>
-spec_table * cliffc_hashtable<TypeK, TypeV>::map;
-template<typename TypeK, typename TypeV>
-spec_table * cliffc_hashtable<TypeK, TypeV>::id_map;
-template<typename TypeK, typename TypeV>
-id_tag_t * cliffc_hashtable<TypeK, TypeV>::tag;
-
-
-#endif
-
diff --git a/output/cliffc-hashtable/main.cc b/output/cliffc-hashtable/main.cc
deleted file mode 100644 (file)
index 8b6f75e..0000000
+++ /dev/null
@@ -1,111 +0,0 @@
-#include <iostream>
-#include <threads.h>
-#include "cliffc_hashtable.h"
-
-using namespace std;
-
-template<typename TypeK, typename TypeV>
-slot* const cliffc_hashtable<TypeK, TypeV>::MATCH_ANY = new slot(false, NULL);
-
-template<typename TypeK, typename TypeV>
-slot* const cliffc_hashtable<TypeK, TypeV>::NO_MATCH_OLD = new slot(false, NULL);
-
-template<typename TypeK, typename TypeV>
-slot* const cliffc_hashtable<TypeK, TypeV>::TOMBPRIME = new slot(true, NULL);
-
-template<typename TypeK, typename TypeV>
-slot* const cliffc_hashtable<TypeK, TypeV>::TOMBSTONE = new slot(false, NULL);
-
-
-class IntWrapper {
-       private:
-               public:
-           int _val;
-
-               IntWrapper(int val) : _val(val) {}
-
-               IntWrapper() : _val(0) {}
-
-               IntWrapper(IntWrapper& copy) : _val(copy._val) {}
-
-               int get() {
-                       return _val;
-               }
-
-               int hashCode() {
-                       return _val;
-               }
-               
-               bool operator==(const IntWrapper& rhs) {
-                       return false;
-               }
-
-               bool equals(const void *another) {
-                       if (another == NULL)
-                               return false;
-                       IntWrapper *ptr =
-                               (IntWrapper*) another;
-                       return ptr->_val == _val;
-               }
-};
-
-cliffc_hashtable<IntWrapper, IntWrapper> *table;
-IntWrapper *val1, *val2;
-IntWrapper *k0, *k1, *k2, *k3, *k4, *k5;
-IntWrapper *v0, *v1, *v2, *v3, *v4, *v5;
-
-void threadA(void *arg) {
-       IntWrapper *Res;
-       int res;
-       Res = table->put(k3, v3);
-       res = Res == NULL ? 0 : Res->_val;
-       printf("Put1: key_%d, val_%d, res_%d\n", k3->_val, v3->_val, res);
-
-       Res = table->get(k2);
-       res = Res == NULL ? 0 : Res->_val;
-       printf("Get2: key_%d, res_%d\n", k2->_val, res);
-}
-
-void threadB(void *arg) {
-       IntWrapper *Res;
-       int res;
-       Res = table->put(k2, v2);
-       res = Res == NULL ? 0 : Res->_val;
-       printf("Put3: key_%d, val_%d, res_%d\n", k2->_val, v2->_val, res);
-
-       Res = table->get(k3);
-       res = Res == NULL ? 0 : Res->_val;
-       printf("Get4: key_%d, res_%d\n", k3->_val, res);
-}
-
-void threadC(void *arg) {
-}
-
-int user_main(int argc, char *argv[]) {
-       thrd_t t1, t2, t3;
-       table = new cliffc_hashtable<IntWrapper, IntWrapper>(32);
-    k1 = new IntWrapper(3);
-       k2 = new IntWrapper(5);
-       k3 = new IntWrapper(11);
-       k4 = new IntWrapper(7);
-       k5 = new IntWrapper(13);
-
-       v0 = new IntWrapper(2048);
-       v1 = new IntWrapper(1024);
-       v2 = new IntWrapper(47);
-       v3 = new IntWrapper(73);
-       v4 = new IntWrapper(81);
-       v5 = new IntWrapper(99);
-
-       thrd_create(&t1, threadA, NULL);
-       thrd_create(&t2, threadB, NULL);
-       thrd_create(&t3, threadC, NULL);
-       thrd_join(t1);
-       thrd_join(t2);
-       thrd_join(t3);
-       
-       return 0;
-}
-
-
-
diff --git a/output/concurrent-hashmap/ConcurrentHashMap.java b/output/concurrent-hashmap/ConcurrentHashMap.java
deleted file mode 100644 (file)
index 23a4ed4..0000000
+++ /dev/null
@@ -1,1224 +0,0 @@
-/*
-  File: ConcurrentHashMap
-
-  Written by Doug Lea. Adapted and released, under explicit
-  permission, from JDK1.2 HashMap.java and Hashtable.java which
-  carries the following copyright:
-
-     * Copyright 1997 by Sun Microsystems, Inc.,
-     * 901 San Antonio Road, Palo Alto, California, 94303, U.S.A.
-     * All rights reserved.
-     *
-     * This software is the confidential and proprietary information
-     * of Sun Microsystems, Inc. ("Confidential Information").  You
-     * shall not disclose such Confidential Information and shall use
-     * it only in accordance with the terms of the license agreement
-     * you entered into with Sun.
-
-  History:
-  Date       Who                What
-  26nov2000  dl               Created, based on ConcurrentReaderHashMap
-  12jan2001  dl               public release
-  17nov2001  dl               Minor tunings
-  24oct2003  dl               Segment implements Serializable
-*/
-
-package EDU.oswego.cs.dl.util.concurrent;
-
-import java.util.Map;
-import java.util.AbstractMap;
-import java.util.AbstractSet;
-import java.util.AbstractCollection;
-import java.util.Collection;
-import java.util.Set;
-import java.util.Iterator;
-import java.util.Enumeration;
-import java.util.NoSuchElementException;
-
-import java.io.Serializable;
-import java.io.IOException;
-import java.io.ObjectInputStream;
-import java.io.ObjectOutputStream;
-
-
-/**
- * A version of Hashtable supporting 
- * concurrency for both retrievals and updates:
- *
- * <dl> 
- * <dt> Retrievals
- *
- * <dd> Retrievals may overlap updates.  (This is the same policy as
- * ConcurrentReaderHashMap.)  Successful retrievals using get(key) and
- * containsKey(key) usually run without locking. Unsuccessful
- * retrievals (i.e., when the key is not present) do involve brief
- * synchronization (locking).  Because retrieval operations can
- * ordinarily overlap with update operations (i.e., put, remove, and
- * their derivatives), retrievals can only be guaranteed to return the
- * results of the most recently <em>completed</em> operations holding
- * upon their onset. Retrieval operations may or may not return
- * results reflecting in-progress writing operations.  However, the
- * retrieval operations do always return consistent results -- either
- * those holding before any single modification or after it, but never
- * a nonsense result.  For aggregate operations such as putAll and
- * clear, concurrent reads may reflect insertion or removal of only
- * some entries.  
- * <p>
- *
- * Iterators and Enumerations (i.e., those returned by
- * keySet().iterator(), entrySet().iterator(), values().iterator(),
- * keys(), and elements()) return elements reflecting the state of the
- * hash table at some point at or since the creation of the
- * iterator/enumeration.  They will return at most one instance of
- * each element (via next()/nextElement()), but might or might not
- * reflect puts and removes that have been processed since they were
- * created.  They do <em>not</em> throw ConcurrentModificationException.
- * However, these iterators are designed to be used by only one
- * thread at a time. Passing an iterator across multiple threads may
- * lead to unpredictable results if the table is being concurrently
- * modified.  <p>
- *
- *
- * <dt> Updates
- *
- * <dd> This class supports a hard-wired preset <em>concurrency
- * level</em> of 32. This allows a maximum of 32 put and/or remove
- * operations to proceed concurrently. This level is an upper bound on
- * concurrency, not a guarantee, since it interacts with how
- * well-strewn elements are across bins of the table. (The preset
- * value in part reflects the fact that even on large multiprocessors,
- * factors other than synchronization tend to be bottlenecks when more
- * than 32 threads concurrently attempt updates.)
- * Additionally, operations triggering internal resizing and clearing
- * do not execute concurrently with any operation.  
- * <p>
- *
- * There is <em>NOT</em> any support for locking the entire table to
- * prevent updates. This makes it imposssible, for example, to
- * add an element only if it is not already present, since another
- * thread may be in the process of doing the same thing.
- * If you need such capabilities, consider instead using the
- * ConcurrentReaderHashMap class. 
- *
- * </dl>
- *
- * Because of how concurrency control is split up, the
- * size() and isEmpty() methods require accumulations across 32
- * control segments, and so might be slightly slower than you expect.
- * <p>
- *
- * This class may be used as a direct replacement for
- * java.util.Hashtable in any application that does not rely
- * on the ability to lock the entire table to prevent updates.  
- * As of this writing, it performs much faster than Hashtable in
- * typical multi-threaded applications with multiple readers and writers.
- * Like Hashtable but unlike java.util.HashMap,
- * this class does NOT allow <tt>null</tt> to be used as a key or
- * value. 
- * <p> 
- *
- * Implementation note: A slightly
- * faster implementation of this class will be possible once planned
- * Java Memory Model revisions are in place.
- *
- * <p>[<a href="http://gee.cs.oswego.edu/dl/classes/EDU/oswego/cs/dl/util/concurrent/intro.html"> Introduction to this package. </a>]
-
- **/
-
-
-public class ConcurrentHashMap 
-  extends    AbstractMap 
-  implements Map, Cloneable, Serializable {
-
-  /*
-    The basic strategy is an optimistic-style scheme based on
-    the guarantee that the hash table and its lists are always
-    kept in a consistent enough state to be read without locking:
-
-    * Read operations first proceed without locking, by traversing the
-       apparently correct list of the apparently correct bin. If an
-       entry is found, but not invalidated (value field null), it is
-       returned. If not found, operations must recheck (after a memory
-       barrier) to make sure they are using both the right list and
-       the right table (which can change under resizes). If
-       invalidated, reads must acquire main update lock to wait out
-       the update, and then re-traverse.
-
-    * All list additions are at the front of each bin, making it easy
-       to check changes, and also fast to traverse.  Entry next
-       pointers are never assigned. Remove() builds new nodes when
-       necessary to preserve this.
-
-    * Remove() (also clear()) invalidates removed nodes to alert read
-       operations that they must wait out the full modifications.
-
-    * Locking for puts, removes (and, when necessary gets, etc)
-      is controlled by Segments, each covering a portion of the
-      table. During operations requiring global exclusivity (mainly
-      resize and clear), ALL of these locks are acquired at once.
-      Note that these segments are NOT contiguous -- they are based
-      on the least 5 bits of hashcodes. This ensures that the same
-      segment controls the same slots before and after resizing, which
-      is necessary for supporting concurrent retrievals. This
-      comes at the price of a mismatch of logical vs physical locality,
-      but this seems not to be a performance problem in practice.
-  */
-
-  /**
-   * The hash table data.
-   */
-  protected transient Entry[] table;
-
-
-  /** 
-   * The number of concurrency control segments.
-   * The value can be at most 32 since ints are used
-   * as bitsets over segments. Emprically, it doesn't
-   * seem to pay to decrease it either, so the value should be at least 32.
-   * In other words, do not redefine this :-)
-   **/
-
-  protected static final int CONCURRENCY_LEVEL = 32;
-
-  /**
-   * Mask value for indexing into segments
-   **/
-
-  protected static final int SEGMENT_MASK = CONCURRENCY_LEVEL - 1;
-
-  /**
-   * Bookkeeping for each concurrency control segment.
-   * Each segment contains a local count of the number of 
-   * elements in its region.
-   * However, the main use of a Segment is for its lock.
-   **/
-  protected final static class Segment implements Serializable {
-    /**
-     * The number of elements in this segment's region.
-     * It is always updated within synchronized blocks.
-     **/
-    protected int count;
-
-    /**
-     * Get the count under synch. 
-     **/
-    protected synchronized int getCount() { return count; }
-
-    /**
-     * Force a synchronization
-     **/
-    protected synchronized void synch() {}
-  }
-
-  /**
-   * The array of concurrency control segments.
-   **/
-
-  protected final Segment[] segments = new Segment[CONCURRENCY_LEVEL]; 
-
-
-  /**
-   * The default initial number of table slots for this table (32).
-   * Used when not otherwise specified in constructor.
-   **/
-  public static int DEFAULT_INITIAL_CAPACITY = 32; 
-
-
-  /**
-   * The minimum capacity, used if a lower value is implicitly specified
-   * by either of the constructors with arguments.  
-   * MUST be a power of two.
-   */
-  private static final int MINIMUM_CAPACITY = 32;
-  
-  /**
-   * The maximum capacity, used if a higher value is implicitly specified
-   * by either of the constructors with arguments.
-   * MUST be a power of two <= 1<<30.
-   */
-  private static final int MAXIMUM_CAPACITY = 1 << 30;
-  
-  /**
-   * The default load factor for this table (0.75)
-   * Used when not otherwise specified in constructor.
-   **/
-
-  public static final float DEFAULT_LOAD_FACTOR = 0.75f; 
-
-  /**
-   * The load factor for the hash table.
-   *
-   * @serial
-   */
-  protected final float loadFactor;
-
-  /**
-   * Per-segment resize threshold.  
-   *
-   * @serial
-   */
-  protected int threshold;
-
-
-  /**
-   * Number of segments voting for resize. The table is
-   * doubled when 1/4 of the segments reach threshold.
-   * Volatile but updated without synch since this is just a heuristic.
-   **/
-
-  protected transient volatile int votesForResize;
-
-
-  /**
-   * Return the number of set bits in w.
-   * For a derivation of this algorithm, see
-   * "Algorithms and data structures with applications to 
-   *  graphics and geometry", by Jurg Nievergelt and Klaus Hinrichs,
-   *  Prentice Hall, 1993.
-   * See also notes by Torsten Sillke at
-   * http://www.mathematik.uni-bielefeld.de/~sillke/PROBLEMS/bitcount
-   **/
-  protected static int bitcount(int w) {
-    w -= (0xaaaaaaaa & w) >>> 1;
-    w = (w & 0x33333333) + ((w >>> 2) & 0x33333333);
-    w = (w + (w >>> 4)) & 0x0f0f0f0f;
-    w += w >>> 8;
-    w += w >>> 16;
-    return w & 0xff;
-  }
-
-  /**
-   * Returns the appropriate capacity (power of two) for the specified 
-   * initial capacity argument.
-   */
-  private int p2capacity(int initialCapacity) {
-    int cap = initialCapacity;
-    
-    // Compute the appropriate capacity
-    int result;
-    if (cap > MAXIMUM_CAPACITY || cap < 0) {
-      result = MAXIMUM_CAPACITY;
-    } else {
-      result = MINIMUM_CAPACITY;
-      while (result < cap)
-        result <<= 1;
-    }
-    return result;
-  }
-
-  /**
-   * Return hash code for Object x. Since we are using power-of-two
-   * tables, it is worth the effort to improve hashcode via
-   * the same multiplicative scheme as used in IdentityHashMap.
-   */
-  protected static int hash(Object x) {
-    int h = x.hashCode();
-    // Multiply by 127 (quickly, via shifts), and mix in some high
-    // bits to help guard against bunching of codes that are
-    // consecutive or equally spaced.
-    return ((h << 7) - h + (h >>> 9) + (h >>> 17));
-  }
-
-
-  /** 
-   * Check for equality of non-null references x and y. 
-   **/
-  protected boolean eq(Object x, Object y) {
-    return x == y || x.equals(y);
-  }
-
-  /** Create table array and set the per-segment threshold **/
-  protected Entry[] newTable(int capacity) {
-    threshold = (int)(capacity * loadFactor / CONCURRENCY_LEVEL) + 1;
-    return new Entry[capacity];
-  }
-
-  /**
-   * Constructs a new, empty map with the specified initial 
-   * capacity and the specified load factor.
-   *
-   * @param initialCapacity the initial capacity.
-   *  The actual initial capacity is rounded to the nearest power of two.
-   * @param loadFactor  the load factor threshold, used to control resizing.
-   *   This value is used in an approximate way: When at least
-   *   a quarter of the segments of the table reach per-segment threshold, or
-   *   one of the segments itself exceeds overall threshold,
-   *   the table is doubled. 
-   *   This will on average cause resizing when the table-wide
-   *   load factor is slightly less than the threshold. If you'd like
-   *   to avoid resizing, you can set this to a ridiculously large
-   *   value.
-   * @throws IllegalArgumentException  if the load factor is nonpositive.
-   */
-  public ConcurrentHashMap(int initialCapacity, 
-                           float loadFactor) {
-    if (!(loadFactor > 0))
-      throw new IllegalArgumentException("Illegal Load factor: "+
-                                         loadFactor);
-    this.loadFactor = loadFactor;
-    for (int i = 0; i < segments.length; ++i) 
-      segments[i] = new Segment();
-    int cap = p2capacity(initialCapacity);
-    table = newTable(cap);
-  }
-
-  /**
-   * Constructs a new, empty map with the specified initial 
-   * capacity and default load factor.
-   *
-   * @param   initialCapacity   the initial capacity of the 
-   *                            ConcurrentHashMap.
-   * @throws    IllegalArgumentException if the initial maximum number 
-   *              of elements is less
-   *              than zero.
-   */
-  public ConcurrentHashMap(int initialCapacity) {
-    this(initialCapacity, DEFAULT_LOAD_FACTOR);
-  }
-
-  /**
-   * Constructs a new, empty map with a default initial capacity
-   * and default load factor.
-   */
-  public ConcurrentHashMap() {
-    this(DEFAULT_INITIAL_CAPACITY, DEFAULT_LOAD_FACTOR);
-  }
-
-  /**
-   * Constructs a new map with the same mappings as the given map.  The
-   * map is created with a capacity of twice the number of mappings in
-   * the given map or 32 (whichever is greater), and a default load factor.
-   */
-  public ConcurrentHashMap(Map t) {
-    this(Math.max((int) (t.size() / DEFAULT_LOAD_FACTOR) + 1, 
-                  MINIMUM_CAPACITY),
-         DEFAULT_LOAD_FACTOR);
-    putAll(t);
-  }
-
-  /**
-   * Returns the number of key-value mappings in this map.
-   *
-   * @return the number of key-value mappings in this map.
-   */
-  public int size() {
-    int c = 0;
-    for (int i = 0; i < segments.length; ++i) 
-      c += segments[i].getCount();
-    return c;
-  }
-
-  /**
-   * Returns <tt>true</tt> if this map contains no key-value mappings.
-   *
-   * @return <tt>true</tt> if this map contains no key-value mappings.
-   */
-  public boolean isEmpty() {
-    for (int i = 0; i < segments.length; ++i) 
-      if (segments[i].getCount() != 0)
-        return false;
-    return true;
-  }
-
-
-  /**
-   * Returns the value to which the specified key is mapped in this table.
-   *
-   * @param   key   a key in the table.
-   * @return  the value to which the key is mapped in this table;
-   *          <code>null</code> if the key is not mapped to any value in
-   *          this table.
-   * @exception  NullPointerException  if the key is
-   *               <code>null</code>.
-   * @see     #put(Object, Object)
-   */
-  public Object get(Object key) {
-    int hash = hash(key);     // throws null pointer exception if key null
-
-    // Try first without locking...
-    Entry[] tab = table;
-    int index = hash & (tab.length - 1);
-    Entry first = tab[index];
-    Entry e;
-
-    for (e = first; e != null; e = e.next) {
-      if (e.hash == hash && eq(key, e.key)) {
-        Object value = e.value;
-        if (value != null) 
-          return value;
-        else
-          break;
-      }
-    }
-
-    // Recheck under synch if key apparently not there or interference
-    Segment seg = segments[hash & SEGMENT_MASK];
-    synchronized(seg) { 
-      tab = table;
-      index = hash & (tab.length - 1);
-      Entry newFirst = tab[index];
-      if (e != null || first != newFirst) {
-        for (e = newFirst; e != null; e = e.next) {
-          if (e.hash == hash && eq(key, e.key)) 
-            return e.value;
-        }
-      }
-      return null;
-    }
-  }
-
-  /**
-   * Tests if the specified object is a key in this table.
-   * 
-   * @param   key   possible key.
-   * @return  <code>true</code> if and only if the specified object 
-   *          is a key in this table, as determined by the 
-   *          <tt>equals</tt> method; <code>false</code> otherwise.
-   * @exception  NullPointerException  if the key is
-   *               <code>null</code>.
-   * @see     #contains(Object)
-   */
-
-  public boolean containsKey(Object key) {
-    return get(key) != null;
-  }
-  
-
-  /**
-   * Maps the specified <code>key</code> to the specified 
-   * <code>value</code> in this table. Neither the key nor the 
-   * value can be <code>null</code>. (Note that this policy is
-   * the same as for java.util.Hashtable, but unlike java.util.HashMap,
-   * which does accept nulls as valid keys and values.)<p>
-   *
-   * The value can be retrieved by calling the <code>get</code> method 
-   * with a key that is equal to the original key. 
-   *
-   * @param      key     the table key.
-   * @param      value   the value.
-   * @return     the previous value of the specified key in this table,
-   *             or <code>null</code> if it did not have one.
-   * @exception  NullPointerException  if the key or value is
-   *               <code>null</code>.
-   * @see     Object#equals(Object)
-   * @see     #get(Object)
-   */
-  public Object put(Object key, Object value) {
-    if (value == null) 
-      throw new NullPointerException();
-    
-    int hash = hash(key);
-    Segment seg = segments[hash & SEGMENT_MASK];
-    int segcount;
-    Entry[] tab;
-    int votes;
-
-    synchronized(seg) {
-      tab = table;
-      int index = hash & (tab.length-1);
-      Entry first = tab[index];
-
-      for (Entry e = first; e != null; e = e.next) {
-        if (e.hash == hash && eq(key, e.key)) {
-          Object oldValue = e.value; 
-          e.value = value;
-          return oldValue;
-        }
-      }
-
-      //  Add to front of list
-      Entry newEntry = new Entry(hash, key, value, first);
-      tab[index] = newEntry;
-
-      if ((segcount = ++seg.count) < threshold)
-        return null;
-
-      int bit = (1 << (hash & SEGMENT_MASK));
-      votes = votesForResize;
-      if ((votes & bit) == 0)
-        votes = votesForResize |= bit;
-    }
-
-    // Attempt resize if 1/4 segs vote,
-    // or if this seg itself reaches the overall threshold.
-    // (The latter check is just a safeguard to avoid pathological cases.)
-    if (bitcount(votes) >= CONCURRENCY_LEVEL / 4  ||
-        segcount > (threshold * CONCURRENCY_LEVEL)) 
-      resize(0, tab);
-
-    return null;
-  }
-
-  /**
-   * Gather all locks in order to call rehash, by
-   * recursing within synch blocks for each segment index.
-   * @param index the current segment. initially call value must be 0
-   * @param assumedTab the state of table on first call to resize. If
-   * this changes on any call, the attempt is aborted because the
-   * table has already been resized by another thread.
-   */
-
-  protected void resize(int index, Entry[] assumedTab) {
-    Segment seg = segments[index];
-    synchronized(seg) {
-      if (assumedTab == table) {
-        int next = index+1;
-        if (next < segments.length)
-          resize(next, assumedTab);
-        else
-          rehash();
-      }
-    }
-  }
-
-  /**
-   * Rehashes the contents of this map into a new table
-   * with a larger capacity. 
-   */
-  protected void rehash() {
-    votesForResize = 0; // reset
-
-    Entry[] oldTable = table;
-    int oldCapacity = oldTable.length;
-
-    if (oldCapacity >= MAXIMUM_CAPACITY) {
-      threshold = Integer.MAX_VALUE; // avoid retriggering
-      return;
-    }
-    
-    int newCapacity = oldCapacity << 1;
-    Entry[] newTable = newTable(newCapacity);
-    int mask = newCapacity - 1;
-
-    /*
-     * Reclassify nodes in each list to new Map.  Because we are
-     * using power-of-two expansion, the elements from each bin
-     * must either stay at same index, or move to
-     * oldCapacity+index. We also eliminate unnecessary node
-     * creation by catching cases where old nodes can be reused
-     * because their next fields won't change. Statistically, at
-     * the default threshhold, only about one-sixth of them need
-     * cloning. (The nodes they replace will be garbage
-     * collectable as soon as they are no longer referenced by any
-     * reader thread that may be in the midst of traversing table
-     * right now.)
-     */
-    
-    for (int i = 0; i < oldCapacity ; i++) {
-      // We need to guarantee that any existing reads of old Map can
-      //  proceed. So we cannot yet null out each bin.  
-      Entry e = oldTable[i];
-      
-      if (e != null) {
-        int idx = e.hash & mask;
-        Entry next = e.next;
-        
-        //  Single node on list
-        if (next == null) 
-          newTable[idx] = e;
-        
-        else {    
-          // Reuse trailing consecutive sequence of all same bit
-          Entry lastRun = e;
-          int lastIdx = idx;
-          for (Entry last = next; last != null; last = last.next) {
-            int k = last.hash & mask;
-            if (k != lastIdx) {
-              lastIdx = k;
-              lastRun = last;
-            }
-          }
-          newTable[lastIdx] = lastRun;
-          
-          // Clone all remaining nodes
-          for (Entry p = e; p != lastRun; p = p.next) {
-            int k = p.hash & mask;
-            newTable[k] = new Entry(p.hash, p.key, 
-                                    p.value, newTable[k]);
-          }
-        }
-      }
-    }
-    
-    table = newTable;
-  }
-
-
-  /**
-   * Removes the key (and its corresponding value) from this 
-   * table. This method does nothing if the key is not in the table.
-   *
-   * @param   key   the key that needs to be removed.
-   * @return  the value to which the key had been mapped in this table,
-   *          or <code>null</code> if the key did not have a mapping.
-   * @exception  NullPointerException  if the key is
-   *               <code>null</code>.
-   */
-  public Object remove(Object key) {
-    return remove(key, null); 
-  }
-
-
-  /**
-   * Removes the (key, value) pair from this 
-   * table. This method does nothing if the key is not in the table,
-   * or if the key is associated with a different value. This method
-   * is needed by EntrySet.
-   *
-   * @param   key   the key that needs to be removed.
-   * @param   value   the associated value. If the value is null,
-   *                   it means "any value".
-   * @return  the value to which the key had been mapped in this table,
-   *          or <code>null</code> if the key did not have a mapping.
-   * @exception  NullPointerException  if the key is
-   *               <code>null</code>.
-   */
-
-  protected Object remove(Object key, Object value) {
-    /*
-      Find the entry, then 
-        1. Set value field to null, to force get() to retry
-        2. Rebuild the list without this entry.
-           All entries following removed node can stay in list, but
-           all preceeding ones need to be cloned.  Traversals rely
-           on this strategy to ensure that elements will not be
-          repeated during iteration.
-    */
-
-    int hash = hash(key);
-    Segment seg = segments[hash & SEGMENT_MASK];
-
-    synchronized(seg) {
-      Entry[] tab = table;
-      int index = hash & (tab.length-1);
-      Entry first = tab[index];
-      Entry e = first;
-
-      for (;;) {
-        if (e == null)
-          return null;
-        if (e.hash == hash && eq(key, e.key)) 
-          break;
-        e = e.next;
-      }
-
-      Object oldValue = e.value;
-      if (value != null && !value.equals(oldValue))
-        return null;
-     
-      e.value = null;
-
-      Entry head = e.next;
-      for (Entry p = first; p != e; p = p.next) 
-        head = new Entry(p.hash, p.key, p.value, head);
-      tab[index] = head;
-      seg.count--;
-      return oldValue;
-    }
-  }
-
-
-  /**
-   * Returns <tt>true</tt> if this map maps one or more keys to the
-   * specified value. Note: This method requires a full internal
-   * traversal of the hash table, and so is much slower than
-   * method <tt>containsKey</tt>.
-   *
-   * @param value value whose presence in this map is to be tested.
-   * @return <tt>true</tt> if this map maps one or more keys to the
-   * specified value.  
-   * @exception  NullPointerException  if the value is <code>null</code>.
-   */
-  public boolean containsValue(Object value) {
-
-    if (value == null) throw new NullPointerException();
-
-    for (int s = 0; s < segments.length; ++s) {
-      Segment seg = segments[s];
-      Entry[] tab;
-      synchronized(seg) { tab = table; }
-      for (int i = s; i < tab.length; i+= segments.length) {
-        for (Entry e = tab[i]; e != null; e = e.next) 
-          if (value.equals(e.value))
-            return true;
-      }
-    }
-    return false;
-  }
-
-  /**
-   * Tests if some key maps into the specified value in this table.
-   * This operation is more expensive than the <code>containsKey</code>
-   * method.<p>
-   *
-   * Note that this method is identical in functionality to containsValue,
-   * (which is part of the Map interface in the collections framework).
-   * 
-   * @param      value   a value to search for.
-   * @return     <code>true</code> if and only if some key maps to the
-   *             <code>value</code> argument in this table as 
-   *             determined by the <tt>equals</tt> method;
-   *             <code>false</code> otherwise.
-   * @exception  NullPointerException  if the value is <code>null</code>.
-   * @see        #containsKey(Object)
-   * @see        #containsValue(Object)
-   * @see         Map
-   */
-
-  public boolean contains(Object value) {
-    return containsValue(value);
-  }
-
-  /**
-   * Copies all of the mappings from the specified map to this one.
-   * 
-   * These mappings replace any mappings that this map had for any of the
-   * keys currently in the specified Map.
-   *
-   * @param t Mappings to be stored in this map.
-   */
-
-  public void putAll(Map t) {
-    int n = t.size();
-    if (n == 0)
-      return;
-
-    // Expand enough to hold at least n elements without resizing.
-    // We can only resize table by factor of two at a time.
-    // It is faster to rehash with fewer elements, so do it now.
-    for(;;) {
-      Entry[] tab;
-      int max;
-      synchronized(segments[0]) { // must synch on some segment. pick 0.
-        tab = table;
-        max = threshold * CONCURRENCY_LEVEL;
-      }
-      if (n < max)
-        break;
-      resize(0, tab);
-    }
-
-    for (Iterator it = t.entrySet().iterator(); it.hasNext();) {
-      Map.Entry entry = (Map.Entry) it.next();
-      put(entry.getKey(), entry.getValue());
-    }
-  }
-
-  /**
-   * Removes all mappings from this map.
-   */
-
-  public void clear() {
-    // We don't need all locks at once so long as locks
-    //   are obtained in low to high order
-    for (int s = 0; s < segments.length; ++s) {
-      Segment seg = segments[s];
-      synchronized(seg) {
-        Entry[] tab = table;
-        for (int i = s; i < tab.length; i+= segments.length) {
-          for (Entry e = tab[i]; e != null; e = e.next) 
-            e.value = null; 
-          tab[i] = null;
-          seg.count = 0;
-        }
-      }
-    }
-  }
-
-  /**
-   * Returns a shallow copy of this 
-   * <tt>ConcurrentHashMap</tt> instance: the keys and
-   * values themselves are not cloned.
-   *
-   * @return a shallow copy of this map.
-   */
-
-  public Object clone() {
-    // We cannot call super.clone, since it would share final segments array,
-    // and there's no way to reassign finals.
-    return new ConcurrentHashMap(this);
-  }
-
-  // Views
-
-  protected transient Set keySet = null;
-  protected transient Set entrySet = null;
-  protected transient Collection values = null;
-
-  /**
-   * Returns a set view of the keys contained in this map.  The set is
-   * backed by the map, so changes to the map are reflected in the set, and
-   * vice-versa.  The set supports element removal, which removes the
-   * corresponding mapping from this map, via the <tt>Iterator.remove</tt>,
-   * <tt>Set.remove</tt>, <tt>removeAll</tt>, <tt>retainAll</tt>, and
-   * <tt>clear</tt> operations.  It does not support the <tt>add</tt> or
-   * <tt>addAll</tt> operations.
-   *
-   * @return a set view of the keys contained in this map.
-   */
-  
-  public Set keySet() {
-    Set ks = keySet;
-    return (ks != null)? ks : (keySet = new KeySet());
-  }
-  
-  private class KeySet extends AbstractSet {
-    public Iterator iterator() {
-      return new KeyIterator();
-    }
-    public int size() {
-      return ConcurrentHashMap.this.size();
-    }
-    public boolean contains(Object o) {
-      return ConcurrentHashMap.this.containsKey(o);
-    }
-    public boolean remove(Object o) {
-      return ConcurrentHashMap.this.remove(o) != null;
-    }
-    public void clear() {
-      ConcurrentHashMap.this.clear();
-    }
-  }
-
-  /**
-   * Returns a collection view of the values contained in this map.  The
-   * collection is backed by the map, so changes to the map are reflected in
-   * the collection, and vice-versa.  The collection supports element
-   * removal, which removes the corresponding mapping from this map, via the
-   * <tt>Iterator.remove</tt>, <tt>Collection.remove</tt>,
-   * <tt>removeAll</tt>, <tt>retainAll</tt>, and <tt>clear</tt> operations.
-   * It does not support the <tt>add</tt> or <tt>addAll</tt> operations.
-   *
-   * @return a collection view of the values contained in this map.
-   */
-  
-  public Collection values() {
-    Collection vs = values;
-    return (vs != null)? vs : (values = new Values());
-  }
-  
-  private class Values extends AbstractCollection {
-    public Iterator iterator() {
-      return new ValueIterator();
-    }
-    public int size() {
-      return ConcurrentHashMap.this.size();
-    }
-    public boolean contains(Object o) {
-      return ConcurrentHashMap.this.containsValue(o);
-    }
-    public void clear() {
-      ConcurrentHashMap.this.clear();
-    }
-  }
-
-  /**
-   * Returns a collection view of the mappings contained in this map.  Each
-   * element in the returned collection is a <tt>Map.Entry</tt>.  The
-   * collection is backed by the map, so changes to the map are reflected in
-   * the collection, and vice-versa.  The collection supports element
-   * removal, which removes the corresponding mapping from the map, via the
-   * <tt>Iterator.remove</tt>, <tt>Collection.remove</tt>,
-   * <tt>removeAll</tt>, <tt>retainAll</tt>, and <tt>clear</tt> operations.
-   * It does not support the <tt>add</tt> or <tt>addAll</tt> operations.
-   *
-   * @return a collection view of the mappings contained in this map.
-   */
-  
-  public Set entrySet() {
-    Set es = entrySet;
-    return (es != null) ? es : (entrySet = new EntrySet());
-  }
-
-  private class EntrySet extends AbstractSet {
-    public Iterator iterator() {
-      return new HashIterator();
-    }
-    public boolean contains(Object o) {
-      if (!(o instanceof Map.Entry))
-        return false;
-      Map.Entry entry = (Map.Entry)o;
-      Object v = ConcurrentHashMap.this.get(entry.getKey());
-      return v != null && v.equals(entry.getValue());
-    }
-    public boolean remove(Object o) {
-      if (!(o instanceof Map.Entry))
-        return false;
-      Map.Entry e = (Map.Entry)o;
-      return ConcurrentHashMap.this.remove(e.getKey(), e.getValue()) != null;
-    }
-    public int size() {
-      return ConcurrentHashMap.this.size();
-    }
-    public void clear() {
-      ConcurrentHashMap.this.clear();
-    }
-  }
-
-  /**
-   * Returns an enumeration of the keys in this table.
-   *
-   * @return  an enumeration of the keys in this table.
-   * @see     Enumeration
-   * @see     #elements()
-   * @see      #keySet()
-   * @see      Map
-   */
-  public Enumeration keys() {
-    return new KeyIterator();
-  }
-
-  /**
-   * Returns an enumeration of the values in this table.
-   * Use the Enumeration methods on the returned object to fetch the elements
-   * sequentially.
-   *
-   * @return  an enumeration of the values in this table.
-   * @see     java.util.Enumeration
-   * @see     #keys()
-   * @see      #values()
-   * @see      Map
-   */
-  
-  public Enumeration elements() {
-    return new ValueIterator();
-  }
-
-  /**
-   * ConcurrentHashMap collision list entry.
-   */
-
-  protected static class Entry implements Map.Entry {
-    /* 
-       The use of volatile for value field ensures that
-       we can detect status changes without synchronization.
-       The other fields are never changed, and are
-       marked as final. 
-    */
-
-    protected final Object key;
-    protected volatile Object value;
-    protected final int hash;
-    protected final Entry next;
-
-    Entry(int hash, Object key, Object value, Entry next) {
-      this.value = value;
-      this.hash = hash;
-      this.key = key;
-      this.next = next;
-    }
-
-    // Map.Entry Ops 
-
-    public Object getKey() {
-      return key;
-    }
-
-    /**
-     * Get the value.  Note: In an entrySet or entrySet.iterator,
-     * unless you can guarantee lack of concurrent modification,
-     * <tt>getValue</tt> <em>might</em> return null, reflecting the
-     * fact that the entry has been concurrently removed. However,
-     * there are no assurances that concurrent removals will be
-     * reflected using this method.
-     * 
-     * @return     the current value, or null if the entry has been 
-     * detectably removed.
-     **/
-    public Object getValue() {
-      return value; 
-    }
-
-    /**
-     * Set the value of this entry.  Note: In an entrySet or
-     * entrySet.iterator), unless you can guarantee lack of concurrent
-     * modification, <tt>setValue</tt> is not strictly guaranteed to
-     * actually replace the value field obtained via the <tt>get</tt>
-     * operation of the underlying hash table in multithreaded
-     * applications.  If iterator-wide synchronization is not used,
-     * and any other concurrent <tt>put</tt> or <tt>remove</tt>
-     * operations occur, sometimes even to <em>other</em> entries,
-     * then this change is not guaranteed to be reflected in the hash
-     * table. (It might, or it might not. There are no assurances
-     * either way.)
-     *
-     * @param      value   the new value.
-     * @return     the previous value, or null if entry has been detectably
-     * removed.
-     * @exception  NullPointerException  if the value is <code>null</code>.
-     * 
-     **/
-
-    public Object setValue(Object value) {
-      if (value == null)
-        throw new NullPointerException();
-      Object oldValue = this.value;
-      this.value = value;
-      return oldValue;
-    }
-
-    public boolean equals(Object o) {
-      if (!(o instanceof Map.Entry))
-        return false;
-      Map.Entry e = (Map.Entry)o;
-      return (key.equals(e.getKey()) && value.equals(e.getValue()));
-    }
-    
-    public int hashCode() {
-      return  key.hashCode() ^ value.hashCode();
-    }
-    
-    public String toString() {
-      return key + "=" + value;
-    }
-
-  }
-
-  protected class HashIterator implements Iterator, Enumeration {
-    protected final Entry[] tab;           // snapshot of table
-    protected int index;                   // current slot 
-    protected Entry entry = null;          // current node of slot
-    protected Object currentKey;           // key for current node
-    protected Object currentValue;         // value for current node
-    protected Entry lastReturned = null;   // last node returned by next
-
-    protected HashIterator() {
-      // force all segments to synch
-      synchronized(segments[0]) { tab = table; }
-      for (int i = 1; i < segments.length; ++i) segments[i].synch();
-      index = tab.length - 1;
-    }
-
-    public boolean hasMoreElements() { return hasNext(); }
-    public Object nextElement() { return next(); }
-
-    public boolean hasNext() {
-      /*
-        currentkey and currentValue are set here to ensure that next()
-        returns normally if hasNext() returns true. This avoids
-        surprises especially when final element is removed during
-        traversal -- instead, we just ignore the removal during
-        current traversal.  
-      */
-
-      for (;;) {
-        if (entry != null) {
-          Object v = entry.value;
-          if (v != null) {
-            currentKey = entry.key;
-            currentValue = v;
-            return true;
-          }
-          else
-            entry = entry.next;
-        }
-
-        while (entry == null && index >= 0)
-          entry = tab[index--];
-
-        if (entry == null) {
-          currentKey = currentValue = null;
-          return false;
-        }
-      }
-    }
-
-    protected Object returnValueOfNext() { return entry; }
-
-    public Object next() {
-      if (currentKey == null && !hasNext())
-        throw new NoSuchElementException();
-
-      Object result = returnValueOfNext();
-      lastReturned = entry;
-      currentKey = currentValue = null;
-      entry = entry.next;
-      return result;
-    }
-
-    public void remove() {
-      if (lastReturned == null)
-        throw new IllegalStateException();
-      ConcurrentHashMap.this.remove(lastReturned.key);
-      lastReturned = null;
-    }
-
-  }
-
-  protected class KeyIterator extends HashIterator {
-    protected Object returnValueOfNext() { return currentKey; }
-  }
-  
-  protected class ValueIterator extends HashIterator {
-    protected Object returnValueOfNext() { return currentValue; }
-  }
-  
-  /**
-   * Save the state of the <tt>ConcurrentHashMap</tt> 
-   * instance to a stream (i.e.,
-   * serialize it).
-   *
-   * @serialData  
-   * An estimate of the table size, followed by
-   * the key (Object) and value (Object)
-   * for each key-value mapping, followed by a null pair.
-   * The key-value mappings are emitted in no particular order.
-   */
-
-  private void writeObject(java.io.ObjectOutputStream s)
-    throws IOException  {
-    // Write out the loadfactor, and any hidden stuff
-    s.defaultWriteObject();
-
-    // Write out capacity estimate. It is OK if this
-    // changes during the write, since it is only used by
-    // readObject to set initial capacity, to avoid needless resizings.
-
-    int cap;
-    synchronized(segments[0]) { cap = table.length; }
-    s.writeInt(cap);
-
-    // Write out keys and values (alternating)
-    for (int k = 0; k < segments.length; ++k) {
-      Segment seg = segments[k];
-      Entry[] tab;
-      synchronized(seg) { tab = table; }
-      for (int i = k; i < tab.length; i+= segments.length) {
-        for (Entry e = tab[i]; e != null; e = e.next) {
-          s.writeObject(e.key);
-          s.writeObject(e.value);
-        }
-      }
-    }
-
-    s.writeObject(null);
-    s.writeObject(null);
-  }
-
-  /**
-   * Reconstitute the <tt>ConcurrentHashMap</tt> 
-   * instance from a stream (i.e.,
-   * deserialize it).
-   */
-  private void readObject(java.io.ObjectInputStream s)
-    throws IOException, ClassNotFoundException  {
-    // Read in the threshold, loadfactor, and any hidden stuff
-    s.defaultReadObject();
-
-    int cap = s.readInt();
-    table = newTable(cap);
-    for (int i = 0; i < segments.length; ++i) 
-      segments[i] = new Segment();
-
-
-    // Read the keys and values, and put the mappings in the table
-    for (;;) {
-      Object key = s.readObject();
-      Object value = s.readObject();
-      if (key == null)
-        break;
-      put(key, value);
-    }
-  }
-}
diff --git a/output/concurrent-hashmap/Makefile b/output/concurrent-hashmap/Makefile
deleted file mode 100644 (file)
index 6b615a1..0000000
+++ /dev/null
@@ -1,15 +0,0 @@
-include ../benchmarks.mk
-
-BENCH := hashmap
-TESTS := main testcase1
-
-all: $(TESTS)
-
-$(BENCH).o : $(BENCH).h
-       $(CXX) -o $@ $< $(CXXFLAGS) -c $(LDFLAGS)
-
-$(TESTS): % : %.cc $(BENCH).o
-       $(CXX) -o $@ $< $(CXXFLAGS) $(LDFLAGS)
-
-clean:
-       rm -f *.o *.d $(TESTS)
diff --git a/output/concurrent-hashmap/hashmap.h b/output/concurrent-hashmap/hashmap.h
deleted file mode 100644 (file)
index 5a05cd3..0000000
+++ /dev/null
@@ -1,471 +0,0 @@
-#ifndef _HASHMAP_H
-#define _HASHMAP_H
-
-#include <iostream>
-#include <atomic>
-#include "stdio.h" 
-#include <stdlib.h>
-#include <mutex>
-
-#include <spec_lib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h" 
-
-
-#include "common.h"
-
-#define relaxed memory_order_relaxed
-#define release memory_order_release
-#define acquire memory_order_acquire
-#define acq_rel memory_order_acq_rel
-#define seq_cst memory_order_seq_cst
-
-using namespace std;
-
-
-
-class Entry {
-       public:
-       int key;
-       atomic_int value;
-       int hash;
-       atomic<Entry*> next;
-
-       Entry(int h, int k, int v, Entry *n) {
-               this->hash = h;
-               this->key = k;
-               this->value.store(v, relaxed);
-               this->next.store(n, relaxed);
-       }
-};
-
-class Segment {
-       public:
-       int count;
-       mutex segMutex;
-
-       void lock() {
-               segMutex.lock();
-       }
-
-       void unlock() {
-               segMutex.unlock();
-       }
-
-       Segment() {
-               this->count = 0;
-       }
-};
-
-
-class HashMap {
-       public:
-
-/* All other user-defined structs */
-static IntegerMap * __map;
-/* All other user-defined functions */
-/* Definition of interface info struct: Put */
-typedef struct Put_info {
-int __RET__;
-int key;
-int value;
-} Put_info;
-/* End of info struct definition: Put */
-
-/* ID function of interface: Put */
-inline static call_id_t Put_id(void *info, thread_id_t __TID__) {
-       Put_info* theInfo = (Put_info*)info;
-       int __RET__ = theInfo->__RET__;
-       int key = theInfo->key;
-       int value = theInfo->value;
-
-       call_id_t __ID__ = value;
-       return __ID__;
-}
-/* End of ID function: Put */
-
-/* Check action function of interface: Put */
-inline static bool Put_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Put_info* theInfo = (Put_info*)info;
-       int __RET__ = theInfo->__RET__;
-       int key = theInfo->key;
-       int value = theInfo->value;
-
-       putIntegerMap ( __map , key , value ) ;
-       return true;
-}
-/* End of check action function: Put */
-
-/* Definition of interface info struct: Get */
-typedef struct Get_info {
-int __RET__;
-int key;
-} Get_info;
-/* End of info struct definition: Get */
-
-/* ID function of interface: Get */
-inline static call_id_t Get_id(void *info, thread_id_t __TID__) {
-       Get_info* theInfo = (Get_info*)info;
-       int __RET__ = theInfo->__RET__;
-       int key = theInfo->key;
-
-       call_id_t __ID__ = __RET__;
-       return __ID__;
-}
-/* End of ID function: Get */
-
-/* Check action function of interface: Get */
-inline static bool Get_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Get_info* theInfo = (Get_info*)info;
-       int __RET__ = theInfo->__RET__;
-       int key = theInfo->key;
-
-       int res = getIntegerMap ( __map , key ) ;
-       check_passed = __RET__ ? res == __RET__ : true;
-       if (!check_passed)
-               return false;
-       return true;
-}
-/* End of check action function: Get */
-
-#define INTERFACE_SIZE 2
-static void** func_ptr_table;
-static hb_rule** hb_rule_table;
-static commutativity_rule** commutativity_rule_table;
-inline static bool CommutativityCondition0(void *info1, void *info2) {
-       Put_info *_info1 = (Put_info*) info1;
-       Put_info *_info2 = (Put_info*) info2;
-       return _info1-> key != _info2-> key;
-}
-inline static bool CommutativityCondition1(void *info1, void *info2) {
-       Put_info *_info1 = (Put_info*) info1;
-       Get_info *_info2 = (Get_info*) info2;
-       return _info1-> key != _info2-> key;
-}
-inline static bool CommutativityCondition2(void *info1, void *info2) {
-       Get_info *_info1 = (Get_info*) info1;
-       Get_info *_info2 = (Get_info*) info2;
-       return true;
-}
-
-/* Initialization of sequential varialbes */
-static void __SPEC_INIT__() {
-       __map = createIntegerMap ( ) ;
-}
-
-/* Cleanup routine of sequential variables */
-static bool __SPEC_CLEANUP__() {
-       if ( __map ) destroyIntegerMap ( __map ) ;
-       return true ;
-}
-
-/* Define function for sequential code initialization */
-inline static void __sequential_init() {
-       /* Init func_ptr_table */
-       func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
-       func_ptr_table[2 * 1] = (void*) &Put_id;
-       func_ptr_table[2 * 1 + 1] = (void*) &Put_check_action;
-       func_ptr_table[2 * 0] = (void*) &Get_id;
-       func_ptr_table[2 * 0 + 1] = (void*) &Get_check_action;
-       /* Put(true) -> Get(true) */
-       struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit0->interface_num_before = 1; // Put
-       hbConditionInit0->hb_condition_num_before = 0; // 
-       hbConditionInit0->interface_num_after = 0; // Get
-       hbConditionInit0->hb_condition_num_after = 0; // 
-       /* Init hb_rule_table */
-       hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
-       #define HB_RULE_TABLE_SIZE 1
-       hb_rule_table[0] = hbConditionInit0;
-       /* Init commutativity_rule_table */
-       commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 3);
-       commutativity_rule* rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 1;
-       rule->interface_num_after = 1;
-       rule->rule = "_Method1 . key != _Method2 . key";
-       rule->condition = CommutativityCondition0;
-       commutativity_rule_table[0] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 1;
-       rule->interface_num_after = 0;
-       rule->rule = "_Method1 . key != _Method2 . key";
-       rule->condition = CommutativityCondition1;
-       commutativity_rule_table[1] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 0;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition2;
-       commutativity_rule_table[2] = rule;
-       /* Pass init info, including function table info & HB rules & Commutativity Rules */
-       struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
-       anno_init->init_func = (void_func_t) __SPEC_INIT__;
-       anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
-       anno_init->func_table = func_ptr_table;
-       anno_init->func_table_size = INTERFACE_SIZE;
-       anno_init->hb_rule_table = hb_rule_table;
-       anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
-       anno_init->commutativity_rule_table = commutativity_rule_table;
-       anno_init->commutativity_rule_table_size = 3;
-       struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       init->type = INIT;
-       init->annotation = anno_init;
-       cdsannotate(SPEC_ANALYSIS, init);
-
-}
-
-/* End of Global construct generation in class */
-       
-
-       atomic<Entry*> *table;
-
-       int capacity;
-       int size;
-
-       static const int CONCURRENCY_LEVEL = 4;
-
-       static const int SEGMENT_MASK = CONCURRENCY_LEVEL - 1;
-
-       Segment *segments[CONCURRENCY_LEVEL];
-
-       static const int DEFAULT_INITIAL_CAPACITY = 16;
-
-               
-       HashMap() {
-       __sequential_init();
-               
-               this->size = 0;
-               this->capacity = DEFAULT_INITIAL_CAPACITY;
-               this->table = new atomic<Entry*>[capacity];
-               for (int i = 0; i < capacity; i++) {
-                       atomic_init(&table[i], NULL);
-               }
-               for (int i = 0; i < CONCURRENCY_LEVEL; i++) {
-                       segments[i] = new Segment;
-               }
-       }
-
-       int hashKey(int key) {
-               return key;
-       }
-       
-
-
-int get(int key) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 0; // Get
-               interface_begin->interface_name = "Get";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       int __RET__ = __wrapper__get(key);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 0; // Get
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Get_info* info = (Get_info*) malloc(sizeof(Get_info));
-       info->__RET__ = __RET__;
-       info->key = key;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 0; // Get
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-       return __RET__;
-}
-       
-int __wrapper__get(int key) {
-               ASSERT (key);
-               int hash = hashKey(key);
-
-                               atomic<Entry*> *tab = table;
-               int index = hash & (capacity - 1);
-               atomic<Entry*> *first = &tab[index];
-               Entry *e;
-               int res = 0;
-
-                                                                                               
-               
-               Entry *firstPtr = first->load(acquire);
-
-               e = firstPtr;
-               while (e != NULL) {
-                       if (key, e->key) {
-                               
-                               res = e->value.load(seq_cst);
-       /* Automatically generated code for commit point define check: GetReadValue1 */
-
-       if (res != 0) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 0;
-               cp_define_check->label_name = "GetReadValue1";
-               cp_define_check->interface_num = 0;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-                               
-                               if (res != 0)
-                                       return res;
-                               else
-                                       break;
-                       }
-                                                                       e = e->next.load(relaxed);
-               }
-       
-                               Segment *seg = segments[hash & SEGMENT_MASK];
-               seg->lock();            
-                               Entry *newFirstPtr = first->load(relaxed);
-       /* Automatically generated code for commit point define check: GetReadEntry */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 1;
-               cp_define_check->label_name = "GetReadEntry";
-               cp_define_check->interface_num = 0;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-               
-               if (e != NULL || firstPtr != newFirstPtr) {
-                       e = newFirstPtr;
-                       while (e != NULL) {
-                               if (key == e->key) {
-                                                                               res = e->value.load(relaxed);
-       /* Automatically generated code for commit point define check: GetReadValue2 */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 2;
-               cp_define_check->label_name = "GetReadValue2";
-               cp_define_check->interface_num = 0;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-                                       
-                                       seg->unlock();                                  return res;
-                               }
-                                                               e = e->next.load(relaxed);
-                       }
-               }
-               seg->unlock();          return 0;
-       }
-
-
-int put(int key, int value) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 1; // Put
-               interface_begin->interface_name = "Put";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       int __RET__ = __wrapper__put(key, value);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 1; // Put
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Put_info* info = (Put_info*) malloc(sizeof(Put_info));
-       info->__RET__ = __RET__;
-       info->key = key;
-       info->value = value;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 1; // Put
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-       return __RET__;
-}
-       
-int __wrapper__put(int key, int value) {
-               ASSERT (key && value);
-               int hash = hashKey(key);
-               Segment *seg = segments[hash & SEGMENT_MASK];
-               atomic<Entry*> *tab;
-
-               seg->lock();            tab = table;
-               int index = hash & (capacity - 1);
-
-               atomic<Entry*> *first = &tab[index];
-               Entry *e;
-               int oldValue = 0;
-       
-                               Entry *firstPtr = first->load(relaxed);
-               e = firstPtr;
-               while (e != NULL) {
-                       if (key == e->key) {
-                                                                                               oldValue = e->value.load(relaxed);
-                               
-                               
-                               e->value.store(value, seq_cst);
-       /* Automatically generated code for commit point define check: PutUpdateValue */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 3;
-               cp_define_check->label_name = "PutUpdateValue";
-               cp_define_check->interface_num = 1;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-                               
-                               seg->unlock();                          return oldValue;
-                       }
-                                               e = e->next.load(relaxed);
-               }
-
-                               Entry *newEntry = new Entry(hash, key, value, firstPtr);
-               
-               
-                               first->store(newEntry, release);
-       /* Automatically generated code for commit point define check: PutInsertValue */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 4;
-               cp_define_check->label_name = "PutInsertValue";
-               cp_define_check->interface_num = 1;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-               
-               seg->unlock();          return 0;
-       }
-};
-void** HashMap::func_ptr_table;
-hb_rule** HashMap::hb_rule_table;
-commutativity_rule** HashMap::commutativity_rule_table;
-IntegerMap * HashMap::__map;
-
-
-#endif
-
diff --git a/output/concurrent-hashmap/hashmap.o b/output/concurrent-hashmap/hashmap.o
deleted file mode 100644 (file)
index 268350d..0000000
Binary files a/output/concurrent-hashmap/hashmap.o and /dev/null differ
diff --git a/output/concurrent-hashmap/main b/output/concurrent-hashmap/main
deleted file mode 100755 (executable)
index a9b7a82..0000000
Binary files a/output/concurrent-hashmap/main and /dev/null differ
diff --git a/output/concurrent-hashmap/main.cc b/output/concurrent-hashmap/main.cc
deleted file mode 100644 (file)
index f39f3b6..0000000
+++ /dev/null
@@ -1,35 +0,0 @@
-#include <iostream>
-#include <threads.h>
-#include "hashmap.h"
-
-HashMap *table;
-
-void threadA(void *arg) {
-       table->put(1, 1);
-       printf("Thrd A: Put %d -> %d\n", 1, 1);
-       int r1 = table->get(2);
-       printf("Thrd A: Get %d\n", r1);
-}
-
-void threadB(void *arg) {
-       table->put(2, 2);
-       printf("Thrd B: Put %d -> %d\n", 2, 2);
-       int r2 = table->get(1);
-       printf("Thrd B: Get %d\n", r2);
-}
-
-int user_main(int argc, char *argv[]) {
-       thrd_t t1, t2;
-
-       table = new HashMap;
-
-       thrd_create(&t1, threadA, NULL);
-       thrd_create(&t2, threadB, NULL);
-       thrd_join(t1);
-       thrd_join(t2);
-       
-       return 0;
-}
-
-
-
diff --git a/output/concurrent-hashmap/note.txt b/output/concurrent-hashmap/note.txt
deleted file mode 100644 (file)
index f080a48..0000000
+++ /dev/null
@@ -1,17 +0,0 @@
-#Non-SC:
-The following case can be non-SC.
-
-Thrd1                                          Thrd2
-put(k1, v1); // a                      put(k2, v2); // c
-get(k2); // b                          get(k1); // d
-
-When b and d both read the old head of the list (and they later grab the lock,
-making it the interface SC), it's non-SC because neither reads the updated
-value.
-
-Run testcase1 to make the store and load of value slot to be seq_cst.
-
-Then run testcase2 with "-o annotation" to get store and load of key slot to be
-release/acquire.
-
-0m0.015s + 0m0.000 = 0m0.015s 
diff --git a/output/concurrent-hashmap/testcase1 b/output/concurrent-hashmap/testcase1
deleted file mode 100755 (executable)
index 54701c1..0000000
Binary files a/output/concurrent-hashmap/testcase1 and /dev/null differ
diff --git a/output/concurrent-hashmap/testcase1.cc b/output/concurrent-hashmap/testcase1.cc
deleted file mode 100644 (file)
index 059718e..0000000
+++ /dev/null
@@ -1,37 +0,0 @@
-#include <iostream>
-#include <threads.h>
-#include "hashmap.h"
-
-HashMap *table;
-
-void threadA(void *arg) {
-       table->put(1, 11);
-       printf("Thrd A: Put %d -> %d\n", 1, 11);
-       int r1 = table->get(2);
-       printf("Thrd A: Get %d\n", r1);
-}
-
-void threadB(void *arg) {
-       table->put(2, 22);
-       printf("Thrd B: Put %d -> %d\n", 2, 22);
-       int r2 = table->get(1);
-       printf("Thrd B: Get %d\n", r2);
-}
-
-int user_main(int argc, char *argv[]) {
-       thrd_t t1, t2;
-
-       table = new HashMap;
-       table->put(1, 1);
-       table->put(2, 2);
-
-       thrd_create(&t1, threadA, NULL);
-       thrd_create(&t2, threadB, NULL);
-       thrd_join(t1);
-       thrd_join(t2);
-       
-       return 0;
-}
-
-
-
diff --git a/output/include/unrelacy.h b/output/include/unrelacy.h
deleted file mode 100644 (file)
index 729d76f..0000000
+++ /dev/null
@@ -1,96 +0,0 @@
-#ifndef __UNRELACY_H__
-#define __UNRELACY_H__
-
-#include <stdatomic.h>
-#include <stdlib.h>
-#include <stdio.h>
-#include <mutex>
-#include <condition_variable>
-
-#include <model-assert.h>
-#include <librace.h>
-
-#define $
-
-#define ASSERT(expr) MODEL_ASSERT(expr)
-#define RL_ASSERT(expr) MODEL_ASSERT(expr)
-
-#define RL_NEW new
-#define RL_DELETE(expr) delete expr
-
-#define mo_seqcst memory_order_relaxed
-#define mo_release memory_order_release
-#define mo_acquire memory_order_acquire
-#define mo_acq_rel memory_order_acq_rel
-#define mo_relaxed memory_order_relaxed
-
-namespace rl {
-
-       /* This 'useless' struct is declared just so we can use partial template
-        * specialization in our store and load functions. */
-       template <typename T, size_t n>
-       struct useless {
-               static void store(void *addr, T val);
-               static T load(const void *addr);
-       };
-
-       template <typename T>
-       struct useless<T, 1> {
-               static void store(void *addr, T val) { store_8(addr, (uint8_t)val); }
-               static T load(const void *addr) { return (T)load_8(addr); }
-       };
-
-       template <typename T>
-       struct useless<T, 2> {
-               static void store(void *addr, T val) { store_16(addr, (uint16_t)val); }
-               static T load(const void *addr) { return (T)load_16(addr); }
-       };
-
-       template <typename T>
-       struct useless<T, 4> {
-               static void store(void *addr, T val) { store_32(addr, (uint32_t)val); }
-               static T load(const void *addr) { return (T)load_32(addr); }
-       };
-
-       template <typename T>
-       struct useless<T, 8> {
-               static void store(void *addr, T val) { store_64(addr, (uint64_t)val); }
-               static T load(const void *addr) { return (T)load_64(addr); }
-       };
-
-       template <typename T>
-       struct var {
-               var() { useless<T, sizeof(T)>::store(&value, 0); }
-               var(T v) { useless<T, sizeof(T)>::store(&value, v); }
-               var(var const& r) {
-                       value = r.value;
-               }
-               ~var() { }
-
-               void operator = (T v) { useless<T, sizeof(T)>::store(&value, v); }
-               T operator () () { return useless<T, sizeof(T)>::load(&value); }
-               void operator += (T v) {
-                       useless<T, sizeof(T)>::store(&value,
-                                       useless<T, sizeof(T)>::load(&value) + v);
-               }
-               bool operator == (const struct var<T> v) const { return useless<T, sizeof(T)>::load(&value) == useless<T, sizeof(T)>::load(&v.value); }
-
-               T value;
-       };
-
-       class backoff_t
-       {
-        public:
-               typedef int debug_info_param;
-               void yield(debug_info_param info) { }
-               void yield() { }
-       };
-
-
-       typedef backoff_t backoff;
-       typedef backoff_t linear_backoff;
-       typedef backoff_t exp_backoff;
-
-}
-
-#endif /* __UNRELACY_H__ */
diff --git a/output/linuxrwlocks/Makefile b/output/linuxrwlocks/Makefile
deleted file mode 100644 (file)
index c62b36a..0000000
+++ /dev/null
@@ -1,11 +0,0 @@
-include ../benchmarks.mk
-
-TESTNAME = linuxrwlocks testcase1 testcase2
-
-all: $(TESTNAME)
-
-$(TESTNAME): % : %.c
-       $(CC) -o $@ $< $(CFLAGS) $(LDFLAGS)
-
-clean:
-       rm -f $(TESTNAME) *.o
diff --git a/output/linuxrwlocks/linuxrwlocks b/output/linuxrwlocks/linuxrwlocks
deleted file mode 100755 (executable)
index ecd7511..0000000
Binary files a/output/linuxrwlocks/linuxrwlocks and /dev/null differ
diff --git a/output/linuxrwlocks/linuxrwlocks.c b/output/linuxrwlocks/linuxrwlocks.c
deleted file mode 100644 (file)
index 5929374..0000000
+++ /dev/null
@@ -1,940 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h"
-
-#include "librace.h"
-
-#define RW_LOCK_BIAS            0x00100000
-#define WRITE_LOCK_CMP          RW_LOCK_BIAS
-
-typedef union {
-       atomic_int lock;
-} rwlock_t;
-
-
-
-
-
-
-
-/* All other user-defined structs */
-static bool writer_lock_acquired;
-static int reader_lock_cnt;
-/* All other user-defined functions */
-/* Definition of interface info struct: Write_Trylock */
-typedef struct Write_Trylock_info {
-int __RET__;
-rwlock_t * rw;
-} Write_Trylock_info;
-/* End of info struct definition: Write_Trylock */
-
-/* ID function of interface: Write_Trylock */
-inline static call_id_t Write_Trylock_id(void *info, thread_id_t __TID__) {
-       Write_Trylock_info* theInfo = (Write_Trylock_info*)info;
-       int __RET__ = theInfo->__RET__;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Write_Trylock */
-
-/* Check action function of interface: Write_Trylock */
-inline static bool Write_Trylock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Write_Trylock_info* theInfo = (Write_Trylock_info*)info;
-       int __RET__ = theInfo->__RET__;
-       rwlock_t * rw = theInfo->rw;
-
-       if ( __RET__ == 1 ) writer_lock_acquired = true ;
-       return true;
-}
-/* End of check action function: Write_Trylock */
-
-/* Definition of interface info struct: Read_Trylock */
-typedef struct Read_Trylock_info {
-int __RET__;
-rwlock_t * rw;
-} Read_Trylock_info;
-/* End of info struct definition: Read_Trylock */
-
-/* ID function of interface: Read_Trylock */
-inline static call_id_t Read_Trylock_id(void *info, thread_id_t __TID__) {
-       Read_Trylock_info* theInfo = (Read_Trylock_info*)info;
-       int __RET__ = theInfo->__RET__;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Read_Trylock */
-
-/* Check action function of interface: Read_Trylock */
-inline static bool Read_Trylock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Read_Trylock_info* theInfo = (Read_Trylock_info*)info;
-       int __RET__ = theInfo->__RET__;
-       rwlock_t * rw = theInfo->rw;
-
-       if ( __RET__ ) reader_lock_cnt ++ ;
-       check_passed = __RET__ == ! writer_lock_acquired || ! __RET__;
-       if (!check_passed)
-               return false;
-       return true;
-}
-/* End of check action function: Read_Trylock */
-
-/* Definition of interface info struct: Write_Lock */
-typedef struct Write_Lock_info {
-rwlock_t * rw;
-} Write_Lock_info;
-/* End of info struct definition: Write_Lock */
-
-/* ID function of interface: Write_Lock */
-inline static call_id_t Write_Lock_id(void *info, thread_id_t __TID__) {
-       Write_Lock_info* theInfo = (Write_Lock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Write_Lock */
-
-/* Check action function of interface: Write_Lock */
-inline static bool Write_Lock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Write_Lock_info* theInfo = (Write_Lock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       check_passed = ! writer_lock_acquired && reader_lock_cnt == 0;
-       if (!check_passed)
-               return false;
-       writer_lock_acquired = true ;
-       return true;
-}
-/* End of check action function: Write_Lock */
-
-/* Definition of interface info struct: Write_Unlock */
-typedef struct Write_Unlock_info {
-rwlock_t * rw;
-} Write_Unlock_info;
-/* End of info struct definition: Write_Unlock */
-
-/* ID function of interface: Write_Unlock */
-inline static call_id_t Write_Unlock_id(void *info, thread_id_t __TID__) {
-       Write_Unlock_info* theInfo = (Write_Unlock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Write_Unlock */
-
-/* Check action function of interface: Write_Unlock */
-inline static bool Write_Unlock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Write_Unlock_info* theInfo = (Write_Unlock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       check_passed = reader_lock_cnt == 0 && writer_lock_acquired;
-       if (!check_passed)
-               return false;
-       writer_lock_acquired = false ;
-       return true;
-}
-/* End of check action function: Write_Unlock */
-
-/* Definition of interface info struct: Read_Unlock */
-typedef struct Read_Unlock_info {
-rwlock_t * rw;
-} Read_Unlock_info;
-/* End of info struct definition: Read_Unlock */
-
-/* ID function of interface: Read_Unlock */
-inline static call_id_t Read_Unlock_id(void *info, thread_id_t __TID__) {
-       Read_Unlock_info* theInfo = (Read_Unlock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Read_Unlock */
-
-/* Check action function of interface: Read_Unlock */
-inline static bool Read_Unlock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Read_Unlock_info* theInfo = (Read_Unlock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       check_passed = reader_lock_cnt > 0 && ! writer_lock_acquired;
-       if (!check_passed)
-               return false;
-       reader_lock_cnt -- ;
-       return true;
-}
-/* End of check action function: Read_Unlock */
-
-/* Definition of interface info struct: Read_Lock */
-typedef struct Read_Lock_info {
-rwlock_t * rw;
-} Read_Lock_info;
-/* End of info struct definition: Read_Lock */
-
-/* ID function of interface: Read_Lock */
-inline static call_id_t Read_Lock_id(void *info, thread_id_t __TID__) {
-       Read_Lock_info* theInfo = (Read_Lock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Read_Lock */
-
-/* Check action function of interface: Read_Lock */
-inline static bool Read_Lock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Read_Lock_info* theInfo = (Read_Lock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       check_passed = ! writer_lock_acquired;
-       if (!check_passed)
-               return false;
-       reader_lock_cnt ++ ;
-       return true;
-}
-/* End of check action function: Read_Lock */
-
-#define INTERFACE_SIZE 6
-static void** func_ptr_table;
-static hb_rule** hb_rule_table;
-static commutativity_rule** commutativity_rule_table;
-inline static bool CommutativityCondition0(void *info1, void *info2) {
-       Read_Lock_info *_info1 = (Read_Lock_info*) info1;
-       Read_Lock_info *_info2 = (Read_Lock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition1(void *info1, void *info2) {
-       Read_Lock_info *_info1 = (Read_Lock_info*) info1;
-       Read_Unlock_info *_info2 = (Read_Unlock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition2(void *info1, void *info2) {
-       Read_Lock_info *_info1 = (Read_Lock_info*) info1;
-       Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition3(void *info1, void *info2) {
-       Read_Lock_info *_info1 = (Read_Lock_info*) info1;
-       Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
-       return ! _info2-> __RET__;
-}
-inline static bool CommutativityCondition4(void *info1, void *info2) {
-       Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
-       Read_Unlock_info *_info2 = (Read_Unlock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition5(void *info1, void *info2) {
-       Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
-       Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition6(void *info1, void *info2) {
-       Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
-       Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
-       return ! _info2-> __RET__;
-}
-inline static bool CommutativityCondition7(void *info1, void *info2) {
-       Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
-       Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition8(void *info1, void *info2) {
-       Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
-       Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
-       return ! _info1-> __RET__ || ! _info2-> __RET__;
-}
-inline static bool CommutativityCondition9(void *info1, void *info2) {
-       Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
-       Write_Lock_info *_info2 = (Write_Lock_info*) info2;
-       return ! _info1-> __RET__;
-}
-inline static bool CommutativityCondition10(void *info1, void *info2) {
-       Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
-       Write_Unlock_info *_info2 = (Write_Unlock_info*) info2;
-       return ! _info1-> __RET__;
-}
-inline static bool CommutativityCondition11(void *info1, void *info2) {
-       Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
-       Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
-       return ! _info1-> __RET__ || ! _info2-> __RET__;
-}
-inline static bool CommutativityCondition12(void *info1, void *info2) {
-       Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
-       Write_Unlock_info *_info2 = (Write_Unlock_info*) info2;
-       return ! _info1-> __RET__;
-}
-inline static bool CommutativityCondition13(void *info1, void *info2) {
-       Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
-       Write_Lock_info *_info2 = (Write_Lock_info*) info2;
-       return ! _info1-> __RET__;
-}
-
-/* Initialization of sequential varialbes */
-static void __SPEC_INIT__() {
-       writer_lock_acquired = false ;
-       reader_lock_cnt = 0 ;
-}
-
-/* Cleanup routine of sequential variables */
-static bool __SPEC_CLEANUP__() {
-       return true;
-}
-
-/* Define function for sequential code initialization */
-inline static void __sequential_init() {
-       /* Init func_ptr_table */
-       func_ptr_table = (void**) malloc(sizeof(void*) * 6 * 2);
-       func_ptr_table[2 * 3] = (void*) &Write_Trylock_id;
-       func_ptr_table[2 * 3 + 1] = (void*) &Write_Trylock_check_action;
-       func_ptr_table[2 * 2] = (void*) &Read_Trylock_id;
-       func_ptr_table[2 * 2 + 1] = (void*) &Read_Trylock_check_action;
-       func_ptr_table[2 * 1] = (void*) &Write_Lock_id;
-       func_ptr_table[2 * 1 + 1] = (void*) &Write_Lock_check_action;
-       func_ptr_table[2 * 5] = (void*) &Write_Unlock_id;
-       func_ptr_table[2 * 5 + 1] = (void*) &Write_Unlock_check_action;
-       func_ptr_table[2 * 4] = (void*) &Read_Unlock_id;
-       func_ptr_table[2 * 4 + 1] = (void*) &Read_Unlock_check_action;
-       func_ptr_table[2 * 0] = (void*) &Read_Lock_id;
-       func_ptr_table[2 * 0 + 1] = (void*) &Read_Lock_check_action;
-       /* Read_Unlock(true) -> Write_Lock(true) */
-       struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit0->interface_num_before = 4; // Read_Unlock
-       hbConditionInit0->hb_condition_num_before = 0; // 
-       hbConditionInit0->interface_num_after = 1; // Write_Lock
-       hbConditionInit0->hb_condition_num_after = 0; // 
-       /* Read_Unlock(true) -> Write_Trylock(HB_Write_Trylock_Succ) */
-       struct hb_rule *hbConditionInit1 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit1->interface_num_before = 4; // Read_Unlock
-       hbConditionInit1->hb_condition_num_before = 0; // 
-       hbConditionInit1->interface_num_after = 3; // Write_Trylock
-       hbConditionInit1->hb_condition_num_after = 1; // HB_Write_Trylock_Succ
-       /* Write_Unlock(true) -> Write_Lock(true) */
-       struct hb_rule *hbConditionInit2 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit2->interface_num_before = 5; // Write_Unlock
-       hbConditionInit2->hb_condition_num_before = 0; // 
-       hbConditionInit2->interface_num_after = 1; // Write_Lock
-       hbConditionInit2->hb_condition_num_after = 0; // 
-       /* Write_Unlock(true) -> Write_Trylock(HB_Write_Trylock_Succ) */
-       struct hb_rule *hbConditionInit3 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit3->interface_num_before = 5; // Write_Unlock
-       hbConditionInit3->hb_condition_num_before = 0; // 
-       hbConditionInit3->interface_num_after = 3; // Write_Trylock
-       hbConditionInit3->hb_condition_num_after = 1; // HB_Write_Trylock_Succ
-       /* Write_Unlock(true) -> Read_Lock(true) */
-       struct hb_rule *hbConditionInit4 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit4->interface_num_before = 5; // Write_Unlock
-       hbConditionInit4->hb_condition_num_before = 0; // 
-       hbConditionInit4->interface_num_after = 0; // Read_Lock
-       hbConditionInit4->hb_condition_num_after = 0; // 
-       /* Write_Unlock(true) -> Read_Trylock(HB_Read_Trylock_Succ) */
-       struct hb_rule *hbConditionInit5 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit5->interface_num_before = 5; // Write_Unlock
-       hbConditionInit5->hb_condition_num_before = 0; // 
-       hbConditionInit5->interface_num_after = 2; // Read_Trylock
-       hbConditionInit5->hb_condition_num_after = 2; // HB_Read_Trylock_Succ
-       /* Init hb_rule_table */
-       hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 6);
-       #define HB_RULE_TABLE_SIZE 6
-       hb_rule_table[0] = hbConditionInit0;
-       hb_rule_table[1] = hbConditionInit1;
-       hb_rule_table[2] = hbConditionInit2;
-       hb_rule_table[3] = hbConditionInit3;
-       hb_rule_table[4] = hbConditionInit4;
-       hb_rule_table[5] = hbConditionInit5;
-       /* Init commutativity_rule_table */
-       commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 14);
-       commutativity_rule* rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 0;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition0;
-       commutativity_rule_table[0] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 4;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition1;
-       commutativity_rule_table[1] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 2;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition2;
-       commutativity_rule_table[2] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 3;
-       rule->rule = "! _Method2 . __RET__";
-       rule->condition = CommutativityCondition3;
-       commutativity_rule_table[3] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 4;
-       rule->interface_num_after = 4;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition4;
-       commutativity_rule_table[4] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 4;
-       rule->interface_num_after = 2;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition5;
-       commutativity_rule_table[5] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 4;
-       rule->interface_num_after = 3;
-       rule->rule = "! _Method2 . __RET__";
-       rule->condition = CommutativityCondition6;
-       commutativity_rule_table[6] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 2;
-       rule->interface_num_after = 2;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition7;
-       commutativity_rule_table[7] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 2;
-       rule->interface_num_after = 3;
-       rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
-       rule->condition = CommutativityCondition8;
-       commutativity_rule_table[8] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 2;
-       rule->interface_num_after = 1;
-       rule->rule = "! _Method1 . __RET__";
-       rule->condition = CommutativityCondition9;
-       commutativity_rule_table[9] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 2;
-       rule->interface_num_after = 5;
-       rule->rule = "! _Method1 . __RET__";
-       rule->condition = CommutativityCondition10;
-       commutativity_rule_table[10] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 3;
-       rule->interface_num_after = 3;
-       rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
-       rule->condition = CommutativityCondition11;
-       commutativity_rule_table[11] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 3;
-       rule->interface_num_after = 5;
-       rule->rule = "! _Method1 . __RET__";
-       rule->condition = CommutativityCondition12;
-       commutativity_rule_table[12] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 3;
-       rule->interface_num_after = 1;
-       rule->rule = "! _Method1 . __RET__";
-       rule->condition = CommutativityCondition13;
-       commutativity_rule_table[13] = rule;
-       /* Pass init info, including function table info & HB rules & Commutativity Rules */
-       struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
-       anno_init->init_func = (void_func_t) __SPEC_INIT__;
-       anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
-       anno_init->func_table = func_ptr_table;
-       anno_init->func_table_size = INTERFACE_SIZE;
-       anno_init->hb_rule_table = hb_rule_table;
-       anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
-       anno_init->commutativity_rule_table = commutativity_rule_table;
-       anno_init->commutativity_rule_table_size = 14;
-       struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       init->type = INIT;
-       init->annotation = anno_init;
-       cdsannotate(SPEC_ANALYSIS, init);
-
-}
-
-/* End of Global construct generation in class */
-
-
-static inline int read_can_lock(rwlock_t *lock)
-{
-       return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
-}
-
-static inline int write_can_lock(rwlock_t *lock)
-{
-       return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
-}
-
-
-void __wrapper__read_lock(rwlock_t * rw);
-
-void read_lock(rwlock_t * rw) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 0; // Read_Lock
-               interface_begin->interface_name = "Read_Lock";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       __wrapper__read_lock(rw);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 0; // Read_Lock
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Read_Lock_info* info = (Read_Lock_info*) malloc(sizeof(Read_Lock_info));
-       info->rw = rw;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 0; // Read_Lock
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-}
-
-void __wrapper__read_lock(rwlock_t * rw)
-{
-       
-       
-       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
-       /* Automatically generated code for commit point define check: Read_Lock_Success_1 */
-
-       if (priorvalue > 0) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 0;
-               cp_define_check->label_name = "Read_Lock_Success_1";
-               cp_define_check->interface_num = 0;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-       
-       while (priorvalue <= 0) {
-               atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
-               while (atomic_load_explicit(&rw->lock, memory_order_relaxed) <= 0) {
-                       thrd_yield();
-               }
-               
-               priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
-       /* Automatically generated code for commit point define check: Read_Lock_Success_2 */
-
-       if (priorvalue > 0) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 1;
-               cp_define_check->label_name = "Read_Lock_Success_2";
-               cp_define_check->interface_num = 0;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-               
-       }
-}
-
-
-void __wrapper__write_lock(rwlock_t * rw);
-
-void write_lock(rwlock_t * rw) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 1; // Write_Lock
-               interface_begin->interface_name = "Write_Lock";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       __wrapper__write_lock(rw);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 1; // Write_Lock
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Write_Lock_info* info = (Write_Lock_info*) malloc(sizeof(Write_Lock_info));
-       info->rw = rw;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 1; // Write_Lock
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-}
-
-void __wrapper__write_lock(rwlock_t * rw)
-{
-       
-       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
-       /* Automatically generated code for commit point define check: Write_Lock_Success_1 */
-
-       if (priorvalue == RW_LOCK_BIAS) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 2;
-               cp_define_check->label_name = "Write_Lock_Success_1";
-               cp_define_check->interface_num = 1;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-       
-       while (priorvalue != RW_LOCK_BIAS) {
-               atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
-               while (atomic_load_explicit(&rw->lock, memory_order_relaxed) != RW_LOCK_BIAS) {
-                       thrd_yield();
-               }
-               
-               priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
-       /* Automatically generated code for commit point define check: Write_Lock_Success_2 */
-
-       if (priorvalue == RW_LOCK_BIAS) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 3;
-               cp_define_check->label_name = "Write_Lock_Success_2";
-               cp_define_check->interface_num = 1;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-               
-       }
-}
-
-int __wrapper__read_trylock(rwlock_t * rw);
-
-int read_trylock(rwlock_t * rw) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 2; // Read_Trylock
-               interface_begin->interface_name = "Read_Trylock";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       int __RET__ = __wrapper__read_trylock(rw);
-       if (__RET__ == 1) {
-               struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-               hb_condition->interface_num = 2; // Read_Trylock
-               hb_condition->hb_condition_num = 2;
-               struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_hb_condition->type = HB_CONDITION;
-               annotation_hb_condition->annotation = hb_condition;
-               cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-       }
-
-       Read_Trylock_info* info = (Read_Trylock_info*) malloc(sizeof(Read_Trylock_info));
-       info->__RET__ = __RET__;
-       info->rw = rw;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 2; // Read_Trylock
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-       return __RET__;
-}
-
-int __wrapper__read_trylock(rwlock_t * rw)
-{
-       
-       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
-       /* Automatically generated code for potential commit point: Potential_Read_Trylock_Point */
-
-       if (true) {
-               struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
-               potential_cp_define->label_num = 4;
-               potential_cp_define->label_name = "Potential_Read_Trylock_Point";
-               struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
-               annotation_potential_cp_define->annotation = potential_cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
-       }
-       
-       if (priorvalue > 0) {
-       /* Automatically generated code for commit point define: Read_Trylock_Succ_Point */
-
-       if (true) {
-               struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
-               cp_define->label_num = 5;
-               cp_define->label_name = "Read_Trylock_Succ_Point";
-               cp_define->potential_cp_label_num = 4;
-               cp_define->potential_label_name = "Potential_Read_Trylock_Point";
-               cp_define->interface_num = 2;
-               struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define->type = CP_DEFINE;
-               annotation_cp_define->annotation = cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
-       }
-               
-               return 1;
-       }
-       /* Automatically generated code for commit point define: Read_Trylock_Fail_Point */
-
-       if (true) {
-               struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
-               cp_define->label_num = 6;
-               cp_define->label_name = "Read_Trylock_Fail_Point";
-               cp_define->potential_cp_label_num = 4;
-               cp_define->potential_label_name = "Potential_Read_Trylock_Point";
-               cp_define->interface_num = 2;
-               struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define->type = CP_DEFINE;
-               annotation_cp_define->annotation = cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
-       }
-       
-       atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
-       return 0;
-}
-
-int __wrapper__write_trylock(rwlock_t * rw);
-
-int write_trylock(rwlock_t * rw) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 3; // Write_Trylock
-               interface_begin->interface_name = "Write_Trylock";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       int __RET__ = __wrapper__write_trylock(rw);
-       if (__RET__ == 1) {
-               struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-               hb_condition->interface_num = 3; // Write_Trylock
-               hb_condition->hb_condition_num = 1;
-               struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_hb_condition->type = HB_CONDITION;
-               annotation_hb_condition->annotation = hb_condition;
-               cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-       }
-
-       Write_Trylock_info* info = (Write_Trylock_info*) malloc(sizeof(Write_Trylock_info));
-       info->__RET__ = __RET__;
-       info->rw = rw;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 3; // Write_Trylock
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-       return __RET__;
-}
-
-int __wrapper__write_trylock(rwlock_t * rw)
-{
-       
-       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
-       /* Automatically generated code for potential commit point: Potential_Write_Trylock_Point */
-
-       if (true) {
-               struct anno_potential_cp_define *potential_cp_define = (struct anno_potential_cp_define*) malloc(sizeof(struct anno_potential_cp_define));
-               potential_cp_define->label_num = 7;
-               potential_cp_define->label_name = "Potential_Write_Trylock_Point";
-               struct spec_annotation *annotation_potential_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_potential_cp_define->type = POTENTIAL_CP_DEFINE;
-               annotation_potential_cp_define->annotation = potential_cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_potential_cp_define);
-       }
-               
-       if (priorvalue == RW_LOCK_BIAS) {
-       /* Automatically generated code for commit point define: Write_Trylock_Succ_Point */
-
-       if (true) {
-               struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
-               cp_define->label_num = 8;
-               cp_define->label_name = "Write_Trylock_Succ_Point";
-               cp_define->potential_cp_label_num = 7;
-               cp_define->potential_label_name = "Potential_Write_Trylock_Point";
-               cp_define->interface_num = 3;
-               struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define->type = CP_DEFINE;
-               annotation_cp_define->annotation = cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
-       }
-               
-               return 1;
-       }
-       /* Automatically generated code for commit point define: Write_Trylock_Fail_Point */
-
-       if (true) {
-               struct anno_cp_define *cp_define = (struct anno_cp_define*) malloc(sizeof(struct anno_cp_define));
-               cp_define->label_num = 9;
-               cp_define->label_name = "Write_Trylock_Fail_Point";
-               cp_define->potential_cp_label_num = 7;
-               cp_define->potential_label_name = "Potential_Write_Trylock_Point";
-               cp_define->interface_num = 3;
-               struct spec_annotation *annotation_cp_define = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define->type = CP_DEFINE;
-               annotation_cp_define->annotation = cp_define;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define);
-       }
-       
-       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
-       return 0;
-}
-
-void __wrapper__read_unlock(rwlock_t * rw);
-
-void read_unlock(rwlock_t * rw) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 4; // Read_Unlock
-               interface_begin->interface_name = "Read_Unlock";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       __wrapper__read_unlock(rw);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 4; // Read_Unlock
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Read_Unlock_info* info = (Read_Unlock_info*) malloc(sizeof(Read_Unlock_info));
-       info->rw = rw;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 4; // Read_Unlock
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-}
-
-void __wrapper__read_unlock(rwlock_t * rw)
-{
-       
-       atomic_fetch_add_explicit(&rw->lock, 1, memory_order_release);
-       /* Automatically generated code for commit point define check: Read_Unlock_Point */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 10;
-               cp_define_check->label_name = "Read_Unlock_Point";
-               cp_define_check->interface_num = 4;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-       
-}
-
-void __wrapper__write_unlock(rwlock_t * rw);
-
-void write_unlock(rwlock_t * rw) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 5; // Write_Unlock
-               interface_begin->interface_name = "Write_Unlock";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       __wrapper__write_unlock(rw);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 5; // Write_Unlock
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Write_Unlock_info* info = (Write_Unlock_info*) malloc(sizeof(Write_Unlock_info));
-       info->rw = rw;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 5; // Write_Unlock
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-}
-
-void __wrapper__write_unlock(rwlock_t * rw)
-{
-       
-       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_release);
-       /* Automatically generated code for commit point define check: Write_Unlock_Point */
-
-       if (true) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 11;
-               cp_define_check->label_name = "Write_Unlock_Point";
-               cp_define_check->interface_num = 5;
-               struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-               annotation_cp_define_check->type = CP_DEFINE_CHECK;
-               annotation_cp_define_check->annotation = cp_define_check;
-               cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
-       }
-       
-
-       
-}
-
-rwlock_t mylock;
-int shareddata;
-
-static void a(void *obj)
-{
-       read_lock(&mylock);
-                       read_unlock(&mylock);
-       
-       write_lock(&mylock);
-               shareddata = 47;
-       write_unlock(&mylock);
-}
-
-static void b(void *obj)
-{
-       if (read_trylock(&mylock) == 1) {
-                               read_unlock(&mylock);
-       }
-       
-       if (write_trylock(&mylock) == 1) {
-                               write_unlock(&mylock);
-       }
-}
-
-int user_main(int argc, char **argv)
-{
-       __sequential_init();
-       
-       thrd_t t1, t2;
-       atomic_init(&mylock.lock, RW_LOCK_BIAS);
-
-       thrd_create(&t1, (thrd_start_t)&a, NULL);
-       thrd_create(&t2, (thrd_start_t)&b, NULL);
-
-       thrd_join(t1);
-       thrd_join(t2);
-
-       return 0;
-}
-
diff --git a/output/linuxrwlocks/testcase1 b/output/linuxrwlocks/testcase1
deleted file mode 100755 (executable)
index b92d0b9..0000000
Binary files a/output/linuxrwlocks/testcase1 and /dev/null differ
diff --git a/output/linuxrwlocks/testcase1.c b/output/linuxrwlocks/testcase1.c
deleted file mode 100644 (file)
index f47527c..0000000
+++ /dev/null
@@ -1,926 +0,0 @@
-#include <stdio.h>
-#include <threads.h>
-#include <stdatomic.h>
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h"
-
-#include "librace.h"
-
-#define RW_LOCK_BIAS            0x00100000
-#define WRITE_LOCK_CMP          RW_LOCK_BIAS
-
-typedef union {
-       atomic_int lock;
-} rwlock_t;
-
-
-
-
-
-
-
-/* All other user-defined structs */
-static bool writer_lock_acquired;
-static int reader_lock_cnt;
-/* All other user-defined functions */
-/* Definition of interface info struct: Write_Trylock */
-typedef struct Write_Trylock_info {
-int __RET__;
-rwlock_t * rw;
-} Write_Trylock_info;
-/* End of info struct definition: Write_Trylock */
-
-/* ID function of interface: Write_Trylock */
-inline static call_id_t Write_Trylock_id(void *info, thread_id_t __TID__) {
-       Write_Trylock_info* theInfo = (Write_Trylock_info*)info;
-       int __RET__ = theInfo->__RET__;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Write_Trylock */
-
-/* Check action function of interface: Write_Trylock */
-inline static bool Write_Trylock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Write_Trylock_info* theInfo = (Write_Trylock_info*)info;
-       int __RET__ = theInfo->__RET__;
-       rwlock_t * rw = theInfo->rw;
-
-       if ( __RET__ == 1 ) writer_lock_acquired = true ;
-       return true;
-}
-/* End of check action function: Write_Trylock */
-
-/* Definition of interface info struct: Read_Trylock */
-typedef struct Read_Trylock_info {
-int __RET__;
-rwlock_t * rw;
-} Read_Trylock_info;
-/* End of info struct definition: Read_Trylock */
-
-/* ID function of interface: Read_Trylock */
-inline static call_id_t Read_Trylock_id(void *info, thread_id_t __TID__) {
-       Read_Trylock_info* theInfo = (Read_Trylock_info*)info;
-       int __RET__ = theInfo->__RET__;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Read_Trylock */
-
-/* Check action function of interface: Read_Trylock */
-inline static bool Read_Trylock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Read_Trylock_info* theInfo = (Read_Trylock_info*)info;
-       int __RET__ = theInfo->__RET__;
-       rwlock_t * rw = theInfo->rw;
-
-       if ( __RET__ ) reader_lock_cnt ++ ;
-       check_passed = __RET__ == ! writer_lock_acquired || ! __RET__;
-       if (!check_passed)
-               return false;
-       return true;
-}
-/* End of check action function: Read_Trylock */
-
-/* Definition of interface info struct: Write_Lock */
-typedef struct Write_Lock_info {
-rwlock_t * rw;
-} Write_Lock_info;
-/* End of info struct definition: Write_Lock */
-
-/* ID function of interface: Write_Lock */
-inline static call_id_t Write_Lock_id(void *info, thread_id_t __TID__) {
-       Write_Lock_info* theInfo = (Write_Lock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Write_Lock */
-
-/* Check action function of interface: Write_Lock */
-inline static bool Write_Lock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Write_Lock_info* theInfo = (Write_Lock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       check_passed = ! writer_lock_acquired && reader_lock_cnt == 0;
-       if (!check_passed)
-               return false;
-       writer_lock_acquired = true ;
-       return true;
-}
-/* End of check action function: Write_Lock */
-
-/* Definition of interface info struct: Write_Unlock */
-typedef struct Write_Unlock_info {
-rwlock_t * rw;
-} Write_Unlock_info;
-/* End of info struct definition: Write_Unlock */
-
-/* ID function of interface: Write_Unlock */
-inline static call_id_t Write_Unlock_id(void *info, thread_id_t __TID__) {
-       Write_Unlock_info* theInfo = (Write_Unlock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Write_Unlock */
-
-/* Check action function of interface: Write_Unlock */
-inline static bool Write_Unlock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Write_Unlock_info* theInfo = (Write_Unlock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       check_passed = reader_lock_cnt == 0 && writer_lock_acquired;
-       if (!check_passed)
-               return false;
-       writer_lock_acquired = false ;
-       return true;
-}
-/* End of check action function: Write_Unlock */
-
-/* Definition of interface info struct: Read_Unlock */
-typedef struct Read_Unlock_info {
-rwlock_t * rw;
-} Read_Unlock_info;
-/* End of info struct definition: Read_Unlock */
-
-/* ID function of interface: Read_Unlock */
-inline static call_id_t Read_Unlock_id(void *info, thread_id_t __TID__) {
-       Read_Unlock_info* theInfo = (Read_Unlock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Read_Unlock */
-
-/* Check action function of interface: Read_Unlock */
-inline static bool Read_Unlock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Read_Unlock_info* theInfo = (Read_Unlock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       check_passed = reader_lock_cnt > 0 && ! writer_lock_acquired;
-       if (!check_passed)
-               return false;
-       reader_lock_cnt -- ;
-       return true;
-}
-/* End of check action function: Read_Unlock */
-
-/* Definition of interface info struct: Read_Lock */
-typedef struct Read_Lock_info {
-rwlock_t * rw;
-} Read_Lock_info;
-/* End of info struct definition: Read_Lock */
-
-/* ID function of interface: Read_Lock */
-inline static call_id_t Read_Lock_id(void *info, thread_id_t __TID__) {
-       Read_Lock_info* theInfo = (Read_Lock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       call_id_t __ID__ = 0;
-       return __ID__;
-}
-/* End of ID function: Read_Lock */
-
-/* Check action function of interface: Read_Lock */
-inline static bool Read_Lock_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
-       bool check_passed;
-       Read_Lock_info* theInfo = (Read_Lock_info*)info;
-       rwlock_t * rw = theInfo->rw;
-
-       check_passed = ! writer_lock_acquired;
-       if (!check_passed)
-               return false;
-       reader_lock_cnt ++ ;
-       return true;
-}
-/* End of check action function: Read_Lock */
-
-#define INTERFACE_SIZE 6
-static void** func_ptr_table;
-static hb_rule** hb_rule_table;
-static commutativity_rule** commutativity_rule_table;
-inline static bool CommutativityCondition0(void *info1, void *info2) {
-       Read_Lock_info *_info1 = (Read_Lock_info*) info1;
-       Read_Lock_info *_info2 = (Read_Lock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition1(void *info1, void *info2) {
-       Read_Lock_info *_info1 = (Read_Lock_info*) info1;
-       Read_Unlock_info *_info2 = (Read_Unlock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition2(void *info1, void *info2) {
-       Read_Lock_info *_info1 = (Read_Lock_info*) info1;
-       Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition3(void *info1, void *info2) {
-       Read_Lock_info *_info1 = (Read_Lock_info*) info1;
-       Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
-       return ! _info2-> __RET__;
-}
-inline static bool CommutativityCondition4(void *info1, void *info2) {
-       Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
-       Read_Unlock_info *_info2 = (Read_Unlock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition5(void *info1, void *info2) {
-       Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
-       Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition6(void *info1, void *info2) {
-       Read_Unlock_info *_info1 = (Read_Unlock_info*) info1;
-       Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
-       return ! _info2-> __RET__;
-}
-inline static bool CommutativityCondition7(void *info1, void *info2) {
-       Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
-       Read_Trylock_info *_info2 = (Read_Trylock_info*) info2;
-       return true;
-}
-inline static bool CommutativityCondition8(void *info1, void *info2) {
-       Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
-       Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
-       return ! _info1-> __RET__ || ! _info2-> __RET__;
-}
-inline static bool CommutativityCondition9(void *info1, void *info2) {
-       Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
-       Write_Lock_info *_info2 = (Write_Lock_info*) info2;
-       return ! _info1-> __RET__;
-}
-inline static bool CommutativityCondition10(void *info1, void *info2) {
-       Read_Trylock_info *_info1 = (Read_Trylock_info*) info1;
-       Write_Unlock_info *_info2 = (Write_Unlock_info*) info2;
-       return ! _info1-> __RET__;
-}
-inline static bool CommutativityCondition11(void *info1, void *info2) {
-       Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
-       Write_Trylock_info *_info2 = (Write_Trylock_info*) info2;
-       return ! _info1-> __RET__ || ! _info2-> __RET__;
-}
-inline static bool CommutativityCondition12(void *info1, void *info2) {
-       Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
-       Write_Unlock_info *_info2 = (Write_Unlock_info*) info2;
-       return ! _info1-> __RET__;
-}
-inline static bool CommutativityCondition13(void *info1, void *info2) {
-       Write_Trylock_info *_info1 = (Write_Trylock_info*) info1;
-       Write_Lock_info *_info2 = (Write_Lock_info*) info2;
-       return ! _info1-> __RET__;
-}
-
-/* Initialization of sequential varialbes */
-static void __SPEC_INIT__() {
-       writer_lock_acquired = false ;
-       reader_lock_cnt = 0 ;
-}
-
-/* Cleanup routine of sequential variables */
-static bool __SPEC_CLEANUP__() {
-       return true;
-}
-
-/* Define function for sequential code initialization */
-inline static void __sequential_init() {
-       /* Init func_ptr_table */
-       func_ptr_table = (void**) malloc(sizeof(void*) * 6 * 2);
-       func_ptr_table[2 * 3] = (void*) &Write_Trylock_id;
-       func_ptr_table[2 * 3 + 1] = (void*) &Write_Trylock_check_action;
-       func_ptr_table[2 * 2] = (void*) &Read_Trylock_id;
-       func_ptr_table[2 * 2 + 1] = (void*) &Read_Trylock_check_action;
-       func_ptr_table[2 * 1] = (void*) &Write_Lock_id;
-       func_ptr_table[2 * 1 + 1] = (void*) &Write_Lock_check_action;
-       func_ptr_table[2 * 5] = (void*) &Write_Unlock_id;
-       func_ptr_table[2 * 5 + 1] = (void*) &Write_Unlock_check_action;
-       func_ptr_table[2 * 4] = (void*) &Read_Unlock_id;
-       func_ptr_table[2 * 4 + 1] = (void*) &Read_Unlock_check_action;
-       func_ptr_table[2 * 0] = (void*) &Read_Lock_id;
-       func_ptr_table[2 * 0 + 1] = (void*) &Read_Lock_check_action;
-       /* Read_Unlock(true) -> Write_Lock(true) */
-       struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit0->interface_num_before = 4; // Read_Unlock
-       hbConditionInit0->hb_condition_num_before = 0; // 
-       hbConditionInit0->interface_num_after = 1; // Write_Lock
-       hbConditionInit0->hb_condition_num_after = 0; // 
-       /* Read_Unlock(true) -> Write_Trylock(HB_Write_Trylock_Succ) */
-       struct hb_rule *hbConditionInit1 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit1->interface_num_before = 4; // Read_Unlock
-       hbConditionInit1->hb_condition_num_before = 0; // 
-       hbConditionInit1->interface_num_after = 3; // Write_Trylock
-       hbConditionInit1->hb_condition_num_after = 1; // HB_Write_Trylock_Succ
-       /* Write_Unlock(true) -> Write_Lock(true) */
-       struct hb_rule *hbConditionInit2 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit2->interface_num_before = 5; // Write_Unlock
-       hbConditionInit2->hb_condition_num_before = 0; // 
-       hbConditionInit2->interface_num_after = 1; // Write_Lock
-       hbConditionInit2->hb_condition_num_after = 0; // 
-       /* Write_Unlock(true) -> Write_Trylock(HB_Write_Trylock_Succ) */
-       struct hb_rule *hbConditionInit3 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit3->interface_num_before = 5; // Write_Unlock
-       hbConditionInit3->hb_condition_num_before = 0; // 
-       hbConditionInit3->interface_num_after = 3; // Write_Trylock
-       hbConditionInit3->hb_condition_num_after = 1; // HB_Write_Trylock_Succ
-       /* Write_Unlock(true) -> Read_Lock(true) */
-       struct hb_rule *hbConditionInit4 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit4->interface_num_before = 5; // Write_Unlock
-       hbConditionInit4->hb_condition_num_before = 0; // 
-       hbConditionInit4->interface_num_after = 0; // Read_Lock
-       hbConditionInit4->hb_condition_num_after = 0; // 
-       /* Write_Unlock(true) -> Read_Trylock(HB_Read_Trylock_Succ) */
-       struct hb_rule *hbConditionInit5 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
-       hbConditionInit5->interface_num_before = 5; // Write_Unlock
-       hbConditionInit5->hb_condition_num_before = 0; // 
-       hbConditionInit5->interface_num_after = 2; // Read_Trylock
-       hbConditionInit5->hb_condition_num_after = 2; // HB_Read_Trylock_Succ
-       /* Init hb_rule_table */
-       hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 6);
-       #define HB_RULE_TABLE_SIZE 6
-       hb_rule_table[0] = hbConditionInit0;
-       hb_rule_table[1] = hbConditionInit1;
-       hb_rule_table[2] = hbConditionInit2;
-       hb_rule_table[3] = hbConditionInit3;
-       hb_rule_table[4] = hbConditionInit4;
-       hb_rule_table[5] = hbConditionInit5;
-       /* Init commutativity_rule_table */
-       commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 14);
-       commutativity_rule* rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 0;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition0;
-       commutativity_rule_table[0] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 4;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition1;
-       commutativity_rule_table[1] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 2;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition2;
-       commutativity_rule_table[2] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 0;
-       rule->interface_num_after = 3;
-       rule->rule = "! _Method2 . __RET__";
-       rule->condition = CommutativityCondition3;
-       commutativity_rule_table[3] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 4;
-       rule->interface_num_after = 4;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition4;
-       commutativity_rule_table[4] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 4;
-       rule->interface_num_after = 2;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition5;
-       commutativity_rule_table[5] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 4;
-       rule->interface_num_after = 3;
-       rule->rule = "! _Method2 . __RET__";
-       rule->condition = CommutativityCondition6;
-       commutativity_rule_table[6] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 2;
-       rule->interface_num_after = 2;
-       rule->rule = "true";
-       rule->condition = CommutativityCondition7;
-       commutativity_rule_table[7] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 2;
-       rule->interface_num_after = 3;
-       rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
-       rule->condition = CommutativityCondition8;
-       commutativity_rule_table[8] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 2;
-       rule->interface_num_after = 1;
-       rule->rule = "! _Method1 . __RET__";
-       rule->condition = CommutativityCondition9;
-       commutativity_rule_table[9] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 2;
-       rule->interface_num_after = 5;
-       rule->rule = "! _Method1 . __RET__";
-       rule->condition = CommutativityCondition10;
-       commutativity_rule_table[10] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 3;
-       rule->interface_num_after = 3;
-       rule->rule = "! _Method1 . __RET__ || ! _Method2 . __RET__";
-       rule->condition = CommutativityCondition11;
-       commutativity_rule_table[11] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 3;
-       rule->interface_num_after = 5;
-       rule->rule = "! _Method1 . __RET__";
-       rule->condition = CommutativityCondition12;
-       commutativity_rule_table[12] = rule;
-       rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
-       rule->interface_num_before = 3;
-       rule->interface_num_after = 1;
-       rule->rule = "! _Method1 . __RET__";
-       rule->condition = CommutativityCondition13;
-       commutativity_rule_table[13] = rule;
-       /* Pass init info, including function table info & HB rules & Commutativity Rules */
-       struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
-       anno_init->init_func = (void_func_t) __SPEC_INIT__;
-       anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
-       anno_init->func_table = func_ptr_table;
-       anno_init->func_table_size = INTERFACE_SIZE;
-       anno_init->hb_rule_table = hb_rule_table;
-       anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
-       anno_init->commutativity_rule_table = commutativity_rule_table;
-       anno_init->commutativity_rule_table_size = 14;
-       struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       init->type = INIT;
-       init->annotation = anno_init;
-       cdsannotate(SPEC_ANALYSIS, init);
-
-}
-
-/* End of Global construct generation in class */
-
-
-static inline int read_can_lock(rwlock_t *lock)
-{
-       return atomic_load_explicit(&lock->lock, memory_order_relaxed) > 0;
-}
-
-static inline int write_can_lock(rwlock_t *lock)
-{
-       return atomic_load_explicit(&lock->lock, memory_order_relaxed) == RW_LOCK_BIAS;
-}
-
-
-void __wrapper__read_lock(rwlock_t * rw);
-
-void read_lock(rwlock_t * rw) {
-       /* Interface begins */
-       struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
-       interface_begin->interface_num = 0; // Read_Lock
-               interface_begin->interface_name = "Read_Lock";
-       struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_interface_begin->type = INTERFACE_BEGIN;
-       annotation_interface_begin->annotation = interface_begin;
-       cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
-       __wrapper__read_lock(rw);
-       struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
-       hb_condition->interface_num = 0; // Read_Lock
-       hb_condition->hb_condition_num = 0;
-       struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annotation_hb_condition->type = HB_CONDITION;
-       annotation_hb_condition->annotation = hb_condition;
-       cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
-
-       Read_Lock_info* info = (Read_Lock_info*) malloc(sizeof(Read_Lock_info));
-       info->rw = rw;
-       struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
-       interface_end->interface_num = 0; // Read_Lock
-       interface_end->info = info;
-       struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
-       annoation_interface_end->type = INTERFACE_END;
-       annoation_interface_end->annotation = interface_end;
-       cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
-}
-
-void __wrapper__read_lock(rwlock_t * rw)
-{
-       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
-       /* Automatically generated code for commit point define check: Read_Lock_Success_1 */
-
-       if (priorvalue > 0) {
-               struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
-               cp_define_check->label_num = 0;
-               cp_define_check->label_name = "Read_Lock_Success_1";
-               cp_define_check->interface_num