From: Peizhao Ou Date: Tue, 25 Mar 2014 18:52:46 +0000 (-0700) Subject: add Commit point clear construct X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=161d269d279b9c77640e8658d794d503db8ad8a2;p=cdsspec-compiler.git add Commit point clear construct --- diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c index 11e5e99..c9fc8a9 100644 --- a/benchmark/chase-lev-deque-bugfix/deque.c +++ b/benchmark/chase-lev-deque-bugfix/deque.c @@ -30,7 +30,7 @@ int take(Deque *q) { /** @Begin @Commit_point_define_check: t > b - @Label: Take_Point_1 + @Label: Take_Point1 @End */ int x; diff --git a/benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp b/benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp deleted file mode 100644 index a868efd..0000000 Binary files a/benchmark/cliffc-hashtable/.cliffc_hashtable.h.swp and /dev/null differ diff --git a/benchmark/cliffc-hashtable/cliffc_hashtable.h b/benchmark/cliffc-hashtable/cliffc_hashtable.h index 5c32ca0..3cef980 100644 --- a/benchmark/cliffc-hashtable/cliffc_hashtable.h +++ b/benchmark/cliffc-hashtable/cliffc_hashtable.h @@ -151,27 +151,7 @@ class cliffc_hashtable { 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 @@ -222,6 +202,7 @@ friend class CHM; 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; @@ -244,6 +225,7 @@ friend class CHM; 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; @@ -255,15 +237,19 @@ friend class CHM; 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; @@ -272,6 +258,7 @@ friend class CHM; 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; @@ -285,7 +272,7 @@ friend class CHM; 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; @@ -309,6 +296,7 @@ friend class CHM; 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)) @@ -332,7 +320,9 @@ friend class CHM; // 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); } @@ -423,7 +413,8 @@ friend class CHM; /** @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); @@ -443,7 +434,14 @@ friend class CHM; 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)); @@ -453,7 +451,7 @@ friend class CHM; /** @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 @@ -612,6 +610,7 @@ friend class CHM; 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 @@ -674,8 +673,17 @@ friend class CHM; // 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; } /** @@ -686,6 +694,7 @@ friend class CHM; // 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); /** @@ -713,12 +722,11 @@ friend class CHM; @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 @@ -731,7 +739,7 @@ friend class CHM; @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 @@ -745,11 +753,12 @@ friend class CHM; 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, @@ -769,7 +778,14 @@ friend class CHM; 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); @@ -840,6 +856,7 @@ friend class CHM; // 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))) { @@ -862,7 +879,7 @@ friend class CHM; !(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 @@ -871,14 +888,14 @@ friend class CHM; @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 @@ -893,7 +910,7 @@ friend class CHM; # 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 @@ -919,6 +936,7 @@ friend class CHM; // 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 diff --git a/benchmark/cliffc-hashtable/main.cc b/benchmark/cliffc-hashtable/main.cc index 3e52744..7e7a305 100644 --- a/benchmark/cliffc-hashtable/main.cc +++ b/benchmark/cliffc-hashtable/main.cc @@ -55,8 +55,8 @@ IntWrapper *k0, *k1, *k2, *k3, *k4, *k5; 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); /* diff --git a/grammer/spec_compiler.jj b/grammer/spec_compiler.jj index 37749aa..43faebf 100644 --- a/grammer/spec_compiler.jj +++ b/grammer/spec_compiler.jj @@ -66,6 +66,13 @@ @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 @@ -122,6 +129,7 @@ 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.CPClearConstruct; import edu.uci.eecs.specCompiler.specExtraction.ConditionalInterface; import edu.uci.eecs.specCompiler.specExtraction.SequentialDefineSubConstruct; import edu.uci.eecs.specCompiler.specExtraction.InterfaceDefineConstruct; @@ -373,6 +381,8 @@ SKIP : { | +| + | } @@ -885,6 +895,7 @@ Construct ParseSpec() : 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() | @@ -1120,6 +1131,25 @@ CPDefineConstruct Commit_point_define() : } } +CPClearConstruct Commit_point_clear() : +{ + CPClearConstruct res; + String label, condition; + ArrayList content; +} +{ + + { res = null; } + + (content = C_CPP_CODE(null) { condition = stringArray2String(content); }) +