add treiber stack
authorPeizhao Ou <peizhaoo@uci.edu>
Wed, 3 Sep 2014 22:17:59 +0000 (15:17 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Wed, 3 Sep 2014 22:17:59 +0000 (15:17 -0700)
.gitignore
Makefile
cliffc-hashtable/Makefile
cliffc-hashtable/cliffc_hashtable.h
cliffc-hashtable/main.cc
treiber-stack/Makefile [new file with mode: 0644]
treiber-stack/main.c [new file with mode: 0644]
treiber-stack/my_stack.c [new file with mode: 0644]
treiber-stack/my_stack.h [new file with mode: 0644]

index 870563c..9a81599 100644 (file)
@@ -23,3 +23,4 @@ mpmc-queue/mpmc-1r2w-noinit
 mpmc-queue/mpmc-queue-noinit
 mpmc-queue/mpmc-2r1w
 mpmc-queue/mpmc-queue-rdwr
+treiber-stack/main
index 5ae090b..662ebce 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 DIRS := barrier mcs-lock mpmc-queue spsc-queue spsc-bugfix linuxrwlocks \
        dekker-fences chase-lev-deque ms-queue chase-lev-deque-bugfix seqlock \
-       cliffc-hashtable
+       cliffc-hashtable treiber-stack
 
 .PHONY: $(DIRS)
 
index f1feb46..f1e5227 100644 (file)
@@ -1,14 +1,11 @@
 include ../benchmarks.mk
 
-TESTS := table table-normal
+TESTS := table 
 
 all: $(TESTS)
 
 table: main.cc
        $(CXX) -o $@ $^ $(SPEC_OBJ) $(CXXFLAGS) -std=c++0x $(LDFLAGS)
 
-table-normal: main.cc
-       $(CXX) -o $@ $^ -std=c++0x -DNORMAL
-
 clean:
        rm -f *.o *.d $(TESTS)
index 0e7cacd..c5c251c 100644 (file)
@@ -1,10 +1,17 @@
-#ifndef _CLIFFC_HASHTABLE_H
-#define _CLIFFC_HASHTABLE_H
+#ifndef CLIFFC_HASHTABLE_H
+#define CLIFFC_HASHTABLE_H
 
 #include <iostream>
 #include <atomic>
-#include <memory>
+#include "stdio.h" 
+//#include <common.h>
+#ifdef STANDALONE
 #include <assert.h>
+#define MODEL_ASSERT assert 
+#else
+#include <model-assert.h>
+#endif
+#include <stdlib.h>
 
 using namespace std;
 
@@ -15,7 +22,7 @@ using namespace std;
        the static fields.
 */
 
-template<typename TypeK, typename TypeV, class Hash, class KeyEqualsTo, class ValEqualsTo>
+template<typename TypeK, typename TypeV>
 class cliffc_hashtable;
 
 /**
@@ -29,7 +36,7 @@ struct kvs_data {
        
        kvs_data(int sz) {
                _size = sz;
-               int real_size = sizeof(atomic<void*>) * 2 + 2;
+               int real_size = sz * 2 + 2;
                _data = new atomic<void*>[real_size];
                // The control block should be initialized in resize()
                // Init the hash record array
@@ -38,14 +45,11 @@ struct kvs_data {
                for (i = 0; i < _size; i++) {
                        hashes[i] = 0;
                }
-               
-               // Initialize the array
-               _data[0].store(NULL, memory_order_relaxed);
-               _data[1].store(hashes, memory_order_relaxed);
                // Init the data to Null slot
                for (i = 2; i < real_size; i++) {
                        _data[i].store(NULL, memory_order_relaxed);
                }
+               _data[1].store(hashes, memory_order_relaxed);
        }
 
        ~kvs_data() {
@@ -63,14 +67,21 @@ struct slot {
                _prime = prime;
                _ptr = ptr;
        }
-
 };
 
 
 /**
+       TypeK must have defined function "int hashCode()" which return the hash
+       code for the its object, and "int equals(TypeK anotherKey)" which is
+       used to judge equality.
        TypeK and TypeV should define their own copy constructor.
 */
-template<typename TypeK, typename TypeV, class Hash, class KeyEqualsTo, class ValEqualsTo>
+/**
+       @Begin
+       @Class_begin
+       @End
+*/
+template<typename TypeK, typename TypeV>
 class cliffc_hashtable {
        /**
                # The synchronization we have for the hashtable gives us the property of
@@ -78,50 +89,66 @@ class cliffc_hashtable {
                # correctness. The key thing is to identify all the commit point.
        
                @Begin
+               @Options:
+                       LANG = CPP;
+                       CLASS = cliffc_hashtable;
                @Global_define:
-
-                       spec_hashtable<TypeK, TypeV*> __map;
-                       spec_hashtable<TypeK, Tag> __id_map;
-                       Tag __tag;
-
-                       static bool _val_equals(TypeV *ptr1, TypeV *ptr2) {
-                               // ...
+                       @DeclareVar:
+                       spec_table *map;
+                       spec_table *id_map;
+                       id_tag_t *tag;
+                       @InitVar:
+                               map = new_spec_table_default(equals_key);
+                               id_map = new_spec_table_default(equals_id);
+                               tag = new_id_tag();
+
+                       @DefineFunc:
+                       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);
                        }
                        
+                       @DefineFunc:
+                       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);
+                       }
+
+                       @DefineFunc:
+                       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;
+                       }
+
+                       @DefineFunc:
                        # 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;
+                       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 {
-                                       return __id_map.get(key);
+                                       call_id_t res = (call_id_t) spec_table_get(id_map, key);
+                                       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
        */
 
@@ -149,6 +176,7 @@ friend class CHM;
        
                public:
                CHM(int size) {
+                       _newkvs.store(NULL, memory_order_relaxed);
                        _size.store(size, memory_order_relaxed);
                        _slots.store(0, memory_order_relaxed);
        
@@ -168,6 +196,8 @@ 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;
@@ -190,24 +220,31 @@ 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;
        
                        newkvs = new kvs_data(newsz);
                        void *chm = (void*) new CHM(sz);
+                       //model_print("hey2\n");
                        newkvs->_data[0].store(chm, memory_order_relaxed);
        
                        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_release)) {
+                                       memory_order_relaxed)) {
                                // Should clean the allocated area
                                delete newkvs;
+                               /**** FIXME: miss ****/
                                newkvs = _newkvs.load(memory_order_acquire);
                        }
                        return newkvs;
