edits

diff --git a/benchmark/concurrent-hashmap/hashmap.h b/benchmark/concurrent-hashmap/hashmap.h
index 904d0b84e9233ce79246c404eec439eb86ebe62e..99973e3cedc0cefcd007fdd6abcf80d4188472ff 100644 (file)
--- a/benchmark/concurrent-hashmap/hashmap.h
+++ b/benchmark/concurrent-hashmap/hashmap.h
@@ -130,7 +130,7 @@ class HashMap {
        /**
                @Begin
                @Interface: Get 
        /**
                @Begin
                @Interface: Get 

-               @Commit_point_set: GetReadValue1 | GetReadEntry | GetReadValue2
+               @Commit_point_set: GetReadValue1 | GetReadValue2 | GetReadNothing

                @ID: __RET__ 
                @Action:
                        int res = getIntegerMap(__map, key);
                @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
                
                // 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) {
                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
                                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);
 
                // 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) {
                if (e != NULL || firstPtr != newFirstPtr) {
                        e = newFirstPtr;
                        while (e != NULL) {


@@ -213,6 +207,12 @@ class HashMap {
                        }
                }
                seg->unlock(); // Critical region ends
                        }
                }
                seg->unlock(); // Critical region ends

+               /**
+                       @Begin
+                       @Commit_point_define_check: true 
+                       @Label: GetReadNothing
+                       @End
+               */

                return 0;
        }
 
                return 0;
        }
 


@@ -249,7 +249,7 @@ class HashMap {
                                // with the previous put()),  no need to be acquire
                                oldValue = e->value.load(relaxed);
                                
                                // 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
                                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);
                
                // 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);
                // Publish the newEntry to others
                first->store(newEntry, release);

+               /**
+                       @Begin
+                       @Commit_point_clear: true 
+                       @Label: PutClear
+                       @End
+               */
+

                /**
                        @Begin
                        @Commit_point_define_check: true 
                /**
                        @Begin
                        @Commit_point_define_check: true 

diff --git a/benchmark/mpmc-queue/mpmc-queue.h b/benchmark/mpmc-queue/mpmc-queue.h
index dff677773971717e6c584be1fdd021d347ed293d..ff6a168f1c248cc2db457f8fa7b7da8dc818f91a 100644 (file)
--- a/benchmark/mpmc-queue/mpmc-queue.h
+++ b/benchmark/mpmc-queue/mpmc-queue.h
@@ -19,7 +19,9 @@ struct mpmc_boundq_1_alt
 private:
        
        unsigned int MASK;
 private:
        
        unsigned int MASK;

-
+       
+       atomic<t_element*> arr;
+       

        // elements should generally be cache-line-size padded :
        t_element               m_array[t_size];
 
        // elements should generally be cache-line-size padded :
        t_element               m_array[t_size];
 


@@ -31,7 +33,7 @@ private:
 
 public:
 
 
 public:
 

-       mpmc_boundq_1_alt()
+       mpmc_boundq_1_alt(int _MASK = 0xFFFF)

        {
        /**
                @Begin
        {
        /**
                @Begin


@@ -42,7 +44,8 @@ public:
                m_read = 0;
                m_written = 0;
                // For this we want MASK = 1; MASK wrap around
                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
        /**
                @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
                @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
                //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;
                        @End
                */
                unsigned int rd,wr;


@@ -103,31 +106,29 @@ public:
                        wr = rdwr & MASK;
 
                        if ( wr == rd ) { // empty
                        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;
                        }
                                return false;
                        }

-                       

                        /**** Inadmissibility (testcase2.cc, MASK = 1, size = 1) ****/
                        bool succ =
                        /**** 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;
                                break;

-                       else
+                       } else {
+                               /**
+                                       @Begin
+                                       @Commit_point_clear: true
+                                       @Label: FetchClear1
+                                       @End
+                               */
+
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: true
+                                       @Label: FetchReadRW2
+                                       @End
+                               */

                                thrd_yield();
                                thrd_yield();

+                       }

                }
 
                // (*1)
                }
 
                // (*1)


@@ -135,12 +136,6 @@ public:
                while (true) {
                        /**** Inadmissibility ****/
                        int written = m_written.load(mo_acquire);
                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 {
                        if ((written & MASK) != wr) {
                                thrd_yield();
                        } else {


@@ -148,16 +143,23 @@ public:
                                break;
                        }
                }
                                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
                /**
                        @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
                */
                        @End
                */

-
-               t_element * p = & ( m_array[ rd % t_size ] );

                
                return p;
        }
                
                return p;
        }


@@ -165,7 +167,7 @@ public:
        /**
                @Begin
                @Interface: Consume
        /**
                @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
                @ID: (call_id_t) bin 
                //@Action: model_print("Consume: %d\n", bin);
                @End


@@ -176,7 +178,7 @@ public:
                /**
                        @Begin
                        @Commit_point_define_check: true
                /**
                        @Begin
                        @Commit_point_define_check: true

-                       @Label: Consume_R_RMW
+                       @Label: ConsumeFetchAdd

                        @End
                */
        }
                        @End
                */
        }


@@ -186,7 +188,7 @@ public:
        /**
                @Begin
                @Interface: Prepare 
        /**
                @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
                @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
                //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;
                        @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
                        //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);
                                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);
                        //printf("wr=%d\n", (wr+1)&MASK);

-                       if (succ)
+                       if (succ) {

                                break;
                                break;

-                       else
+                       } else {
+                               /**
+                                       @Begin
+                                       @Commit_point_clear: true
+                                       @Label: PrepareClear1
+                                       @End
+                               */
+
+                               /**
+                                       @Begin
+                                       @Commit_point_define_check: true
+                                       @Label: PrepareReadRW2
+                                       @End
+                               */

                                thrd_yield();
                                thrd_yield();

+                       }

                }
 
                // (*1)
                }
 
                // (*1)


@@ -241,27 +243,29 @@ public:
                while (true) {
                        /**** Inadmissibility ****/
                        int read = m_read.load(mo_acquire);
                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;
                }
 
                        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
                /**
                        @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
                */
                        @End
                */

-
-               t_element * p = & ( m_array[ wr % t_size ] );

 
                return p;
        }
 
                return p;
        }

diff --git a/benchmark/mpmc-queue/testcase2.cc b/benchmark/mpmc-queue/testcase2.cc
index a26f9811242dd9fbb303753afe8db07ba6192cdf..f03ea410f744d0e476e2004d8db47017b4a69846 100644 (file)
--- a/benchmark/mpmc-queue/testcase2.cc
+++ b/benchmark/mpmc-queue/testcase2.cc
@@ -61,7 +61,7 @@ void threadB(struct mpmc_boundq_1_alt<int32_t, 1> *queue)
 
 int user_main(int argc, char **argv)
 {
 
 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");
        thrd_t A, A1, B;
 
        printf("Adding initial element\n");

diff --git a/benchmark/mpmc-queue/testcase3.cc b/benchmark/mpmc-queue/testcase3.cc
index b171c750ebb98be7b59e10baebb609dc955c00ee..a0a857e961408c136125804e7a5fbbf90955ac0d 100644 (file)
--- a/benchmark/mpmc-queue/testcase3.cc
+++ b/benchmark/mpmc-queue/testcase3.cc
@@ -74,7 +74,7 @@ void threadC(struct mpmc_boundq_1_alt<int32_t, 1> *queue)
 
 int user_main(int argc, char **argv)
 {
 
 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");
        thrd_t A, A1, B, B1, C, C1;
 
        printf("Adding initial element\n");