/**
@Begin
@Commit_point_define_check: t > b
- @Label: Take_Point_1
+ @Label: Take_Point1
@End
*/
int x;
return res;
}
}
-
- @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
Put->Get
Put->Put
@End
kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) {
//model_print("resizing...\n");
+ /**** FIXME: miss ****/
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
if (newkvs != NULL)
return newkvs;
if (newsz < oldlen) newsz = oldlen;
// Last check cause the 'new' below is expensive
+ /**** FIXME: miss ****/
newkvs = _newkvs.load(memory_order_acquire);
//model_print("hey1\n");
if (newkvs != NULL) return newkvs;
kvs_data *cur_newkvs;
// Another check after the slow allocation
+ /**** FIXME: miss ****/
if ((cur_newkvs = _newkvs.load(memory_order_acquire)) != NULL)
return cur_newkvs;
// CAS the _newkvs to the allocated table
kvs_data *desired = (kvs_data*) NULL;
kvs_data *expected = (kvs_data*) newkvs;
+ /**** FIXME: miss ****/
+ //model_print("release in resize!\n");
if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
memory_order_relaxed)) {
// Should clean the allocated area
delete newkvs;
+ /**** FIXME: miss ****/
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);
+ /**** FIXME: miss ****/
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
int oldlen = oldkvs->_size;
int min_copy_work = oldlen > 1024 ? 1024 : oldlen;
copyidx = _copy_idx.load(memory_order_relaxed);
while (copyidx < (oldlen << 1) &&
!_copy_idx.compare_exchange_strong(copyidx, copyidx +
- min_copy_work, memory_order_release, memory_order_relaxed))
+ min_copy_work, memory_order_relaxed, memory_order_relaxed))
copyidx = _copy_idx.load(memory_order_relaxed);
if (!(copyidx < (oldlen << 1)))
panic_start = copyidx;
kvs_data* copy_slot_and_check(cliffc_hashtable *topmap, kvs_data
*oldkvs, int idx, void *should_help) {
+ /**** FIXME: miss ****/
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
// We're only here cause the caller saw a Prime
if (copy_slot(topmap, idx, oldkvs, newkvs))
// Promote the new table to the current table
if (copyDone + workdone == oldlen &&
topmap->_kvs.load(memory_order_relaxed) == oldkvs) {
+ /**** FIXME: miss ****/
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
+ /**** CDSChecker error ****/
topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
memory_order_relaxed);
}
/**
@Begin
@Interface: Get
- @Commit_point_set: Get_Success_Point1 | Get_Success_Point2 | Get_Success_Point3
+ //@Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3 | Get_ReadKVS
+ @Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3
@ID: getKeyTag(key)
@Action:
TypeV *_Old_Val = (TypeV*) spec_table_get(map, key);
TypeV* get(TypeK *key) {
slot *key_slot = new slot(false, key);
int fullhash = hash(key_slot);
+ /**** CDSChecker error ****/
kvs_data *kvs = _kvs.load(memory_order_acquire);
+ /**
+ //@Begin
+ @Commit_point_define_check: true
+ @Label: Get_ReadKVS
+ @End
+ */
slot *V = get_impl(this, kvs, key_slot, fullhash);
if (V == NULL) return NULL;
MODEL_ASSERT (!is_prime(V));
/**
@Begin
@Interface: Put
- @Commit_point_set: Write_Success_Point
+ @Commit_point_set: Put_Point
@ID: getKeyTag(key)
@Action:
# Remember this old value at checking point
MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
// Corresponding to the volatile read in get_impl() and putIfMatch in
// Cliff Click's Java implementation
+ /**** CDSChecker error & hb violation ****/
slot *res = (slot*) kvs->_data[idx * 2 + 3].load(memory_order_acquire);
/**
@Begin
// Together with key() preserve the happens-before relationship on newly
// inserted keys
static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
- return kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
+ bool res = kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
desired, memory_order_relaxed, memory_order_relaxed);
+ /**
+ # If it is a successful put instead of a copy or any other internal
+ # operantions, expected != NULL
+ @Begin
+ @Potential_commit_point_define: res
+ @Label: Write_Key_Point
+ @End
+ */
+ return res;
}
/**
// inserted values
static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
*desired) {
+ /**** CDSChecker error & HB violation ****/
bool res = kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
desired, memory_order_acq_rel, memory_order_relaxed);
/**
@Begin
@Commit_point_define: K == NULL
@Potential_commit_point_label: Read_Key_Point
- @Label: Get_Success_Point_1
+ @Label: Get_Point1
@End
*/
slot *V = val(kvs, idx);
-
if (K == NULL) {
//model_print("Key is null\n");
return NULL; // A miss
@Begin
@Commit_point_define: true
@Potential_commit_point_label: Read_Val_Point
- @Label: Get_Success_Point_2
+ @Label: Get_Point2
@End
*/
return (V == TOMBSTONE) ? NULL : V; // Return this value
key_slot == TOMBSTONE) {
// Retry in new table
// Atomic read can be here
+ /**** FIXME: miss ****/
kvs_data *newkvs = chm->_newkvs.load(memory_order_acquire);
/**
@Begin
@Commit_point_define_check: newkvs == NULL
- @Label: Get_Success_Point_3
+ @Label: Get_Point3
@End
*/
return newkvs == NULL ? NULL : get_impl(topmap,
slot *key_slot = new slot(false, key);
slot *value_slot = new slot(false, value);
+ /**** FIXME: miss ****/
kvs_data *kvs = _kvs.load(memory_order_acquire);
+ /**
+ //@Begin
+ @Commit_point_define_check: true
+ @Label: Put_ReadKVS
+ @End
+ */
slot *res = putIfMatch(this, kvs, key_slot, value_slot, old_val);
// Only when copy_slot() call putIfMatch() will it return NULL
MODEL_ASSERT (res != NULL);
// Here it tries to resize cause it doesn't want other threads to stop
// its progress (eagerly try to resize soon)
+ /**** FIXME: miss ****/
newkvs = chm->_newkvs.load(memory_order_acquire);
if (newkvs == NULL &&
((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) {
!(V == NULL && expVal == TOMBSTONE) &&
(expVal == NULL || !valeq(expVal, V))) {
/**
- @Begin
+ //@Begin
@Commit_point_define: expVal == TOMBSTONE
@Potential_commit_point_label: Read_Val_Point
@Label: PutIfAbsent_Fail_Point
@End
*/
/**
- @Begin
+ //@Begin
@Commit_point_define: expVal != NULL && val_slot == TOMBSTONE
@Potential_commit_point_label: Read_Val_Point
@Label: RemoveIfMatch_Fail_Point
@End
*/
/**
- @Begin
+ //@Begin
@Commit_point_define: expVal != NULL && !valeq(expVal, V)
@Potential_commit_point_label: Read_Val_Point
@Label: ReplaceIfMatch_Fail_Point
# The only point where a successful put happens
@Commit_point_define: true
@Potential_commit_point_label: Write_Val_Point
- @Label: Write_Success_Point
+ @Label: Put_Point
@End
*/
if (expVal != NULL) { // Not called by a table-copy
// Help along an existing table-resize. This is a fast cut-out wrapper.
kvs_data* help_copy(kvs_data *helper) {
+ /**** FIXME: miss ****/
kvs_data *topkvs = _kvs.load(memory_order_acquire);
CHM *topchm = get_chm(topkvs);
// No cpy in progress
IntWrapper *v0, *v1, *v2, *v3, *v4, *v5;
void threadA(void *arg) {
- table->put(k3, v3);
table->put(k1, v4);
+ table->put(k3, v3);
//table->put(k2, v2);
//table->put(k3, v3);
/*
@Label: ...
@End
+ // Commit point clear (just as a normal commit point, but it is used to
+ // clear all commit points)
+ @Begin
+ @Commit_point_clear: ...
+ @Label: ...
+ @End
+
e) Entry point construct
@Begin
@Entry_point
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.CPClearConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct;
import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct;
<COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
|
<COMMIT_POINT_DEFINE: "@Commit_point_define:">
+|
+ <COMMIT_POINT_CLEAR: "@Commit_point_clear:">
|
<POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
}
LOOKAHEAD(2) res = Potential_commit_point_define() |
LOOKAHEAD(2) res = Commit_point_define() |
LOOKAHEAD(2) res = Commit_point_define_check() |
+ LOOKAHEAD(2) res = Commit_point_clear() |
LOOKAHEAD(2) res = Entry_point() |
LOOKAHEAD(2) res = Class_begin() |
LOOKAHEAD(2) res = Class_end() |
}
}
+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() :
{
import java.util.HashSet;
import java.util.Iterator;
+import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ClassEndConstruct;
}
codeAdditions.get(construct.file).add(addition);
}
+
+ private void CPClear2Code(CPClearConstruct construct) {
+ int lineNum = construct.beginLineNum;
+ ArrayList<String> newCode = CodeVariables.generateCPClear(
+ _semantics, construct);
+
+ CodeAddition addition = new CodeAddition(lineNum, newCode);
+ if (!codeAdditions.containsKey(construct.file)) {
+ codeAdditions.put(construct.file, new ArrayList<CodeAddition>());
+ }
+ codeAdditions.get(construct.file).add(addition);
+ }
+
/**
* private void ClassEnd2Code(ClassEndConstruct construct) { int lineNum =
CPDefine2Code((CPDefineConstruct) construct);
} else if (construct instanceof CPDefineCheckConstruct) {
CPDefineCheck2Code((CPDefineCheckConstruct) construct);
+ } else if (construct instanceof CPClearConstruct) {
+ CPClear2Code((CPClearConstruct) construct);
} else if (construct instanceof EntryPointConstruct) {
EntryPoint2Code((EntryPointConstruct) construct);
}
import edu.uci.eecs.specCompiler.grammerParser.utilParser.UtilParser;
import edu.uci.eecs.specCompiler.grammerParser.utilParser.ParseException;
+import edu.uci.eecs.specCompiler.specExtraction.CPClearConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineCheckConstruct;
import edu.uci.eecs.specCompiler.specExtraction.CPDefineConstruct;
import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface;
public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potential_cp_define";
public static final String ANNO_CP_DEFINE = "anno_cp_define";
public static final String ANNO_CP_DEFINE_CHECK = "anno_cp_define_check";
+ public static final String ANNO_CP_CLEAR = "anno_cp_clear";
public static final String ANNO_HB_CONDITION = "anno_hb_condition";
// Specification variables
newCode.add("\t" + "}");
return newCode;
}
-
+
+ public static String getCPInterfaceNum(SemanticsChecker semantics, String commitPointLabel) {
+ HashMap<String, InterfaceConstruct> cp2Interface = semantics.CPLabel2InterfaceConstruct;
+ InterfaceConstruct iConstruct = cp2Interface.get(commitPointLabel);
+ String interfaceName = iConstruct.name;
+ String interfaceNum = Integer.toString(semantics.interface2Num
+ .get(interfaceName));
+ return interfaceNum;
+ }
+
+ /**
+ * <p>
+ * Commit point define check should be unique to each interface, meaning that they
+ * are not shared between different interfaces
+ * </p>
+ *
+ * @param semantics
+ * @param construct
+ * @return
+ */
public static ArrayList<String> generateCPDefineCheck(
SemanticsChecker semantics, CPDefineCheckConstruct construct) {
ArrayList<String> newCode = new ArrayList<String>();
+ construct.label));
newCode.add("");
// Add annotation
+
newCode.add("\t" + "if (" + construct.condition + ") {");
String structName = "cp_define_check", anno = "annotation_cp_define_check";
newCode.add("\t\t"
+ STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_DEFINE_CHECK, structName));
String labelNum = Integer.toString(semantics.commitPointLabel2Num
.get(construct.label));
+ String interfaceNum = getCPInterfaceNum(semantics, construct.label);
+ newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum));
+ newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
+ newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
+ newCode.add("\t\t"
+ + ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
+ newCode.add("\t\t" + ASSIGN_TO_PTR(anno, "annotation", structName));
+ newCode.add("\t\t" + ANNOTATE(semantics, anno));
+ newCode.add("\t" + "}");
+ return newCode;
+ }
+
+ /**
+ * <p>
+ * Commit point define check should be unique to each interface, meaning that they
+ * are not shared between different interfaces
+ * </p>
+ *
+ * @param semantics
+ * @param construct
+ * @return
+ */
+ public static ArrayList<String> generateCPClear(
+ SemanticsChecker semantics, CPClearConstruct construct) {
+ ArrayList<String> newCode = new ArrayList<String>();
+ // Add atomic return variable if the predicate accesses to it
+ if (construct.condition.indexOf(MACRO_ATOMIC_RETURN) != -1) {
+ addAtomicReturn(semantics, construct);
+ }
+ // Generate redundant header files
+ newCode.add("\t"
+ + COMMENT("Automatically generated code for commit point clear: "
+ + construct.label));
+ newCode.add("");
+ // Add annotation
+
+ newCode.add("\t" + "if (" + construct.condition + ") {");
+ String structName = "cp_clear", anno = "annotation_cp_clear";
+ newCode.add("\t\t"
+ + STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_CLEAR, structName));
+ String labelNum = Integer.toString(semantics.commitPointLabel2Num
+ .get(construct.label));
+ String interfaceNum = getCPInterfaceNum(semantics, construct.label);
newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "label_num", labelNum));
+ newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
newCode.add("\t\t"
+ ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE_CHECK));
return newCode;
}
+ /**
+ * <p>
+ * Commit point define should be unique to each interface, meaning that they
+ * are not shared between different interfaces
+ * </p>
+ *
+ * @param semantics
+ * @param construct
+ * @return
+ */
public static ArrayList<String> generateCPDefine(
SemanticsChecker semantics, CPDefineConstruct construct) {
ArrayList<String> newCode = new ArrayList<String>();
+ STRUCT_NEW_DECLARE_DEFINE(ANNO_CP_DEFINE, structName));
String labelNum = Integer.toString(semantics.commitPointLabel2Num
.get(construct.label));
+ String interfaceNum = getCPInterfaceNum(semantics, construct.label);
String potentialLabelNum = Integer
.toString(semantics.commitPointLabel2Num
.get(construct.potentialCPLabel));
newCode.add("\t\t"
+ ASSIGN_TO_PTR(structName, "potential_cp_label_num",
potentialLabelNum));
+ newCode.add("\t\t" + ASSIGN_TO_PTR(structName, "interface_num", interfaceNum));
newCode.add("\t\t" + STRUCT_NEW_DECLARE_DEFINE(SPEC_ANNOTATION, anno));
newCode.add("\t\t"
+ ASSIGN_TO_PTR(anno, "type", SPEC_ANNO_TYPE_CP_DEFINE));
public final HashMap<String, PotentialCPDefineConstruct> potentialCPLabel2Construct;
public final HashMap<String, InterfaceConstruct> interfaceName2Construct;
public final HashMap<String, InterfaceDefineConstruct> interfaceName2DefineConstruct;
- public final HashMap<String, ArrayList<InterfaceConstruct>> CPLabel2InterfaceConstruct;
+ public final HashMap<String, InterfaceConstruct> CPLabel2InterfaceConstruct;
public final HashMap<String, Integer> interface2Num;
public final HashMap<Integer, String> num2Interface;
this.potentialCPLabel2Construct = new HashMap<String, PotentialCPDefineConstruct>();
this.interfaceName2Construct = new HashMap<String, InterfaceConstruct>();
this.interfaceName2DefineConstruct = new HashMap<String, InterfaceDefineConstruct>();
- this.CPLabel2InterfaceConstruct = new HashMap<String, ArrayList<InterfaceConstruct>>();
+ this.CPLabel2InterfaceConstruct = new HashMap<String, InterfaceConstruct>();
this.entryPointConstructs = new ArrayList<EntryPointConstruct>();
this.classBeginConstruct = null;
this.classEndConstruct = null;
for (int j = 0; j < iConstruct.commitPointSet.size(); j++) {
String label = iConstruct.commitPointSet.get(j);
+// if (!CPLabel2InterfaceConstruct.containsKey(label)) {
+// CPLabel2InterfaceConstruct.put(label,
+// new ArrayList<InterfaceConstruct>());
+// }
+// CPLabel2InterfaceConstruct.get(label).add(iConstruct);
if (!CPLabel2InterfaceConstruct.containsKey(label)) {
- CPLabel2InterfaceConstruct.put(label,
- new ArrayList<InterfaceConstruct>());
+ CPLabel2InterfaceConstruct.put(label, iConstruct);
+ } else {
+ throw new SemanticsCheckerException(
+ "Commit point has multiple interfaces!");
}
- CPLabel2InterfaceConstruct.get(label).add(iConstruct);
+
}
}
}
--- /dev/null
+package edu.uci.eecs.specCompiler.specExtraction;
+
+import java.io.File;
+
+public class CPClearConstruct extends Construct {
+ public final String label;
+ public final String condition;
+
+ public CPClearConstruct(File file, int beginLineNum, String label,
+ String condition) {
+ super(file, beginLineNum);
+ this.label = label;
+ this.condition = condition;
+ }
+
+ public String toString() {
+ StringBuffer res = new StringBuffer();
+ res.append("@Commit_point_define_check:\n");
+ res.append("Label: " + label + "\n");
+ res.append("Condition: " + condition + "\n");
+ return res.toString();
+ }
+}
public String toString() {
StringBuffer res = new StringBuffer();
- res.append("@Commit_point_define_check:\n");
+ res.append("@Commit_point_clear:\n");
res.append("Label: " + label + "\n");
res.append("Condition: " + condition + "\n");
return res.toString();
projects / cdsspec-compiler.git / commitdiff