@@ -215,7 +252,8 @@ friend class CHM;
        
                void help_copy_impl(cliffc_hashtable *topmap, kvs_data *oldkvs,
                        bool copy_all) {
-                       assert (get_chm(oldkvs) == this);
+                       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;
@@ -223,13 +261,13 @@ friend class CHM;
                        // Just follow Cliff Click's code here
                        int panic_start = -1;
                        int copyidx;
-                       while (_copy_done.load(memory_order_acquire) < oldlen) {
-                               copyidx = _copy_idx.load(memory_order_acquire);
+                       while (_copy_done.load(memory_order_relaxed) < oldlen) {
+                               copyidx = _copy_idx.load(memory_order_relaxed);
                                if (panic_start == -1) { // No painc
-                                       copyidx = _copy_idx.load(memory_order_acquire);
+                                       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_release))
+                                                       min_copy_work, memory_order_relaxed, memory_order_relaxed))
                                                copyidx = _copy_idx.load(memory_order_relaxed);
                                        if (!(copyidx < (oldlen << 1)))
                                                panic_start = copyidx;
@@ -253,10 +291,10 @@ 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.load(memory_order_relaxed)))
+                       if (copy_slot(topmap, idx, oldkvs, newkvs))
                                copy_check_and_promote(topmap, oldkvs, 1); // Record the slot copied
                        return (should_help == NULL) ? newkvs : topmap->help_copy(newkvs);
                }
@@ -276,10 +314,13 @@ friend class CHM;
        
                        // Promote the new table to the current table
                        if (copyDone + workdone == oldlen &&
-                               topmap->_kvs.load(memory_order_acquire) == oldkvs)
-                               topmap->_kvs.compare_exchange_strong(oldkvs,
-                                       _newkvs.load(memory_order_relaxed), memory_order_release,
-                                       memory_order_release);
+                               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);
+                       }
                }
        
                bool copy_slot(cliffc_hashtable *topmap, int idx, kvs_data *oldkvs,
@@ -320,7 +361,7 @@ friend class CHM;
        
 
        private:
-       static const int Default_Init_Size = 8; // Intial table size
+       static const int Default_Init_Size = 4; // Intial table size
 
        static slot* const MATCH_ANY;
        static slot* const NO_MATCH_OLD;
@@ -330,10 +371,6 @@ friend class CHM;
 
        static const int REPROBE_LIMIT = 10; // Forces a table-resize
 
-       static Hash hashFunc;
-       static KeyEqualsTo keyEqualsTo;
-       static ValEqualsTo valEqualsTo;
-
        atomic<kvs_data*> _kvs;
 
        public:
@@ -341,163 +378,199 @@ friend class CHM;
                // Should initialize the CHM for the construction of the table
                // For other CHM in kvs_data, they should be initialzed in resize()
                // because the size is determined dynamically
+               /**
+                       @Begin
+                       @Entry_point
+                       @End
+               */
                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_release);
+               _kvs.store(kvs, memory_order_relaxed);
        }
 
        cliffc_hashtable(int init_size) {
                // Should initialize the CHM for the construction of the table
                // For other CHM in kvs_data, they should be initialzed in resize()
                // because the size is determined dynamically
+
+               /**
+                       @Begin
+                       @Entry_point
+                       @End
+               */
                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_release);
