edits
authorPeizhao Ou <peizhaoo@uci.edu>
Thu, 19 Nov 2015 22:16:13 +0000 (14:16 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Thu, 19 Nov 2015 22:16:13 +0000 (14:16 -0800)
benchmark/concurrent-hashmap/hashmap.h
benchmark/mpmc-queue/mpmc-queue.h
benchmark/mpmc-queue/testcase2.cc
benchmark/mpmc-queue/testcase3.cc

index 904d0b8..99973e3 100644 (file)
@@ -130,7 +130,7 @@ class HashMap {
        /**
                @Begin
                @Interface: Get 
-               @Commit_point_set: GetReadValue1 | GetReadEntry | GetReadValue2
+               @Commit_point_set: GetReadValue1 | GetReadValue2 | GetReadNothing
                @ID: __RET__ 
                @Action:
                        int res = getIntegerMap(__map, key);
@@ -156,13 +156,13 @@ class HashMap {
                // lock, we ignore this operation for the SC analysis, and otherwise we
                // take it into consideration
                
-               /**** UL ****/
+               /**** UL (main.cc) ****/
                Entry *firstPtr = first->load(acquire);
 
                e = firstPtr;
                while (e != NULL) {
                        if (key, e->key) {
-                               /**** inadmissible ****/
+                               /**** inadmissible (testcase1.cc) ****/
                                res = e->value.load(seq_cst);
                                /**
                                        @Begin
@@ -187,12 +187,6 @@ class HashMap {
 
                // Synchronized by locking, no need to be load acquire
                Entry *newFirstPtr = first->load(relaxed);
-               /**
-                       @Begin
-                       @Commit_point_define_check: true 
-                       @Label: GetReadEntry
-                       @End
-               */
                if (e != NULL || firstPtr != newFirstPtr) {
                        e = newFirstPtr;
                        while (e != NULL) {
@@ -213,6 +207,12 @@ class HashMap {
                        }
                }
                seg->unlock(); // Critical region ends
+               /**
+                       @Begin
+                       @Commit_point_define_check: true 
+                       @Label: GetReadNothing
+                       @End
+               */
                return 0;
        }
 
@@ -249,7 +249,7 @@ class HashMap {
                                // with the previous put()),  no need to be acquire
                                oldValue = e->value.load(relaxed);
                                
-                               /**** inadmissible ****/
+                               /**** inadmissible (testcase1.cc) ****/
                                e->value.store(value, seq_cst);
                                /**
                                        @Begin
@@ -267,9 +267,16 @@ class HashMap {
                // Add to front of list
                Entry *newEntry = new Entry(hash, key, value, firstPtr);
                
-               /**** UL ****/
+               /**** UL (main.cc) ****/
                // Publish the newEntry to others
                first->store(newEntry, release);
+               /**
+                       @Begin
+                       @Commit_point_clear: true 
+                       @Label: PutClear
+                       @End
+               */
+
                /**
                        @Begin
                        @Commit_point_define_check: true 
index dff6777..ff6a168 100644 (file)
@@ -19,7 +19,9 @@ struct mpmc_boundq_1_alt
 private:
        
        unsigned int MASK;
-
+       
+       atomic<t_element*> arr;
+       
        // elements should generally be cache-line-size padded :
        t_element               m_array[t_size];
 
@@ -31,7 +33,7 @@ private:
 
 public:
 
-       mpmc_boundq_1_alt()
+       mpmc_boundq_1_alt(int _MASK = 0xFFFF)
        {
        /**
                @Begin
@@ -42,7 +44,8 @@ public:
                m_read = 0;
                m_written = 0;
                // For this we want MASK = 1; MASK wrap around
-               MASK = 0x1; // 11
+               MASK = _MASK; //0x11;
+               arr = m_array;
        }
        
 
@@ -82,7 +85,7 @@ public:
        /**
                @Begin
                @Interface: Fetch
-               @Commit_point_set: Fetch_RW_Load_Empty | Fetch_RW_RMW | Fetch_W_Load
+               @Commit_point_set: FetchReadRW1 | FetchReadRW2 | FetchReadPointer
                @ID: (call_id_t) __RET__
                //@Action: model_print("Fetch: %d\n", __RET__);
                @End
@@ -93,8 +96,8 @@ public:
                //unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
-                       @Potential_commit_point_define: true
-                       @Label: Fetch_Potential_RW_Load
+                       @Commit_point_define_check: true
+                       @Label: FetchReadRW1
                        @End
                */
                unsigned int rd,wr;
@@ -103,31 +106,29 @@ public:
                        wr = rdwr & MASK;
 
                        if ( wr == rd ) { // empty
-
-                               /**
-                                       @Begin
-                                       @Commit_point_define: true
-                                       @Potential_commit_point_label: Fetch_Potential_RW_Load
-                                       @Label: Fetch_RW_Load_Empty
-                                       @End
-                               */
-
                                return false;
                        }
-                       
                        /**** Inadmissibility (testcase2.cc, MASK = 1, size = 1) ****/
                        bool succ =
-                       m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
-                       /**
-                               @Begin
-                               @Commit_point_define_check: succ
-                               @Label: Fetch_RW_RMW
-                               @End
-                       */
-                       if (succ)
+                               m_rdwr.compare_exchange_weak(rdwr,rdwr+(1<<16),mo_acq_rel);
+                       if (succ) {
                                break;
-                       else
+                       } else {
+                               /**
+                                       @Begin
+                                       @Commit_point_clear: true
+                                       @Label: FetchClear1
+                                       @End
+                               */
+
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: true
+                                       @Label: FetchReadRW2
+                                       @End
+                               */
                                thrd_yield();
+                       }
                }
 
                // (*1)
@@ -135,12 +136,6 @@ public:
                while (true) {
                        /**** Inadmissibility ****/
                        int written = m_written.load(mo_acquire);
-                       /**
-                               @Begin
-                               @Potential_commit_point_define: true
-                               @Label: Fetch_Potential_W_Load
-                               @End
-                       */
                        if ((written & MASK) != wr) {
                                thrd_yield();
                        } else {
@@ -148,16 +143,23 @@ public:
                                break;
                        }
                }
-               
+               t_element * p = & ( m_array[ rd % t_size ] );
+
+               // This is just a hack to tell the CDSChecker that we have a memory
+               // operation here
+               arr.load(memory_order_relaxed);
                /**
                        @Begin
-                       @Commit_point_define: true
-                       @Potential_commit_point_label: Fetch_Potential_W_Load
-                       @Label: Fetch_W_Load
+                       @Commit_point_clear: true
+                       @Label: FetchClear2
+                       @End
+               */
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: FetchReadPointer
                        @End
                */
-
-               t_element * p = & ( m_array[ rd % t_size ] );
                
                return p;
        }
@@ -165,7 +167,7 @@ public:
        /**
                @Begin
                @Interface: Consume
-               @Commit_point_set: Consume_R_RMW
+               @Commit_point_set: ConsumeFetchAdd
                @ID: (call_id_t) bin 
                //@Action: model_print("Consume: %d\n", bin);
                @End
@@ -176,7 +178,7 @@ public:
                /**
                        @Begin
                        @Commit_point_define_check: true
-                       @Label: Consume_R_RMW
+                       @Label: ConsumeFetchAdd
                        @End
                */
        }
@@ -186,7 +188,7 @@ public:
        /**
                @Begin
                @Interface: Prepare 
-               @Commit_point_set: Prepare_RW_Load_Full | Prepare_RW_RMW | Prepare_R_Load
+               @Commit_point_set: PrepareReadRW1 | PrepareReadRW2 | PrepareReadPointer
                @ID: (call_id_t) __RET__
                //@Action: model_print("Prepare: %d\n", __RET__);
                @End
@@ -198,8 +200,8 @@ public:
                //unsigned int rdwr = m_rdwr.load(mo_relaxed);
                /**
                        @Begin
-                       @Potential_commit_point_define: true
-                       @Label: Prepare_Potential_RW_Load
+                       @Commit_point_define_check: true
+                       @Label: PrepareReadRW1
                        @End
                */
                unsigned int rd,wr;
@@ -209,31 +211,31 @@ public:
                        //printf("write_prepare: rd=%d, wr=%d\n", rd, wr);
 
                        if ( wr == ((rd + t_size)&MASK) ) { // full
-
-                               /**
-                                       @Begin
-                                       @Commit_point_define: true
-                                       @Potential_commit_point_label: Prepare_Potential_RW_Load
-                                       @Label: Prepare_RW_Load_Full
-                                       @End
-                               */
                                return NULL;
                        }
                        
                        /**** Inadmissibility (testcase3.cc, MASK = 1, size = 1) ****/
                        bool succ = m_rdwr.compare_exchange_weak(rdwr,(rd<<16) |
                                ((wr+1)&MASK),mo_acq_rel);
-                       /**
-                               @Begin
-                               @Commit_point_define_check: succ
-                               @Label: Prepare_RW_RMW
-                               @End
-                       */
                        //printf("wr=%d\n", (wr+1)&MASK);
-                       if (succ)
+                       if (succ) {
                                break;
-                       else
+                       } else {
+                               /**
+                                       @Begin
+                                       @Commit_point_clear: true
+                                       @Label: PrepareClear1
+                                       @End
+                               */
+
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: true
+                                       @Label: PrepareReadRW2
+                                       @End
+                               */
                                thrd_yield();
+                       }
                }
 
                // (*1)
@@ -241,27 +243,29 @@ public:
                while (true) {
                        /**** Inadmissibility ****/
                        int read = m_read.load(mo_acquire);
-                       /**
-                               @Begin
-                               @Potential_commit_point_define: true
-                               @Label: Prepare_Potential_R_Load
-                               @End
-                       */
                        if ((read & MASK) != rd)
                                thrd_yield();
                        else
                                break;
                }
 
+               t_element * p = & ( m_array[ wr % t_size ] );
+
+               // This is also just a hack to tell the CDSChecker that we have a memory
+               // operation here
+               arr.load(memory_order_relaxed);
                /**
                        @Begin
-                       @Commit_point_define: true
-                       @Potential_commit_point_label: Prepare_Potential_R_Load
-                       @Label: Prepare_R_Load
+                       @Commit_point_clear: true
+                       @Label: PrepareClear2
+                       @End
+               */
+               /**
+                       @Begin
+                       @Commit_point_define_check: true
+                       @Label: PrepareReadPointer
                        @End
                */
-
-               t_element * p = & ( m_array[ wr % t_size ] );
 
                return p;
        }
index a26f981..f03ea41 100644 (file)
@@ -61,7 +61,7 @@ void threadB(struct mpmc_boundq_1_alt<int32_t, 1> *queue)
 
 int user_main(int argc, char **argv)
 {
-       struct mpmc_boundq_1_alt<int32_t, 1> queue;
+       struct mpmc_boundq_1_alt<int32_t, 1> queue(0x1);
        thrd_t A, A1, B;
 
        printf("Adding initial element\n");
index b171c75..a0a857e 100644 (file)
@@ -74,7 +74,7 @@ void threadC(struct mpmc_boundq_1_alt<int32_t, 1> *queue)
 
 int user_main(int argc, char **argv)
 {
-       struct mpmc_boundq_1_alt<int32_t, 1> queue;
+       struct mpmc_boundq_1_alt<int32_t, 1> queue(0x1);
        thrd_t A, A1, B, B1, C, C1;
 
        printf("Adding initial element\n");