+               _kvs.store(kvs, memory_order_relaxed);
        }
 
        /**
                @Begin
                @Interface: Get
-               @Commit_point_set: Read_Val_Point1 | Read_Val_Point2 | Read_Val_Point3
-               @ID: _getKeyTag(key)
+               //@Commit_point_set: Get_Point1 | Get_Point2 | Get_ReadKVS | Get_ReadNewKVS | Get_Clear
+               @Commit_point_set: Get_Point1 | Get_Point2 | Get_Clear
+               //@Commit_point_set: Get_Point1 | Get_Point2 | Get_Point3
+               @ID: getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
+                       TypeV *_Old_Val = (TypeV*) spec_table_get(map, key);
+                       //bool passed = equals_val(_Old_Val, __RET__);
+                       bool passed = false;
+                       if (!passed) {
+                               int old = _Old_Val == NULL ? 0 : _Old_Val->_val;
+                               int ret = __RET__ == NULL ? 0 : __RET__->_val;
+                               //model_print("Get: key: %d, _Old_Val: %d, RET: %d\n",
+                               //key->_val, old, ret);
+                       }
                @Post_check:
-                       _equals_val(_Old_Val, __RET__)
+                       //__RET__ == NULL ? true : equals_val(_Old_Val, __RET__)
+                       equals_val(_Old_Val, __RET__)
                @End
        */
-       TypeV* get(TypeK& key) {
-               void *key_ptr = (void*) new TypeK(key);
-               slot *key_slot = new slot(false, key_ptr);
+       TypeV* get(TypeK *key) {
+               slot *key_slot = new slot(false, key);
                int fullhash = hash(key_slot);
-               slot *V = get_impl(this, _kvs.load(memory_order_relaxed), key_slot, fullhash);
+               /**** 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;
-               assert (!is_prime(V));
+               MODEL_ASSERT (!is_prime(V));
                return (TypeV*) V->_ptr;
        }
 
        /**
                @Begin
                @Interface: Put
-               @Commit_point_set: Write_Val_Point
-               @ID: _getKeyTag(key)
+               //@Commit_point_set: Put_Point | Put_ReadKVS | Put_ReadNewKVS | Put_WriteKey
+               @Commit_point_set: Put_Point | Put_WriteKey
+               @ID: getKeyTag(key)
                @Action:
                        # Remember this old value at checking point
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
-                       @Code: __map.put(key, &val);
+                       TypeV *_Old_Val = (TypeV*) spec_table_get(map, key);
+                       spec_table_put(map, key, val);
+                       //bool passed = equals_val(__RET__, _Old_Val);
+                       bool passed = false;
+                       if (!passed) {
+                               int old = _Old_Val == NULL ? 0 : _Old_Val->_val;
+                               int ret = __RET__ == NULL ? 0 : __RET__->_val;
+                               //model_print("Put: key: %d, val: %d, _Old_Val: %d, RET: %d\n",
+                               //      key->_val, val->_val, old, ret);
+                       }
                @Post_check:
-                       _equals_val(__RET__, _Old_Val)
+                       equals_val(__RET__, _Old_Val)
                @End
        */
-       TypeV* put(TypeK& key, TypeV& val) {
+       TypeV* put(TypeK *key, TypeV *val) {
                return putIfMatch(key, val, NO_MATCH_OLD);
        }
 
        /**
-               @Begin
+//             @Begin
                @Interface: PutIfAbsent
                @Commit_point_set:
-                       Write_Val_Point | PutIfAbsent_Fail_Point
-               @Condition: __map.get(key) == NULL
+                       Write_Success_Point | PutIfAbsent_Fail_Point
+               @Condition: !spec_table_contains(map, key)
                @HB_condition:
                        COND_PutIfAbsentSucc :: __RET__ == NULL
-               @ID: _getKeyTag(key)
+               @ID: getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
-                       @Code:
-                       if (COND_SAT)
-                               __map.put(key, &value);
+                       void *_Old_Val = spec_table_get(map, key);
+                       if (__COND_SAT__)
+                               spec_table_put(map, key, value);
                @Post_check:
-                       COND_SAT ? __RET__ == NULL : _equals_val(_Old_Val, __RET__) 
+                       __COND_SAT__ ? __RET__ == NULL : equals_val(_Old_Val, __RET__) 
                @End
        */
-       TypeV* putIfAbsent(TypeK& key, TypeV& value) {
+       TypeV* putIfAbsent(TypeK *key, TypeV *value) {
                return putIfMatch(key, val, TOMBSTONE);
        }
 
        /**
-               @Begin
+//             @Begin
                @Interface: RemoveAny
-               @Commit_point_set: Write_Val_Point
-               @ID: _getKeyTag(key)
+               @Commit_point_set: Write_Success_Point
+               @ID: getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
-                       @Code: __map.put(key, NULL);
+                       void *_Old_Val = spec_table_get(map, key);
+                       spec_table_put(map, key, NULL);
                @Post_check:
-                       _equals_val(__RET__, _Old_Val)
+                       equals_val(__RET__, _Old_Val)
                @End
        */
-       TypeV* remove(TypeKkey) {
+       TypeV* remove(TypeK *key) {
                return putIfMatch(key, TOMBSTONE, NO_MATCH_OLD);
        }
 
        /**
-               @Begin
+//             @Begin
                @Interface: RemoveIfMatch
                @Commit_point_set:
-                       Write_Val_Point | RemoveIfMatch_Fail_Point
+                       Write_Success_Point | RemoveIfMatch_Fail_Point
                @Condition:
-                       _equals_val(__map.get(key), &val)
+                       equals_val(spec_table_get(map, key), val)
                @HB_condition:
                        COND_RemoveIfMatchSucc :: __RET__ == true
-               @ID: _getKeyTag(key)
+               @ID: getKeyTag(key)
                @Action:
-                       @Code:
-                       if (COND_SAT)
-                               __map.put(key, NULL);
+                       if (__COND_SAT__)
+                               spec_table_put(map, key, NULL);
                @Post_check:
-                       COND_SAT ? __RET__ : !__RET__
+                       __COND_SAT__ ? __RET__ : !__RET__
                @End
        */
-       bool remove(TypeK& key, TypeV& val) {
+       bool remove(TypeK *key, TypeV *val) {
                slot *val_slot = val == NULL ? NULL : new slot(false, val);
                return putIfMatch(key, TOMBSTONE, val) == val;
 
        }
 
        /**
-               @Begin
+//             @Begin
                @Interface: ReplaceAny
                @Commit_point_set:
-                       Write_Val_Point
-               @ID: _getKeyTag(key)
+                       Write_Success_Point
+               @ID: getKeyTag(key)
                @Action:
-                       @DefineVar: TypeV *_Old_Val = __map.get(key)
+                       void *_Old_Val = spec_table_get(map, key);
                @Post_check:
-                       _equals_val(__RET__, _Old_Val)
+                       equals_val(__RET__, _Old_Val)
                @End
        */
-       TypeV* replace(TypeK& key, TypeV& val) {
+       TypeV* replace(TypeK *key, TypeV *val) {
                return putIfMatch(key, val, MATCH_ANY);
        }
 
        /**
-               @Begin
+//             @Begin
                @Interface: ReplaceIfMatch
                @Commit_point_set:
-                       Write_Val_Point | ReplaceIfMatch_Fail_Point
+                       Write_Success_Point | ReplaceIfMatch_Fail_Point
                @Condition:
-                       _equals_val(__map.get(key), &oldval)
+                       equals_val(spec_table_get(map, key), oldval)
                @HB_condition:
                        COND_ReplaceIfMatchSucc :: __RET__ == true
-               @ID: _getKeyTag(key)
+               @ID: getKeyTag(key)
                @Action:
-                       @Code:
-                       if (COND_SAT)
-                               __map.put(key, &newval);
+                       if (__COND_SAT__)
+                               spec_table_put(map, key, newval);
                @Post_check:
-                       COND_SAT ? __RET__ : !__RET__
+                       __COND_SAT__ ? __RET__ : !__RET__
                @End
        */
-       bool replace(TypeK& key, TypeV& oldval, TypeV& newval) {
+       bool replace(TypeK *key, TypeV *oldval, TypeV *newval) {
                return putIfMatch(key, newval, oldval) == oldval;
        }
 
        private:
        static CHM* get_chm(kvs_data* kvs) {
-               return (CHM*) kvs->_data[0].load(memory_order_relaxed);
+               CHM *res = (CHM*) kvs->_data[0].load(memory_order_relaxed);
+               return res;
        }
 
        static int* get_hashes(kvs_data *kvs) {
@@ -506,10 +579,19 @@ friend class CHM;
        
        // Preserve happens-before semantics on newly inserted keys
        static inline slot* key(kvs_data *kvs, int idx) {
-               assert (idx >= 0 && idx < kvs->_size);
+               MODEL_ASSERT (idx >= 0 && idx < kvs->_size);
                // Corresponding to the volatile read in get_impl() and putIfMatch in
                // Cliff Click's Java implementation
-               return (slot*) kvs->_data[idx * 2 + 2].load(memory_order_acquire);
+               slot *res = (slot*) kvs->_data[idx * 2 + 2].load(memory_order_relaxed);
+               /**
+                       @Begin
+                       # This is a complicated potential commit point since many many functions are
+                       # calling val().
+                       @Potential_commit_point_define: true
+                       @Label: Read_Key_Point
+                       @End
+               */
+               return res;
        }
 
        /**
@@ -522,9 +604,10 @@ friend class CHM;
        */
        // Preserve happens-before semantics on newly inserted values
        static inline slot* val(kvs_data *kvs, int idx) {
-               assert (idx >= 0 && idx < kvs->_size);
+               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
@@ -540,9 +623,9 @@ friend class CHM;
        }
 
        static int hash(slot *key_slot) {
-               assert(key_slot != NULL && key_slot->_ptr != NULL);
+               MODEL_ASSERT(key_slot != NULL && key_slot->_ptr != NULL);
                TypeK* key = (TypeK*) key_slot->_ptr;
-               int h = hashFunc(*key);
+               int h = key->hashCode();
                // Spread bits according to Cliff Click's code
                h += (h << 15) ^ 0xffffcd7d;
                h ^= (h >> 10);
@@ -568,27 +651,36 @@ friend class CHM;
        static bool keyeq(slot *K, slot *key_slot, int *hashes, int hash,
                int fullhash) {
                // Caller should've checked this.
-               assert (K != NULL);
+               MODEL_ASSERT (K != NULL);
                TypeK* key_ptr = (TypeK*) key_slot->_ptr;
                return
                        K == key_slot ||
                                ((hashes[hash] == 0 || hashes[hash] == fullhash) &&
                                K != TOMBSTONE &&
-                               keyEqualsTo(*key_ptr, *((TypeK*) K->_ptr)));
+                               key_ptr->equals(K->_ptr));
        }
 
        static bool valeq(slot *val_slot1, slot *val_slot2) {
-               assert (val_slot1 != NULL);
+               MODEL_ASSERT (val_slot1 != NULL);
                TypeK* ptr1 = (TypeV*) val_slot1->_ptr;
                if (val_slot2 == NULL || ptr1 == NULL) return false;
-               return valEqualsTo(*ptr1, *((TypeV*) val_slot2->_ptr));
+               return ptr1->equals(val_slot2->_ptr);
        }
        
        // 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,
-                       desired, memory_order_release, memory_order_release);
+               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;
        }
 
        /**
@@ -599,13 +691,14 @@ 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_release, memory_order_release);
+                       desired, memory_order_acq_rel, 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: __ATOMIC_RET__ == true
+                       @Potential_commit_point_define: res
                        @Label: Write_Val_Point
                        @End
                */
@@ -622,25 +715,35 @@ friend class CHM;
                int reprobe_cnt = 0;
                while (true) {
                        slot *K = key(kvs, idx);
-                       slot *V = val(kvs, idx);
                        /**
                                @Begin
-                               @Commit_point_define: V == NULL
-                               @Potential_commit_point_label: Read_Val_Point
-                               @Label: Get_Success_Point_1
+                               @Commit_point_define: K == NULL
+                               @Potential_commit_point_label: Read_Key_Point
+                               @Label: Get_Point1
                                @End
                        */
-
-                       if (V == NULL) return NULL; // A miss
+                       slot *V = val(kvs, idx);
+                       
+                       if (K == NULL) {
+                               //model_print("Key is null\n");
+                               return NULL; // A miss
+                       }
                        
                        if (keyeq(K, key_slot, hashes, idx, fullhash)) {
                                // Key hit! Check if table-resize in progress
                                if (!is_prime(V)) {
+                                       /**
+                                               @Begin
+                                               @Commit_point_clear: true
+                                               @Label: Get_Clear
+                                               @End
+                                       */
+
                                        /**
                                                @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
@@ -653,12 +756,13 @@ friend class CHM;
                        if (++reprobe_cnt >= REPROBE_LIMIT ||
                                key_slot == TOMBSTONE) {
                                // Retry in new table
-                               // Atomic read (acquire) can be here 
+                               // 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
+                                       //@Begin
+                                       @Commit_point_define_check: true
+                                       @Label: Get_ReadNewKVS
                                        @End
                                */
                                return newkvs == NULL ? NULL : get_impl(topmap,
@@ -670,21 +774,26 @@ friend class CHM;
        }
 
        // A wrapper of the essential function putIfMatch()
-       TypeV* putIfMatch(TypeK& key, TypeV& value, slot *old_val) {
+       TypeV* putIfMatch(TypeK *key, TypeV *value, slot *old_val) {
                // TODO: Should throw an exception rather return NULL
                if (old_val == NULL) {
                        return NULL;
                }
-               void *key_ptr = (void*) new TypeK(key);
-               slot *key_slot = new slot(false, key_ptr);
+               slot *key_slot = new slot(false, key);
 
-               void *val_ptr = (void*) new TypeV(value);
-               slot *value_slot = new slot(false, val_ptr);
-               slot *res = putIfMatch(this, _kvs.load(memory_order_relaxed), key_slot,
-                       value_slot, old_val);
+               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
-               assert (res != NULL); 
-               assert (!is_prime(res));
+               MODEL_ASSERT (res != NULL); 
+               MODEL_ASSERT (!is_prime(res));
                return res == TOMBSTONE ? NULL : (TypeV*) res->_ptr;
        }
 
@@ -697,9 +806,9 @@ friend class CHM;
        */
        static slot* putIfMatch(cliffc_hashtable *topmap, kvs_data *kvs, slot
                *key_slot, slot *val_slot, slot *expVal) {
-               assert (val_slot != NULL);
-               assert (!is_prime(val_slot));
-               assert (!is_prime(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;
@@ -720,12 +829,19 @@ friend class CHM;
                                if (val_slot == TOMBSTONE) return val_slot;
                                // Claim the null key-slot
                                if (CAS_key(kvs, idx, NULL, key_slot)) {
+                                       /**
+                                               @Begin
+                                               @Commit_point_define: true
+                                               @Potential_commit_point_label: Write_Key_Point
+                                               @Label: Put_WriteKey
+                                               @End
+                                       */
                                        chm->_slots.fetch_add(1, memory_order_relaxed); // Inc key-slots-used count
                                        hashes[idx] = fullhash; // Memorize full hash
                                        break;
                                }
                                K = key(kvs, idx); // CAS failed, get updated value
-                               assert (K != NULL);
+                               MODEL_ASSERT (K != NULL);
                        }
 
                        // Key slot not null, there exists a Key here
@@ -738,6 +854,7 @@ friend class CHM;
                        if (++reprobe_cnt >= reprobe_limit(len) ||
                                K == TOMBSTONE) { // Found a Tombstone key, no more keys
                                newkvs = chm->resize(topmap, kvs);
+                               //model_print("resize1\n");
                                // Help along an existing copy
                                if (expVal != NULL) topmap->help_copy(newkvs);
                                return putIfMatch(topmap, newkvs, key_slot, val_slot, expVal);
@@ -750,10 +867,19 @@ 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);
+               /**
+                       //@Begin
+                       @Commit_point_define_check: true
+                       @Label: Put_ReadNewKVS
+                       @End
+               */
                if (newkvs == NULL &&
-                       ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V)))
+                       ((V == NULL && chm->table_full(reprobe_cnt, len)) || is_prime(V))) {
+                       //model_print("resize2\n");
                        newkvs = chm->resize(topmap, kvs); // Force the copy to start
+               }
                
                // Finish the copy and then put it in the new table
                if (newkvs != NULL)
@@ -762,7 +888,7 @@ friend class CHM;
                
                // Decided to update the existing table
                while (true) {
-                       assert (!is_prime(V));
+                       MODEL_ASSERT (!is_prime(V));
 
                        if (expVal != NO_MATCH_OLD &&
                                V != expVal &&
@@ -770,7 +896,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
@@ -779,15 +905,15 @@ 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
-                                       @Commit_point_define: !valeq(expVal, V)
+                                       //@Begin
+                                       @Commit_point_define: expVal != NULL && !valeq(expVal, V)
                                        @Potential_commit_point_label: Read_Val_Point
                                        @Label: ReplaceIfMatch_Fail_Point
                                        @End
@@ -801,7 +927,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
@@ -827,13 +953,19 @@ 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
-               if (topchm->_newkvs.load(memory_order_acquire) == NULL) return helper;
+               if (topchm->_newkvs.load(memory_order_relaxed) == NULL) return helper;
                topchm->help_copy_impl(this, topkvs, false);
                return helper;
        }
 };
+/**
+       @Begin
+       @Class_end
+       @End
+*/
 
 #endif
index 997703c..8d94528 100644 (file)
 #include <iostream>
-
+#include <threads.h>
 #include "cliffc_hashtable.h"
 
-#ifndef NORMAL
-#include "threads.h"
-#endif
+using namespace std;
 
-template<typename TypeK, typename TypeV, class Hash, class KeyEqualsTo, class ValEqualsTo>
-slot* const cliffc_hashtable<TypeK, TypeV, Hash, KeyEqualsTo, ValEqualsTo>::MATCH_ANY = new slot(false, NULL);
+template<typename TypeK, typename TypeV>
+slot* const cliffc_hashtable<TypeK, TypeV>::MATCH_ANY = new slot(false, NULL);
 
-template<typename TypeK, typename TypeV, class Hash, class KeyEqualsTo, class ValEqualsTo>
-slot* const cliffc_hashtable<TypeK, TypeV, Hash, KeyEqualsTo, ValEqualsTo>::NO_MATCH_OLD = 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, class Hash, class KeyEqualsTo, class ValEqualsTo>
-slot* const cliffc_hashtable<TypeK, TypeV, Hash, KeyEqualsTo, ValEqualsTo>::TOMBPRIME = new slot(true, NULL);
+template<typename TypeK, typename TypeV>
+slot* const cliffc_hashtable<TypeK, TypeV>::TOMBPRIME = new slot(true, NULL);
 
-template<typename TypeK, typename TypeV, class Hash, class KeyEqualsTo, class ValEqualsTo>
-slot* const cliffc_hashtable<TypeK, TypeV, Hash, KeyEqualsTo, ValEqualsTo>::TOMBSTONE = new slot(false, NULL);
+template<typename TypeK, typename TypeV>
+slot* const cliffc_hashtable<TypeK, TypeV>::TOMBSTONE = new slot(false, NULL);
 
-template<typename TypeK, typename TypeV, class Hash, class KeyEqualsTo, class ValEqualsTo>
-Hash cliffc_hashtable<TypeK, TypeV, Hash, KeyEqualsTo, ValEqualsTo>::hashFunc;
 
-template<typename TypeK, typename TypeV, class Hash, class KeyEqualsTo, class ValEqualsTo>
-KeyEqualsTo cliffc_hashtable<TypeK, TypeV, Hash, KeyEqualsTo, ValEqualsTo>::keyEqualsTo;
+class IntWrapper {
+       private:
+               public:
+           int _val;
 
-template<typename TypeK, typename TypeV, class Hash, class KeyEqualsTo, class ValEqualsTo>
-ValEqualsTo cliffc_hashtable<TypeK, TypeV, Hash, KeyEqualsTo, ValEqualsTo>::valEqualsTo;
+               IntWrapper(int val) : _val(val) {}
 
-class HashInt {
-       public:
-       int operator()(const int &val) const {
-               return val;
-       }
-};
+               IntWrapper() : _val(0) {}
+
+               IntWrapper(IntWrapper& copy) : _val(copy._val) {}
 
-class EqualsToInt {
-       public:
-       bool operator()(const int &val1, const int &val2) const {
-               return val1 == val2;
-       }
+               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;
+               }
 };
 
-int *k1, *k2, *v1, *v2;
-cliffc_hashtable<int, int, HashInt, EqualsToInt, EqualsToInt> *table;
+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) {
-       table->put(*k1, *v1);
-       int *r1 = table->get(*k2);
-       if (r1) {
-               printf("r1=%d\n", *r1);
-       } else {
-               printf("r1=NULL\n");
-       }
+       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) {
-       table->put(*k2, *v2);
-       int *r2 = table->get(*k1);
-       if (r2) {
-               printf("r2=%d\n", *r2);
-       } else {
-               printf("r2=NULL\n");
-       }
+       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);
 }
 
-
-#ifdef NORMAL
-int main(int argc, char *argv[]) {
-       table = new cliffc_hashtable<int, int, HashInt, EqualsToInt, EqualsToInt>();
-       k1 = new int(3);
-       k2 = new int(4);
-       v1 = new int(1);
-       v2 = new int(2);
+int user_main(int argc, char *argv[]) {
+       thrd_t t1, t2;
+       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_join(t1);
+       thrd_join(t2);
        
-       table->put(*k1, *v1);
-       table->put(*k2, *v2);
-       int *r1 = table->get(*k2);
-       if (r1) {
-               printf("r1=%d\n", *r1);
-       } else {
-               printf("r1=NULL\n");
-       }
-
        return 0;
 }
-#else
-int user_main(int argc, char *argv[]) {
-       table = new cliffc_hashtable<int, int, HashInt, EqualsToInt, EqualsToInt>();
-       k1 = new int(3);
-       k2 = new int(4);
-       v1 = new int(1);
-       v2 = new int(2);
 
-       thrd_t A, B, C;
-       thrd_create(&A, &threadA, NULL);
-       thrd_create(&B, &threadB, NULL);
 
-       thrd_join(A);
-       thrd_join(B);
-
-       return 0;
-}
-#endif
diff --git a/treiber-stack/Makefile b/treiber-stack/Makefile
new file mode 100644 (file)
index 0000000..99cac3f
--- /dev/null
@@ -0,0 +1,10 @@
+include ../benchmarks.mk
+
+main: my_stack.o main.c
+       $(CC) -o $@ $^ $(CFLAGS) $(LDFLAGS)
+
+%.o: %.c
+       $(CC) -c -o $@ $^ $(CFLAGS)
+
+clean:
+       rm -f *.o
diff --git a/treiber-stack/main.c b/treiber-stack/main.c
new file mode 100644 (file)
index 0000000..d27242e
--- /dev/null
@@ -0,0 +1,89 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <threads.h>
+
+#include "my_stack.h"
+#include "model-assert.h"
+
+static int procs = 4;
+static stack_t *stack;
+static thrd_t *threads;
+static int num_threads;
+
+unsigned int idx1, idx2;
+unsigned int a, b;
+
+
+atomic_int x[3];
+
+int get_thread_num()
+{
+       thrd_t curr = thrd_current();
+       int i;
+       for (i = 0; i < num_threads; i++)
+               if (curr.priv == threads[i].priv)
+                       return i;
+       MODEL_ASSERT(0);
+       return -1;
+}
+
+static void main_task(void *param)
+{
+       unsigned int val;
+       int pid = *((int *)param);
+
+       if (pid % 4 == 0) {
+               atomic_store_explicit(&x[1], 17, relaxed);
+               push(stack, 1);
+       } else if (pid % 4 == 1) {
+               atomic_store_explicit(&x[2], 37, relaxed);
+               push(stack, 2);
+       } else if (pid % 4 == 2) {/*
+               idx1 = pop(stack);
+               if (idx1 != 0) {
+                       a = atomic_load_explicit(&x[idx1], relaxed);
+                       printf("a: %d\n", a);
+               }*/
+       } else {
+               idx2 = pop(stack);
+               if (idx2 != 0) {
+                       b = atomic_load_explicit(&x[idx2], relaxed);
+                       printf("b: %d\n", b);
+               }
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       int i;
+       int *param;
+       unsigned int in_sum = 0, out_sum = 0;
+
+       atomic_init(&x[1], 0);
+       atomic_init(&x[2], 0);
+
+       stack = calloc(1, sizeof(*stack));
+
+       num_threads = procs;
+       threads = malloc(num_threads * sizeof(thrd_t));
+       param = malloc(num_threads * sizeof(*param));
+
+       init_stack(stack, num_threads);
+       
+       for (i = 0; i < num_threads; i++) {
+               param[i] = i;
+               thrd_create(&threads[i], main_task, &param[i]);
+       }
+       for (i = 0; i < num_threads; i++)
+               thrd_join(threads[i]);
+
+       bool correct = false;
+       //correct |= (a == 17 || a == 37 || a == 0);
+       //MODEL_ASSERT(correct);
+
+       free(param);
+       free(threads);
+       free(stack);
+       
+       return 0;
+}
diff --git a/treiber-stack/my_stack.c b/treiber-stack/my_stack.c
new file mode 100644 (file)
index 0000000..5f3cc89
--- /dev/null
@@ -0,0 +1,123 @@
+#include <threads.h>
+#include <stdlib.h>
+#include "librace.h"
+#include "model-assert.h"
+
+#include "my_stack.h"
+
+#define MAX_FREELIST 4 /* Each thread can own up to MAX_FREELIST free nodes */
+#define INITIAL_FREE 2 /* Each thread starts with INITIAL_FREE free nodes */
+
+#define POISON_IDX 0x666
+
+static unsigned int (*free_lists)[MAX_FREELIST];
+
+/* Search this thread's free list for a "new" node */
+static unsigned int new_node()
+{
+       int i;
+       int t = get_thread_num();
+       for (i = 0; i < MAX_FREELIST; i++) {
+               //unsigned int node = load_32(&free_lists[t][i]);
+               unsigned int node = free_lists[t][i];
+               if (node) {
+                       //store_32(&free_lists[t][i], 0);
+                       free_lists[t][i] = 0;
+                       return node;
+               }
+       }
+       /* free_list is empty? */
+       MODEL_ASSERT(0);
+       return 0;
+}
+
+/* Place this node index back on this thread's free list */
+static void reclaim(unsigned int node)
+{
+       int i;
+       int t = get_thread_num();
+
+       /* Don't reclaim NULL node */
+       //MODEL_ASSERT(node);
+
+       for (i = 0; i < MAX_FREELIST; i++) {
+               /* Should never race with our own thread here */
+               //unsigned int idx = load_32(&free_lists[t][i]);
+               unsigned int idx = free_lists[t][i];
+
+               /* Found empty spot in free list */
+               if (idx == 0) {
+                       //store_32(&free_lists[t][i], node);
+                       free_lists[t][i] = node;
+                       return;
+               }
+       }
+       /* free list is full? */
+       MODEL_ASSERT(0);
+}
+
+void init_stack(stack_t *s, int num_threads)
+{
+       int i, j;
+
+       /* Initialize each thread's free list with INITIAL_FREE pointers */
+       /* The actual nodes are initialized with poison indexes */
+       free_lists = malloc(num_threads * sizeof(*free_lists));
+       for (i = 0; i < num_threads; i++) {
+               for (j = 0; j < INITIAL_FREE; j++) {
+                       free_lists[i][j] = 1 + i * MAX_FREELIST + j;
+                       atomic_init(&s->nodes[free_lists[i][j]].next, MAKE_POINTER(POISON_IDX, 0));
+               }
+       }
+
+       /* initialize stack */
+       atomic_init(&s->top, MAKE_POINTER(0, 0));
+}
+
+void push(stack_t *s, unsigned int val) {
+       unsigned int nodeIdx = new_node();
+       node_t *node = &s->nodes[nodeIdx];
+       node->value = val;
+       pointer oldTop, newTop;
+       bool success;
+       while (true) {
+               // acquire
+               oldTop = atomic_load_explicit(&s->top, acquire);
+               newTop = MAKE_POINTER(nodeIdx, get_count(oldTop) + 1);
+               // relaxed
+               atomic_store_explicit(&node->next, oldTop, relaxed);
+
+               // release & relaxed
+               success = atomic_compare_exchange_strong_explicit(&s->top, &oldTop,
+                       newTop, release, relaxed);
+               if (success)
+                       break;
+       } 
+}
+
+unsigned int pop(stack_t *s) 
+{
+       pointer oldTop, newTop, next;
+       node_t *node;
+       bool success;
+       int val;
+       while (true) {
+               // acquire
+               oldTop = atomic_load_explicit(&s->top, acquire);
+               if (get_ptr(oldTop) == 0)
+                       return 0;
+               node = &s->nodes[get_ptr(oldTop)];
+               // relaxed
+               next = atomic_load_explicit(&node->next, relaxed);
+               newTop = MAKE_POINTER(get_ptr(next), get_count(oldTop) + 1);
+               // release & relaxed
+               success = atomic_compare_exchange_strong_explicit(&s->top, &oldTop,
+                       newTop, release, relaxed);
+               if (success)
+                       break;
+       }
+       val = node->value;
+       /* Reclaim the used slot */
+       reclaim(get_ptr(oldTop));
+       return val;
+}
diff --git a/treiber-stack/my_stack.h b/treiber-stack/my_stack.h
new file mode 100644 (file)
index 0000000..8d4d789
--- /dev/null
@@ -0,0 +1,35 @@
+#include <stdatomic.h>
+
+#define release memory_order_release 
+#define acquire memory_order_acquire 
+#define relaxed memory_order_relaxed
+
+#define MAX_NODES                      0xf
+
+typedef unsigned long long pointer;
+typedef atomic_ullong pointer_t;
+
+#define MAKE_POINTER(ptr, count)       ((((pointer)count) << 32) | ptr)
+#define PTR_MASK 0xffffffffLL
+#define COUNT_MASK (0xffffffffLL << 32)
+
+static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
+static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
+static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
+static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
+
+typedef struct node {
+       unsigned int value;
+       pointer_t next;
+
+} node_t;
+
+typedef struct {
+       pointer_t top;
+       node_t nodes[MAX_NODES + 1];
+} stack_t;
+
+void init_stack(stack_t *s, int num_threads);
+void push(stack_t *s, unsigned int val);
+unsigned int pop(stack_t *s);
+int get_thread_num();